Zulip Chat Archive

Stream: general

Topic: How to update lean3?

Thorsten Altenkirch (Nov 01 2022 at 13:46):

How do I update my lean 3 installation? I guess I need to use elan?

Julian Berman (Nov 01 2022 at 14:03):

That's the most common way to do so for users yeah -- but if you're using it you don't need to physically do anything typically if/once it's installed. If you're in a directory with a leanpkg.toml file, that declares what version of Lean is supposed to be used, and elan will automatically use that version (whether it's newer or older or whatever)

Julian Berman (Nov 01 2022 at 14:03):

(Or in Lean 4 it's a similar newer version of that file)

Kevin Buzzard (Nov 01 2022 at 15:59):

If you're working inside a lean 3 project and using leanproject to manage it then it should be as simple as leanproject up.

Eric Wieser (Nov 01 2022 at 21:41):

It's pretty rare that you want to manually upgrade lean3; usually you just want to upgrade mathlib and take the lean version it asks for

Thorsten Altenkirch (Nov 03 2022 at 10:48):

Thank you. I am currently not using mathlib to simplify the installation for the students. I need to update because I have incompatible versions on my laptop and my desktop. I am still not sure how to do this.

Mario Carneiro (Nov 03 2022 at 10:57):

What Kevin said - if you have a lean project not depending on mathlib then leanproject up should do the trick

Kevin Buzzard (Nov 03 2022 at 23:04):

If you do not even have leanproject installed then you can manually edit the leanpkg.toml file in your project I guess...

Thorsten Altenkirch (Nov 07 2022 at 11:37):

I have actually a globally installed lean project. But I get:

(base) psztxa@IMAC-DGKYNHM5JV3X L11 % leanproject up
info: downloading component 'lean'
error: binary package was not provided for 'darwin'
Command '['leanpkg', 'upgrade']' returned non-zero exit status 1.