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.

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

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.

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

@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)

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...

@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)

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

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 ?

Ah, but it is not merged

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

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

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

I really don't know how the nix CI works

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...

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.

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

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

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

OK, so I will merge it and restart MCA job

Thanks for attending so quickly to the matter!

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)

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

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