Stream: Coq users

Topic: Ocaml recommended version


view this post on Zulip Laurent Théry (Mar 15 2022 at 08:29):

I am installing coq via opam. What is the recommended ocaml version.? In the doc here ir is mentionned 4.05.0, is it ok?

view this post on Zulip Karl Palmskog (Mar 15 2022 at 08:34):

4.05.0 has a bug where some plugins will not compile under certain circumstances. In the past, we generally recommended 4.07.1 (which does not have the bug of 4.05.0, and does not have the rare plugin loading issue in >= 4.08)

view this post on Zulip Karl Palmskog (Mar 15 2022 at 08:35):

the latest Coq Platform release currently uses OCaml 4.10.2, so you know that version at least builds the stuff in the Platform

view this post on Zulip Laurent Théry (Mar 15 2022 at 08:39):

@Karl Palmskog Thanks, I will go for 4.10.2

view this post on Zulip Laurent Théry (Mar 15 2022 at 08:53):

no luck, there is something wrong with my conf

#=== ERROR while compiling ocaml-base-compiler.4.10.2 =========================#
# context     2.1.1 | linux/x86_64 |  | https://opam.ocaml.org#d022af4a
# path        /home/thery/opam-coq.8.12.0/4.10.2/.opam-switch/build/ocaml-base-compiler.4.10.2
# command     /home/thery/opam-coq.8.12.0/opam-init/hooks/sandbox.sh build make -j1 world.opt
# exit-code   2
# env-file    /home/thery/opam-coq.8.12.0/log/ocaml-base-compiler-302821-c56e18.env
# output-file /home/thery/opam-coq.8.12.0/log/ocaml-base-compiler-302821-c56e18.out
### output ###
# [...]
# gcc -c -O2 -fno-strict-aliasing -fwrapv -Wall -fno-common -fno-tree-vrp -ffunction-sections -g -D_FILE_OFFSET_BITS=64 -D_REENTRANT -DCAML_NAME_SPACE   -DNATIVE_CODE -DTARGET_amd64 -DMODEL_default -DSYS_linux   -o signals_n.o signals.c
# gcc -c -O2 -fno-strict-aliasing -fwrapv -Wall -fno-common -fno-tree-vrp -ffunction-sections -g -D_FILE_OFFSET_BITS=64 -D_REENTRANT -DCAML_NAME_SPACE   -DNATIVE_CODE -DTARGET_amd64 -DMODEL_default -DSYS_linux   -o signals_nat_n.o signals_nat.c
# signals_nat.c:194:13: error: variably modified sig_alt_stack at file scope
#   194 | static char sig_alt_stack[SIGSTKSZ];

``

view this post on Zulip Karl Palmskog (Mar 15 2022 at 08:54):

hmm, that looks like a gcc version issue?

view this post on Zulip Laurent Théry (Mar 15 2022 at 08:58):

% gcc --version
gcc (GCC) 11.2.1 20220127 (Red Hat 11.2.1-9)

view this post on Zulip Pierre Roux (Mar 15 2022 at 09:04):

That's quite recent, maybe not supported by OCaml 4.10.

view this post on Zulip Karl Palmskog (Mar 15 2022 at 09:05):

right, if your gcc is that up to date, you may have to try 4.13 (which not all Coq plugins, etc., support)

view this post on Zulip Laurent Théry (Mar 15 2022 at 09:06):

bad luck, thanks

view this post on Zulip Guillaume Melquiond (Mar 15 2022 at 09:08):

The incompatibility is with the glibc. It will be fixed in the next release of OCaml.

view this post on Zulip Karl Palmskog (Mar 15 2022 at 09:09):

oh, so not even 4.13 works?

view this post on Zulip Guillaume Melquiond (Mar 15 2022 at 09:10):

My mistake, the patch indeed made its way into 4.13.

view this post on Zulip Laurent Théry (Mar 15 2022 at 09:10):

Is it this the problem?

view this post on Zulip Karl Palmskog (Mar 15 2022 at 09:11):

OK, but it's still valuable to know that certain new glibc versions do not support OCaml <= 4.12. Should we open a Platform issue pre-emptively @Michael Soegtrop?

view this post on Zulip Guillaume Melquiond (Mar 15 2022 at 09:11):

Laurent Théry said:

Is it this the problem?

Yes.

view this post on Zulip Guillaume Melquiond (Mar 15 2022 at 09:34):

Actually, while vanilla OCaml releases do not have the fix, the Opam packages ship with the patch. So, if you have an Opam-provided OCaml, you should be fine, even with an older release (as long as you compiled it recently).

view this post on Zulip Karl Palmskog (Mar 15 2022 at 09:35):

hmm, but how far back do those fixes go? Clearly, Laurent's opam installation of 4.10.2 failed...

view this post on Zulip Guillaume Melquiond (Mar 15 2022 at 09:37):

That is what I was saying: you need to have compiled OCaml after the Opam package was patched. They have patched quite far back; even 4.05 has the fix.

view this post on Zulip Karl Palmskog (Mar 15 2022 at 09:39):

the packages were seemingly updated in January 2022: https://github.com/ocaml/opam-repository/commit/05035330325eb132d95446aecab07eddd88f110a

view this post on Zulip Karl Palmskog (Mar 15 2022 at 09:40):

maybe @Laurent Théry could just try opam update and then reinstall 4.10.2 then?

view this post on Zulip Guillaume Melquiond (Mar 15 2022 at 09:41):

In fact, they have patched the Opam packages all the way back, so even 3.07 has the patch.

view this post on Zulip Michael Soegtrop (Mar 15 2022 at 12:08):

@Karl Palmskog : as far as I can tell this was merged back to at least OCaml 4.10.2 - which is the version Coq Platform is using.

view this post on Zulip Michael Soegtrop (Mar 15 2022 at 12:09):

@Laurent Théry : I would say one of the best tested OCaml versions for Coq is the one Coq Platform is using (there is massive CI on it). Coq Platform currently uses 4.10.2.

view this post on Zulip Paolo Giarrusso (Mar 15 2022 at 20:13):

Beware 4.10.2 has a nontrivial performance bug (20-30% slowdown), unless you're using the backported patch?

view this post on Zulip Paolo Giarrusso (Mar 15 2022 at 20:14):

4.07.1+flambda avoids that (but doesn't work on ARM-Macos)

view this post on Zulip Emilio Jesús Gallego Arias (Mar 15 2022 at 22:59):

I recommend 4.13

view this post on Zulip Emilio Jesús Gallego Arias (Mar 15 2022 at 22:59):

4.13+flambda actually in most cases

view this post on Zulip Laurent Théry (Mar 16 2022 at 08:11):

@Paolo Giarrusso is there an easy way to know if the version I have has the backported patch?

view this post on Zulip Laurent Théry (Mar 16 2022 at 08:18):

Following Coq-Platform choice seems reasonable to me so I will go for 4.10.2. Is there a way to do a PR so to change 4.05.0 into 4.10.2 in web documentation i(https://coq.inria.fr/opam-using.html)

Found, it is https://github.com/coq/www. did a PR

view this post on Zulip Michael Soegtrop (Mar 16 2022 at 08:19):

@Laurent Théry : as long as you use opam to install ocaml, ocamlc won't build if you need the patch (have a modified C library) and don't have the patch. I am not sure what happens if you install a binary ocamlc (say via a system package manager).

view this post on Zulip Paolo Giarrusso (Mar 16 2022 at 08:58):

sorry, I shouldn’t have said just “the backported patch” — AFAICT @Michael Soegtrop is talking about the patch restoring compatibility with newer glibc. I was talking of https://github.com/coq/coq/issues/11652#issuecomment-1039700928

view this post on Zulip Laurent Théry (Mar 16 2022 at 09:03):

I am lost there are two different patches or it is the same?

view this post on Zulip Karl Palmskog (Mar 16 2022 at 10:15):

two different patches are discussed:

Since the status of the second patch is unclear, it's probably better to go with 4.07.1+flambda or 4.13.1+flambda to ensure good performance.

view this post on Zulip Michael Soegtrop (Mar 16 2022 at 13:04):

@Karl Palmskog : thanks for the hint on the performance issue - do you have the github issue?

I don't see performance issues with 4.10.2 - it is quite fast in my application (which uses a lot of nasty automation) and I also didn't hear anything negative from Coq Platform users. So I would still recommend to use what is most tested.

Maybe we should included a speed test in Coq Platform CI.

view this post on Zulip Karl Palmskog (Mar 16 2022 at 13:18):

@Michael Soegtrop I think it's well-known that flambda-enabled compilers are typically significantly faster for Coq compilation (5-10% at least?). But I'd have to defer to @Emilio Jesús Gallego Arias for the exact performance numbers and whole story.

view this post on Zulip Karl Palmskog (Mar 16 2022 at 13:19):

I don't know about the specific performance problems in 4.10.2, do you have some link @Paolo Giarrusso?

view this post on Zulip Michael Soegtrop (Mar 16 2022 at 13:20):

I anyway plan to update OCaml for 2022.03. So I guess what I should try is 4.13+flambda?

view this post on Zulip Paolo Giarrusso (Mar 16 2022 at 14:05):

For the performance issue I gave the link above. Last I checked coq-elpi wasn’t compatible with 4.13, but opam knows.

view this post on Zulip Karl Palmskog (Mar 16 2022 at 14:12):

ah OK, so this was the performance-on-4.10.2-link: https://github.com/coq/coq/issues/11652#issuecomment-1039700928

view this post on Zulip Paolo Giarrusso (Mar 16 2022 at 14:24):

yes — and it's not a blocker, just suboptimal. From the OP of that issue (https://github.com/coq/coq/issues/11652):

That resulted in an almost 14% slowdown for the full Iris build time. As you can see, every single file got slower, some by almost 30%.

view this post on Zulip Paolo Giarrusso (Mar 16 2022 at 14:27):

The patch is https://github.com/ocaml/ocaml/commit/a52f49bd2c18b548d7d420f4f628b0acda5b62b9, and I think one could backport it easily for one OCaml version in the Opam package. Backporting it to all affected OCaml variants would be more work, and I don't know how upstream opam packagers handle that — clearly somebody must have a script :sweat_smile:

view this post on Zulip Emilio Jesús Gallego Arias (Mar 16 2022 at 14:28):

4.10 still had the performance problem and it is serious, tho I think we added a workaround Coq side, so it may be gone finally. But indeed, no reason to prefer 4.10 to any other more modern OCaml

view this post on Zulip Paolo Giarrusso (Mar 16 2022 at 14:41):

elpi is in the Coq Platform, and even the latest elpi (elpi.1.14.1) demands "camlp5" {< "7.99"} which in turn means "ocaml" {>= "4.02" & < "4.13.0"}.

view this post on Zulip Paolo Giarrusso (Mar 16 2022 at 14:44):

Upgrading to Camlp5 8 raises other problems — I use some hacks on GitHub (and I could share links), but they're not too robust — Emilio Enrico plans to replace camlp5, but that's not as easy :sweat_smile: .

view this post on Zulip Théo Zimmermann (Mar 16 2022 at 14:47):

Enrico (not Emilio)

view this post on Zulip Paolo Giarrusso (Mar 16 2022 at 14:54):

thanks my bad. (And I was thinking of the right person...)

view this post on Zulip Notification Bot (Mar 17 2022 at 07:15):

Laurent Théry has marked this topic as resolved.

view this post on Zulip Alexander Gryzlov (Mar 17 2022 at 10:09):

Emilio Jesús Gallego Arias said:

4.13+flambda actually in most cases

I have a stupid question - is this called 4.13.1+options now?

view this post on Zulip Laurent Théry (Mar 17 2022 at 10:20):

it seems that the +options let you choose between several options : https://ocaml.org/releases/4.13.1.html

view this post on Zulip Alexander Gryzlov (Mar 17 2022 at 10:24):

oh I see, thanks!

view this post on Zulip Emilio Jesús Gallego Arias (Mar 17 2022 at 13:22):

Yes it is named differently now!

view this post on Zulip Michael Soegtrop (Mar 21 2022 at 10:35):

@Emilio Jesús Gallego Arias : I tried Coq Platform with 4.13.1+flambda, but elpi is not compatible with it, because it requires camlp5 7.x. Are there reasons against 4.12+flambda?

view this post on Zulip Michael Soegtrop (Mar 21 2022 at 10:37):

4.12.1+flambda to be specific. There is also a 4.12.2 but only half.

view this post on Zulip Emilio Jesús Gallego Arias (Mar 21 2022 at 10:56):

4.12 is good in my book too

view this post on Zulip Emilio Jesús Gallego Arias (Mar 21 2022 at 10:57):

Maybe have a look at the OCaml changelog for 4.13, but 4.12 was already a very good version I understand

view this post on Zulip Michael Soegtrop (Mar 21 2022 at 11:00):

@Emilio Jesús Gallego Arias : thanks for the confirmation. I will try with 4.12.1+flambda then.

view this post on Zulip Notification Bot (Mar 21 2022 at 11:00):

Karl Palmskog has marked this topic as unresolved.

view this post on Zulip Karl Palmskog (Mar 21 2022 at 11:01):

I think I've asked before that Coq core devs explicitly recommend an OCaml version + options, this is probably as close as we might get

view this post on Zulip Karl Palmskog (Mar 21 2022 at 11:02):

@Michael Soegtrop maybe it would be useful to have a Platform specific performance benchmark, e.g., time compilation of MathComp, Stdpp, Iris (with the same number of cores, across different operating systems)

view this post on Zulip Michael Soegtrop (Mar 21 2022 at 11:03):

Or the compilation time of the complete platform in sequential mode ...

view this post on Zulip Karl Palmskog (Mar 21 2022 at 11:04):

but that will 5+ hours at this point, if we include UniMath, right?

view this post on Zulip Michael Soegtrop (Mar 21 2022 at 11:04):

I have good statistics on CI run times ...

view this post on Zulip Michael Soegtrop (Mar 21 2022 at 11:05):

Yes, something like this. But as I said, one could do statistics over the nightly CI runs.

view this post on Zulip Karl Palmskog (Mar 21 2022 at 11:06):

sure, but CI run times will include a bunch of stuff not related to Coq, maybe reuse coq-bench scripts?

view this post on Zulip Michael Soegtrop (Mar 21 2022 at 11:06):

Emilio Jesús Gallego Arias said:

Maybe have a look at the OCaml changelog for 4.13, but 4.12 was already a very good version I understand

The only possibly relevant entry I see there are improvements to the garbage collector - this could be relevant to Coq.

view this post on Zulip Michael Soegtrop (Mar 21 2022 at 11:07):

Karl Palmskog said:

sure, but CI run times will include a bunch of stuff not related to Coq, maybe reuse coq-bench scripts?

Yes, but it somehow reflects the real thing - it should be close to what users experience. I would think that the CI overhead is small compared to building Coq stuff.

view this post on Zulip Alexander Gryzlov (Mar 21 2022 at 11:25):

Michael Soegtrop said:

Emilio Jesús Gallego Arias : I tried Coq Platform with 4.13.1+flambda, but elpi is not compatible with it, because it requires camlp5 7.x. Are there reasons against 4.12+flambda?

Yeah, I had the same issue, which boils down to merging https://github.com/LPCIC/elpi/pull/110 AFAICS

view this post on Zulip Paolo Giarrusso (Mar 21 2022 at 11:43):

:+1: to that MR, I think Camlp5 8 should finally work on homebrew (at least, it worked for me).

view this post on Zulip Paolo Giarrusso (Mar 21 2022 at 11:44):

BTW, I think alectryon and elpi remain incompatible on recent OCaml (already 4.10), until the findlib fixes in Coq 8.16. But it hasn’t been a blocker for the platform, just a known issue (hopefully already googlable).

view this post on Zulip Guillaume Melquiond (Mar 21 2022 at 12:18):

Keep in mind that Flambda sometimes struggles on automatically generated OCaml code, e.g., Extraction or native_compute, as some of its algorithms have not yet been as optimized as those from the vanilla compiler. So, depending on the application, I would refrain from using Flambda. (That said, there are also some extracted algorithms that are usable only when compiled with Flambda, as they instantly cause a stack overflow otherwise.)


Last updated: Feb 01 2023 at 13:03 UTC