Stream: Coq devs & plugin devs

Topic: min OCaml version for 8.12 (and 8.13)


view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Enrico Tassi (Jun 05 2020 at 10:24):

Can you say more about the linking problem and the affected plugins?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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!

view this post on Zulip 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: Oct 15 2021 at 21:02 UTC