Stream: math-comp devs

Topic: MathComp 1.11.0 OPAM packages Coq compatibility

Karl Palmskog (Jun 09 2020 at 14:57):

@affeldt-aist @Cyril Cohen so the submitted 1.11.0 OPAM packages in coq-released explicitly support Coq dev versions (= "dev"). Is this something that you plan to support going forward? Based on experience, it hasn't taken that long before MC releases break with Coq master.

Cyril Cohen (Jun 09 2020 at 14:57):

Karl Palmskog said:

affeldt-aist Cyril Cohen so the submitted 1.10 OPAM packages in coq-released explicitly support Coq dev versions (= "dev"). Is this something that you plan to support going forward? Based on experience, it hasn't taken that long before MC releases break with Coq master.

I believe this is a mistake indeed...

Notification Bot (Jun 09 2020 at 14:58):

This topic was moved here from #math-comp users > MathComp 1.11.0 OPAM packages Coq compatibility by Cyril Cohen

Karl Palmskog (Jun 09 2020 at 14:58):

in that case, may I ask that you also change CeCILL-B to CECILL-B to adhere to SPDX?

Reynald Affeldt (Jun 09 2020 at 15:24):

the dev option and the license cast should be fixed now

Karl Palmskog (Jun 09 2020 at 15:26):

thanks, the CI problems only seem to affect the testing of the JSON index construction (i.e., not packages). So I'll merge when the relevant jobs have completed successfully,

Erik Martin-Dorel (Jun 10 2020 at 12:14):

Cyril Cohen said:

Karl Palmskog said:

affeldt-aist Cyril Cohen so the submitted 1.10 OPAM packages in coq-released explicitly support Coq dev versions (= "dev"). Is this something that you plan to support going forward? Based on experience, it hasn't taken that long before MC releases break with Coq master.

I believe this is a mistake indeed...

Hi @Cyril Cohen @Karl Palmskog, regarding this question, maybe having the latest mathcomp stable version maked as compatible with coq:dev when it is released was a good idea a priori? (cf. e.g. this PR https://github.com/coq/opam-coq-archive/pull/779); anyway dropping the (= "dev") constraint as from the release is a working solution as well (and simpler to maintain!)
so it really depends on whether @Cyril Cohen thinks whether it's useful to provide images such as mathcomp/mathcomp:latest-coq-dev (with latest stable mathcomp and coq.dev, when it is possible), or if it's not worth the effort.

Cyril Cohen (Jun 10 2020 at 12:17):

I do not, know, I guess it could be useful to test math-comp related projects wrt mathcomp + coq dev...

Cyril Cohen (Jun 10 2020 at 12:18):

I'm really divded... I am a bit upset that we always have to compromise between user/developer environement stability and CI

Cyril Cohen (Jun 10 2020 at 12:19):

I think the CI should do the workaround, but it looks like it takes a lot of effort. Would there be a solution which does not compromise with restrictions that are user oriented and still allow more fredom for CI?

Cyril Cohen (Jun 10 2020 at 12:20):

how about rebinding opam to opam --ignore-constraints everything in the docker scripts?

Erik Martin-Dorel (Jun 10 2020 at 12:21):

I'm not very fan of the --ignore-constraints option, it has many quirks… and it is not really a solution but a workaround that hinders the dependencies resolution.

Erik Martin-Dorel (Jun 10 2020 at 12:22):

Basically this question is mostly a packaging issue outside the math-comp repo itself, and the effort is not considerable: I have already some cron task that can check every day that latest mathcomp still compiles with coq.dev

Cyril Cohen (Jun 10 2020 at 12:22):

can we have an automatically patched clone of the opam coq repo?

Erik Martin-Dorel (Jun 10 2020 at 12:23):

Cyril Cohen said:

can we have an automatically patched clone of the opam coq repo?

I guess this would be more work, basically the only action required from our side with what I proposed is to wait the day that latest-mathcomp does not compile anymore with coq.dev, then open one PR that mark the file accordingly…

Cyril Cohen (Jun 10 2020 at 12:24):

true...

Erik Martin-Dorel (Jun 10 2020 at 12:25):

and maybe this has the upside to notify the mathcomp team early of one such incompatibility

Erik Martin-Dorel (Jun 10 2020 at 12:27):

so what do we do?
I can open a PR that re-add (= "dev") if need be (if you fully agree with this solution of course)

Karl Palmskog (Jun 10 2020 at 12:50):

it's fine if you explicitly want to support this, but then you also have to modify the released packages and submit PRs as soon as compatibility breaks.

Erik Martin-Dorel (Jun 10 2020 at 12:51):

Yes, that's exactly what I was proposing

Erik Martin-Dorel (Jun 10 2020 at 12:52):

(But I wait for @Cyril Cohen's green light to open that PR)

Cyril Cohen (Jun 10 2020 at 13:21):

Erik Martin-Dorel said:

(But I wait for Cyril Cohen's green light to open that PR)

I'm ok with it.

Erik Martin-Dorel (Jun 10 2020 at 13:33):

@Cyril Cohen done; BTW you may want to directly push another commit in math-comp master, reverting 313e443?

Last updated: May 31 2023 at 02:31 UTC