Stream: Coq devs & plugin devs

Topic: mathcomp failing


view this post on Zulip Gaëtan Gilbert (May 11 2023 at 07:14):

mathcomp is failing in CI, eg https://gitlab.com/coq/coq/-/jobs/4265090732
cc @Enrico Tassi

view this post on Zulip Enrico Tassi (May 11 2023 at 07:39):

Sure, master moved on MC 2.0, I'll move CI to branch mathcomp-1 and propose a path to switch to mathcomp 2

view this post on Zulip Enrico Tassi (May 11 2023 at 07:42):

https://github.com/coq/coq/pull/17595

view this post on Zulip Enrico Tassi (May 11 2023 at 07:56):

I did schedule a slot at the next call, btw

view this post on Zulip Gaëtan Gilbert (May 11 2023 at 10:55):

is it more complicated than just adding elpi/hb as a dependency?

view this post on Zulip Pierre Roux (May 11 2023 at 10:57):

no

view this post on Zulip Enrico Tassi (May 11 2023 at 10:58):

It should not, but:


Last updated: Jun 17 2024 at 22:01 UTC