How to specify Lean version for my project

Stream: lean4

[Shaonan Wu]

Dear all,

I am a new user of Lean, and I have encountered an issue. When I create a project with mathlib, the VSCode extension automatically creates the project with the latest Lean version and updates all dependencies. However, I would like to create a project with an older Lean version and its corresponding dependencies.

Could you please advise me on how to manage the Lean version of a Lean project? Additionally, I would greatly appreciate it if you could provide guidance on how to use Lean effectively.

[Kim Morrison]

I'm assuming you mean an older version of Lean 4, rather than Lean 3 (which is end-of-life).

The lean version for a project is controlled by the lean-toolchain file. e.g. you can go back to v4.5.0 by replacing the contents of lean-toolchain with leanprover/lean4:v4.5.0.

If your project has dependencies, in your lakefile.lean you will need to specify appropriate tags/branches/commits of the dependencies which are compatible with the Lean version you want to use.

[Kim Morrison]

If you tell us which Lean version you want (and why?) we can give more detailed help.

[Shaonan Wu]

Scott Morrison said:

If you tell us which Lean version you want (and why?) we can give more detailed help.

Thank you. I want to use lean4 : v4.3.0 rc 2 and mathlib4 to start a project.

[Kim Morrison]

Okay, you're in luck: there is a v4.3.0-rc2 tag for Mathlib. So just change lean-toolchain as above, and then in your lakefile you should have a line:

require mathlib from git "https://github.com/leanprover-community/mathlib4" @ "v4.3.0-rc2"

May I ask why you want to use such an old version?

[Shaonan Wu]

Scott Morrison said:

Okay, you're in luck: there is a v4.3.0-rc2 tag for Mathlib. So just change lean-toolchain as above, and then in your lakefile you should have a line:

require mathlib from git "https://github.com/leanprover-community/mathlib4" @ "v4.3.0-rc2"

May I ask why you want to use such an old version?

Thank you for your reply!
I am using Leandojo to trace my custom repository, but it is not working and returns the error message 'subprocess error.CalledProcessError: Command 'lake env lean --threads 24 --run ExtractData.lean' returned a non-zero exit status 1.' I have also tried an older version of Leandojo, but it did not resolve the issue. I suspect that the problem may be related to the Lean 4 version. I noticed that the official example for tracing Lean 4 using Leandojo is v4.3.0-rc2, so I would like to try that version.
The repo is a simple custom repository with only one Lean file, which can be built successfully on my local machine.

[Kim Morrison]

@Shaonan Wu, I'm not sure of the current maintenance state of LeanDojo. You might also try the export_infotree command in https://github.com/semorrison/lean-training-data. It hasn't been maintained recently, either, but at least you can complain to me if you find it is not working with the latest versions.

It does not give output at all isomorphic to LeanDojo's but it is similar.

[Shaonan Wu]

Thank you. I will try it later. The Lean community is so nice for newcomers.

---- Replied Message ----
| From | Zulip notifications<noreply@zulip.com> |
| Date | 03/06/2024 17:09 |
| To | Shaonan Wu<eureka_wu_123@163.com> |
| Cc | |
| Subject | #lean4 > How to specify Lean version for my project |

Scott Morrison: @Shaonan Wu, I'm not sure of the current maintenance state of LeanDojo. You might also try the export_infotree command in https://github.com/semorrison/lean-training-data. It hasn't been maintained recently, either, but at least you can complain to me if you find it is not working with the latest versions.

It does not give output at all isomorphic to LeanDojo's but it is similar.

[Shaonan Wu]

Thank you again! I have resolved this question by downgrading my Lean version, and now I am kind of curious about how to determine if there is a mathlib version compatible with my current Lean version.

[Kim Morrison]

if you want to use v4.X.0, look for a v4.X.0 tag on the mathlib4 repo