Christian Doczkal (Apr 06 2020 at 15:42): Christian Doczkal (Apr 06 2020 at 15:42):Hi, my graph theory development is CI testing against mathcomp+finmap and I'm getting strange build errors (not failures) because coq-mathcomp-finmap-1.4.0 fails to build in the CI environment while it builds fine locally. Does someone have an idea what may be going on? I hope this is the the right place to ask. See the build info.
Anton Trunov (Apr 06 2020 at 15:47):@Christian Doczkal Are you on Coq 8.11.1?
Anton Trunov (Apr 06 2020 at 15:47):finmap-1.4.0 is not compatible with the recently released Coq 8.11.1
Christian Doczkal (Apr 06 2020 at 15:48):Yes, you are right, I am still on 8.11.0
Cyril Cohen (Apr 06 2020 at 15:48)::cry:
Cyril Cohen (Apr 06 2020 at 15:48):@Anton Trunov do you know what is the source of the incompatibility?
Anton Trunov (Apr 06 2020 at 15:49):@Cyril Cohen it’s this https://github.com/math-comp/finmap/issues/62
Anton Trunov (Apr 06 2020 at 15:49):it looks like that change from coq.dev finally made its way into coq 8.11.1
Anton Trunov (Apr 06 2020 at 15:50):I opened https://github.com/coq/opam-coq-archive/pull/1231 to constraint finmap to 8.11.0 at most
Anton Trunov (Apr 06 2020 at 15:50):I guess it could be a time to make a new release. I tried locally and finmap’s master branch is compatible with coq 8.11.1
Christian Doczkal (Apr 06 2020 at 15:51):I concur, finmap.dev does build agains coq.dev and mathcomp.dev.
Cyril Cohen (Apr 06 2020 at 15:52):So if I release finmap-1.4.1 using the current master branch, everything will be alright?
Anton Trunov (Apr 06 2020 at 15:52):that’s right
Cyril Cohen (Apr 06 2020 at 15:53):I relaunched the CI on relevant docker images just to be sure
Anton Trunov (Apr 06 2020 at 15:55):Here is a test on my machine (macOS)
$ opam install coq-mathcomp-finmap.dev
The following actions will be performed:
∗ install coq-mathcomp-finmap dev
<><> Gathering sources ><><><><><><><><><><><><><><><><><><><><><><><><><><> 🐫
[coq-mathcomp-finmap.dev] synchronised from git+https://github.com/math-comp/finmap.git#master
<><> Processing actions <><><><><><><><><><><><><><><><><><><><><><><><><><> 🐫
∗ installed coq-mathcomp-finmap.dev
Done.
$ coqc -v
The Coq Proof Assistant, version 8.11.1 (April 2020)
compiled on Apr 6 2020 14:51:38 with OCaml 4.09.0
will do then...
Anton Trunov (Apr 06 2020 at 15:56):Great! If you push a tag, I can take care of the opam repository
Cyril Cohen (Apr 06 2020 at 15:56):great
Cyril Cohen (Apr 06 2020 at 16:06):here you go https://github.com/math-comp/finmap/releases/tag/1.4.1
Anton Trunov (Apr 06 2020 at 16:10):Thanks! Here is the PR: https://github.com/coq/opam-coq-archive/pull/1232
Christian Doczkal (Apr 06 2020 at 16:17):Thanks @Anton Trunov and @Cyril Cohen for the quick reaction. This way I can hopefully have my CI green in the very near future :+1:
Anton Trunov (Apr 06 2020 at 16:18):Thanks everyone (and no problem)! Once the PR is merged it’s usually a matter of a few ours before the packages are available on opam.
Anton Trunov (Apr 06 2020 at 16:19):@Cyril Cohen Perhaps we should add finmap to Coq’s CI to avoid this breakage in the future. I can help with that too. Although, as you may already know there are certain conditions described here https://github.com/coq/coq/blob/master/dev/ci/README-users.md
Emilio Jesús Gallego Arias (Apr 06 2020 at 19:57):I'm a bit uneasy with 8.11.1 introducing this kind of incompatibility
Anton Trunov (Apr 06 2020 at 19:57):@Emilio Jesús Gallego Arias me too
Emilio Jesús Gallego Arias (Apr 06 2020 at 19:58):so feel free to propose a revert for 8.11.2 if you think that would be the most appropiate
Anton Trunov (Apr 06 2020 at 19:58):I fixed all the dependencies of coq-mathcomp-finmap, but I’m not sure what else might be broken
Emilio Jesús Gallego Arias (Apr 06 2020 at 20:00):we'll see, just mentioning it as to encourage the revert if it is causing too much pain; certainly breaking finmap was not intended
Emilio Jesús Gallego Arias (Apr 06 2020 at 20:00):regarding inclusion of projects in the CI, including finmap Ilya's new stuff etc...
Emilio Jesús Gallego Arias (Apr 06 2020 at 20:00):the policy is that we welcome anything upstream wants to include
Emilio Jesús Gallego Arias (Apr 06 2020 at 20:01):we are gonna get less pro-active in adding stuff to the CI ourselves, so in some sense, if the developers of contribs don't bother submitting to Coq's CI , then we won't add them
Emilio Jesús Gallego Arias (Apr 06 2020 at 20:01):we are just waiting for the process to greatly improve
Anton Trunov (Apr 06 2020 at 20:02):Is it fine to add ceramist to Coq’s CI provided it compiles for about 50 minutes on 2 cores?
Emilio Jesús Gallego Arias (Apr 06 2020 at 20:10):Sure it is
Emilio Jesús Gallego Arias (Apr 06 2020 at 20:10):we have far more heavy stuff
Anton Trunov (Apr 06 2020 at 20:11):Awesome! Let us wait for Cyril’s decision on finmap first.
Anton Trunov (Apr 06 2020 at 20:16):I added issue https://github.com/math-comp/finmap/issues/65 to track this.
Emilio Jesús Gallego Arias (Apr 06 2020 at 20:19):Great, thanks @Anton Trunov
Anton Trunov (Apr 06 2020 at 20:21):My pleasure :)
Emilio Jesús Gallego Arias (Apr 06 2020 at 20:38):@Anton Trunov you know why coq-ceramist is called ceramist ?
Emilio Jesús Gallego Arias (Apr 06 2020 at 20:38):That's an interesting name
Anton Trunov (Apr 06 2020 at 20:41):@Emilio Jesús Gallego Arias It stands for "CERtified Approximate MembershIp STructures".
Emilio Jesús Gallego Arias (Apr 06 2020 at 20:47):Nice :) and the pottery part? Is someone on the dev team a ceramist themselves?
Anton Trunov (Apr 06 2020 at 20:58):Oh, that I don’t know. But I’ll try to ask Ilya :)
Théo Zimmermann (Jun 03 2020 at 12:56):I just learned about this 8.11.1 breakage. I concur with Emilio that breaking a library in a patch-level release was certainly not intended. Was the source of the incompatibility clearly identified? From what I understood of the timeline, it was identified as soon as March 8th that there was an incompatibility with Coq master, so about one month before the 8.11.1 release and it would have been possible to prevent this issue to happen, if only Coq devs had known about this (apparently accidental) breakage.
Last updated: Feb 08 2023 at 07:02 UTC