Ask for a guide for switching versions

Stream: new members

[Nick_adfor]

Today, to change the version of Lean to an old one, I ended up damaging the new version.

Lean still doesn't have a simple installation package. Is there a guide for switching versions?

I've found some steps:
Change the active toolchain, change the order of environment variables, change elan……(I cannot remember them all. Maybe if more people answer this question, we can have a doc.)

I probably spent too much time on multiple "lake build". And it seems that lake build is completely unnecessary when switching versions. (Yet I don't know that.)

[Ruben Van de Velde]

In your project, you change the version in the lean-toolchain file, and lake will use that version

[Ruben Van de Velde]

If you depend on other libraries, you might need to update them to match the new version, but otherwise that's all there is to it

[Nick_adfor]

In fact I need a easy way to change my Mathlib version. I have downloaded two others' packages. One is 4.18.0-rc1, the other is 4.16.0. I have not checked the compatibility of the two version. Maybe the two packages can run both on 4.18.0-rc1 and 4.16.0, but still I want to find a easy way to change the Mathlib version. Lake build needs long time and I have no that patience to wait long every time l change the version.

Lean-toolchain might be the only containing the version information. But lean-toolchains are everywhere (in plausible, in Qq, etc.) Is there a easy way to change them all? Can I just use two dependent folder containing two different version, so that if I open one of the folder, the Mathlib version changes to the corresponding?

[Nick_adfor]

Ruben Van de Velde said:

If you depend on other libraries, you might need to update them to match the new version, but otherwise that's all there is to it

Do you have any experience in version change?

[Kevin Buzzard]

In FLT (if I understand correctly) we offer tagged versions of the code base which run on each stable version of lean. Are you lucky enough to be in this situation?

[Nick_adfor]

Kevin Buzzard said:

In FLT (if I understand correctly) we offer tagged versions of the code base which run on each stable version of lean. Are you lucky enough to be in this situation?

Thank you professor! I can import two versions of FLT work to get two different version folder : )

[Jon Eugster]

I think it's useful to clear some terminology. Each Lean project (i.e. separate folders on disk) has it's own Lean version (defined in lean-toolchain) and a list of packages including their versions (defined in the lakefile.lean or lakefile.toml and then fixed in lake-manifest.lean). When you change the lean-toolchain of a project, you must ensure that the package versions are also compatible. In a lakefile.lean you can have a string like require "leanprover-community" / "mathlib" @ "v4.17.0" to specify a specific version. (in .toml it's done by adding a field rev = "v4.17.0" to the corresponding [[require]])

Normally, I personally recommend the following setup for a package that follows stable releases of Lean and automatically finds the correct packages. (as Kevin mentioned, that requires all dependencies to define these version tags).

If you do have further problems, you could share the require statements written in your lakefile.lean (or .toml). That would help ensuring your project is set up the best way possible.