<discord2>
<Perry> Given that patch, see if you can take things from there? I've patched stdlib.etex, bigarray.mli, and intf-c.etex. If there's more we can do it later, I'm happy to help with this. Just tell me what you need.
mfp has quit [Ping timeout: 260 seconds]
sh0t has quit [Remote host closed the connection]
gtrak has quit [Ping timeout: 246 seconds]
cbot_ has joined #ocaml
<discord2>
<Perry> Oh, and 'm not sure what one is supposed to do to libbigarray.etex.
cbot has quit [Ping timeout: 246 seconds]
jimmyrcom_ has joined #ocaml
<octachron>
Perry, I will have look tomorrow
ziyourenxiang has quit [Ping timeout: 240 seconds]
<discord2>
<Perry> No rush. Let me know how it goes (perhaps in the github issue tracker.)
shinnya has quit [Ping timeout: 256 seconds]
noitakomentaja has quit [Ping timeout: 255 seconds]
pierpal has joined #ocaml
pierpal has quit [Ping timeout: 255 seconds]
moolc has joined #ocaml
jbrown has quit [Ping timeout: 248 seconds]
silver has quit [Read error: Connection reset by peer]
hdon has quit [Ping timeout: 246 seconds]
dogui_ has quit [Ping timeout: 240 seconds]
dogui has joined #ocaml
spew has joined #ocaml
hdon has joined #ocaml
spew has quit [Ping timeout: 246 seconds]
_etc has joined #ocaml
hdon has quit [Ping timeout: 240 seconds]
johnelse_ has quit [Ping timeout: 256 seconds]
_etc2 has joined #ocaml
johnelse has joined #ocaml
_etc has quit [Ping timeout: 246 seconds]
tormen has joined #ocaml
<_etc2>
Hello! Does anyone know how to get a unique/absolute path given an env and a path that isn't absolute?
spew has joined #ocaml
sh0t has joined #ocaml
<_etc2>
I've already called the typechecker and am hoping to see if any paths come from some place outside of the section I'm considering
tormen_ has quit [Ping timeout: 240 seconds]
moolc has left #ocaml ["ERC (IRC client for Emacs 27.0.50)"]
<_etc2>
All to check whether a given piece of ast has free variables: if there's a different way to do this I'd be happy too :)
spew has quit [Read error: Connection reset by peer]
jbrown has joined #ocaml
sh0t has quit [Remote host closed the connection]
sh0t has joined #ocaml
sh0t has quit [Remote host closed the connection]
sh0t has joined #ocaml
_etc2 has quit [Remote host closed the connection]
sh0t has quit [Remote host closed the connection]
krkini is now known as kini
sh0t has joined #ocaml
struktured has joined #ocaml
zlsyx has quit [Remote host closed the connection]
pierpal has joined #ocaml
sh0t has quit [Remote host closed the connection]
sh0t has joined #ocaml
pierpal has quit [Read error: Connection reset by peer]
sh0t has quit [Remote host closed the connection]
jao has quit [Ping timeout: 240 seconds]
jbrown has quit [Ping timeout: 246 seconds]
pierpa has quit [Quit: Page closed]
malina has joined #ocaml
MercurialAlchemi has joined #ocaml
mbuf has joined #ocaml
m4lvin has quit [Remote host closed the connection]
m4lvin has joined #ocaml
<keep_learning>
Hi Everyone, I have OCaml code extracted from Coq with some axioms and when I am trying to realize those axioms with some OCaml code
<discord2>
<Christophe> Does it know that type pubkey = Big_int.big_int, type 'a ballot = 'a -> 'a -> pubkey and type 'a eballot = 'a -> 'a -> pubkey*pubkey ?
<discord2>
<Christophe> I would be surprised if the 'a1 = cand part was the problem
dtornabene has quit [Read error: Connection reset by peer]
dtornabene has joined #ocaml
dtornabene_ has joined #ocaml
dtornabene has quit [Ping timeout: 240 seconds]
ia0 has quit [Quit: reboot]
malina has quit [Ping timeout: 240 seconds]
ia0 has joined #ocaml
jimmyrcom_ has quit [Ping timeout: 256 seconds]
Haudegen has quit [Remote host closed the connection]
argent_smith has quit [Quit: Leaving.]
<discord2>
<Perry> Drup: is the extra indirection because of the shape of the data structure or because of the compiler?
malina has joined #ocaml
<flux[m]>
hmm, bigarrays live outside the ocaml heap, right? so it needs a pointer to that object.
<flux[m]>
the point of bigarrays is that ocaml GC doesn't move them around, so I believe that would be the explanation
<discord2>
<Perry> That indeed explains it.
<discord2>
<Perry> So here's why I'm asking (I mentioned this before): sedlex, for efficiency reasons, uses strings as arrays of 8 bit values. This leads to slightly gross looking code. I'm kind of interested in using actual arrays, but of course, OCaml's arrays don't know how to store only an 8 bit or 16 bit value or what have you. I imagine there are other times when this comes up, too. I'm interested in the long run if this can be fixed. In the short run, I
<discord2>
suppose it isn't that important.
<discord2>
<Perry> (Fixed = add mechanisms for handling packed arrays of various sizes of ints etc.)
TarVanimelde has quit [Quit: TarVanimelde]
<discord2>
<Perry> (long run = arbitrarily far in the future.)
<flux[m]>
you could write 8/16/32 accessors in C for the OCaml arrays and use them, but not sure if that would be a beneficial to performance
baroud has joined #ocaml
<discord2>
<Perry> I think the issue is caching, so it wouldn't be.
MercurialAlchemi has quit [Ping timeout: 246 seconds]
jao has quit [Ping timeout: 250 seconds]
sh0t has quit [Remote host closed the connection]
gtrak has joined #ocaml
mrvn has quit [Ping timeout: 248 seconds]
noitakomentaja has quit [Ping timeout: 255 seconds]
hdon has joined #ocaml
gtrak has quit [Ping timeout: 246 seconds]
MercurialAlchemi has joined #ocaml
gtrak has joined #ocaml
shinnya has joined #ocaml
hdon has quit [Ping timeout: 264 seconds]
steenuil_ has joined #ocaml
steenuil has quit [Read error: Connection reset by peer]
steenuil_ is now known as steenuil
baroud has quit [Ping timeout: 240 seconds]
FreeBirdLjj has quit [Remote host closed the connection]
MercurialAlchemi has quit [Ping timeout: 260 seconds]
dhil has joined #ocaml
<Drup>
Perry that's not the only explanation: bigarrays are slices, you can take subbigarrays, and so on
<Drup>
so you need additional informations that strings, which are just a pointer to a chunk of memory
<Drup>
Perry: I linked you to a proposal for arrays for abritrary datatypes, didn't I ?
<Drup>
In any case, if you want to improve the code, you should just define some indexing operators in a separate module that do the appropriate operations
<discord2>
<Perry> Drup: you may have linked me to that proposal. I don't remember it, but that's not surprising. URL?
<discord2>
<Perry> Oh neat! And no, I didn't see this before!
sh0t has joined #ocaml
<discord2>
<Perry> Really neat!
<discord2>
<Perry> Drup: I didn't quite understand the "if you want to improve the code" bit. You mean for Sedlex? I could do that, but the tables themselves remain ugly. But this is a very minor concern.
jao has joined #ocaml
FreeBirdLjj has joined #ocaml
<Drup>
I think you find them ugly just because you are not used to it :p
<discord2>
<Perry> Nah, I think they're ugly. But it's really a minor thing. It just irritated me a bit that arrays of small unboxed integers etc. didn't exist. But there's a proposal, so my irritation just went down 80%!
FreeBirdLjj has quit [Ping timeout: 256 seconds]
<discord2>
<Perry> Unfortunately I'm not yet skilled enough to help make that happen, but eventually.
troydm has quit [Quit: What is Hope? That all of your wishes and all of your dreams come true? To turn back time because things were not supposed to happen like that (C) Rau Le Creuset]
<Drup>
that proposals as issues on its own, unfortunately
<Drup>
has*
struktured has quit [Ping timeout: 240 seconds]
troydm has joined #ocaml
<discord2>
<Perry> Sure, but it's being discussed. If it doesn't happen for a while, well, it isn't like there aren't more things I'd like that aren't also being discussed endlessly...
zolk3ri has quit [Ping timeout: 255 seconds]
nicoo has quit [Remote host closed the connection]
nicoo has joined #ocaml
<discord2>
<Perry> (Modular implicits say.)
<discord2>
<Perry> The important thing is that it is in the queue, and I might even be able to help someday.
zolk3ri has joined #ocaml
FreeBirdLjj has joined #ocaml
<discord2>
<Perry> BTW, if someone gave me the choice between Leo working on this or modular implicits, I'd say the latter of course. 😃
dogui has quit [Ping timeout: 256 seconds]
<discord2>
<Bluddy> With Leo's current plans for modular implicits, we aren't going to see them for ages. So I'd rather he work on this.
<discord2>
<Perry> We could cut the gordion knot by cloning him.
dogui has joined #ocaml
<companion_cube>
can't we just stop talking about things that won't be merged for years? :/
shinnya has quit [Ping timeout: 255 seconds]
<discord2>
<hcarty> companion_cube++
<discord2>
<Perry> companion_cube: you find it depressing?
<Drup>
more like pointless
<companion_cube>
pointless, indeed
gpietro has joined #ocaml
sh0t has quit [Read error: Connection reset by peer]
<Drup>
Very few people can have meaningful contribution, so the discussions turn in circle
<discord2>
<Bluddy> not pointless if it can help us prioritize
<Drup>
that's precisely pointless
freusque has quit [Quit: WeeChat 2.0]
<Drup>
you're not going to prioritize shit on modular implicits, you are not involved in the needed technical work and, no offense, you don't have the level to contribute to it. The work depend on people that have their own whim and will work on things at their own pace
<Drup>
if you really want to contribute, make donnation to the OCaml fundation, that would be more productive
<companion_cube>
even then…
zolk3ri has left #ocaml [#ocaml]
<companion_cube>
good luck steering very busy researchers a way they don't want
<Drup>
at least it would be productive for something :p
<discord2>
<Bluddy> i guess you didn't pay attention. i was saying modular implicits are now many years away due to leo's new scope for its implementation, so i'd rather get something modest like unboxed arrays into the language
<Drup>
again, you are trying to decide what Leo should work on
<discord2>
<Bluddy> there's already a PR for it. it doesn't require much work.
<discord2>
<Bluddy> whatever, i don't want to argue.
FreeBirdLjj has quit [Ping timeout: 248 seconds]
sh0t has joined #ocaml
gpietro has quit [Read error: Connection reset by peer]
<companion_cube>
there's a PR for unboxed arrays‽ neat
<Drup>
not unboxed, no
<Drup>
well, defined what you mean by "unboxed", but that PR is a bit more subtle than that
<companion_cube>
I don't have much hope for flat memory layout in OCaml anyway…
<Drup>
(and it's nowhere near ready for merge, given than nobody agrees with Leo that language features are the right ones)
<companion_cube>
:D
<Drup>
his*
Haudegen has quit [Remote host closed the connection]
<octachron>
Bluddy, since you estimate this requires not much work, you should ask Leo to take the helm for the polishing of the PR. I would not be surprised that Leo would be quite willing to unload the polishing, refining, and implementation details part of this PR from him shoulder
<discord2>
<Perry> octachron, speaking of PRs, let me know in the next day or so what else I have to do to get the Bigarray docs sorted. I'm anxious to merge something just so that the manual will build correctly without errors.
<discord2>
<Perry> I'm happy to do what's needed if there's more, just point me at it.
<discord2>
<Perry> BTW, I noticed on my machine lots of unnecessary stuff gets rebuilt every time I touch the manual and re-make. I presume patches to fix that would be welcome?
<octachron>
Perry, sure. Any simplification or improvement of the build process is welcome
<octachron>
Bluddy, but honestly, my opinion is that there is still a lot of design work to do around this PR to make it more consensual and better fitting in the language
yomimono has quit [Ping timeout: 264 seconds]
<discord2>
<Perry> Bluddy posted something suggesting that the minimal parts be put in without most of the language extensions. That seems like it might work. The language extensions could then be put off until someone has a good idea how to do them in a harmonious way.
<discord2>
<Perry> The issue is mostly the syntax as I understood it from the PR.
FreeBirdLjj has joined #ocaml
sh0t has quit [Read error: Connection reset by peer]
gpietro has joined #ocaml
FreeBirdLjj has quit [Remote host closed the connection]
FreeBirdLjj has joined #ocaml
jimmyrcom_ has joined #ocaml
dedgrant_ has quit [Quit: Leaving]
<steenuil>
I really don't understand the build process of the manual
<steenuil>
there's at least four different programs written in Perl, C, and OCaml that try to quote the text in verbatim blocks before (I assume) it is fed into hevea
<octachron>
steenuil, good point, I should remove the tools that not used anymore
<steenuil>
which one is actually used now?
<octachron>
only the one documented in manual/README.md are actually used
<steenuil>
ah, right
<octachron>
aka texquote2 for quoting, transf for BNF grammar and caml_tex2 for the code examples
FreeBirdLjj has quit [Remote host closed the connection]
yomimono has joined #ocaml
<octachron>
Perry, your patch for bigarray looks nice. Concerning libbigarray.etex itself, I would replace it by a small introduction saying that the bigarray module libray has been integrated to the stdlib
<octachron>
except for the map_file function which is now part of the Unix module
<octachron>
and that the bigarray library bundled with the compiler now is compatibility library with exactly the same interface than before: i.e. with map_files included
mrvn has joined #ocaml
<companion_cube>
Bluddy[m]: really, a wiki easier than a PR to awesome ocaml‽
dedgrant has joined #ocaml
FreeBirdLjj has joined #ocaml
argent_smith has joined #ocaml
hdon has joined #ocaml
<discord2>
<Bluddy> companion_cube: definitely. Awesome ocaml is managed by one person, and a PR to anything slows you down and increases friction. Additionally, awesome ocaml has a flat structure, making finding things difficult. It also doesn't allow you expand the scope of documentation to cover other things, like relevant type theory.
<kakadu>
Bluddy[m]: What do you mean by flat structure?
<kakadu>
I think that it is as flat as wiki
<kakadu>
you can prepare links between markdown pages
<kakadu>
AFAIR
<discord2>
<Bluddy> companion_cube: If anything, you might ask why not ocaml.org. But ocaml.org requires content that is high quality content a-priori, unlike a wiki that can evolve incrementally. And once again, PRs are a pain point. Editing pages in the wiki, I had to iterate through probably 20 versions before I was happy with the result for just a small edit. PR-based processes don't allow for that.
j0sh has joined #ocaml
Haudegen has joined #ocaml
_whitelogger has joined #ocaml
<discord2>
<Bluddy> kakadu: I believe github pages (ie. github-hosted websites) allow you to link between pages made in markdown freely, but you don't get that effortlessly by default on github. That's why all the awesome pages are flat.
<discord2>
<Perry> octachron: I don't quite understand the bit about the bigarray library bundled with the compiler, but I'll prepare an edit and you can correct it.
<kakadu>
Bluddy[m]: So, [I'm a relative reference to a repository file](../blob/master/LICENSE) doesn't go to effortless category?
<octachron>
Perry, even in 4.07 there is still a bigarray library (i.e. a bigarray.cm(x)a files) bundled with the compiler for the sake of compatibility
gpietro has quit [Remote host closed the connection]
<discord2>
<Perry> From what I can tell, all that is still relevant is the compatibility library linking information.
<discord2>
<Perry> Anything else we need? I could submit a pull request if not.
<discord2>
<Perry> I should probably rename the section "the compatibility bigarray library"
malina has quit [Ping timeout: 246 seconds]
<discord2>
<Perry> actually, I think I'll call it "legacy" rather than "compatibility"
<octachron>
Perry, this seems nice. I tend to agree with the legacy name; but the last time, for the num library, Xavier Leroy disagreed. So I would keep the current name for the sake of consistency.
<discord2>
<Bluddy> kakadu: that's a pretty good point. I'll reconsider my approach.
<discord2>
<Bluddy> I don't like github wikis, but a repo with links to md files might be the best alternative
<discord2>
<Perry> octachron: so don't call it "the legacy bigarray library"?
<discord2>
<Perry> Also: htmlman/stdlib.html doesn't seem to link to everything in libref/index.html !
<discord2>
<Perry> is that intentional? I just noticed Unix isn't linked.
<octachron>
Perry, yes: stdlib.etex links to the standard library modules, and only them
<octachron>
unix is a separate library
<discord2>
<Perry> Ah. So how do I find the link to the Unix library in the documentation then? It isn't obvious, because I don't think it is linked from the Unix library chapter. But I may have missed it.
<octachron>
index.html contains link to all modules from the stdlib, bundled libraries, and compiler-libs (in other words, it is a bit messy currently)
<discord2>
<Perry> Ah! The htmlman/libunix.html does link to it, but not at the top! I will submit a distinct PR for this.
<discord2>
<Perry> And I'm reverting the name of the bigarray compat description.
jimmyrcom_ has quit [Ping timeout: 246 seconds]
<discord2>
<Perry> Octachron: Should I provide a pull request for the Bigarray fixes, or should I just hand you a patch?
FreeBirdLjj has quit [Remote host closed the connection]
<octachron>
Perry, a pull request would be nice. I don't see much point in me doing a PR in your stead, since you do have a github account
jbrown has quit [Ping timeout: 240 seconds]
FreeBirdLjj has joined #ocaml
<discord2>
<Perry> Cool. I'm almost done with it now.
<discord2>
<Perry> I'm now going to submit a pull request to tweak the Unix documentation.
FreeBirdLjj has quit [Ping timeout: 256 seconds]
dhil has quit [Ping timeout: 268 seconds]
<discord2>
<Perry> In hevea/latex, is there an equivalent of "ifouthtml" that is "ifnotouthtml"
<discord2>
<Perry> that is, a reversed test?
<octachron>
No, however there is a latexonly environment, or you can use \else
_whitelogger has joined #ocaml
<octachron>
\begin{latexonly}…\end{latexonly}
RalfJ has quit [Remote host closed the connection]
RalfJ has joined #ocaml
FreeBirdLjj has joined #ocaml
pierpal has quit [Quit: Poof]
pierpal has joined #ocaml
ctrlsbstr has joined #ocaml
pierpal has quit [Ping timeout: 248 seconds]
FreeBirdLjj has quit [Ping timeout: 248 seconds]
jbrown has joined #ocaml
bacam has quit [Quit: reboot]
noitakomentaja has joined #ocaml
jnavila has joined #ocaml
bacam has joined #ocaml
Haudegen has quit [Read error: Connection reset by peer]
muelleme has joined #ocaml
fantasticsid has joined #ocaml
pierpal has joined #ocaml
pierpal has joined #ocaml
pierpal has quit [Ping timeout: 264 seconds]
fantasti` has joined #ocaml
fantasticsid has quit [Ping timeout: 255 seconds]
Haudegen has joined #ocaml
noitakomentaja has quit [Ping timeout: 255 seconds]
zlsyx has quit [Quit: Leaving...]
FreeBirdLjj has joined #ocaml
ctrlsbstr has quit [Quit: My MacBook has gone to sleep. ZZZzzz…]
ctrlsbstr has joined #ocaml
noitakomentaja has joined #ocaml
FreeBirdLjj has quit [Ping timeout: 250 seconds]
fantasti` has quit [Quit: ERC (IRC client for Emacs 27.0.50)]
jnavila has quit [Remote host closed the connection]
_andre has quit [Quit: leaving]
ctrlsbstr has quit [Quit: My MacBook has gone to sleep. ZZZzzz…]
ctrlsbstr has joined #ocaml
silenc3r has joined #ocaml
<silenc3r>
Which one is faster Sequence.cons or Sequence.snoc?
argent_smith has quit [Quit: Leaving.]
<Drup>
silenc3r: if you are going to use "cons" a lot, consider not using Sequence at all.
noitakomentaja has quit [Ping timeout: 255 seconds]
<Drup>
(or rewriting things differently)
<silenc3r>
Drup: so I'm better off with using plain list?
<discord2>
<Perry> It will be easier to figure out how to make your application run fast if you explain what it is doing.
muelleme has quit [Ping timeout: 250 seconds]
hdon has quit [Ping timeout: 260 seconds]
<Drup>
silenc3r: if you just want to cons a lot, yes
<Drup>
or buffers
isd has joined #ocaml
<silenc3r>
Perry: It's plenty fast at the moment, I was just wondering about performance of these two functions.
<silenc3r>
Drup: that's all I need to know, thanks
jimmyrcom_ has joined #ocaml
<discord2>
<Perry> Performance is never an isolated question. If you do something once and it takes a few microseconds in a program that runs for an hour, no one cares. If you run something millions of times a second, it might matter, but of course, then the question becomes why are you doing it, and is there a better way to do the thing.
<discord2>
<Perry> It's often difficult to help people with performance related questions because they pose them too narrowly, asking just "does this call take a long time", without giving you the needed context to answer what they really want to know.
shinnya has joined #ocaml
jimmyrcom_ has quit [Ping timeout: 260 seconds]
<Drup>
what you say is not wrong, but sometimes, "how efficient is operation X on datastructure Y compared to datastructure Z" is a fairly valid question, even in isolation :p
<mrvn>
unless you have to consider cache effects
gtrak has quit [Ping timeout: 255 seconds]
ctrlsbstr has quit [Quit: My MacBook has gone to sleep. ZZZzzz…]
hdon has joined #ocaml
govg has quit [Ping timeout: 240 seconds]
govg has joined #ocaml
<discord2>
<Perry> Drup: that's certainly true, and we talk about that sort of thing a lot in algorithms classes and such, but in the real world, for example, using bubble sort on a list of length 10 once in a two hour program isn't interesting. 😃
<discord2>
<Perry> I think we are both in agreement of course.
hdon has quit [Changing host]
hdon has joined #ocaml
govg has quit [Ping timeout: 246 seconds]
FreeBirdLjj has joined #ocaml
sz0 has joined #ocaml
silenc3r has quit [Quit: Leaving]
muelleme has joined #ocaml
kakadu has quit [Remote host closed the connection]
muelleme has quit [Ping timeout: 260 seconds]
<discord2>
<mars0i> Wait, what? Is Bigarray going away? Just scanning the earlier posts. I just started learningBigarray. Owl is based on it.
<mrvn>
No way. they can't. what should replace it?
<discord2>
<mars0i> What is this talk of Bigarray as "legacy"?
<Drup>
Bigarray is not going away, on the contrary
<Drup>
it's moving into the normal standard library, instead of being one of the additional packages
<Drup>
And mmap is moved to Unix
<mrvn>
would be nice to have a bigarray of a Ctype struct.
<Drup>
mrvn: that's what cstruct is
<discord2>
<mars0i> Ahh. (Sigh of relief.)
<mrvn>
Drup: I never looked at the source but how does it cope with the fact that some struct members may be bytes, others ints and so on?
<mrvn>
potentially even unaligned longs.
<discord2>
<mars0i> OK I knew that was too bad to be true. I just wanted to know what the deal was.
<steenuil>
I've been trying to make hevea output html classes for the verbatim envs for a while now and I've come to the conclusion that either:
<steenuil>
a. the alltt env is somehow broken
<steenuil>
b. the hevea documentation is lying about \setenvclass
cbot has joined #ocaml
<steenuil>
and to tell you the truth, I don't really like either of those options
Haudegen has quit [Remote host closed the connection]
FreeBirdLjj has quit [Ping timeout: 256 seconds]
<discord2>
<Perry> steenuil: now that it is on github, you can file a trouble ticket.