Reynald Affeldt (Jul 06 2023 at 08:14): 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.
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...
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.
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.
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)
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...
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)
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}".
This was fixed in HB by @Pierre Roux I think here https://github.com/math-comp/hierarchy-builder/pull/372
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 ?
Enrico Tassi (Jul 06 2023 at 08:56):Ah, but it is not merged
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 :-/
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?
Enrico Tassi (Jul 06 2023 at 08:59):I really don't know how the nix CI works
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...
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.
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?
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
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
Enrico Tassi (Jul 06 2023 at 09:43):OK, so I will merge it and restart MCA job
Reynald Affeldt (Jul 06 2023 at 10:21):Thanks for attending so quickly to the matter!
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)
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...
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: Nov 29 2023 at 22:01 UTC