Notification Bot (Sep 12 2023 at 17:43): Notification Bot (Sep 12 2023 at 17:43):Karl Palmskog has marked this topic as unresolved.
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)
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...
Notification Bot (Sep 12 2023 at 18:05):Karl Palmskog has marked this topic as unresolved.
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.
That's with ocaml 5.0 right? As long as ocaml 4 flambda is still supported, I hope we should be good for now?
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
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
Paolo Giarrusso (Sep 13 2023 at 06:32):Yeah I saw the fix from avsm and your comment
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
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."?
Karl Palmskog (Sep 13 2023 at 06:49):it seems that the error actually comes from Dune
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
Guillaume Melquiond (Sep 13 2023 at 06:50):So, coqc finished "successfully" but without creating a .vo file?
Guillaume Melquiond (Sep 13 2023 at 06:51):This smells like a compiler bug.
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.
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
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)
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.
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
Guillaume Melquiond (Sep 13 2023 at 07:28):So, it is really coqc that fails.
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).
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
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)
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
releasedopam repo)
Same here @Karl Palmskog , I think the coq-serapi release should happen once the coq packages have arrived to the core opam repos.
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)
Gaëtan Gilbert (Sep 13 2023 at 15:52):in this case the code is quite clear that it discards the exn
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.
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
Enrico Tassi (Sep 13 2023 at 20:54):Great!
Emilio Jesús Gallego Arias (Sep 14 2023 at 18:43):@Karl Palmskog releases from my part are done.
Karl Palmskog (Sep 14 2023 at 18:45):thanks, I will monitor when we have all packages merged/ready for Docker
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
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
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
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
Karl Palmskog (Sep 14 2023 at 18:53):maybe that at least gives some ideas for a proper benchmarking run
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?
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
Karl Palmskog (Sep 14 2023 at 19:20):I personally don't use coq-native, no
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.
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.
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
Erik Martin-Dorel (Sep 20 2023 at 00:05):Tomorrow, I will update the mathcomp+mathcomp-dev images in Docker Hub
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:
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 !
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.
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: Nov 29 2023 at 22:01 UTC