Stream: math-comp users

Topic: finmap-1.4.0 incompatibility with Coq 8.11.1


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

view this post on Zulip Anton Trunov (Apr 06 2020 at 15:47):

@Christian Doczkal Are you on Coq 8.11.1?

view this post on Zulip Anton Trunov (Apr 06 2020 at 15:47):

finmap-1.4.0 is not compatible with the recently released Coq 8.11.1

view this post on Zulip Christian Doczkal (Apr 06 2020 at 15:48):

Yes, you are right, I am still on 8.11.0

view this post on Zulip Cyril Cohen (Apr 06 2020 at 15:48):

:cry:

view this post on Zulip Cyril Cohen (Apr 06 2020 at 15:48):

@Anton Trunov do you know what is the source of the incompatibility?

view this post on Zulip Anton Trunov (Apr 06 2020 at 15:49):

@Cyril Cohen it’s this https://github.com/math-comp/finmap/issues/62

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

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

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

view this post on Zulip Christian Doczkal (Apr 06 2020 at 15:51):

I concur, finmap.dev does build agains coq.dev and mathcomp.dev.

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

view this post on Zulip Anton Trunov (Apr 06 2020 at 15:52):

that’s right

view this post on Zulip Cyril Cohen (Apr 06 2020 at 15:53):

I relaunched the CI on relevant docker images just to be sure

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

view this post on Zulip Cyril Cohen (Apr 06 2020 at 15:56):

will do then...

view this post on Zulip Anton Trunov (Apr 06 2020 at 15:56):

Great! If you push a tag, I can take care of the opam repository

view this post on Zulip Cyril Cohen (Apr 06 2020 at 15:56):

great

view this post on Zulip Cyril Cohen (Apr 06 2020 at 16:06):

here you go https://github.com/math-comp/finmap/releases/tag/1.4.1

view this post on Zulip Anton Trunov (Apr 06 2020 at 16:10):

Thanks! Here is the PR: https://github.com/coq/opam-coq-archive/pull/1232

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

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

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

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

view this post on Zulip Anton Trunov (Apr 06 2020 at 19:57):

@Emilio Jesús Gallego Arias me too

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

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

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

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

view this post on Zulip Emilio Jesús Gallego Arias (Apr 06 2020 at 20:00):

the policy is that we welcome anything upstream wants to include

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

view this post on Zulip Emilio Jesús Gallego Arias (Apr 06 2020 at 20:01):

we are just waiting for the process to greatly improve

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

view this post on Zulip Emilio Jesús Gallego Arias (Apr 06 2020 at 20:10):

Sure it is

view this post on Zulip Emilio Jesús Gallego Arias (Apr 06 2020 at 20:10):

we have far more heavy stuff

view this post on Zulip Anton Trunov (Apr 06 2020 at 20:11):

Awesome! Let us wait for Cyril’s decision on finmap first.

view this post on Zulip Anton Trunov (Apr 06 2020 at 20:16):

I added issue https://github.com/math-comp/finmap/issues/65 to track this.

view this post on Zulip Emilio Jesús Gallego Arias (Apr 06 2020 at 20:19):

Great, thanks @Anton Trunov

view this post on Zulip Anton Trunov (Apr 06 2020 at 20:21):

My pleasure :)

view this post on Zulip Emilio Jesús Gallego Arias (Apr 06 2020 at 20:38):

@Anton Trunov you know why coq-ceramist is called ceramist ?

view this post on Zulip Emilio Jesús Gallego Arias (Apr 06 2020 at 20:38):

That's an interesting name

view this post on Zulip Anton Trunov (Apr 06 2020 at 20:41):

@Emilio Jesús Gallego Arias It stands for "CERtified Approximate MembershIp STructures".

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

view this post on Zulip Anton Trunov (Apr 06 2020 at 20:58):

Oh, that I don’t know. But I’ll try to ask Ilya :)

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