A recent commit introduces a breaking change in the type of the lemma
take_take. Isn't the usual approach to deprecate?
take_take : forall (T : Type) (i j : nat), i <= j -> forall s : seq T, take i (take j s) = take i s
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.
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.
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.reglangin 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
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: May 31 2023 at 09:01 UTC