lake broken

Stream: lean4

[Bhavik Mehta]

I just did a pull of mathlib 4 (last pull less than a month ago), then lake exe cache get. It gave this message:

info: downloading component 'lean'
Total: 175.2 MiB Speed:  28.9 MiB/s
info: installing component 'lean'
error: could not remove 'toolchain directory' directory: '/Users/bmehta/.elan/toolchains/leanprover--lean4---v4.2.0-rc3'
info: caused by: Directory not empty (os error 66)

and since then my lake isn't working at all:

$ lake exe cache get
error: toolchain 'leanprover/lean4:v4.2.0-rc3' does not have the binary `/Users/bmehta/.elan/toolchains/leanprover--lean4---v4.2.0-rc3/bin/lake`
$ lake help
error: toolchain 'leanprover/lean4:v4.2.0-rc3' does not have the binary `/Users/bmehta/.elan/toolchains/leanprover--lean4---v4.2.0-rc3/bin/lake`

Then I tried removing the directory that it said couldn't be removed, and I made it worse:

$ lake help
error: toolchain 'leanprover/lean4:v4.2.0-rc3' is not installed

How can I recover my lake?

[Matthew Ballard]

Does deleting the corresponding folders in ~/.elan/toolchains and ~/.elan/update-hashes help?

[Andrew Yang]

When I encounter this issue, elan toolchain uninstall leanprover/lean4:v4.2.0-rc3 && elan toolchain install leanprover/lean4:v4.2.0-rc3 usually works for me.

[Bhavik Mehta]

Removing the one in toolchains seemed to make it worse - as in my above message. I'll try in update-hashes now

[Bhavik Mehta]

That seemed to help, thanks. Is there a reason this happens, and is there an issue in lake for it?

[Matthew Ballard]

I manage to get into that state without lake just pushing around toolchains with elan

[Bhavik Mehta]

True, but I got there by just doing lake exe cache get on a set of caches which exist, and I'm pretty sure this is intended usage, so it shouldn't get me into a broken state!

[Matthew Ballard]

I think elan got interrupted or blocked by something

[Matthew Ballard]

Doesn't the installing component: 'lean' come from elan?

[Matthew Ballard]

lake calling elan?

[Bhavik Mehta]

Perhaps, but I haven't changed my elan for a few years and I haven't seen this happen before. In any case, thanks for the fix

[Matthew Ballard]

A few years?

[Bhavik Mehta]

I think so yeah, I've been using it since before 3.4 community was out

[Andrew Yang]

I think maybe both the vscode extension and lake triggered an install of lean at the same time and things break?
At least this is the reason for me.

[Mario Carneiro]

you should run elan self update in that case

[Bhavik Mehta]

$ elan self update
error: self-update is disabled for this build of elan
error: you should probably use your system package manager to update elan

[Bhavik Mehta]

Presumably I should do this too?

[Matthew Ballard]

What is elan --version?

[Bhavik Mehta]

2.0.0

[Matthew Ballard]

Oh ok. I'm only at 2.0.1

[Bhavik Mehta]

Oh okay, shouldn't be too bad then

[Mario Carneiro]

maybe just uninstall the version you got from the system package manager and install using the shell script

[Mario Carneiro]

I'm on elan 3.0.0 guys

[Bhavik Mehta]

Next he'll tell us he's on Lean 5 and zulip 2

[Matthew Ballard]

I thought nix would get the most love :tear:

[Mauricio Collares]

Matthew Ballard said:

I thought nix would get the most love :tear:

Elan 3.0.0 has been on Nixpkgs for more than a month now!

[Jireh Loreaux]

Interestingly enough, just yesterday I updated my elan from 1.4.2 to 3.0.0.

[Bhavik Mehta]

I managed to land in this state again, by again doing git pull on master, then lake exe cache get fails with error

error: toolchain 'leanprover/lean4:v4.3.0-rc2' does not have the binary `/Users/bmehta/.elan/toolchains/leanprover--lean4---v4.3.0-rc2/bin/lake`

My Lean 4 was working fine before the git pull on a version of master from about a week ago, and I did this all with VSCode closed, in terminal. Is there anything I should do to avoid this happening again? It would be annoying to have to take these steps every other time I update mathlib...

[Kevin Buzzard]

https://xkcd.com/1597/

[Mario Carneiro]

I don't think updating mathlib can cause this issue, but the updated version may be referencing an existing (borked) elan toolchain on your machine

[Mario Carneiro]

which is to say, the toolchain was already broken and you are only seeing the issue now because mathlib wants to use it

[Mario Carneiro]

Did this update cause the info: downloading component 'lean' and could not remove 'toolchain directory' directory messages?

[Scott Morrison]

elan toolchain uninstall $(<lean-toolchain) forces a fresh download of whatever toolchain your current project is using.

[Bhavik Mehta]

Mario Carneiro said:

Did this update cause the info: downloading component 'lean' and could not remove 'toolchain directory' directory messages?

I'm not sure - I closed the terminal I had open. I'll keep an eye on it next time I see this, thanks