Enrico Tassi (Aug 03 2023 at 12:02): Enrico Tassi (Aug 03 2023 at 12:02):We have tagged and I'm working on a script to automate opam package publishing.
The result it here: https://github.com/coq/opam-coq-archive/pull/2643
The question is: what is the coq-doc package? (was not there in 8.17)
Karl Palmskog (Aug 03 2023 at 12:05):ah, but weren't you going to publish this on opam-repository per https://github.com/coq/coq/wiki/Coq-Call-2023-03-08
Enrico Tassi (Aug 03 2023 at 12:11):Good point, but I had no time to fulfill the TODOs, so I guess we will do it for 8.19 ;-/
Enrico Tassi (Aug 03 2023 at 12:11):(we are still in time, but I don't have the time)
Karl Palmskog (Aug 03 2023 at 12:11):OK, just double checking
Karl Palmskog (Aug 03 2023 at 12:13):then I think we have the usual ecosystem TODO:
8.18 Docker image Karl Palmskog (Aug 03 2023 at 12:14):I'd be interested to know about whether coq-doc is supposed to be a thing or not (in Platform and elsewhere)
Pierre Roux (Aug 03 2023 at 12:31):Karl Palmskog said:
- get bignums tag
Done: https://github.com/coq-community/bignums/releases/tag/v9.0.0%2Bcoq8.18
Karl Palmskog (Aug 03 2023 at 12:36):OK, I guess I will do the SerAPI tag (a rc1 tag in extra-dev due to 8.18+rc1 not in opam-repository), unless @Emilio Jesús Gallego Arias has anything against it
Karl Palmskog (Aug 03 2023 at 12:51):@Enrico Tassi it looks like the coq-doc package is broken in the CI, maybe we just don't add it to opam repos?
Karl Palmskog (Aug 03 2023 at 12:51):the coqide-server tests are seemingly also broken
Enrico Tassi (Aug 03 2023 at 12:56):It seems the dune rules expect the package coq to be installed, which I guess is not reflected by the dependencies
Enrico Tassi (Aug 03 2023 at 12:56):let me try to fix both by hand for now
Karl Palmskog (Aug 03 2023 at 12:56):ah, but no package should depend on just coq, right? I think you mean coq-core?
Enrico Tassi (Aug 03 2023 at 12:59):I tend to agree, but that is the quick fix
Enrico Tassi (Aug 03 2023 at 12:59):let's see if it works
Enrico Tassi (Aug 03 2023 at 13:00):Installing coqide-server.8.18+rc1
[WARNING] Running as root is not recommended
[ERROR] The compilation of coqide-server.8.18+rc1 failed at "dune build -p coqide-server -j 2 @install @runtest".
#=== ERROR while compiling coqide-server.8.18+rc1 =============================#
# context 2.1.2 | linux/x86_64 | ocaml-base-compiler.4.14.0 | file:///builds/coq/opam-coq-archive/core-dev
# path ~/opam-root-4.14.0-2.1.2-sandbox/4.14.0/.opam-switch/build/coqide-server.8.18+rc1
# command ~/opam-root-4.14.0-2.1.2-sandbox/opam-init/hooks/sandbox.sh build dune build -p coqide-server -j 2 @install @runtest
# exit-code 1
# env-file ~/opam-root-4.14.0-2.1.2-sandbox/log/coqide-server-48004-c69e46.env
# output-file ~/opam-root-4.14.0-2.1.2-sandbox/log/coqide-server-48004-c69e46.out
### output ###
# [...]
# File "test-suite/dune", line 14, characters 0-145:
# 14 | (rule
# 15 | (targets bin.inc)
# 16 | (action (with-stdout-to %{targets} (run ./ocaml_pwd.exe -quoted -trailing-slash ../../install/%{context_name}/bin/ ))))
# (cd _build/default/test-suite && ./ocaml_pwd.exe -quoted -trailing-slash ../../install/default/bin/) > _build/default/test-suite/bin.inc
# Fatal error: exception Sys_error("../../install/default/bin/: No such file or directory")
# File "test-suite/dune", line 10, characters 0-137:
# 10 | (rule
# 11 | (targets libpath.inc)
# 12 | (action (with-stdout-to %{targets} (run ./ocaml_pwd.exe -quoted ../../install/%{context_name}/lib/coq/ ))))
# (cd _build/default/test-suite && ./ocaml_pwd.exe -quoted ../../install/default/lib/coq/) > _build/default/test-suite/libpath.inc
# Fatal error: exception Sys_error("../../install/default/lib/coq/: No such file or directory")
probably not running @runtest would also do, I'll try that
Enrico Tassi (Aug 03 2023 at 14:02):It worked, the packages are merged.
Enrico Tassi (Aug 03 2023 at 14:21):CC @Erik Martin-Dorel for the docker images
Karl Palmskog (Aug 03 2023 at 14:22):in the current setup, Erik needs the SerAPI rc1 package as well in extra-dev, I will try to get this done in the next few hours and ping him
Théo Zimmermann (Aug 04 2023 at 07:53):coq-doc is indeed a non-working opam package for now, but the fix should come soon (?): https://github.com/coq/coq/pull/17808
Karl Palmskog (Aug 04 2023 at 10:13):coq-serapi.8.18+rc1+0.18.0 is out on extra-dev, all ingredients are there for the new 8.18 Docker
Karl Palmskog (Aug 08 2023 at 19:31):the 8.18 Docker image is out, I did a bunch of project releases relying on it. Arguably the remaining automation niceness would be the MathComp 8.18 Docker.
Erik Martin-Dorel (Aug 09 2023 at 12:14):@Karl Palmskog yes, sure! The build is ongoing for coq 8.18+rc1 + mathcomp 1.x:
https://gitlab.inria.fr/math-comp/docker-mathcomp/-/pipelines/843498
Erik Martin-Dorel (Aug 09 2023 at 12:15):Will also prepare a mathcomp 2 counterpart ASAP
Erik Martin-Dorel (Aug 09 2023 at 12:54):The build for coq.18+rc1 + mathcomp 2.0.0 is pending:
https://gitlab.inria.fr/math-comp/docker-mathcomp/-/pipelines/843518
Erik Martin-Dorel (Aug 09 2023 at 14:03):@Karl Palmskog done
Erik Martin-Dorel (Aug 09 2023 at 14:04):Now, a mathcomp stable + coq.dev build is pending:
https://gitlab.inria.fr/math-comp/docker-mathcomp/-/pipelines/843558
Erik Martin-Dorel (Aug 09 2023 at 15:57):@Karl Palmskog done; I'll just need to update the list here, tonight: https://hub.docker.com/r/mathcomp/mathcomp#supported-tags (this is not automated yet, maybe this is feasible now, I'll recheck soon)
Karl Palmskog (Aug 09 2023 at 16:25):great, I'm already rolling out CI updates to projects based on this
Karl Palmskog (Aug 09 2023 at 16:48):will the mathcomp-dev images coq-8.16/coq-8.17 be updated also (and joined by coq-8.18)?
Erik Martin-Dorel (Aug 09 2023 at 18:06):Good point (and thanks for the question!), normally they are updated at each mathcomp.dev commit but it appears there's a nasty issue over there; I'll check and fix this ASAP, hopefully tonight
Erik Martin-Dorel (Aug 09 2023 at 18:06):With 8.18 support of course
Erik Martin-Dorel (Aug 09 2023 at 21:54):Hi @Karl Palmskog, FYI :
mathcomp/mathcomp-dev:coq-*Have a nice evening!
Karl Palmskog (Aug 10 2023 at 07:06):thanks. Just for the record, why the coq-8.16 and coq-8.17 need updating is because there were changes upstream to some non-MC packages in the image, so they rebuild everything from scratch in every CI run (until merge of PR 1056)
Erik Martin-Dorel (Aug 11 2023 at 12:34):FYI @Karl Palmskog, the PR was just merged, and the corresponding pipeline URL is:
https://gitlab.inria.fr/math-comp/math-comp/-/pipelines/844235
Let's :fingers_crossed:
Erik Martin-Dorel (Aug 11 2023 at 13:57):@Karl Palmskog almost! CI was not green this time… now, these pending PRs need to be validated:
Erik Martin-Dorel (Sep 06 2023 at 12:53):@Karl Palmskog
Sorry for the delay, there were several steps in-between, including a webhook missing in gitlab.inria.fr/coq/coq
Now, this pipeline should succeed:
https://gitlab.inria.fr/math-comp/math-comp/-/pipelines/852970
And at this time, all mathcomp-dev images will be up-to-date:
https://hub.docker.com/repository/docker/mathcomp/mathcomp-dev/tags?page=1&ordering=last_updated
Erik Martin-Dorel (Sep 06 2023 at 12:53):(The second novelty is that mathcomp's GitLab CI fully works now for master and for PRs.)
Last updated: Sep 09 2024 at 06:02 UTC