How to update lake?

Stream: new members

[Adomas Baliuka]

I've been updating Lean and Mathlib for a custom project every once in a while (at least 20 times total now) and it has never worked the first time. Every time there's a different error that needs fixing.

What's the correct process for updating? So-far I've been doing:

• rm -rf .lake
• lake update Mathlib -- will fail
• <manually copy toolchain file from mathlib folder to my project>
• rm -rf .lake
• lake update Mathlib

(In previous versions, lake update without Mathlib never worked and I've seen people here saying one should never use it. Is that still so? It's really unfortunate...)

This time, I'm getting (uppon changing the toolchain file and running lake)

error: toolchain 'leanprover/lean4:v4.10.0' is not installed

I tried using elan to update as described here but it didn't help. (tried elan self update and elan update) What should I do? Reinstall lean? Is this information written up somewhere?

[Yaël Dillies]

What I do, and it has never failed so far, is to copy-paste the lean-toolchain file from mathlib to my project, then only run lake update

[Adomas Baliuka]

Yaël Dillies said:

What I do, and it has never failed so far, is to copy-paste the lean-toolchain file from mathlib to my project, then only run lake update

You mean go on GitHub and copy the file manually from there?

[Yaël Dillies]

Well in fact I have a script to do that for me, but basically yes :grinning:

[Adomas Baliuka]

I really wonder why it's not possible to have lake update just work...
In any case, doing what you suggested, I unfortunately get the same error: toolchain not installed
(I now also did elan toolchain install v4.10.0 in addition, but lake update Mathlib still gives the same error)

[Yaël Dillies]

Are you on Windows?

[Adomas Baliuka]

Ubuntu.

I now looked at

> elan show                                                                                                                        main [abfe43f] deleted modified untracked
installed toolchains
--------------------

nightly
leanprover/lean4:4.10.0
leanprover/lean4:nightly-2023-07-12
leanprover/lean4:nightly-2023-08-23
leanprover/lean4:stable (default)
leanprover/lean4:v4.10.0-rc1
leanprover/lean4:v4.10.0-rc2
leanprover/lean4:v4.5.0
leanprover/lean4:v4.6.0-rc1
leanprover/lean4:v4.7.0-rc2
leanprover/lean4:v4.8.0-rc1
leanprover/lean4:v4.8.0-rc2
leanprover/lean4:v4.9.0-rc3
v4.10.0

active toolchain
----------------

leanprover/lean4:v4.10.0 (overridden by '/mnt/data/git/LEAN/formal-qkd/lean-toolchain')
(toolchain not installed)

which really confuses me. The toolchain that's active is "not installed" but also in the list above (actually twice with different names?)...

[Adomas Baliuka]

Yaël Dillies said:

What I do, and it has never failed so far, is to copy-paste the lean-toolchain file from mathlib to my project, then only run lake update

Just to make sure, you run literally lake update, not lake update Mathlib or something like that? Or does one need the lake -R -Kenv=dev update from your script?

[Sebastian Ullrich]

This shouldn't happen but try elan toolchain install leanprover/lean4:v4.10.0

[Adomas Baliuka]

> elan toolchain install leanprover/lean4:v4.10.0

  leanprover/lean4:v4.10.0 unchanged - (toolchain not installed)

[Yaël Dillies]

I run lake -R -Kenv=dev update because of a specificity of my project using doc-gen but only in CI

[Ruben Van de Velde]

Is it weird that there's three different lines that contain 4.10.0 in the elan show output?

[Adomas Baliuka]

It's definitely weird to me...

[Yaël Dillies]

Well, each release candidate is a different toolchain, right?

[Adomas Baliuka]

They have literally the same version. These are not release candidates, right? leanprover/lean4:4.10.0 and v4.10.0 are "different" installed things, leanprover/lean4:v4.10.0 is "not installed" (despite being named identically to something installed)

[Yaël Dillies]

Oh I see

[Ruben Van de Velde]

I might move all of ~/.elan out of the way and see what happens

[Adomas Baliuka]

By "move out of the way" you mean delete it?

[Ruben Van de Velde]

Either that or mv ~/.elan ~/old-.elan in case you want to look at what happened in there afterward

[Adomas Baliuka]

I guess after renaming it I have to reinstall elan? It's no longer there.

So I "carefully look at what it downloads and then" run curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh ?

[Ruben Van de Velde]

Oh, I forgot that elan itself also lives there. Yeah, try that

[Adomas Baliuka]

Ok, that seems to have worked. I guess my new workflow for "updating dependencies for my project is"

• copy-paste toolchain file from Mathlib (curl -L https://raw.githubusercontent.com/leanprover-community/mathlib4/master/lean-toolchain -o lean-toolchain)
• rm -rf .lake
• lake -R update
• <if the above fails>: delete or rename ~/.elan
• reinstall elan ("carefully look at what it downloads and then" run curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh)
• try from the top

[Sebastian Ullrich]

This duplication of toolchains, which presumably caused the final error, will be solved in the next version of elan

[Adomas Baliuka]

Thanks a lot for the help to everyone!!

So I guess you already know the issue. Does anyone nevertheless want to debug this and is interested in the contents of my .elan folder which I renamed? Otherwise I'm deleting it.