Gaëtan Gilbert (Jan 13 2022 at 15:02): 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
Pierre-Marie Pédrot (Jan 14 2022 at 11:18):what do we do with bedrock2 then?
Pierre-Marie Pédrot (Jan 14 2022 at 11:18):@Gaëtan Gilbert did you start writing an overlay?
Pierre-Marie Pédrot (Jan 14 2022 at 11:21):cc @Samuel Gruetter since he's the author of the potentially incriminated commit
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?
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
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
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?
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: Oct 13 2024 at 01:02 UTC