Gaëtan Gilbert (Oct 21 2021 at 20:14): Gaëtan Gilbert (Oct 21 2021 at 20:14):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?
Karl Palmskog (Oct 21 2021 at 20:16):ping @Alexander Gryzlov
Alexander Gryzlov (Oct 21 2021 at 21:03):hmm, so this is with master version of mathcomp?
Alexander Gryzlov (Oct 21 2021 at 21:05):it builds fine with 8.14.0 + mathcomp 1.12.0
Alexander Gryzlov (Oct 21 2021 at 21:10):I'm pretty sure this is linked to https://github.com/math-comp/math-comp/pull/757 because that one touched eq_in_map
Karl Palmskog (Oct 21 2021 at 21:24):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
Alexander Gryzlov (Oct 21 2021 at 22:22):Ok, I found it, they changed the constraint on one of the type params.
Alexander Gryzlov (Oct 22 2021 at 11:20):builds again with the latest fix (https://github.com/math-comp/math-comp/pull/812)
Notification Bot (Oct 22 2021 at 11:35):Alexander Gryzlov has marked this topic as resolved.
Last updated: Apr 20 2024 at 00:02 UTC