Karl Palmskog (Apr 28 2022 at 18:30): Karl Palmskog (Apr 28 2022 at 18:30):is OCaml 4.05.0 finally getting dropped? :tada:
Pierre-Marie Pédrot (Apr 28 2022 at 18:49):Yes, we're now requiring OCaml >= 4.09
Paolo Giarrusso (Apr 28 2022 at 18:59)::broken_heart: no 4.07.1 :-(
Paolo Giarrusso (Apr 28 2022 at 18:59):Look forward to testing 4.09 with the GC patch
Paolo Giarrusso (Apr 28 2022 at 19:03):(I won’t patch all the compilers out there, but I guess I’ll end up patching at least the flambda variant at some point)
Karl Palmskog (Apr 28 2022 at 19:12):wait, is the PR with >= 4.09 already merged? We should update the core-devpackage (coq.dev)
Karl Palmskog (Apr 28 2022 at 19:13):and are we supposed to be using coq-core in extra-dev?
Pierre-Marie Pédrot (Apr 28 2022 at 19:15):I don't know how the opam repo synchronizes with the dev versions, but yes the PR was merged and the opam files from the coq repo itself are up-to-date.
Karl Palmskog (Apr 28 2022 at 19:16):how the opam repo synchronizes with the dev versions
I would call it a stochastic-biological process: when someone gets sufficiently annoyed at failing builds
Karl Palmskog (Apr 28 2022 at 19:17):@Emilio Jesús Gallego Arias should we be using the coq-core and coq opam package division everywhere now in opam, not just in the Coq repo? Or a single coq standalone package outside the repo?
Emilio Jesús Gallego Arias (Apr 28 2022 at 19:26):I think after https://github.com/coq/coq/pull/15560 we can use a split everywhere, should be coq-core,coq-stdlib tho
Emilio Jesús Gallego Arias (Apr 28 2022 at 19:27):The split was blocked because there is a bug in dune for installing coq-native stuff
Emilio Jesús Gallego Arias (Apr 28 2022 at 19:27):which I didnt' get to fix yet
Emilio Jesús Gallego Arias (Apr 28 2022 at 19:27):if you don't use native, it is possible to split today
Emilio Jesús Gallego Arias (Apr 28 2022 at 19:27):does that answer the questions?
Emilio Jesús Gallego Arias (Apr 28 2022 at 19:27):After that PR, I also expect the opam files in the main Coq repos to be the canonical ones, and automatically generated
Karl Palmskog (Apr 28 2022 at 20:03):OK, so it sounds like the bottom line is: keep a single standalone coq.dev package in core-dev opam repo until PR 15560 is merged (?)
Karl Palmskog (Apr 28 2022 at 20:05):since we want to keep compatibility with native
Théo Zimmermann (Apr 29 2022 at 08:54):Paolo Giarrusso said:
(I won’t patch all the compilers out there, but I guess I’ll end up patching at least the flambda variant at some point)
The patch is already in Coq for the direct calls we make to the GC. So I don't think you need to patch anything on your sides.
Paolo Giarrusso (Apr 29 2022 at 09:13):Cool! But which Coq versions? In 8.15.1 I can tell 4.10.2 is slower than 4.13.1/4.14 (on M1).
Enrico Tassi (Apr 29 2022 at 09:15):master
Paolo Giarrusso (Apr 29 2022 at 10:51):Found it: https://github.com/coq/coq/pull/15946. It cherry-picks on 8.15.1, so maybe I'll test that!
Théo Zimmermann (May 03 2022 at 09:11):Karl Palmskog said:
wait, is the PR with >= 4.09 already merged? We should update the
core-devpackage (coq.dev)
Just FWIW, AFAICT this package has not been updated yet, which means that the build of Docker-Coq images has been failing ever since the PR bumping the minimal OCaml version has been merged, which in turns mean that some of the projects which are testing against Coq master have been actually testing against a stalled version lately.
Karl Palmskog (May 03 2022 at 09:12):OK, I'll update it now
Karl Palmskog (May 03 2022 at 09:20):sigh, we now have like 5-6 different Coq opam package definitions, all maintained by different people and with different options
Karl Palmskog (May 03 2022 at 09:21):for example, the OCaml people changed "ocaml-option-nnp" to just "base-nnp", in the Coq 8.15.1 opam package, but you only know if you look
Théo Zimmermann (May 03 2022 at 09:25):Actually, I forgot that the Docker-Coq images actually use the opam definition in https://github.com/coq/coq/blob/master/coq.opam.docker. But the pipeline needs to be adjusted because it still expect to build Coq with a set of fixed OCaml versions. cc @Erik Martin-Dorel
Karl Palmskog (May 03 2022 at 09:28):ah, but if the Docker images use coq.opam.docker, then there are changes from coq.8.15.1 missing. So I hope nobody else uses that package
Karl Palmskog (May 03 2022 at 09:29):if Docker uses coq.dev in core-dev repo, then we at least know when that package is broken... but presumably there are other reasons [for using the master branch coq.opam.docker]?
Karl Palmskog (May 03 2022 at 12:27):both coq.dev and coqide.dev should be as up to date as possible now
Erik Martin-Dorel (May 04 2022 at 12:04):Thanks @Théo Zimmermann for mentioning me :+1:
just FTR could someone recall the PR number where the compilation with 4.07.1 stopped to be supported in coq.master?
Théo Zimmermann (May 04 2022 at 12:06):https://github.com/coq/coq/pull/15947
Erik Martin-Dorel (May 04 2022 at 12:11):regarding the Docker-Coq coqorg/coq:dev build failures, it's a pity we weren't able to discuss together beforehand so that the migration is smoother.
Anyway, as shown in the last pipeline https://gitlab.com/coq-community/docker-coq/-/pipelines/530845030:
coqorg/coq:dev:ocaml-4.12-flambda and coqorg/coq:dev:ocaml-4.13-flambda images are still continuously updated Théo Zimmermann (May 04 2022 at 12:13):Q. 1. if you don't object, I'll remove the corresponding tags from Docker Hub (which is probably better than keeping stalled "dev" images (@Théo Zimmermann, your opinion?))
:+1:
Théo Zimmermann (May 04 2022 at 12:14):Q. 2. from now on, what should be from your opinion, "the standard version of ocaml" that should be selected as a future-proof default version of ocaml, compatible with coq-native? (then this version will replace the one for the single Docker-Coq image with coq-native: https://github.com/coq-community/docker-coq/blob/ac47077378e7a019e321745b5f86986d441077e5/images.yml#L82-L86 )
The Coq Platform has switched to 4.13.1+flambda, so maybe this can be considered a good standard version?
Paolo Giarrusso (May 04 2022 at 13:19):4.14 fixes the OCaml debugger (which helps Coq devs) and has GC improvements (impact on Coq unclear), so it might be worth adding that image? For the first time in a while, I'm not aware of any issues with this version (except the alectryon/serapi + elpi issues, and Coq 8.16 will fix those).
Erik Martin-Dorel (May 04 2022 at 14:00):Hi @Paolo Giarrusso, thanks for your remark!
According to the "docker-coq ocaml versions policy" we had discussed and documented a long time ago, we can provide 4 different ocaml minor versions (with the last patchlevel, and with flambda) for each coq version in Docker-Coq, roughly speaking:
4.09.14.13.1, 4.14.0(> 4.09.1) that could now (for coq ≥ 8.16) be used as "the default ocaml version" in docker-coq images (in lieu of 4.07.1 that was also preferred for benchmarks up to now… cf. the dedicated docker-coq image with coq-native) → what about using ocaml 4.14.0?(Cc @Paolo Giarrusso @Guillaume Melquiond @Karl Palmskog @Enrico Tassi @Emilio Jesús Gallego Arias @Maxime Dénès @Pierre-Marie Pédrot @Pierre Roux @Théo Zimmermann, no objection for this last choice?)
Théo Zimmermann (May 04 2022 at 14:06):There might be a few packages that are not yet compatible with 4.14. We know that at least all the Platform packages are compatible with 4.13. That's why this was my suggestion for the default version.
Emilio Jesús Gallego Arias (May 04 2022 at 15:50):By the way all the mess with opam packages and docker etc... should be gone once we merge #15560
Ralf Jung (May 08 2022 at 09:38):Paolo Giarrusso said:
:broken_heart: no 4.07.1 :-(
yeah on our CI there is a 7% slowdown from 4.07.1 to 4.14.0 :/
Théo Zimmermann (May 08 2022 at 09:57):With Coq master?
Ralf Jung (May 09 2022 at 20:52):with Coq 8.15
Ralf Jung (May 09 2022 at 20:53):Coq master doesnt build on 4.07 so that cannot even be tested^^
Last updated: Oct 12 2024 at 12:01 UTC