Web editors are broken

Stream: general

[Eric Wieser]

Both the FRO and HHU web editors no longer allow importing mathlib

import Mathlib

On the HHU one, the error is

`/elan/toolchains/leanprover--lean4---v4.3.0-rc2/bin/lake print-paths Init Mathlib` failed:

stderr:
error: read-only file system (error code: 30)
  file: ./.lake/lakefile.olean.trace

On the FRO one, it's just unknown package 'Mathlib'

[Jireh Loreaux]

Is this due to the cache breakage?

[Jireh Loreaux]

Sorry, I mean the location of the build directory moving.

[Sebastian Ullrich]

Fixed, thanks. For live.lean-lang, it was an overzealous ProtectHome = "read-only" that clashed with the new lakefile.olean locking.

[Jon Eugster]

Hmm, whatever I do, lake update always results in

[...]
/home/USER/.cache/mathlib/7d56bc4bb976be8d.ltar: bad .trace file
uncaught exception: leantar failed with error code 1
error: mathlib: failed to fetch cache

[Jon Eugster]

I am absolutely not familiar with the plenty changes to lake and cache recently, does somebody know what that means?

[Sebastian Ullrich]

I didn't need to do it but does nuking that cache dir help?

[Jon Eugster]

nope :S I now nuked everything I could think of:

• ~/.cache
• Project/lake-manifest.json
• Project/.lake
• Project/build
• Project/lakefile.olean
• Project/lake-packages

[Sebastian Ullrich]

That error is from leantar but I wouldn't know what changed there /cc @Mario Carneiro

[Mario Carneiro]

did you land the new olean format?

[Sebastian Ullrich]

Nope

[Sebastian Ullrich]

(and it all works on the FRO machine now)

[Mauricio Collares]

What commit is this happening on, exactly?

[Jon Eugster]

Maybe I didn't delete all the files I mentioned above in one go. Now Im getting a different error (Warning: some files were not found in the cache.), which looks like I can figure it out.

[Mauricio Collares]

Yes, this error is happening everywhere. It's probably due to ProofWidgets (9 files missing and all).

[Mario Carneiro]

I don't suppose you can cat .lake/build/lib/Mathlib/LinearAlgebra/Matrix/InvariantBasisNumber.trace for the system that produced that message @Jon Eugster

[Jon Eugster]

I have two other questions on the topic:

1. the new post-update hook means I can drop curl -L https://raw.githubusercontent.com/leanprover-community/mathlib4/master/lean-toolchain -o lean-toolchain now,, which used to copy the correct toolchain for mathlib, doesn't it?
2. Is there a reasonable way to manage installed toolchains? Simultaneously, our server was filled up with tens of GB of lean toolchains, and my current approach is to delete all but the newest one by hand every now and then.

[Jon Eugster]

Mario Carneiro said:

I don't suppose you can cat .lake/build/lib/Mathlib/LinearAlgebra/Matrix/InvariantBasisNumber.trace for the system that produced that message Jon Eugster

I think I already deleted that, sorry

[Mario Carneiro]

the bad .trace file means that an IO error occurred while attempting to read the file, or it had invalid contents

[Mario Carneiro]

it may have been a "read only filesystem" error like the other one

[Mario Carneiro]

No, elan is just as space-hungry as it has always been, no change there

[Sebastian Ullrich]

Elan implements the Null GC

[Mario Carneiro]

it implements the human GC

[Sebastian Ullrich]

It was originally made for crabs so some friction is to be expected

[Jon Eugster]

I guess I could write a bash script that feeds the output of elan toolchain list (except one toolchain) into elan toolchain uninstall, but I'm a bit afraid that it will by accident delete every last toolchain and break everything thereby :thinking:

[Sebastian Ullrich]

There is https://github.com/JLimperg/elan-cleanup. Now if someone wants to translate that to Rust...

[Patrick Massot]

cd elan-cleanup/
pmassot@fixe-massy:~/lean/elan-cleanup$ lake build
info: downloading component 'lean'

Noooo...

[Patrick Massot]

./build/bin/elan-cleanup
uncaught exception: permission denied (error code: 13)

Final outcome: my .elan is now bigger than before trying this.

[Jon Eugster]

Sebastian Ullrich said:

Fixed, thanks. For live.lean-lang, it was an overzealous ProtectHome = "read-only" that clashed with the new lakefile.olean locking.

So what is this fix exactly. Is this something I can change in the source code? Or was that specific to your nix (?) setup?

[Patrick Massot]

I managed to run it but it keeps way too many toolchains because it does not filter out lean-toolchain files that are in lake-packages (or any of its previous and future incarnations).

[Sebastian Ullrich]

Jon Eugster said:

Sebastian Ullrich said:

Fixed, thanks. For live.lean-lang, it was an overzealous ProtectHome = "read-only" that clashed with the new lakefile.olean locking.

So what is this fix exactly. Is this something I can change in the source code? Or was that specific to your nix (?) setup?

It was specific to my systemd setup, there is nothing to do there in your setup AFAIU

[Patrick Massot]

But still it managed to

erasing leanprover-community-lean-3.15.0
erasing leanprover-community-lean-3.28.0
erasing leanprover-community-lean-3.32.1
erasing leanprover/lean4:nightly-2021-10-28
erasing leanprover-community/lean:3.51.1
erasing leanprover/lean4:nightly-2022-08-16
erasing leanprover-community-lean-3.26.0
erasing leanprover-community-lean-3.16.4
erasing leanprover-community/lean:3.18.4
erasing leanprover/lean4:nightly-2022-12-13
erasing nightly-2019-01-13
erasing leanprover-community/lean:3.40.0
erasing leanprover-community/lean:3.36.0
erasing leanprover/lean4:nightly-2023-07-30
erasing leanprover/lean4:nightly-2022-09-03
erasing leanprover-community/lean:3.33.0
erasing leanprover-community-lean-3.14.0
erasing leanprover-community/lean:3.48.0
erasing leanprover-community-lean-3.19.0
erasing leanprover/lean4-pr-releases:pr-release-2393
erasing leanprover-community-lean-3.7.1
erasing leanprover-community-lean-3.18.4
erasing leanprover-community-lean-3.22.0
erasing leanprover-community/lean:3.27.0
erasing leanprover-community-lean-3.16.1
erasing leanprover-community-lean-3.11.0
erasing leanprover/lean4:nightly-2022-12-23
erasing leanprover/lean4:nightly-2023-03-31
erasing leanprover-community-lean-3.7.2
erasing leanprover-community/lean:3.42.1
erasing leanprover/lean4:nightly-2022-11-28
erasing leanprover-community/lean:3.49.1
erasing leanprover/lean4:nightly-2023-05-06
erasing leanprover-community-lean-3.16.3
erasing leanprover-community/lean:3.41.0
erasing leanprover/lean4:nightly-2022-10-03
erasing leanprover-community/lean:3.24.0
erasing leanprover-community/lean:3.15.0
erasing leanprover-community/lean:3.32.1
erasing stable
erasing leanprover-community/lean:3.45.0
erasing leanprover-community/lean:3.31.0
erasing leanprover-community/lean:3.42.0
erasing leanprover-community-lean-3.8.0
erasing leanprover-community-lean-3.16.5
erasing leanprover-community-lean-3.17.1
erasing leanprover/lean4-pr-releases:pr-release-2734
erasing leanprover-community/lean:3.38.0
erasing leanprover/lean4:nightly-2022-08-23
erasing gebner/lean4:reenableeta230506
erasing leanprover-community-lean-3.21.0
erasing leanprover-community/lean:3.43.0
erasing leanprover/lean4:nightly-2023-08-15
erasing leanprover-community/lean:3.39.1
erasing leanprover-community-lean-3.16.2
erasing leanprover/lean4:nightly-2022-07-21
erasing leanprover-community/lean:3.46.0
erasing leanprover-community/lean:3.50.3
erasing leanprover-community-lean-3.31.0
erasing leanprover-community-lean-3.33.0
erasing leanprover-community-lean-3.10.0
erasing leanprover-community-lean-3.6.1
erasing leanprover-community-lean-3.17.0
erasing leanprover/lean4-pr-releases:pr-release-2790
erasing 3.4.2
erasing leanprover-community-lean-3.5.1
erasing 3.4.1
erasing leanprover/lean4:nightly-2023-01-12
erasing leanprover-community/lean:3.35.0
erasing leanprover-community/lean:3.19.0
erasing leanprover/lean4-pr-releases:pr-release-2644
erasing leanprover-community/lean:3.39.0
erasing leanprover/lean4:nightly-2022-08-26
erasing leanprover/lean4:nightly-2022-02-19
erasing leanprover-community/lean:3.39.2
erasing leanprover-community/lean:3.34.0
erasing leanprover-community/lean:3.35.1
erasing leanprover-community/lean:3.37.0
erasing leanprover/lean4:nightly-2023-04-11
erasing nightly-2018-12-12
erasing leanprover-community-lean-3.23.0
erasing leanprover-community-lean-3.30.0
erasing leanprover/lean4:stable
erasing leanprover/lean4:nightly-2023-05-31
erasing leanprover/lean4:nightly-2023-01-17
erasing leanprover-community/lean:3.44.1
erasing leanprover-community-lean-3.20.0
erasing semorrison/lean4:reenableeta230503
erasing leanprover-community-lean-3.27.0
erasing leanprover/lean4:nightly-2022-08-11
erasing leanprover-community-lean-nightly
erasing leanprover/lean4:nightly-2023-07-19
erasing leanprover-community-lean-3.24.0
erasing leanprover-community-lean-3.9.0
erasing leanprover-community/lean:3.5.1
erasing leanprover/lean4:nightly-2023-03-15

[Jon Eugster]

Mine works now again, but it throws

stderr:
error: read-only file system (error code: 30)
  file: ./.lake/lakefile.olean.trace

(see here), which I don't fully understand why it A) needs to write anything there and B) can't do so

[Patrick Massot]

This tool is probably right that I'm not using nightly-2018-12-12 that much, but I feel nostalgic anyway.

[Jon Eugster]

You must have a lot of space keeping toolchains from 2018 around :eyes:

[Jon Eugster]

~/elan-cleanup$ build/bin/elan-cleanup
found toolchain [...]
erasing stable

Guess I don't need a stable lean release...

[Jon Eugster]

Patrick Massot said:

I managed to run it but it keeps way too many toolchains because it does not filter out lean-toolchain files that are in lake-packages (or any of its previous and future incarnations).

Here's a fix for this: https://github.com/JLimperg/elan-cleanup/pull/1

[Kevin Buzzard]

Jon Eugster said:

You must have a lot of space keeping toolchains from 2018 around :eyes:

If Patrick's machine is anything like mine, there will be a lot of toolchains on it... . I bet we both go back to 2017 (or at least Patrick did, until the incident above...)

[Patrick Massot]

Also remember that a Lean 3 toolchain takes up almost no space compared to a Lean 4 one.

[Mauricio Collares]

Mauricio Collares said:

Yes, this error is happening everywhere. It's probably due to ProofWidgets (9 files missing and all).

This should be fixed when #8216 is merged, I think.

Edit: Wait, no, I think that has landed already! The merge commits are a bit funny so I can't be sure.

[Scott Morrison]

btw, this is the magic incantation that Mathlib CI uses for toolchain garbage collection:

# Delete all but the 10 most recent toolchains.
# Make sure to delete both the `~/.elan/toolchains/X` directory and the `~/.elan/update-hashes/X` file.
# Skip symbolic links (`-type d`), the current directory (`! -name .`), and `nightly` and `stable`.
cd ~/.elan/toolchains && find . -maxdepth 1 -type d ! -name . -print0 | xargs -0 ls -1td | grep -v 'nightly$' | grep -v 'stable$' | tail -n +11 | xargs -I {} sh -c 'echo {} && rm -rf "{}" && rm "../update-hashes/{}"' || true

[Jon Eugster]

Interesting, I definitely broke elan before by manually deleting stuff from the .elan folder. I guess rm "../update-hashes/{}"' is the real magic here