Stream: math-comp devs

Topic: breaking change of take_take


view this post on Zulip Karl Palmskog (Oct 16 2022 at 10:21):

A recent commit introduces a breaking change in the type of the lemma take_take. Isn't the usual approach to deprecate?

Old take_take:

take_take
     : forall (T : Type) (i j : nat),
       i <= j -> forall s : seq T, take i (take j s) = take i s

New take_take:

take_take
     : forall (T : Type) (i j : nat) (s : seq T),
       take i (take j s) = take (minn i j) s

What's the recommended way of being compatible with both 1.15 and dev if you use take_take? This is not a theoretical breakage, it happened in RegLang.

view this post on Zulip Karl Palmskog (Oct 16 2022 at 10:22):

I know that the "old" take_take is available at take_takel, but this is not available in 1.15.

view this post on Zulip Cyril Cohen (Oct 16 2022 at 10:43):

Thanks ! When we want to reuse an otherwise taken name, we usually make a 3 version-long change so that deprecation can alert users before the renaming is complete. Since the CI did not spot any breakage, with @Laurent Théry, we exceptionally opted for a direct change.
We need to switch back to a 3 version long change, I will make a proposal to fix this quickly on mathcomp side.
Also, RegLang needs to be added to our CI, could you or someone else add it to nixpkgs?

view this post on Zulip Karl Palmskog (Oct 16 2022 at 10:48):

unfortunately I don't have any practical Nix experience, and am travelling most of next week. Perhaps @Théo Zimmermann could help out with adding RegLang to Nixpks so we can get it into MathComp CI?

view this post on Zulip Laurent Théry (Oct 16 2022 at 10:55):

@Karl Palmskog sorry about that

view this post on Zulip Karl Palmskog (Oct 16 2022 at 11:01):

since MC breakage happens so rarely, we don't really have a method to deal with it. Probably it's a good idea to add MC-related Coq-community projects that are more actively maintained to MC CI.

view this post on Zulip Théo Zimmermann (Oct 16 2022 at 11:31):

FWIW, coqPackages.reglang is already available in nixpkgs.

view this post on Zulip Théo Zimmermann (Oct 16 2022 at 11:32):

Note at the latest version, but this shouldn't be a problem for MC CI I guess.

view this post on Zulip Karl Palmskog (Oct 16 2022 at 11:33):

@Cyril Cohen so is coqPackages.reglangin Nixpks usable for MC CI? Or is there something additional to do?

view this post on Zulip Cyril Cohen (Oct 16 2022 at 11:36):

I naively assumed that if the failure didn't show up, it meant that reglang was not in the CI, but it is, so I do not understand why there was no failure...

view this post on Zulip Karl Palmskog (Oct 16 2022 at 11:38):

if it helps, here is the failing Docker build: https://github.com/coq-community/reglang/actions/runs/3258133743/jobs/5349967410

view this post on Zulip Cyril Cohen (Oct 16 2022 at 11:39):

I think it's because we are testing the latest released version.

view this post on Zulip Karl Palmskog (Oct 16 2022 at 11:41):

I think you are actually testing the version before the current released version. The failure occurs on RegLang 1.1.3, but not on 1.1.2.

view this post on Zulip Cyril Cohen (Oct 16 2022 at 11:41):

Hence what Théo Zimmermann said:

Not at the latest version, but this shouldn't be a problem for MC CI I guess.

view this post on Zulip Karl Palmskog (Oct 16 2022 at 11:42):

here is the relevant RegLang commit that went into 1.1.3, it actually removed a locally bundled take_take version: https://github.com/coq-community/reglang/commit/ba48ad6b6178e62013a3960068d0da8100ef3e59

view this post on Zulip Karl Palmskog (Oct 16 2022 at 11:42):

ah OK, I took Théo's "not latest version" to mean "not master".

view this post on Zulip Théo Zimmermann (Oct 16 2022 at 13:53):

I thought MC would be testing the master version indeed. So if it is not, we should update that package in nixpkgs. Let me know if you need me to do it.

view this post on Zulip Karl Palmskog (Oct 16 2022 at 13:57):

it would be ideal to have both 1.1.3 and master of RegLang in Nixpks, but for MathComp CI maybe only master is needed. If it helps, RegLang master is currently compatible with MC 1.11 and later, and Coq 8.10 and later

view this post on Zulip Théo Zimmermann (Oct 16 2022 at 13:58):

You don't need to "put" master in nixpkgs, except in cases where the dependencies or build process change. MC could already test the master version of reglang by tweaking their .nix/config.nix.

view this post on Zulip Cyril Cohen (Oct 16 2022 at 18:30):

That's already what I did in the PR math-comp/math-comp#936

view this post on Zulip Karl Palmskog (Oct 16 2022 at 18:40):

thanks for making it a deprecation, this saved us some work in RegLang (since we need to be Platform compatible)


Last updated: Jan 29 2023 at 15:02 UTC