IIRC 8.11 requires 4.05. Is this requirement the same for 8.12? IIRC the windows installer uses a more recent version for example.
8.12 should work fine with 4.05.0 ; windows uses 4.08 due to fixes in the Windows OCaml backend. Ideally we would move to 4.08 at some point but until we fix plugin linking that's not doable without breaking a bunch of plugins, also there is the issue of lower GC performance in >= 4.08
OCaml 4.08 lets you overload (let*)
and this makes monadic code look way more natural, this is why I'm asking.
Can you say more about the linking problem and the affected plugins?
https://github.com/coq/coq/issues/12067
I did some experiments with let*
for the tactic monad, and indeed it brings little, which shows the monad is pretty weird indeed.
Hum, the issue talks about many plugins, lists one, and does not say which module is doubly linked. Also coq_makefile has an explicit list of what is linked in Coq to avoid double linking (at least, double linking modules that are already in Coq). Is this list outdated? Would you mind adding more info?
I did some experiments with let* for the tactic monad
My real use case was Lwt... Now that I think about it, the current monad forces the type parameter to be unit
most of the time defeating the whole point of let (and bind). Anyway, this is another story.
Let's just say there are no strong incentives to move to 4.08, I can live with that.
Note that the macOS build was modified to use 4.07 in the v8.11
and v8.12
branches and that the Windows add-on build is not working with OCaml 4.08 either so coq/coq#12415 contains a revert to 4.07 as well.
Hum, OK. Can you say the reason? If we are forced to use 4.07, then we should be aware of that and use everything it offers (over 4.05, which I don't recall but maybe there is something). Thanks for pointing out the 4.08 problem, this really makes it a no-no for what I wanted to do!
Note that fiat-crypto suffers heavily (possibly over a 10x slowdown in compiling extracted code?) transitioning from 4.06 to 4.08, see https://github.com/ocaml/ocaml/issues/7826#issuecomment-625342743
Last updated: May 28 2023 at 13:30 UTC