Stream: Coq devs & plugin devs

Topic: ✔ fcsl_pcm broken


view this post on Zulip 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?

view this post on Zulip Karl Palmskog (Oct 21 2021 at 20:16):

ping @Alexander Gryzlov

view this post on Zulip Alexander Gryzlov (Oct 21 2021 at 21:03):

hmm, so this is with master version of mathcomp?

view this post on Zulip Alexander Gryzlov (Oct 21 2021 at 21:05):

it builds fine with 8.14.0 + mathcomp 1.12.0

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Alexander Gryzlov (Oct 21 2021 at 22:22):

Ok, I found it, they changed the constraint on one of the type params.

view this post on Zulip Alexander Gryzlov (Oct 22 2021 at 11:20):

builds again with the latest fix (https://github.com/math-comp/math-comp/pull/812)

view this post on Zulip Notification Bot (Oct 22 2021 at 11:35):

Alexander Gryzlov has marked this topic as resolved.


Last updated: Feb 06 2023 at 18:03 UTC