Inconsistency detected by ld.so

Stream: lean4

[Yakov Pechersky]

I was on mathlib commit 12e7ef97c27 and did a git pull to move to master, hash d076a503010. I ran lake exe cache get:

lake exe cache get
info: Version 4.1.1 of elan is available! Use `elan self update` to update.
info: downloading https://github.com/leanprover/lean4/releases/download/v4.20.0-rc2/lean-4.20.0-rc2-linux.tar.zst
348.1 MiB / 348.1 MiB (100 %)  33.8 MiB/s ETA:   0 s
info: installing /home/yakov/.elan/toolchains/leanprover--lean4---v4.20.0-rc2
error: compiled configuration is invalid; run with '-R' to reconfigure

seeing the error, I did a rm -rf .lake followed by a lake exe cache get:

lake exe cache get
info: plausible: cloning https://github.com/leanprover-community/plausible
info: plausible: checking out revision '304c5e2f490d546134c06bf8919e13b175272084'
info: LeanSearchClient: cloning https://github.com/leanprover-community/LeanSearchClient
info: LeanSearchClient: checking out revision '25078369972d295301f5a1e53c3e5850cf6d9d4c'
info: importGraph: cloning https://github.com/leanprover-community/import-graph
info: importGraph: checking out revision '24f15e3fbeb4df449dacb61f761a136e9c989a94'
info: proofwidgets: cloning https://github.com/leanprover-community/ProofWidgets4
info: proofwidgets: checking out revision '632ca63a94f47dbd5694cac3fd991354b82b8f7a'
info: aesop: cloning https://github.com/leanprover-community/aesop
info: aesop: checking out revision '9264d548cf1ccf0ba454b82f931f44c37c299fc1'
info: Qq: cloning https://github.com/leanprover-community/quote4
info: Qq: checking out revision '36ce5e17d6ab3c881e0cb1bb727982507e708130'
info: batteries: cloning https://github.com/leanprover-community/batteries
info: batteries: checking out revision '92079574ccbf31af64468cb70f0f9da6c0138997'
info: Cli: cloning https://github.com/leanprover/lean4-cli
info: Cli: checking out revision 'aff4176e5c41737a0d73be74ad9feb6a889bfa98'
Inconsistency detected by ld.so: dl-minimal.c: 126: realloc: Assertion `ptr == alloc_last_block' failed!

[Yakov Pechersky]

I'm on glibc 2.31:

$ ldd --version
ldd (Ubuntu GLIBC 2.31-0ubuntu9.9) 2.31
Copyright (C) 2020 Free Software Foundation, Inc.
This is free software; see the source for copying conditions.  There is NO
warranty; not even for MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.
Written by Roland McGrath and Ulrich Drepper.

[Yakov Pechersky]

Checking out 58e0e1ca408, which is 1 commit behind the v4.20 bump, lake exe cache get retrieves and installs 4.19 without a hitch:

$ lake exe cache get
info: downloading https://releases.lean-lang.org/lean4/v4.19.0/lean-4.19.0-linux.tar.zst
327.9 MiB / 327.9 MiB (100 %)  30.0 MiB/s ETA:   0 s
info: installing /home/yakov/.elan/toolchains/leanprover--lean4---v4.19.0
Attempting to download 6643 file(s)
Downloaded: 6643 file(s) [attempted 6643/6643 = 100%] (100% success)
Decompressing 6643 file(s)
Unpacked in 12342 ms

[Kim Morrison]

I won't have a chance to look at this today, but given the patch added to make rc2 work, I'm not totally surprised. Can anyone else reproduce?

[Sebastian Ullrich]

@Yakov Pechersky Could you please post a stack trace, e.g. using coredumpctl?

[Yakov Pechersky]

Yes, will do, but will need like 24 hours

[Yakov Pechersky]

coredumpctl couldn't find any coredumps (even after I upgraded my WSL to use systemd. So instead, I ran

$ LD_DEBUG=all lake exe cache get 2>&1 | grep -C1 alloc_last_block
     10266:     binding file /home/yakov/math/mathlib4/.lake/build/bin/cache [0] to /lib64/ld-linux-x86-64.so.2 [0]: normal symbol `realloc' [GLIBC_2.2.5]
Inconsistency detected by ld.so: dl-minimal.c: 126: realloc: Assertion `ptr == alloc_last_block' failed!
     10266:     symbol=epoll_pwait;  lookup in file=/home/yakov/math/mathlib4/.lake/build/bin/cache [0]

[Yakov Pechersky]

I'm able to recreate this on the ubuntu:20.04 docker image.

[Yakov Pechersky]

Will share a Dockerfile shortly

[Yakov Pechersky]

FROM ubuntu:20.04

RUN apt update && \
    apt install -y curl git
RUN curl https://elan.lean-lang.org/elan-init.sh -sSf | sh -s -- -y
ENV PATH="/root/.elan/bin:$PATH"
ENV HASH=01239f4904a7e86e772ed7cf0e5712134f840718
RUN git clone https://github.com/leanprover-community/mathlib4 --single-branch && \
    cd mathlib4 && \
    git checkout $HASH
WORKDIR /mathlib4
# run plain to get the v4.20.0-rc2 toolchain first and cache the layer
RUN lake
# hit the problem (has to clone dependencies, then build, then crash)
RUN lake exe cache

[Yakov Pechersky]

 => [6/7] RUN lake                                                                                                                                                                                                                                       39.6s
 => ERROR [7/7] RUN lake exe cache                                                                                                                                                                                                                       16.1s
------
 > [7/7] RUN lake exe cache:
1.340 info: plausible: cloning https://github.com/leanprover-community/plausible
1.340 info: plausible: checking out revision '304c5e2f490d546134c06bf8919e13b175272084'
1.617 info: LeanSearchClient: cloning https://github.com/leanprover-community/LeanSearchClient
1.617 info: LeanSearchClient: checking out revision '25078369972d295301f5a1e53c3e5850cf6d9d4c'
1.959 info: importGraph: cloning https://github.com/leanprover-community/import-graph
1.959 info: importGraph: checking out revision '24f15e3fbeb4df449dacb61f761a136e9c989a94'
2.701 info: proofwidgets: cloning https://github.com/leanprover-community/ProofWidgets4
2.701 info: proofwidgets: checking out revision '632ca63a94f47dbd5694cac3fd991354b82b8f7a'
4.288 info: aesop: cloning https://github.com/leanprover-community/aesop
4.288 info: aesop: checking out revision '9264d548cf1ccf0ba454b82f931f44c37c299fc1'
4.622 info: Qq: cloning https://github.com/leanprover-community/quote4
4.622 info: Qq: checking out revision '36ce5e17d6ab3c881e0cb1bb727982507e708130'
11.20 info: batteries: cloning https://github.com/leanprover-community/batteries
11.20 info: batteries: checking out revision '92079574ccbf31af64468cb70f0f9da6c0138997'
11.57 info: Cli: cloning https://github.com/leanprover/lean4-cli
11.57 info: Cli: checking out revision 'aff4176e5c41737a0d73be74ad9feb6a889bfa98'
11.77 ✔ [2/12] Built Cache.Lean
11.87 ✔ [3/12] Built Cache.Lean:c.o
12.77 ✔ [4/12] Built Cache.IO
13.47 ✔ [5/12] Built Cache.Hashing
14.17 ✔ [6/12] Built Cache.Requests
14.37 ✔ [7/12] Built Cache.Hashing:c.o
14.67 ✔ [8/12] Built Cache.Main
14.67 ✔ [9/12] Built Cache.IO:c.o
15.07 ✔ [10/12] Built Cache.Requests:c.o
15.27 ✔ [11/12] Built Cache.Main:c.o
15.87 ✔ [12/12] Built cache
15.89 Inconsistency detected by ld.so: dl-minimal.c: 126: realloc: Assertion `ptr == alloc_last_block' failed!
------
Dockerfile.recreate:15
--------------------
  13 |     RUN lake
  14 |     # hit the problem (has to clone and try to build first)
  15 | >>> RUN lake exe cache
  16 |
--------------------
ERROR: failed to solve: process "/bin/sh -c lake exe cache" did not complete successfully: exit code: 127

[María Inés de Frutos Fernández]

I am getting this error as well in a project importing mathlib.

[Kim Morrison]

@María Inés de Frutos Fernández, could you tell us more? (e.g. are you also on Linux?)

[María Inés de Frutos Fernández]

Yes, I am also on Ubuntu 20.04.5 .

[Sebastian Ullrich]

I believe this should be fixed in lean#8228, I was able to create a working executable in the Docker container using that cmdline

[Kim Morrison]

We'll have Mathlib on v4.20.0-rc3 asap.

[Sebastian Ullrich]

Confirmed that lake exe cache succeeds in the Docker container with the PR toolchain

[Edward van de Meent]

just want to point out that as discussed in #general > `import Mathlib` not working in `live.lean-lang.org`?, live.lean might be a reproducer for the issue María Inés de Frutos Fernández mentioned.
turns out i was completely wrong about this, apologies

[Floris van Doorn]

Running into the same issue. Thanks for the quick fix!

[Kim Morrison]

Once #24621 has landed in Mathlib, Mathlib will be on v4.20.0-rc3, and hopefully the problems in this thread will be resolved.

[María Inés de Frutos Fernández]

I can confirm that this fixed the issue for me. Thank you very much!