update lean3

Stream: general

[Stavros]

my current lean3 version is old (3, (19, 0)) and i want to update it. i still want to keep lean3, not switch to lean4.

any suggestions how to go about this update? i'm not using mathlib.

the motivation for the update is that the blue squiggly lines (https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/blue.20squiggly.20lines) have come back, and i can no longer get rid of them by downgrading to an earlier VScode lean3 extension...

thank you,
Stavros Tripakis

[Patrick Massot]

Edit leanpkg.toml at the root of your project.

[Patrick Massot]

The lean version is easy to spot there.

[Patrick Massot]

See https://github.com/leanprover-community/lean/releases for existing versions

[Stavros]

i'm sorry but i am confused. first, both leanpkg.toml files in my installation as well as in the latest version 3.51.1 that i downloaded from the above website show the same version:

version = "0.1"

second, what should i edit the file to, and how does this result in updating lean3?

[Patrick Massot]

The leanpkg.toml file in your project should look like

[package]
name = "stavros_project"
version = "0.1"
lean_version = "leanprover-community/lean:3.51.1"
path = "src"

[Stavros]

what if i don't have a "project"? (not sure i do)

[Patrick Massot]

You never need to download a version of Lean if you use elan (which you do if you followed standard installation instructions). I mention the page listing versions only so that you get that "3.51.1" number.

[Patrick Massot]

You should really have a project. We are dangerously close to territories where nobody will be able to help you.

[Bhavik Mehta]

Stavros said:

what if i don't have a "project"? (not sure i do)

Can you show us your leanpkg.toml file?

[Patrick Massot]

There is no such file to show if he has no project

[Patrick Massot]

Stavros, you can try elan default leanprover-community/lean:3.51.1. But really this is uncharted territory.

[Bhavik Mehta]

I thought so too, but he mentions "both leanpkg.toml files", which seems to suggest there's at least one

[Stavros]

$ cat ./Users/Stavros/.elan/toolchains/leanprover-community-lean-3.10.0/lib/lean/leanpkg/leanpkg.toml
[package]
name = "leanpkg"
version = "0.1"

$ cat ./Users/Stavros/.elan/toolchains/leanprover-community-lean-3.39.0/lib/lean/leanpkg/leanpkg.toml
[package]
name = "leanpkg"
version = "0.1"

$ cat ./Users/Stavros/.elan/toolchains/leanprover-community-lean-3.5.1/lib/lean/leanpkg/leanpkg.toml
[package]
name = "leanpkg"
version = "0.1"

$ cat ./Users/Stavros/.elan/toolchains/leanprover-community-lean-3.9.0/lib/lean/leanpkg/leanpkg.toml
[package]
name = "leanpkg"
version = "0.1"

$ cat ./Users/Stavros/.elan/toolchains/stable/lib/lean/leanpkg/leanpkg.toml
[package]
name = "leanpkg"
version = "0.1"

[Stavros]

=>

1. i have no idea what's going on
2. i don't even know where does VScode run lean3 from

[Scott Morrison]

You are showing us leanpkg.toml files inside the toolchains.

We need to know about the leanpkg.toml file in where ever you keep your lean files.

[Scott Morrison]

But echoing @Patrick Massot, I'd strongly encourage you to just transition to Lean 4. Moving between different ancient versions of Lean 3 is not really helping anyone.

[Stavros]

Scott Morrison said:

You are showing us leanpkg.toml files inside the toolchains.

We need to know about the leanpkg.toml file in where ever you keep your lean files.

there is none. i'm not using projects. and i feel i should have the right (?) to use lean without projects.

[Stavros]

Scott Morrison said:

But echoing Patrick Massot, I'd strongly encourage you to just transition to Lean 4. Moving between different ancient versions of Lean 3 is not really helping anyone.

i got the message. still, lean3 is helping my 2nd year undergraduate students, who would like to have a confirmation like 'goals accomplished' to feel confident (and good!) about having finished their proof.

[Stavros]

since updating without projects seems to be uncharted territory, is there perhaps a way to uninstall lean3? (so as to reinstall it)

[Scott Morrison]

Assuming that you've only been using Lean via elan (i.e. per the recommended instructions), then simply deleting your ~/.elan directory and reinstalling elan should be sufficient.

[Scott Morrison]

For both Lean 3 and Lean 4, ideally humans are never installing or uninstalling Lean directly: toolchains are handled by elan.

[Stavros]

Patrick's solution did the trick:

elan default leanprover-community/lean:3.51.1

and i get (almost) no squiggly blue lines anymore, so i'm set for now!

thank you very much @Patrick Massot and all!

[Jireh Loreaux]

So glad you were able to make it work! Sorry you experienced headaches.