Stream: Coq devs & plugin devs

Topic: Coq regression observed with MathComp-Analysis


view this post on Zulip Reynald Affeldt (Jul 06 2023 at 08:14):

We have potentially observed a Coq regression with MathComp-Analysis, see this PR: https://github.com/math-comp/analysis/pull/967 .
MathComp-Analysis master still depends on MathComp 1, we have no problem compiling it.
We also keep a branch compatible with MathComp 2 to which we cherry-pick every new commit,
the PR above is a bunch of such recent commits.
The failing CI seems to be the one testing against coq-dev.
It looks like a universe problem.
I tried to reproduce on my computer but couldn't actually compile MathComp 2 or MathComp-dev with coq-dev,
apparently because of universe problems too.
You can see excerpts of error messages in the conversion of the PR above.

view this post on Zulip Karl Palmskog (Jul 06 2023 at 08:21):

I guess this is why we'd like https://github.com/coq/coq/pull/17722 to be merged...

view this post on Zulip Enrico Tassi (Jul 06 2023 at 08:32):

We have patches for coq-elpi and HB making the job fit a reasonable amount of memory.
I'm working on a coq-elpi release, then the HB one could follow.

view this post on Zulip Enrico Tassi (Jul 06 2023 at 08:33):

Not that after https://github.com/math-comp/hierarchy-builder/pull/373 we can already release HB.

view this post on Zulip Karl Palmskog (Jul 06 2023 at 08:48):

@Reynald Affeldt I can confirm a universe issue with coq.dev/coq-mathomp-algebra.dev, maybe you can report as Coq issue, since a lot of people are going to discover this (mathcomp-dev image is going to break)

view this post on Zulip Karl Palmskog (Jul 06 2023 at 08:48):

unfortunately, Érik just said in an issue he is super busy with grading, so I don't know when he can take care of the Docker breakage...

view this post on Zulip Enrico Tassi (Jul 06 2023 at 08:53):

@Reynald Affeldt @Cyril Cohen can you help me figure out which coq master commit this log is compiling?
https://github.com/math-comp/analysis/actions/runs/5405534213/jobs/9928494286?pr=967
(I can't find it, and it is somewhat needeed to see which PR about universes got merged)

view this post on Zulip Karl Palmskog (Jul 06 2023 at 08:54):

the error, if this rings a bell from some recent PR for someone:

File "./poly.v", line 632, characters 0-101:
Error: Illegal application:
The term "@reverse_coercion" of type
 "forall T' T : Type,
  T' -> ReverseCoercionSource T -> ReverseCoercionTarget T'"
cannot be applied to the terms
 "zmodType" : "Type"
 "Type" : "Type"
 "poly_poly_of__canonical__GRing_Zmodule" : "zmodType"
 "{poly R}" : "Type"
The 2nd term has type "Type@{mathcomp.algebra.poly.15105+1}"
which should be a subtype of "Type@{mathcomp.algebra.poly.15103}".

view this post on Zulip Enrico Tassi (Jul 06 2023 at 08:55):

This was fixed in HB by @Pierre Roux I think here https://github.com/math-comp/hierarchy-builder/pull/372

view this post on Zulip Reynald Affeldt (Jul 06 2023 at 08:55):

Enrico Tassi said:

Reynald Affeldt Cyril Cohen can you help me figure out which coq master commit this log is compiling?
https://github.com/math-comp/analysis/actions/runs/5405534213/jobs/9928494286?pr=967
(I can't find it, and it is somewhat needeed to see which PR about universes got merged)

Can we infer it from this nix information /nix/store/9xviidwjv917dwq2a1sqsz8p8305fvbn-coq-dev.drv ?

view this post on Zulip Enrico Tassi (Jul 06 2023 at 08:56):

Ah, but it is not merged

view this post on Zulip Enrico Tassi (Jul 06 2023 at 08:56):

Can you infer it from this nix information /nix/store/9xviidwjv917dwq2a1sqsz8p8305fvbn-coq-dev.drv ?

nope, nix hashes are another beast I'm afraid :-/

view this post on Zulip Enrico Tassi (Jul 06 2023 at 08:58):

If I merge the PR above and you re-run the job, would that pick up the new master?

view this post on Zulip Enrico Tassi (Jul 06 2023 at 08:59):

I really don't know how the nix CI works

view this post on Zulip Karl Palmskog (Jul 06 2023 at 08:59):

if you merge https://github.com/math-comp/hierarchy-builder/pull/372 it would at least be easy to test in opam if it works...

view this post on Zulip Reynald Affeldt (Jul 06 2023 at 09:00):

Enrico Tassi said:

I really don't know how the nix CI works

I've been through the log but I didn't see commit information about Coq.

view this post on Zulip Karl Palmskog (Jul 06 2023 at 09:30):

if https://github.com/coq/coq/pull/17484 is the "culprit", then the MathComp Docker may have been broken for a while?

view this post on Zulip Pierre Roux (Jul 06 2023 at 09:36):

According to https://github.com/math-comp/analysis/blob/47cddf16b3244f5205b70becaf5beda1391e2942/.nix/config.nix#L51 the CI of Analysis is using the coq-master branch of HB. Same for math-comp proper: https://github.com/math-comp/math-comp/blob/master/.nix/config.nix#L78

view this post on Zulip Pierre Roux (Jul 06 2023 at 09:42):

Enrico Tassi said:

If I merge the PR above and you re-run the job, would that pick up the new master?

Yes it should

view this post on Zulip Enrico Tassi (Jul 06 2023 at 09:43):

OK, so I will merge it and restart MCA job

view this post on Zulip Reynald Affeldt (Jul 06 2023 at 10:21):

Thanks for attending so quickly to the matter!

view this post on Zulip Karl Palmskog (Jul 06 2023 at 10:29):

opam coq-mathcomp-algebra.dev works again, thanks! now we can continue using mathcomp-dev in CI (assuming mathcomp-docker is not broken, else projects can switch to regular Coq-Docker until fixed)

view this post on Zulip Enrico Tassi (Jul 06 2023 at 11:04):

MCA is still broken, but I'm not really sure what I'm doing with the nix CI...

view this post on Zulip Cyril Cohen (Jul 06 2023 at 12:20):

Enrico Tassi said:

I really don't know how the nix CI works

It pulls the master from the date of the CI run


Last updated: May 18 2024 at 10:02 UTC