Enrico Tassi (Jun 05 2020 at 10:21): Enrico Tassi (Jun 05 2020 at 10:21):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.
Emilio Jesús Gallego Arias (Jun 05 2020 at 10:23):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
Enrico Tassi (Jun 05 2020 at 10:24):OCaml 4.08 lets you overload (let*) and this makes monadic code look way more natural, this is why I'm asking.
Enrico Tassi (Jun 05 2020 at 10:24):Can you say more about the linking problem and the affected plugins?
Emilio Jesús Gallego Arias (Jun 05 2020 at 11:43):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.
Enrico Tassi (Jun 05 2020 at 11:55):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.
Théo Zimmermann (Jun 05 2020 at 12:45):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.
Enrico Tassi (Jun 05 2020 at 13:08):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!
Jason Gross (Jun 06 2020 at 04:34):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: Apr 20 2024 at 10:02 UTC