Stream: math-comp devs

Topic: MathComp 1.11.0 OPAM packages Coq compatibility


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

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

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

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

view this post on Zulip Reynald Affeldt (Jun 09 2020 at 15:24):

the dev option and the license cast should be fixed now

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

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

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

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

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

view this post on Zulip Cyril Cohen (Jun 10 2020 at 12:20):

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

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

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

view this post on Zulip Cyril Cohen (Jun 10 2020 at 12:22):

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

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

view this post on Zulip Cyril Cohen (Jun 10 2020 at 12:24):

true...

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

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

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

view this post on Zulip Erik Martin-Dorel (Jun 10 2020 at 12:51):

Yes, that's exactly what I was proposing

view this post on Zulip Erik Martin-Dorel (Jun 10 2020 at 12:52):

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

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

view this post on Zulip 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: Aug 11 2022 at 01:03 UTC