Is there a problem with Lake at the moment?

Stream: mathlib4

[Björn Wehlin]

I've just cloned a fresh copy of leanprover-community/mathlib4 and when I try to run lake exe cache get, I get the following error:

Inconsistency detected by ld.so: dl-minimal.c: 126: realloc: Assertion ptr == alloc_last_block' failed!`

Moreover, I just pushed a commit to the dirac_apply_ne_iff_eq branch, and the Lint checks are failing with /home/runner/work/_temp/010f26bd-1165-4cdc-ad4c-a48d0a6fe859.sh: line 1: lake: command not found

Here are the two failing jobs:

https://github.com/leanprover-community/mathlib4/actions/runs/15250644232/job/42886638626?pr=24616
https://github.com/leanprover-community/mathlib4/actions/runs/15250643433/job/42886636417?pr=24616

[Michael Rothgang]

That sounds like two different errors. The first one is for CI systems (does re-running the failing job help?, at least as a workaround). The other will depend on your local system: what operating system are you running? (lake exe cache get works fine on my computer, so there has to be some platform-specific difference.)

[Björn Wehlin]

Agreed they are two errors -- I was just thinking whether something had moved in the Lake distribution. I'm on Ubuntu 20.04.6 LTS.

Re-running fixed the CI issues (I somehow didn't find the re-run button earlier!)