How to downgrade Lean 4 to Lean 3?

Stream: general

[ramon jales]

I use Manjaro Linux and currently have Lean 4 installed on my machine. How could I install Lean 3?

[Adam Topaz]

If you have elan, then it should be automatic.

[Adam Topaz]

Assuming you are using the standard workflow

[ramon jales]

automatic? Should I execute some command?

[Adam Topaz]

elan automatically switches to the version of lean in a given lean project. If you clone mathlib3 and run lean —version in that folder, you will get 3.?.?…. This assumes you set up lean per the official instructions.

[Adam Topaz]

You can also read elans documentation which will tell you how to set a default lean version globally or in individual folders.

[ramon jales]

I modified the lean-toolchain file and everything worked fine. I didn't know that elan did things automatically for me. Thank you very much.

[ramon jales]

Everthing is working, but... but this warning is appearing on vscode:

You are running Lean in a directory without a leanpkg.toml file, this is NOT
supported.  Please open the directory containing the leanpkg.toml file
instead (using "File / Open Folder...").

[ramon jales]

Do you know what its?

[Scott Morrison]

Every project using Lean 3 should have a leanpkg.toml file (just like every project using Lean 4 should have a lakefile.lean).

[Scott Morrison]

You can find the old documentation at https://leanprover-community.github.io/lean3/

[Scott Morrison]

But really you should just not be using Lean 3 anymore. It is end-of-life.

[ramon jales]

it's just for a paper that a teacher assigned.