Zulip Chat Archive

Stream: general

Topic: Strange build failure

Anatole Dedecker (Dec 10 2021 at 12:57):

I may be misinterpreting something, but there has been a lot of weird failures of the "build mathlib" run since yesterday (at least). The job fails but the log shows the leanpkg build step to be running. I "solved" it in #10682 by re-running all the jobs (twice !), but it also affects e.g. #10705 and #10702. Does anyone know what is happening ?

Andrew Yang (Dec 10 2021 at 13:00):

My PRs are also affected by this, as mentioned here. However I have no idea why this is happening as well.

Anatole Dedecker (Dec 10 2021 at 13:08):

#10701 had the same problem but now reports a (deterministic) timeout in algebraic_geometry/presheafed_space/has_colimits.lean

Anatole Dedecker (Dec 10 2021 at 13:08):

So this seems to be the same problem as https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/mathlib.20broke (sorry for duplicating)

Anatole Dedecker (Dec 10 2021 at 13:18):

Oh and it seems to be affecting master too !? I am currently unable to get working oleans for current master

Ruben Van de Velde (Dec 10 2021 at 13:23):

#10703 should improve presheafed_space a bit - maybe it could have used higher priority

Johan Commelin (Dec 10 2021 at 13:32):

bors just finished a batch

Johan Commelin (Dec 10 2021 at 13:32):

should we bump the prio on that PR?

Anatole Dedecker (Dec 10 2021 at 13:32):

It seems to be part of the next batch

Ruben Van de Velde (Dec 10 2021 at 13:32):

It's in the current batch, yeah

Ruben Van de Velde (Dec 10 2021 at 13:33):

Best case, trying to change priority now doesn't do anything, worst case it cancels this batch

Johan Commelin (Dec 10 2021 at 13:36):

I bumped the prio. If this batch fails, hopefully that means that #10703 will be tried on its own right after the failure.

Junyan Xu (Dec 10 2021 at 13:54):

Links to PRs are failing. Must change "issues" to "pull" now. Strange github regression ...

Johan Commelin (Dec 10 2021 at 13:57):

Johan Commelin (Dec 10 2021 at 15:21):

Let's hope the build failures are now gone

Anatole Dedecker (Dec 10 2021 at 15:43):

I guess we still need to merge master to failing branches, right ?

Eric Wieser (Dec 10 2021 at 15:44):

Only the ones failing with timeouts in algebraic_geometry/presheafed_space/has_colimits.lean. The ones where the server just died (maybe that was another thread), you can restart the build

Last updated: Dec 20 2023 at 11:08 UTC