Stream: coq-community devs & users

Topic: reglang release for 8.13


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

view this post on Zulip Christian Doczkal (Jan 14 2021 at 08:47):

I haven't had the time to investigate yet. Do you know what the issue is?

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

view this post on Zulip Karl Palmskog (Jan 14 2021 at 09:05):

latest master works fine on 8.13

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

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

view this post on Zulip Christian Doczkal (Jan 14 2021 at 09:19):

I tagged the release.

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

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

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

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

view this post on Zulip Christian Doczkal (Jan 14 2021 at 09:39):

Are you talking about updating the constraints for v1.1.1?

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

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

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

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

view this post on Zulip Christian Doczkal (Jan 14 2021 at 09:48):

Okay, I see. Much ado about nothing then.

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

view this post on Zulip Christian Doczkal (Jan 14 2021 at 09:52):

In any event, thanks for your efforts!


Last updated: Feb 04 2023 at 01:03 UTC