Zulip Chat Archive

Stream: mathlib4

Topic: Build issue in CI

Sebastian Zimmer (Oct 21 2023 at 14:59):

My PR is failing CI in the "check environments using lean4checker" stage. Is this stage known to be inconsistent, or have I actually broken something?

Ruben Van de Velde (Oct 21 2023 at 14:59):

Link?

Sebastian Zimmer (Oct 21 2023 at 14:59):

https://github.com/leanprover-community/mathlib4/actions/runs/6597416960/job/17925088444

Ruben Van de Velde (Oct 21 2023 at 16:15):

That vaguely rings a bell, though I thought it had been solved already

Rob Lewis (Oct 21 2023 at 19:13):

Your PR was based on a old-ish version of mathlib4; merging master made the error go away

Last updated: Dec 20 2023 at 11:08 UTC