installing lean 4, keeping lean 3

Stream: lean4

[Kayla Thomas]

Is there anything special I need to do to install lean 4 and keep access to my current install of lean 3? Do I just follow the basic setup here https://leanprover.github.io/lean4/doc/setup.html ?

[Damiano Testa]

For me, it just worked. Also, if you use VSCode, the two extensions almost never get confused.

[Damiano Testa]

Basically, simply do not remove Lean 3 when you install Lean 4 and you should be fine!

[Kayla Thomas]

Great! Thank you!

[Kayla Thomas]

I'm getting an error trying to set up a new project:

$ elan default leanprover/lean4:stable
info: syncing channel updates for 'stable'
info: latest update on stable, lean version v4.0.0-m5
info: downloading component 'lean'
134.4 MiB / 134.4 MiB (100 %)   2.0 MiB/s ETA:   0 s
info: installing component 'lean'
info: default toolchain set to 'leanprover/lean4:stable'

  leanprover/lean4:stable installed - Lean (version 4.0.0, commit 7dbfaf9b7519, Release)


$ elan run leanprover/lean4:nightly-2023-02-04 lake new fol math
error: toolchain 'leanprover/lean4:nightly-2023-02-04' is not installed

$ elan default leanprover/lean4:nightly
info: syncing channel updates for 'nightly'
info: latest update on nightly, lean version nightly-2023-05-22
info: downloading component 'lean'
180.4 MiB / 180.4 MiB (100 %)   3.6 MiB/s ETA:   0 s
info: installing component 'lean'
info: default toolchain set to 'leanprover/lean4:nightly'

  leanprover/lean4:nightly installed - Lean (version 4.0.0-nightly-2023-05-22, commit 8d4dd2311ccf, Release)


$ elan run leanprover/lean4:nightly-2023-02-04 lake new fol math
error: toolchain 'leanprover/lean4:nightly-2023-02-04' is not installed

[Alex J. Best]

Why not use 05-22 it looks like that installed fine?

[Kayla Thomas]

ahh, right. I was taking the version directly from the documentation.

[Kayla Thomas]

:woman_facepalming:

[Kayla Thomas]

hmm

$ elan run leanprover/lean4:nightly-2023-05-22 lake new fol math
error: toolchain 'leanprover/lean4:nightly-2023-05-22' is not installed

[Kayla Thomas]

ok, this works

 elan run leanprover/lean4:nightly lake new fol math
info: Downloading lean-toolchain

[Kayla Thomas]

Thank you.

[Kayla Thomas]

odd

$ cat fol/lean-toolchain
leanprover/lean4:nightly-2023-05-16

[Mario Carneiro]

that's because lake new myproj math will use the version of lean used by the latest version of mathlib

[Kayla Thomas]

So I could have run just lake new fol math without the elan run leanprover/lean4:nightly?

[Kayla Thomas]

Should the first line here be changed? https://github.com/leanprover-community/mathlib4#in-a-new-project

[Mario Carneiro]

Kayla Thomas said:

So I could have run just lake new fol math without the elan run leanprover/lean4:nightly?

I've actually never tried to run lake like that. But it is reasonable to do so, using lake new fol math on its own is risky since it will use whatever version of lake you have installed locally, which means the generated sample lakefile might not be valid for the latest version of lake

[Kayla Thomas]

So elan run leanprover/lean4:nightly lake new fol math was the right command?

[Mario Carneiro]

it's not a very big deal since lake changes that affect the lakefile are rare, but the @[defaultTarget] attribute rename sometimes gets people who e.g. use the last stable milestone release

[Mario Carneiro]

yes

[Kayla Thomas]

Should the doc be changed to that?

[Mario Carneiro]

the use of an explicit date in the readme is definitely suboptimal, that will very obviously get out of date

[Sebastian Ullrich]

:nightly is extremely bad with the current elan, it is essentially a random version depending on the local elan state

[Mario Carneiro]

oh, I thought that would download the latest

[Sebastian Ullrich]

One of the things my elan RFC is supposed to fix

[Mario Carneiro]

Is there any version of the command that doesn't depend on local state? I get why we don't want this but I don't see any options to avoid it other than defensively calling elan toolchain install all the time

[Sebastian Ullrich]

I think this is a non-issue, we're not expecting any Lake breaking changes any time soon. This way the readme instructions at least are deterministic

[Kayla Thomas]

The date in the readme instructions didn't seem to work for me.

[Kayla Thomas]

I might have been doing some wrong though?

[Sebastian Ullrich]

Oh I see now, I will have to check that again tomorrow

[Sebastian Ullrich]

Does lake +leanprover/lean4:nightly-2023-05-22 new fol math work?

[Kayla Thomas]

(deleted)

[Kayla Thomas]

pthomas@PC:~/Desktop/github/tmp$ lake +leanprover/lean4:nightly-2023-05-22 new fol math
info: downloading component 'lean'
 88.2 MiB / 180.4 MiB ( 49 %)   2.5 MiB/s ETA:  37 s   91.5 MiB / 180.4 MiB ( 51 %)  180.4 MiB / 180.4 MiB (100 %)   2.1 MiB/s ETA:   0 s
info: installing component 'lean'
info: Downloading lean-toolchain

[Kayla Thomas]

Did it reinstall lean?

[Mario Carneiro]

no, it installed (that version of) lean

[Mario Carneiro]

elan maintains many versions of lean simultaneously, you can choose between any of them and if you don't have that particular nightly elan will get it for you

[Mario Carneiro]

if you run the same command a second time it will not download lean again

[Kayla Thomas]

I see. How does Visual Code decide which one to use?

[Mario Carneiro]

it uses the lean-toolchain file in the project root

[Kayla Thomas]

Ah. Ok.

[Mario Carneiro]

if you want to upgrade the version of lean used to compile your project you should change that file

[Kayla Thomas]

Ok.

[Mario Carneiro]

Q: Do we have a command to update that file to the latest nightly? I know about lake update for updating dependencies but for updating lean itself I just do it manually right now

[Sebastian Ullrich]

I don't think we do