Stream: Coq users

Topic: Ocaml recommended version

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?

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)

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

Laurent Théry (Mar 15 2022 at 08:39):

@Karl Palmskog Thanks, I will go for 4.10.2

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];

``

Karl Palmskog (Mar 15 2022 at 08:54):

hmm, that looks like a gcc version issue?

Laurent Théry (Mar 15 2022 at 08:58):

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

Pierre Roux (Mar 15 2022 at 09:04):

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

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)

Laurent Théry (Mar 15 2022 at 09:06):

bad luck, thanks

Guillaume Melquiond (Mar 15 2022 at 09:08):

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

Karl Palmskog (Mar 15 2022 at 09:09):

oh, so not even 4.13 works?

Guillaume Melquiond (Mar 15 2022 at 09:10):

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

Laurent Théry (Mar 15 2022 at 09:10):

Is it this the problem?

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?

Guillaume Melquiond (Mar 15 2022 at 09:11):

Laurent Théry said:

Is it this the problem?

Yes.

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).

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...

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.

Karl Palmskog (Mar 15 2022 at 09:39):

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

Karl Palmskog (Mar 15 2022 at 09:40):

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

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.

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.

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.

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?

Paolo Giarrusso (Mar 15 2022 at 20:14):

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

Emilio Jesús Gallego Arias (Mar 15 2022 at 22:59):

I recommend 4.13

Emilio Jesús Gallego Arias (Mar 15 2022 at 22:59):

4.13+flambda actually in most cases

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?

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

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).

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

Laurent Théry (Mar 16 2022 at 09:03):

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

Karl Palmskog (Mar 16 2022 at 10:15):

two different patches are discussed:

• the glibc related patch that makes earlier OCaml versions like 4.10.2 compile on recent glibc/gcc
• a patch to fix the performance bug on 4.10.2

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.

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.

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.

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?

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?

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.

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

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%.

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:

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

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"}.

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: .

Théo Zimmermann (Mar 16 2022 at 14:47):

Enrico (not Emilio)

Paolo Giarrusso (Mar 16 2022 at 14:54):

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

Notification Bot (Mar 17 2022 at 07:15):

Laurent Théry has marked this topic as resolved.

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?

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

Alexander Gryzlov (Mar 17 2022 at 10:24):

oh I see, thanks!

Emilio Jesús Gallego Arias (Mar 17 2022 at 13:22):

Yes it is named differently now!

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?

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.

Emilio Jesús Gallego Arias (Mar 21 2022 at 10:56):

4.12 is good in my book too

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

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.

Notification Bot (Mar 21 2022 at 11:00):

Karl Palmskog has marked this topic as unresolved.

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

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)

Michael Soegtrop (Mar 21 2022 at 11:03):

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

Karl Palmskog (Mar 21 2022 at 11:04):

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

Michael Soegtrop (Mar 21 2022 at 11:04):

I have good statistics on CI run times ...

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.

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?

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.

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.

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

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).

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).

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: Oct 05 2023 at 02:01 UTC