Karl Palmskog (Jan 14 2021 at 08:29): Karl Palmskog (Jan 14 2021 at 08:29):@Christian Doczkal unfortunately reglang 1.1.1 doesn't work on 8.13. Should we release a 1.1.2?
Christian Doczkal (Jan 14 2021 at 08:47):I haven't had the time to investigate yet. Do you know what the issue is?
Christian Doczkal (Jan 14 2021 at 08:51):Hmm, 1.1 was a maintenance release and so was 1.1.1. Not sure what I did there, but I would favor 1.1.2 over 1.1.1.1 ...
Karl Palmskog (Jan 14 2021 at 09:05):latest master works fine on 8.13
Karl Palmskog (Jan 14 2021 at 09:06):here is where 1.1.1 fails on 8.13 with MC 1.12.0:
File "./theories/misc.v", line 142, characters 7-49:
Error: Illegal application (Non-functional construction):
The expression "inj_card_bij val_inj ?i" of type "bijective val"
cannot be applied to the term
"?y" : "?T"
But I think this was fixed like 2 months ago.
Christian Doczkal (Jan 14 2021 at 09:10):Yes, you managed to confuse me by mentioning coq-8.13, this is a change in a lemma-type introduced in mathcomp-1.12, for which we never made a release. I'm currently rerunning the CI on master and, if there are no surprises, I will tag v1.1.2. I'd be happy if you could take care of the opam-archive side.
Christian Doczkal (Jan 14 2021 at 09:19):I tagged the release.
Karl Palmskog (Jan 14 2021 at 09:24):but 1.11.0 doesn't work on 8.13 (to my knowledge, and according to what is in opam)
Christian Doczkal (Jan 14 2021 at 09:30):What's the problem with that for the coq-reglang package? We don't need to rule out incompatible dependencies if opam knows about these incompatibilities already, do we?
Karl Palmskog (Jan 14 2021 at 09:34):you mean you want to skip the Coq bound since it is implied by the ssreflect bound?
Karl Palmskog (Jan 14 2021 at 09:35):I just mean that saying "doesn't work on 8.13" in this case is equivalent to "doesn't work on 1.12.0", so I arbitrarily said the first
Christian Doczkal (Jan 14 2021 at 09:39):Are you talking about updating the constraints for v1.1.1?
Karl Palmskog (Jan 14 2021 at 09:42):I mean, there is no point in doing that, for either the Coq bound (no-op) or the ssreflect bound (will break the package)
Christian Doczkal (Jan 14 2021 at 09:44):Yes, and for 1.1.2 the bounds are <coq-8.14 and <mathcomp-1.13, with 8.13+1.11 being ruled out by existing constraints. Am I missing something?
Karl Palmskog (Jan 14 2021 at 09:45):you said:
you managed to confuse me by mentioning coq-8.13
I said in response:
"doesn't work on 8.13" in this case is equivalent to "doesn't work on 1.12.0", so I arbitrarily said the first
Karl Palmskog (Jan 14 2021 at 09:47):we could call it [1.1.2] the "MC 1.12.0 release of reglang", rather than a release for 8.13, but it amounts to almost the same thing.
Christian Doczkal (Jan 14 2021 at 09:48):Okay, I see. Much ado about nothing then.
Christian Doczkal (Jan 14 2021 at 09:50):I only say compatibility release and what the tested versions are. And yes, 8.13+1.11 is (obviously) not in the list.
Christian Doczkal (Jan 14 2021 at 09:52):In any event, thanks for your efforts!
Last updated: Jun 03 2023 at 18:01 UTC