Stream: Coq devs & plugin devs

Topic: 8.18.0 Docker


view this post on Zulip Notification Bot (Sep 12 2023 at 17:43):

Karl Palmskog has marked this topic as unresolved.

view this post on Zulip Karl Palmskog (Sep 12 2023 at 17:46):

I will ensure both Erik and Jaime are pinged when the 8.18.0 Docker can be created, but we need a bunch of merges and CI stuff to happen before that. Maybe @Emilio Jesús Gallego Arias would like to do the official SerAPI release for 8.18 now, or should I do that? (If I do the SerAPI release I will do it after 8.18.0 is out on opam and we have other core packages for 8.18 in released opam repo)

view this post on Zulip Karl Palmskog (Sep 12 2023 at 18:01):

the 8.18.0 opam PR got "consider for merge" topic now, so it should be done soon...

view this post on Zulip Notification Bot (Sep 12 2023 at 18:05):

Karl Palmskog has marked this topic as unresolved.

view this post on Zulip Karl Palmskog (Sep 13 2023 at 06:20):

any chance for someone knowledgeable about OCaml/flambda/etc. to take a look at these CI errors we got from opam CI (example below)? The current proposed solution is that flambda is completely disabled for OCaml 4.X (and also 5.X which this error came from), which will likely be a problem for many users.

#=== ERROR while compiling coq-stdlib.8.18.0 ==================================#
# context              2.2.0~alpha3~dev | linux/x86_64 | ocaml-options-only-flambda.1 | file:///home/opam/opam-repository
# path                 ~/.opam/5.0/.opam-switch/build/coq-stdlib.8.18.0
# command              ~/.opam/opam-init/hooks/sandbox.sh build dune build -p coq-stdlib -j 127 @install
# exit-code            1
# env-file             ~/.opam/log/coq-stdlib-7-7c4f76.env
# output-file          ~/.opam/log/coq-stdlib-7-7c4f76.out
### output ###
# File "theories/dune", line 1850, characters 1-1429:
# 1850 |  (rule
# 1851 |   (targets NewtonInt.timing NewtonInt.glob NewtonInt.vos NewtonInt.vo)
# 1852 |   (deps ../../theories/Init/Prelude.vo ../../theories/Reals/Rbase.vo
# 1853 |         ../../theories/Reals/Rfunctions.vo ../../theories/Reals/SeqSeries.vo
# 1854 |         ../../theories/Reals/Rtrigo1.vo ../../theories/Reals/Ranalysis.vo)
# 1855 |   (action (chdir ../../. (run coqc -boot -R theories Coq -Q user-contrib/Ltac2 Ltac2 -I /home/opam/.opam/5.0/lib/coq-core/plugins/number_string_notation -I /home/opam/.opam/5.0/lib/coq-core/plugins/zify -I /home/opam/.opam/5.0/lib/coq-core/plugins/tauto -I /home/opam/.opam/5.0/lib/coq-core/plugins/ssreflect -I /home/opam/.opam/5.0/lib/coq-core/plugins/micromega -I /home/opam/.opam/5.0/lib/coq-core/plugins/ltac -I /home/opam/.opam/5.0/lib/coq-core/plugins/extraction -I /home/opam/.opam/5.0/lib/coq-core/plugins/derive -I /home/opam/.opam/5.0/lib/coq-core/plugins/cc -I /home/opam/.opam/5.0/lib/coq-core/plugins/btauto -I /home/opam/.opam/5.0/lib/coq-core/plugins/ssrmatching -I /home/opam/.opam/5.0/lib/coq-core/plugins/rtauto -I /home/opam/.opam/5.0/lib/coq-core/plugins/ring -I /home/opam/.opam/5.0/lib/coq-core/plugins/nsatz -I /home/opam/.opam/5.0/lib/coq-core/plugins/ltac2 -I /home/opam/.opam/5.0/lib/coq-core/plugins/funind -I /home/opam/.opam/5.0/lib/coq-core/plugins/firstorder -w +default -q -w -deprecated-native-compiler-option -native-compiler off -time-file theories/Reals/NewtonInt.timing %{dep:NewtonInt.v}))))
# (cd _build/default && /home/opam/.opam/5.0/bin/coqc -boot -R theories Coq -Q user-contrib/Ltac2 Ltac2 -I /home/opam/.opam/5.0/lib/coq-core/plugins/number_string_notation -I /home/opam/.opam/5.0/lib/coq-core/plugins/zify -I /home/opam/.opam/5.0/lib/coq-core/plugins/tauto -I /home/opam/.opam/5.0/lib/coq-core/plugins/ssreflect -I /home/opam/.opam/5.0/lib/coq-core/plugins/micromega -I /home/opam/.opam/5.0/lib/coq-core/plugins/ltac -I /home/opam/.opam/5.0/lib/coq-core/plugins/extraction -I /home/opam/.opam/5.0/lib/coq-core/plugins/derive -I /home/opam/.opam/5.0/lib/coq-core/plugins/cc -I /home/opam/.opam/5.0/lib/coq-core/plugins/btauto -I /home/opam/.opam/5.0/lib/coq-core/plugins/ssrmatching -I /home/opam/.opam/5.0/lib/coq-core/plugins/rtauto -I /home/opam/.opam/5.0/lib/coq-core/plugins/ring -I /home/opam/.opam/5.0/lib/coq-core/plugins/nsatz -I /home/opam/.opam/5.0/lib/coq-core/plugins/ltac2 -I /home/opam/.opam/5.0/lib/coq-core/plugins/funind -I /home/opam/.opam/5.0/lib/coq-core/plugins/firstorder -w +default -q -w -deprecated-native-compiler-option -native-compiler off -time-file theories/Reals/NewtonInt.timing theories/Reals/NewtonInt.v)
# Error: Can't open ./theories/Reals/NewtonInt.vo.

view this post on Zulip Paolo Giarrusso (Sep 13 2023 at 06:29):

That's with ocaml 5.0 right? As long as ocaml 4 flambda is still supported, I hope we should be good for now?

view this post on Zulip Enrico Tassi (Sep 13 2023 at 06:30):

My understanding is that is ocaml 5.0 + flambda which is problematic, which is not a good combination anyway

view this post on Zulip Karl Palmskog (Sep 13 2023 at 06:32):

@Paolo Giarrusso the problem is that the current "solution" in the PR is to disable flambda also for 4.X

view this post on Zulip Paolo Giarrusso (Sep 13 2023 at 06:32):

Yeah I saw the fix from avsm and your comment

view this post on Zulip Karl Palmskog (Sep 13 2023 at 06:35):

OCaml 4 without flambda as a possibility for 8.18.0 would be near-disaster in my book, this is why I flag up here

view this post on Zulip Guillaume Melquiond (Sep 13 2023 at 06:41):

Just curious because the error message is not clear to me. Is it coqc that complains that it "Can't open ./theories/Reals/NewtonInt.vo."?

view this post on Zulip Karl Palmskog (Sep 13 2023 at 06:49):

it seems that the error actually comes from Dune

view this post on Zulip Karl Palmskog (Sep 13 2023 at 06:49):

maybe Dune expected some .vo file to exist after a coqc command, but it didn't show up due to flambda+OCaml 5 problem

view this post on Zulip Guillaume Melquiond (Sep 13 2023 at 06:50):

So, coqc finished "successfully" but without creating a .vo file?

view this post on Zulip Guillaume Melquiond (Sep 13 2023 at 06:51):

This smells like a compiler bug.

view this post on Zulip Karl Palmskog (Sep 13 2023 at 06:52):

my intuition after staring at the error log is that yes, coqc seems to simply not have built the .vo file but was still happy for some reason.

view this post on Zulip Enrico Tassi (Sep 13 2023 at 06:58):

IMO the bug is unrelated to Coq. Help convincing avms that it is a bogus one is welcome

view this post on Zulip Gaëtan Gilbert (Sep 13 2023 at 07:25):

I think the error comes from coqc
When a rule fails to produce the expected target it seems dune says something like

Error: Rule failed to generate the following targets:
- dev/shim/coqtop

(I modified the shim rule to produce nothing to test it)

view this post on Zulip Guillaume Melquiond (Sep 13 2023 at 07:26):

I am not sure I understand. Even if the bug itself is unrelated to Coq, if Coq is broken as a consequence, it is not bogus.

view this post on Zulip Gaëtan Gilbert (Sep 13 2023 at 07:26):

and Can't open $file looks like https://github.com/coq/coq/blob/0cb5c5eae761c8140d14720ca80f6c7eeebd8c29/lib/objFile.ml#L22

view this post on Zulip Guillaume Melquiond (Sep 13 2023 at 07:28):

So, it is really coqc that fails.

view this post on Zulip Guillaume Melquiond (Sep 13 2023 at 07:41):

It is really unfortunate that Coq silently discards the exception here. It would be helpful to know what has caused the failure (e.g., full disk).

view this post on Zulip Gaëtan Gilbert (Sep 13 2023 at 07:54):

maybe someone can try testing the bad settings with this patch https://github.com/coq/coq/pull/18040

view this post on Zulip Enrico Tassi (Sep 13 2023 at 08:08):

Guillaume Melquiond said:

It is really unfortunate that Coq silently discards the exception here. It would be helpful to know what has caused the failure (e.g., full disk).

This is what I meat, if the problem is that their CI is bogus... (it would not be the first time)

view this post on Zulip Emilio Jesús Gallego Arias (Sep 13 2023 at 11:28):

Karl Palmskog said:

I will ensure both Erik and Jaime are pinged when the 8.18.0 Docker can be created, but we need a bunch of merges and CI stuff to happen before that. Maybe Emilio Jesús Gallego Arias would like to do the official SerAPI release for 8.18 now, or should I do that? (If I do the SerAPI release I will do it after 8.18.0 is out on opam and we have other core packages for 8.18 in released opam repo)

Same here @Karl Palmskog , I think the coq-serapi release should happen once the coq packages have arrived to the core opam repos.

view this post on Zulip Jason Gross (Sep 13 2023 at 15:45):

It is really unfortunate that Coq silently discards the exception here. It would be helpful to know what has caused the failure (e.g., full disk).

Are we sure that Coq silently discards the exception? I have many times seen "no space left on device" as an error when building a Coq project (though I suppose it's possible I've seen it only from coqnative / ocamlopt and not coqc)

view this post on Zulip Gaëtan Gilbert (Sep 13 2023 at 15:52):

in this case the code is quite clear that it discards the exn

view this post on Zulip Karl Palmskog (Sep 13 2023 at 18:12):

the 8.18.0 packages got merged without conflicting with any flambda or OCaml version :tada:

The usual turnaround time for appearing via opam update is maybe 5-8 hours.

view this post on Zulip Karl Palmskog (Sep 13 2023 at 19:28):

apparently it was quicker than usual this time, it's now out. Process of moving plugins to released has begun: https://github.com/coq/opam/pull/2719

view this post on Zulip Enrico Tassi (Sep 13 2023 at 20:54):

Great!

view this post on Zulip Emilio Jesús Gallego Arias (Sep 14 2023 at 18:43):

@Karl Palmskog releases from my part are done.

view this post on Zulip Karl Palmskog (Sep 14 2023 at 18:45):

thanks, I will monitor when we have all packages merged/ready for Docker

view this post on Zulip Karl Palmskog (Sep 14 2023 at 18:46):

apparently OCaml 5.1.0 is out as well, for Coq users that should be the first viable 5.X release

view this post on Zulip Emilio Jesús Gallego Arias (Sep 14 2023 at 18:48):

Karl Palmskog said:

apparently OCaml 5.1.0 is out as well, for Coq users that should be the first viable 5.X release

Do you have a link to the perf numbers? I am still planning to have a look at 5.x perf with OCaml devs at some point this fall

view this post on Zulip Karl Palmskog (Sep 14 2023 at 18:50):

I only have my own time make -jX attempts, that I barely remember now, but where 5.1.0+rcX was typically 5-10% faster than 4.14.1 on a bunch of projects I tried like MathComp

view this post on Zulip Karl Palmskog (Sep 14 2023 at 18:51):

5.0.0 was super slow on projects with many short-running files, this was seemingly fixed

view this post on Zulip Karl Palmskog (Sep 14 2023 at 18:53):

maybe that at least gives some ideas for a proper benchmarking run

view this post on Zulip Emilio Jesús Gallego Arias (Sep 14 2023 at 19:09):

That seems interesting, I assume coq-native wasn't installed on 4.14 right?

view this post on Zulip Emilio Jesús Gallego Arias (Sep 14 2023 at 19:09):

Yes that is useful, I hope to do some benchs, but I need to understand better what GC tweaks the OCaml devs suggest

view this post on Zulip Karl Palmskog (Sep 14 2023 at 19:20):

I personally don't use coq-native, no

view this post on Zulip Emilio Jesús Gallego Arias (Sep 14 2023 at 19:26):

Karl Palmskog said:

5.0.0 was super slow on projects with many short-running files, this was seemingly fixed

yes that bug was the one with the Dynlink loader, so indeed a silly but pretty serious bug in terms of performance.

view this post on Zulip Karl Palmskog (Sep 16 2023 at 11:25):

@Jaime Arias @Erik Martin-Dorel now all opam packages are in place for the Docker image with Coq 8.18.0. In particular, we have coq-serapi.8.18.0+0.18.1 and coq-bignums.9.0.0+8.18 out.

view this post on Zulip Erik Martin-Dorel (Sep 20 2023 at 00:04):

Hi! Thanks a lot @Karl Palmskog and all the devs involved in the release! :+1: :+1:

I just pushed https://github.com/coq-community/docker-coq/commit/23097615ee0089991685ecc2b4066bd75b5a92c8

And you can monitor this gitlab ci pipeline: https://gitlab.com/coq-community/docker-coq/-/pipelines/1010307109

Meanwhile, the docker hub docs (summarizing the available tags) is already up-to-date:

https://hub.docker.com/r/coqorg/coq#supported-tags

view this post on Zulip Erik Martin-Dorel (Sep 20 2023 at 00:05):

Tomorrow, I will update the mathcomp+mathcomp-dev images in Docker Hub

view this post on Zulip Erik Martin-Dorel (Sep 21 2023 at 09:06):

Cc @Karl Palmskog et al.

I will update the mathcomp+mathcomp-dev images in Docker Hub

Done: the mathcomp images involving coq-8.18 are now shipped with 8.18.0, and all images contain the latest opam release, 2.1.5:

view this post on Zulip Pierre Roux (Sep 21 2023 at 12:40):

FTR, it's nice to have an alternative CI in mathcomp, this just caught silent failures in our Nix CI: https://github.com/coq-community/coq-nix-toolbox/pull/162 , thanks @Erik Martin-Dorel !

view this post on Zulip Karl Palmskog (Sep 21 2023 at 12:41):

best CI setup to me is having both:

Lots of issues have been found with this during the years.

view this post on Zulip Erik Martin-Dorel (Sep 21 2023 at 12:45):

Yes, it's good to mix several build systems when several are supported!

FWIW in MathComp's GitLab Inria CI using Docker, we already mix two versions:


Last updated: May 18 2024 at 10:02 UTC