Stream: Coq devs & plugin devs

Topic: mathcomp failing

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

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

Enrico Tassi (May 11 2023 at 07:42):

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

Enrico Tassi (May 11 2023 at 07:56):

I did schedule a slot at the next call, btw

Gaëtan Gilbert (May 11 2023 at 10:55):

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

Pierre Roux (May 11 2023 at 10:57):

no

Enrico Tassi (May 11 2023 at 10:58):

It should not, but:

• it is slower (for now at least)
• we want mc1 to stay tested

Last updated: Nov 29 2023 at 20:01 UTC