lake exe cache get fails on gitpod

Stream: general

[Eric Wieser]

This seems to be due to the change to caching (leantar) that just landed:

$ lake exe cache get
leantar is too old; downloading more recent version
uncaught exception: tar (child): xz: Cannot exec: No such file or directory
tar (child): Error is not recoverable: exiting now
tar: Child returned status 2
tar: Error is not recoverable: exiting now

[Eric Wieser]

sudo apt-get install xz-utils seems to fix it

[Scott Morrison]

Oof, that's worrying though. We may need to add this to all our installation instructions.

[Scott Morrison]

@Mario Carneiro, there's not some cheap way to avoid this dependency?

[Floris van Doorn]

On Windows, after running lake exe cache get on current mathlib4 master and running lake build after that, Lean starts recompiling everything.
This was the output of lake exe cache get.

info: downloading component 'lean'
info: installing component 'lean'
info: updating .\lake-packages\std to revision dff883c55395438ae2a5c65ad5ddba084b600feb
info: updating .\lake-packages\Qq to revision e6ca4e7e6b13ceee845e40a904c1a71ed9866574
info: updating .\lake-packages\aesop to revision f04538ab6ad07642368cf11d2702acc0a9b4bcee
info: cloning https://github.com/mhuisi/lean4-cli.git to .\lake-packages\Cli
info: [1/9] Building Cache.IO
info: [2/9] Building Cache.Hashing
info: [2/9] Compiling Cache.IO
info: [3/9] Building Cache.Requests
info: [6/9] Compiling Cache.Requests
info: [6/9] Building Cache.Main
info: [7/9] Compiling Cache.Main
info: [9/9] Linking cache.exe
leantar is too old; downloading more recent version
Attempting to download 3565 file(s)
Downloaded: 3565 file(s) [attempted 3565/3565 = 100%] (100% success)
Decompressing 3565 file(s)
uncaught exception: no such file or directory (error code: 2)

[Scott Morrison]

Sorry, it seems merging was premature, and we needed to do more testing on other platforms.

[Scott Morrison]

I will make a revert PR now.

[Eric Wieser]

It's rather unfortunate that uncaught exception: no such file or directory (error code: 2) doesn't include the name of the thing that was missing!

[Eric Wieser]

(Though I assume it's also xz)

[Scott Morrison]

#5853

[Mauricio Collares]

The leantar binary will probably need to be modified using patchelf --set-interpreter to run on NixOS:

$ file ./leantar-0.1.1
./leantar-0.1.1: ELF 64-bit LSB pie executable, x86-64, version 1 (SYSV), dynamically linked, interpreter /lib64/ld-linux-x86-64.so.2, BuildID[sha1]=ab923dc1f445c5df139831b216b95a18f2d5f0a5, for GNU/Linux 3.2.0, stripped

Currently it errors out with leantar-0.1.1: cannot execute: required file not found. Can leantar be distributed via elan (as rust-analyzer is distributed via rustup, say) ? Then the NixOS elan package could handle the required patching.

[Sebastian Ullrich]

Mauricio Collares said:

Can leantar be distributed via elan (as rust-analyzer is distributed via rustup, say) ?

There is no such functionality in elan. I would suggest building leantar locally or upstreaming a Nix derivation for it into leantar/Nixpkgs

[Sebastian Ullrich]

Assuming it will not have as many breaking changes as Lean itself

[Sebastian Ullrich]

Of course, if you want to add a conditional patchelf call into Cache, I don't think anyone would mind either

[Sebastian Ullrich]

Eric Wieser said:

It's rather unfortunate that uncaught exception: no such file or directory (error code: 2) doesn't include the name of the thing that was missing!

It is probably from process creation: https://github.com/leanprover/lean4/blob/a3ebfe29ea516e45dba97dfd303cfc11cc47ff04/src/runtime/process.cpp#L433-L434. Which makes sense, LEANTARBIN seems to be missing a .exe file extension on Windows /cc @Mario Carneiro

[Mario Carneiro]

Oof, yes the leantar PR was not ready for merge yet, I was planning on revisiting it once the lean4 bump PR landed

[Mario Carneiro]

Scott Morrison said:

Mario Carneiro, there's not some cheap way to avoid this dependency?

The tar use here is just for unpacking the leantar executable itself. It's using different file extensions depending on what is conventionally aviailable on the OS, but I guess .xz isn't available on linux?

[Mario Carneiro]

tar.gz should be fine I guess

[Mario Carneiro]

Eric Wieser said:

(Though I assume it's also xz)

This is unlikely, leantar is a statically linked executable that comes with all its dependencies. The error message there looks like it is coming from lean

[Mario Carneiro]

The leantar issues should be fixed now. It would be good for those who have reported errors (@Eric Wieser @Mauricio Collares @Julian Berman) to try checking out the leantar branch and seeing if it works before we merge

[Julian Berman]

seems to be working here at least!

[Gabriel Ebner]

This is unlikely, leantar is a statically linked executable that comes with all its dependencies. The error message there looks like it is coming from lean

@Mario Carneiro No it's not:

$ ldd leantar-v0.1.2-x86_64-unknown-linux-gnu/leantar
        linux-vdso.so.1 (0x00007ffd18946000)
        libgcc_s.so.1 => /nix/store/ryvnrp5n6kqv3fl20qy2xgcgdsza7i0m-xgcc-12.3.0-libgcc/lib/libgcc_s.so.1 (0x00007f4d26cb5000)
        libm.so.6 => /nix/store/3n58xw4373jp0ljirf06d8077j15pc4j-glibc-2.37-8/lib/libm.so.6 (0x00007f4d26920000)
        libc.so.6 => /nix/store/3n58xw4373jp0ljirf06d8077j15pc4j-glibc-2.37-8/lib/libc.so.6 (0x00007f4d2673a000)
        /lib64/ld-linux-x86-64.so.2 => /nix/store/3n58xw4373jp0ljirf06d8077j15pc4j-glibc-2.37-8/lib64/ld-linux-x86-64.so.2 (0x00007f4d26cd8000)

[Floris van Doorn]

Mario already knows this, but leantar is now working on Windows!
However, there seem to be some performance issues. On the leantar branch the unpacking seems excessively slow:

Attempting to download 2341 file(s)
Downloaded: 2341 file(s) [attempted 2341/2341 = 100%] (100% success)
Decompressing 3568 file(s)
unpacked in 93668 ms

If I then immediately run the same command again:

$ time lake exe cache get
No files to download
Decompressing 3568 file(s)
unpacked in 225 ms

real    0m20.483s
user    0m0.000s
sys     0m0.000s

Something still took long here...

[Floris van Doorn]

Here is the comparison with the same commands on master:

Floris@Dell-E MINGW64 ~/projects/mathlib4c ((4d8f5b5cb...))
$ time lake exe cache get
info: [1/9] Building Cache.IO
info: [2/9] Building Cache.Hashing
info: [2/9] Compiling Cache.IO
info: [4/9] Building Cache.Requests
info: [6/9] Compiling Cache.Requests
info: [6/9] Building Cache.Main
info: [7/9] Compiling Cache.Main
info: [9/9] Linking cache.exe
Attempting to download 43 file(s)
Downloaded: 43 file(s) [attempted 43/43 = 100%] (100% success)
Decompressing 3569 file(s)

real    1m20.293s
user    0m0.000s
sys     0m0.000s

Floris@Dell-E MINGW64 ~/projects/mathlib4c ((4d8f5b5cb...))
$ time lake exe cache get
No files to download
Decompressing 3569 file(s)

real    0m45.238s
user    0m0.000s
sys     0m0.000s

So the first run of lake exe cache get is slower on the leantar branch (if the printed 90s of unpacking is accurate and measuring real time), but the subsequent run is faster.

[Mario Carneiro]

Gabriel Ebner said:

This is unlikely, leantar is a statically linked executable that comes with all its dependencies. The error message there looks like it is coming from lean

Mario Carneiro No it's not:

$ ldd leantar-v0.1.2-x86_64-unknown-linux-gnu/leantar
        linux-vdso.so.1 (0x00007ffd18946000)
        libgcc_s.so.1 => /nix/store/ryvnrp5n6kqv3fl20qy2xgcgdsza7i0m-xgcc-12.3.0-libgcc/lib/libgcc_s.so.1 (0x00007f4d26cb5000)
        libm.so.6 => /nix/store/3n58xw4373jp0ljirf06d8077j15pc4j-glibc-2.37-8/lib/libm.so.6 (0x00007f4d26920000)
        libc.so.6 => /nix/store/3n58xw4373jp0ljirf06d8077j15pc4j-glibc-2.37-8/lib/libc.so.6 (0x00007f4d2673a000)
        /lib64/ld-linux-x86-64.so.2 => /nix/store/3n58xw4373jp0ljirf06d8077j15pc4j-glibc-2.37-8/lib64/ld-linux-x86-64.so.2 (0x00007f4d26cd8000)

Unclear if you are making this claim, but AFAICT those are all standard .so's. If I link a hello world rust program then I already get everything there except for libm.so.6, and I think zstd might be linking that in (but I don't know of any issues in asking for the <math> library).

[Sebastian Ullrich]

For what it's worth, Linux elan is an actual static executable linked against musl, which avoids the NixOS issue from above (not relevant in elan's case) as well as libc compatibility issues

[Sebastian Ullrich]

leantar-v0.1.2-x86_64-unknown-linux-gnu/leantar uses glibc 2.34 symbols, this will definitely be an issue. Lean is built against 2.27, which is e.g. what Ubuntu 18.04 still uses.

[Gabriel Ebner]

There's a clear definition of what statically linked executable means; namely that it doesn't do dynamic linking. Requiring only some shared libraries is still dynamically linking.

[Gabriel Ebner]

Sebastian has made this work very nicely for elan. You can check out the CI config here: https://github.com/leanprover/elan/blob/master/.github/workflows/ci.yml

[Mario Carneiro]

I would appreciate it if you had some tips for https://github.com/digama0/leangz/actions/runs/5554223604, it doesn't seem to be working and this is not my expertise

[Mario Carneiro]

As I understand it, statically linking everything is a problem for most OSs, because the syscall interface is not stable. You would not statically link kernel32.dll

[Sebastian Ullrich]

I can take a look. The Linux kernel interface is famously stable ("don't break userspace!")

[Mario Carneiro]

it seems like you are using cross for everything, not just the cross-compiles?

[Mario Carneiro]

I modeled the original ci.yml on lean4's

[Sebastian Ullrich]

Yes, cross does some black magic like I think setting up a Docker container with musl. Really dynamically linking against the same glibc as Lean does would be sufficient and save a bit of space, static musl linking is simply the approach that seemed simpler to set up for elan.

[Sebastian Ullrich]

Perhaps the modern solution would be to use cargo zigbuild https://github.com/rust-cross/cargo-zigbuild#specify-glibc-version... what a mess