last master success https://gitlab.com/coq/coq/-/jobs/1702315162
first master failure https://gitlab.com/coq/coq/-/jobs/1702560186
since the difference is "remove -debug" and fcsl itself was last updated in july I guess mathcomp broke it somehow?
ping @Alexander Gryzlov
hmm, so this is with master version of mathcomp?
it builds fine with 8.14.0 + mathcomp 1.12.0
I'm pretty sure this is linked to https://github.com/math-comp/math-comp/pull/757 because that one touched eq_in_map
to my knowledge all projects in Coq's CI that rely on mathcomp are tested with mathcomp master
, so likely a MathComp merge is involved
Ok, I found it, they changed the constraint on one of the type params.
builds again with the latest fix (https://github.com/math-comp/math-comp/pull/812)
Alexander Gryzlov has marked this topic as resolved.
Last updated: Dec 07 2023 at 07:39 UTC