Stream: Coq devs & plugin devs

Topic: >= 4.09 and opam


view this post on Zulip 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)

view this post on Zulip 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)

view this post on Zulip Karl Palmskog (Apr 28 2022 at 19:13):

and are we supposed to be using coq-core in extra-dev?

view this post on Zulip 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.

view this post on Zulip Karl Palmskog (Apr 28 2022 at 19:16):

how the opam repo synchronizes with the dev versions

I would call it a stochastical-biological process: when someone gets sufficiently annoyed at failing builds

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Apr 28 2022 at 19:27):

which I didnt' get to fix yet

view this post on Zulip Emilio Jesús Gallego Arias (Apr 28 2022 at 19:27):

if you don't use native, it is possible to split today

view this post on Zulip Emilio Jesús Gallego Arias (Apr 28 2022 at 19:27):

does that answer the questions?

view this post on Zulip 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

view this post on Zulip 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 (?)

view this post on Zulip Karl Palmskog (Apr 28 2022 at 20:05):

since we want to keep compatibility with native

view this post on Zulip 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.

view this post on Zulip 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).

view this post on Zulip Enrico Tassi (Apr 29 2022 at 09:15):

master

view this post on Zulip 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!

view this post on Zulip 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.

view this post on Zulip Karl Palmskog (May 03 2022 at 09:12):

OK, I'll update it now

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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]?

view this post on Zulip Karl Palmskog (May 03 2022 at 12:27):

both coq.dev and coqide.dev should be as up to date as possible now

view this post on Zulip 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?

view this post on Zulip Théo Zimmermann (May 04 2022 at 12:06):

https://github.com/coq/coq/pull/15947

view this post on Zulip 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:

view this post on Zulip 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:

view this post on Zulip 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?

view this post on Zulip 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).

view this post on Zulip 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:

(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?)

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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 :/

view this post on Zulip Théo Zimmermann (May 08 2022 at 09:57):

With Coq master?

view this post on Zulip Ralf Jung (May 09 2022 at 20:52):

with Coq 8.15

view this post on Zulip Ralf Jung (May 09 2022 at 20:53):

Coq master doesnt build on 4.07 so that cannot even be tested^^


Last updated: Feb 06 2023 at 00:03 UTC