leangz error

Stream: general

[Scott Morrison]

@Mario Carneiro, on the lean-pr-testing-2591 branch, running lake build and then lake exe cache put outputs:

% lake exe cache put
Compressing cache
uncaught exception: thread 'main' panicked at 'range end index 3037491200 out of range for slice of length 650064', /Users/runner/work/leangz/leangz/src/lgz.rs:1041:30
note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace

It doesn't reproduce on the second run, but thought I would post this anyway in case you have an idea.

[Patrick Massot]

I don't see this message but trying to get cache consistently says:

Attempting to download 3225 file(s)
Downloaded: 0 file(s) [attempted 3225/3225 = 100%] (0% success)
Warning: some files were not found in the cache.
This usually means that your local checkout of mathlib4 has diverged from upstream.
If you push your commits to a branch of the mathlib4 repository, CI will build the oleans and they will be available later.

this is in a project depending on mathlib updated a couple of hours ago.

[Patrick Massot]

The latest mathlib commit was #7462.

[Siddhartha Gadgil]

When I had this error it was because of a mismatch of toolchains with mathlib.

[Scott Morrison]

@Patrick Massot, if you're still seeing this perhaps you can link to the project so there's something reproducible?

[Patrick Massot]

Siddharta, this was my first reaction, but toolchain match.

[Patrick Massot]

Scott, this is happening in the algebra branch of mathematics_in_lean_source. I think the current state on GitHub has mismatched toolchains, but fixing this does not fix the above issue.

[Scott Morrison]

Hence the suggestion to link to something reproducible?

[Mario Carneiro]

That's almost certainly a corrupted olean file. (More precisely, it read a bignum object with a capacity field that is far too large)

[Mario Carneiro]

I don't see why such an error would not be reproducible though. lake exe cache put does not modify the .olean files, so if you run it twice in a row you should get the same result

[Patrick Massot]

@Scott Morrison , I don't understand what is not reproducible. You can run

git clone git@github.com:avigad/mathematics_in_lean_source.git
cd mathematics_in_lean_source/
git checkout algebra
lake exe cache get

[Patrick Massot]

The weird thing is that it works inside the mathlib folder itself if I checkout the same commit.

[Patrick Massot]

And deleting $HOME/.cache/mathlib doesn't help.

[Patrick Massot]

Actually it not only doesn't help, it triggers:

$ lake exe cache get
leantar is too old; downloading more recent version
Attempting to download 3796 file(s)
Downloaded: 571 file(s) [attempted 3796/3796 = 100%] (15% success)
uncaught exception: no such file or directory (error code: 2)
  file: /home/pmassot/.cache/mathlib/curl.cfg

[Patrick Massot]

I just ran lake update && cp lake-packages/mathlib/lean-toolchain . and lake exe cache get and this time everything worked. So there is indeed an issue that is specific to mathlib@71a0cb812bdefdf75535d8cc894026f1eaca4ba1. I'm still curious to know whether anyone else can reproduce (I didn't push to mil so the reproducing instructions from 10 minutes ago are still accurate).

[Sebastien Gouezel]

I can not reproduce (but some files were already in my cache):

Attempting to download 3225 file(s)
Downloaded: 0 file(s) [attempted 3225/3225 = 100%] (0% success)
Warning: some files were not found in the cache.
This usually means that your local checkout of mathlib4 has diverged from upstream.
If you push your commits to a branch of the mathlib4 repository, CI will build the oleans and they will be available later.
Decompressing 571 file(s)
unpacked in 3226 ms

[Sebastien Gouezel]

(Well, it reproduces the fact that there is no cache to download, but it doesn't reproduce your weird error message).

[Patrick Massot]

Thanks Sébastien, this already reproduces the main issue.

[Scott Morrison]

Patrick Massot said:

Scott Morrison , I don't understand what is not reproducible.

I was referring to your statement "I think the current state on GitHub has mismatched toolchains, but fixing this does not fix the above issue."

[Scott Morrison]

I get:

% lake exe cache get
info: cloning https://github.com/leanprover-community/mathlib4 to ./lake-packages/mathlib
info: cloning https://github.com/leanprover/std4 to ./lake-packages/std
info: cloning https://github.com/gebner/quote4 to ./lake-packages/Qq
info: cloning https://github.com/JLimperg/aesop to ./lake-packages/aesop
info: cloning https://github.com/mhuisi/lean4-cli.git to ./lake-packages/Cli
info: cloning https://github.com/EdAyers/ProofWidgets4 to ./lake-packages/proofwidgets
info: [0/6] Fetching proofwidgets cloud release
info: [1/9] Building Cache.IO
info: [2/9] Compiling Cache.IO
info: [2/9] Building Cache.Hashing
info: [3/9] Compiling Cache.Hashing
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
info: stderr:
ld64.lld: warning: /usr/lib/system/libsystem_kernel.dylib has version 13.5.0, which is newer than target minimum of 13.0.0
ld64.lld: warning: /usr/lib/system/libsystem_platform.dylib has version 13.5.0, which is newer than target minimum of 13.0.0
ld64.lld: warning: /usr/lib/system/libsystem_pthread.dylib has version 13.5.0, which is newer than target minimum of 13.0.0
Attempting to download 591 file(s)
Downloaded: 591 file(s) [attempted 591/591 = 100%] (100% success)
Decompressing 3797 file(s)
unpacked in 3398 ms

[Patrick Massot]

Sorry, the repository moved in the mean time. The weird errors were on deb72e6c3eb34837f709fd3088d0ae9f887e681c