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.
I know that the "old" take_take
is available at take_takel
, but this is not available in 1.15.
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?
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?
@Karl Palmskog sorry about that
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.
FWIW, coqPackages.reglang
is already available in nixpkgs.
Note at the latest version, but this shouldn't be a problem for MC CI I guess.
@Cyril Cohen so is coqPackages.reglang
in Nixpks usable for MC CI? Or is there something additional to do?
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...
if it helps, here is the failing Docker build: https://github.com/coq-community/reglang/actions/runs/3258133743/jobs/5349967410
I think it's because we are testing the latest released version.
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.
Hence what Théo Zimmermann said:
Not at the latest version, but this shouldn't be a problem for MC CI I guess.
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
ah OK, I took Théo's "not latest version" to mean "not master".
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.
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
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
.
That's already what I did in the PR math-comp/math-comp#936
thanks for making it a deprecation, this saved us some work in RegLang (since we need to be Platform compatible)
Last updated: Oct 13 2024 at 01:02 UTC