Zulip Chat Archive
Stream: lean4
Topic: lake build'ing mathlib HEAD
Julian Berman (Oct 21 2023 at 13:37):
EDIT for TLDR now that a fix is known: Update to Lean v4.2.0-rc4 ASAP, and if you were previously on v4.2.0-rc2 or v4.2.0-rc3 and have a project which you built using one of these two versions, you need to delete a file called lakefile.olean in your project directory after adjusting your lean-toolchain to say rc4 before running anything else.
I'm getting a weird looking error from trying to lake build current mathlib HEAD (at the minute seems like that's 512169bb5. Seems to happen even after a lake clean:
~/Development/Mathlib4 is a git repository on master
⊙ lake clean julian@Mini
error: invalid argument (error code: 22, invalid argument)
file: ./lake-packages/Qq/.
~/Development/Mathlib4 is a git repository on master
⊙ lake build julian@Mini
info: Qq: URL has changed; deleting './lake-packages/Qq' and cloning again
info: cloning https://github.com/leanprover-community/quote4 to ./lake-packages/Qq
error: 'Mathlib': no such file or directory (error code: 2)
file: ./]/./Mathlib.lean
I'm on macOS in case that's not clear from the path there. Not sure what's up yet, but just in case anyone's seen it already? Will post the explanation when I figure it out if not.
Julian Berman (Oct 21 2023 at 13:39):
Somehow surprisingly to me I'm also noticing that lake clean is not idempotent. Is that expected? E.g. here's me just running it a bunch of times in a row, where it seems to be noticing new things one by one about mathlib4 deps:
~/Development/Mathlib4 is a git repository on master
⊙ lake clean -h julian@Mini
Remove build outputs
USAGE:
lake clean [<package>...]
If no package is specified, deletes the build directories of every package in
the workspace. Otherwise, just deletes those of the specified packages.
~/Development/Mathlib4 is a git repository on master
⊙ lake clean julian@Mini
error: invalid argument (error code: 22, invalid argument)
file: ./lake-packages/aesop/.
~/Development/Mathlib4 is a git repository on master
⊙ lake clean julian@Mini
info: aesop: URL has changed; deleting './lake-packages/aesop' and cloning again
info: cloning https://github.com/leanprover-community/aesop to ./lake-packages/aesop
error: invalid argument (error code: 22, invalid argument)
file: ./lake-packages/Cli/.
~/Development/Mathlib4 is a git repository on master
⊙ lake clean julian@Mini
info: Cli: URL has changed; deleting './lake-packages/Cli' and cloning again
info: cloning https://github.com/leanprover/lean4-cli to ./lake-packages/Cli
error: invalid argument (error code: 22, invalid argument)
file: ./lake-packages/proofwidgets/.
~/Development/Mathlib4 is a git repository on master
⊙ lake clean julian@Mini
info: proofwidgets: URL has changed; deleting './lake-packages/proofwidgets' and cloning again
info: cloning https://github.com/leanprover-community/ProofWidgets4 to ./lake-packages/proofwidgets
error: invalid argument (error code: 22, invalid argument)
file: ./.
~/Development/Mathlib4
⊙ lake clean julian@Mini
error: no such file or directory (error code: 2)
file: ./lakefile.lean
~/Development/Mathlib4
⊙ lake clean julian@Mini
error: no such file or directory (error code: 2)
file: ./lakefile.lean
~/Development/Mathlib4
⊙ lake clean julian@Mini
error: no such file or directory (error code: 2)
file: ./lakefile.lean
~/Development/Mathlib4
⊙ lake clean julian@Mini
error: no such file or directory (error code: 2)
file: ./lakefile.lean
Julian Berman (Oct 21 2023 at 13:40):
Oh boy that's not good! So the reason at the end it now can't find lakefile.lean is... it just deleted my entire mathlib repository contents :/
Julian Berman (Oct 21 2023 at 13:41):
I guess I'm quite happy that's all it did, hopefully it hasn't deleted random other files on my hard drive. Time to check :(
Kevin Buzzard (Oct 21 2023 at 13:41):
This is ... erm... a known feature of lake currently. @Mac Malone help!
Julian Berman (Oct 21 2023 at 13:45):
It's all gone so I'm not sure what I can even further share to diagnose. I don't know anything clearly but certainly the "delete stuff other than build artifacts" behavior seems pretty concerning. All-in-all as long as I didn't just lose random other files, no big deal personally it's just some random side work -- in case the idea is helpful though maybe just making sure every single place lake touches file paths it uses absolute paths and absolutely refuses to remove relative ones, let alone ones above a know build directory is a thing to look into. I'm hesitant to volunteer though.
Yaël Dillies (Oct 21 2023 at 13:47):
Julian Berman (Oct 21 2023 at 13:49):
Well... the only thing I can add is lake exe cache get is definitely not related, as I didn't run that, just lake build. I did switch branches, but I don't remember at what point in the sequence. My shell history will maybe remind me. Going to file an issue after reading that thread I guess if no one else did.
Ruben Van de Velde (Oct 21 2023 at 13:50):
Remove lakefile.olean
Julian Berman (Oct 21 2023 at 13:52):
At this point, lake clean removed it don't worry :)
Julian Berman (Oct 21 2023 at 13:53):
Of course I did search for ./]/ before posting but it looks like in that thread that others were getting different versions of the fun corrupted path. Bleh.
Utensil Song (Oct 21 2023 at 13:54):
The takeaway of that topic is that lake runs with the old lakefile.olean even if Lean version and the data structures of Lake are changed, which causes a field shift thus causes issues like yours. And there isn't a simple solution yet because there is no version info in lakefile.olean for detecting that this is happening.
Utensil Song (Oct 21 2023 at 14:00):
For now, if I change something in lakefile or toolchain, or have any trouble with lake, I'll always run lake -R [the rest of the command] where -R would rebuild lakefile itself and reconfigure lake for the project.
Kevin Buzzard (Oct 21 2023 at 14:01):
Surely the simple solution is "roll back some changes immediately before something really bad happens to someone"
Kevin Buzzard (Oct 21 2023 at 14:01):
I mean, arguably, something really bad already happened to two people.
Julian Berman (Oct 21 2023 at 14:09):
(I filed https://github.com/leanprover/lean4/issues/2731 though it's difficult to provide any useful information beyond what's in the other thread, so hopefully Mac or anyone who'll work on it already has a lead)
Julian Berman (Oct 21 2023 at 14:10):
I certainly will personally avoid lake clean until it's fixed, but yeah it does seem like this will cause someone even bigger issues if left unfixed.
Mauricio Collares (Oct 21 2023 at 14:19):
The best solution so far is to upgrade to lean 4.2.0-rc4 (and delete lakefile.olean if you ever used rc2 or rc3)
Mauricio Collares (Oct 21 2023 at 14:21):
https://github.com/leanprover/lean4/commit/6c206737370bc41139bb60100d0e69437d39c84d reverts an ABI change
Mauricio Collares (Oct 21 2023 at 14:22):
See also the release notes for rc4: https://github.com/leanprover/lean4/releases/tag/v4.2.0-rc4
Julian Berman (Oct 21 2023 at 14:24):
This was already after upgrading to rc4 -- though I don't see what in the release notes would hint to this, I don't think anyone will know ABI changes have anything to do with this sort of behavior.
Julian Berman (Oct 21 2023 at 14:24):
I see there's an open PR to make lake clean remove the .olean though.
Eric Wieser (Oct 21 2023 at 14:39):
Kevin Buzzard said:
Surely the simple solution is "roll back some changes immediately before something really bad happens to someone"
This won't help much because the version of lake that gets used is the one that people have in their lean-toolchain, which could point at the broken version.
Kevin Buzzard (Oct 21 2023 at 14:47):
Aah I see. OK well :fingers_crossed: for everyone...
Utensil Song (Oct 21 2023 at 15:35):
Will an announcement help? The release log says "Anyone using rc1, rc2, or rc3 should upgrade to rc4", but most might not be even aware of the issues with rc2 and rc3.
In addition to the announcement, may be some hints on how to ensure safety with the old tool chain, is replacing all lake commands to lake -R gonna be safe?
Richard Copley (Oct 21 2023 at 16:48):
@Julian Berman
It's probably not lost. lake build simply checks out a different revision: the revision specified in lake-manifest.json, which comes (via lake update) from the revision specified in the lakefile.lean. To avoid this, use a filesystem path in lakefile.lean, for example:
require mathlib from "lake-packages/mathlib"
To recover your commits, assuming that git hasn't garbage-collected them yet:
- Take a copy of the entire repo, so that you can experiment without fear
- In your shell, CD into the copy and type
git reflogfor a list of recent commits - Find the commit hash for the commit you want
- Type
git reset --hard <commit>
Julian Berman (Oct 21 2023 at 16:56):
@Richard Copley I know about the reflog -- it's lost :) -- lake blew away the .git directory entirely. Also I should say again I was in Mathlib4. Thanks for the idea though!
Richard Copley (Oct 21 2023 at 17:10):
Oh no! Sorry for making assumptions. And I thought lake build doing checkouts was already pretty unexpected!
Mac Malone (Oct 21 2023 at 19:33):
Kevin Buzzard said:
Surely the simple solution is "roll back some changes immediately before something really bad happens to someone"
The current problem is actually likely due to the rollback. :sob: The problem is now likely incompatibility between different old Lean versions (which cannot be fixed with new changes because the old versions will still exist and cause this problem). :sweat:
Eric Wieser (Oct 21 2023 at 19:40):
Is it worth a post in #general or #announce warning against using lake clean at all, while we work out what went wrong? It would be a shame for anyone else's work to get deleted.
Alex J. Best (Oct 21 2023 at 19:50):
Eric Wieser said:
Is it worth a post in #general or #announce warning against using
lake cleanat all, while we work out what went wrong? It would be a shame for anyone else's work to get deleted.
Agree, I have also managed to delete an entire repo this way (fortunately it was a fresh checkout of std so nothing lost but it could be really bad for some people)
Eric Wieser (Oct 21 2023 at 19:53):
Does this mean you have a repro?
Eric Wieser (Oct 21 2023 at 19:53):
(please test it on gitpod or something to avoid deleting anything of value!)
Mario Carneiro (Oct 21 2023 at 20:02):
Mac Malone said:
Kevin Buzzard said:
Surely the simple solution is "roll back some changes immediately before something really bad happens to someone"
The current problem is actually likely due to the rollback. :sob: The problem is now likely incompatibility between different old Lean versions (which cannot be fixed with new changes because the old versions will still exist and cause this problem). :sweat:
One way to fix this would be to patch the old versions themselves. That is, backport the bugfix to rc2 and rc3, and then update the old releases, meaning that elan will deliver the bugfixed versions of rc2 and rc3 instead of the original ones
Mario Carneiro (Oct 21 2023 at 20:04):
Either that or just delete the elan releases for rc2 and rc3 entirely and live with the breakage, but I think they have existed for a bit too long to avoid promulgation in the ecosystem so this would break any lean projects that have these versions in the lakefile
Mario Carneiro (Oct 21 2023 at 20:09):
I did manage to reproduce the bug a second time, but probably not by a normal method: On a working rc1 project, I used elan override set lean4-debug to point to a development version of lean (made some time after rc3), and lake commands were borked.
Mac Malone (Oct 21 2023 at 20:12):
@Mario Carneiro Yeah, elan override causing a olean mismatch is to be expected currently.
Mario Carneiro (Oct 21 2023 at 20:14):
Of course backport bugfixing will also produce more instances of this problem, but at least these problems will be fixed by clearing your elan cache and will not recur
Sebastian Ullrich (Oct 21 2023 at 20:14):
Hey all, apologies for any troubles this bug has caused. As has been mentioned, this has been fixed in 4.2.0-rc4 such that switching between it and any stable version is safe. Unfortunately, moving between these versions and rc2/3 in any direction is still unsafe and you should remove any lakefile.olean manually in this case (it is always safe to remove as the file is just a cache). We have also updated the release notes for rc2-4 with this information.
Alex J. Best (Oct 21 2023 at 20:44):
Eric Wieser said:
Does this mean you have a repro?
no because everything is gone and its hard to remember exactly which branches I was switching from/ to
Eric Wieser (Oct 21 2023 at 21:17):
Eric Wieser said:
Is it worth a post in #general or #announce warning against using
lake cleanat all, while we work out what went wrong? It would be a shame for anyone else's work to get deleted.
This is now done, thanks Sebastian Ullrich!
Julian Berman (Oct 21 2023 at 22:34):
In case for whatever reason it's useful to someone, in updating a different package I intentionally didn't delete the .olean file to see whether Lake would again delete the project directory, and it didn't, it segfaulted instead. My reproducer for that (the segfault behavior, here on macOS) is:
versions=(4.2.0-rc3 4.2.0-rc4); mkdir test && cd test; for version in $versions; do gh release download -R leanprover/lean4 "v$version" -p "lean-$version-darwin_aarch64.tar.zst" && tar xf "lean-$version-darwin_aarch64.tar.zst" && rm "lean-$version-darwin_aarch64.tar.zst"; done && mkdir foo && cd foo && ../*$versions[1]*/bin/lake init foo && ../*$versions[1]*/bin/lake build && ../*$versions[2]*/bin/lake build which if you indeed make the first version 2 or 3 will segfault (1 will not), and produce:
[0/6] Building Foo.Basic
[1/6] Compiling Foo.Basic
[1/6] Building Foo
[2/6] Compiling Foo
[2/6] Building Main
[3/6] Compiling Main
[6/6] Linking foo
zsh: segmentation fault ../*$versions[2]*/bin/lake build
So, not a reproducer of the original issue, and the fix it sounds like is the same (manually delete the .olean if you were on rc2 or rc3), but figured I may as well post it since it took me 2 or 3 minutes to get the CLI right.
Mario Carneiro (Oct 22 2023 at 22:07):
@Julian Berman I think this case is analogous to the one I reported using elan override. The existing defense against using out of date lakefile.oleans is to check that lean-toolchain has changed; your CLI is just calling two different binaries directly without touching that file, so it doesn't seem representative of what someone would stumble on if they weren't actively hacking lean versions. (BTW if you wanted to reproduce deletion of your project folder you should probably try using lake clean instead of lake build.)
Last updated: Dec 20 2023 at 11:08 UTC