nightly sandbox broken

Stream: lean4

[Kim Morrison]

The nightly version of the sandbox seems to be broken for me, e.g. here. It gets stuck on "Waiting for Lean server to start...".

Could someone confirm they see the same behaviour?

[Kim Morrison]

I actually can't remember who set up the nightly version of the sandbox --- if some remembers, perhaps we can ping them here, thanks. :-)

[Joachim Breitner]

Pinging @Joachim Breitner .

[Joachim Breitner]

Hmm, I see a confusing lake error in the log

info: mathlibLatest: no previous manifest, creating one from scratch
info: mathlib: running post-update hooks
⚠ [1/10] Fetched proofwidgets:optRelease
info: proofwidgets: wanted prebuilt release, but no tag found for revision
warning: failed to fetch cloud release; falling back to local build
No files to download
Decompressing 4729 file(s)
Unpacked in 62 ms
Completed successfully!
⚠ [1/4742] Fetched proofwidgets:optRelease
info: proofwidgets: wanted prebuilt release, but no tag found for revision
warning: failed to fetch cloud release; falling back to local build
ℹ [246/4742] Replayed MathlibLatest.Logic
info: ././././MathlibLatest/Logic.lean:14:2: Try this: exact not_or
✖ [429/4742] Fetching proofwidgets:release
info: proofwidgets: wanted prebuilt release, but no tag found for revision
error: failed to fetch cloud release
Some builds logged failures:
- proofwidgets:release
error: build failed

[Joachim Breitner]

Ah, rm -rf’ing enough things made it work. All works again. I should maybe make the scripts more robust by starting with a fresh directory and switch over atomically; I do that already on loogle. And I should move loogle to the FRO-paid machine. But now it’s working again, so less pressing again :-)

[Kim Morrison]

Anyone else seeing the normal sandbox broken too? At https://live.lean-lang.org/ I just getting "Waiting for Lean server to start..."

[Kim Morrison]

I think we need a bot that checks this periodically and posts about failures to start.

[John Tristan]

Broken for me as well

[Joachim Breitner]

:eyes:

[Joachim Breitner]

Ok, fixed it. The problem was that I did a system update due a security advisory. This changed the GLIBC used by the sandbox server, but not the one used by the downloaded lake toolchains. The sandboxing script was using the the former, when it should be using the latter.

Fixed this by using the libc as embedded in the toolchain.

There is still a similar breakage possible after nix gc, I expect, which affects all nixpkgs’ elan, filed an issue about possibly fixing this.