Stream: Coq devs & plugin devs

Topic: bedrock2 ci broken


view this post on Zulip Pierre-Marie Pédrot (Mar 25 2021 at 13:45):

It seems that bedrock2 doesn't compile on the CI, likely due to an interaction with Ltac2.

view this post on Zulip Pierre-Marie Pédrot (Mar 25 2021 at 13:46):

Any idea what's going on?

view this post on Zulip Pierre-Marie Pédrot (Mar 25 2021 at 13:46):

see e.g. https://github.com/coq/coq/pull/14002/checks?check_run_id=2193554701

view this post on Zulip Enrico Tassi (Mar 25 2021 at 13:46):

The error message is fishy, since AFAICT the Assert_failure exception is declared only once in that file.

view this post on Zulip Pierre-Marie Pédrot (Mar 25 2021 at 13:49):

Looks like a bug in the redeclaration check.

view this post on Zulip Pierre-Marie Pédrot (Mar 25 2021 at 13:54):

Reported here: https://github.com/coq/coq/issues/14003

view this post on Zulip Pierre-Marie Pédrot (Mar 25 2021 at 13:54):

I don't know why it wasn't caught by the CI.

view this post on Zulip Pierre-Marie Pédrot (Mar 25 2021 at 14:40):

Fix here: https://github.com/coq/coq/pull/14004


Last updated: Oct 21 2021 at 19:03 UTC