Stream: Coq devs & plugin devs

Topic: bedrock failing


view this post on Zulip Gaëtan Gilbert (Jan 13 2022 at 15:02):

https://gitlab.com/coq/coq/-/jobs/1968718087 last master success
https://gitlab.com/coq/coq/-/jobs/1970969936 first master failure
reverting #14137 still failed so probably an upstream change? https://github.com/mit-plv/bedrock2/commit/7da0aa05e3cde246bdef974660f0aa3415b3aef7 only candidate

view this post on Zulip Pierre-Marie Pédrot (Jan 14 2022 at 11:18):

what do we do with bedrock2 then?

view this post on Zulip Pierre-Marie Pédrot (Jan 14 2022 at 11:18):

@Gaëtan Gilbert did you start writing an overlay?

view this post on Zulip Pierre-Marie Pédrot (Jan 14 2022 at 11:21):

cc @Samuel Gruetter since he's the author of the potentially incriminated commit

view this post on Zulip Matthieu Sozeau (Jan 14 2022 at 11:52):

Tangentially related question: do we have support for overlays pointing to only a commit, not a branch name?

view this post on Zulip Gaëtan Gilbert (Jan 14 2022 at 12:02):

Matthieu Sozeau said:

Tangentially related question: do we have support for overlays pointing to only a commit, not a branch name?

no

view this post on Zulip Gaëtan Gilbert (Jan 14 2022 at 12:05):

Pierre-Marie Pédrot said:

Gaëtan Gilbert did you start writing an overlay?

having a look now

view this post on Zulip Samuel Gruetter (Jan 14 2022 at 12:50):

The error at https://gitlab.com/coq/coq/-/jobs/1970969936 looks like a bug in lia to me, has anyone already analyzed that?

view this post on Zulip Gaëtan Gilbert (Jan 14 2022 at 14:05):

looks like a zarith bug: I can reproduce on zarith 1.10 (what we have in CI) but not on 1.12
(unless I messed up while reproducing)
let's see what https://github.com/coq/coq/pull/15483 says


Last updated: Feb 02 2023 at 13:03 UTC