You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
chore: bump suggested Lean version for making new projects (#729)
The recent Lean releases have added useful functionality to the `lake
new ... math` template, so suggest to use a newer version.
Note that the version only affects the initial project generation and
not its dependencies: `lake` will automatically install the latest
Mathlib as a dependency.
Copy file name to clipboardExpand all lines: templates/install/project.md
+1-1Lines changed: 1 addition & 1 deletion
Display the source diff
Display the rich diff
Original file line number
Diff line number
Diff line change
@@ -75,7 +75,7 @@ We will now create a new project depending on mathlib. The following
75
75
commands should be typed in a terminal.
76
76
77
77
* Go to a folder where you want to create a project in a subfolder
78
-
`my_project`, and type `lake +leanprover/lean4:nightly-2024-04-24 new my_project math`. Do not worry about the date in the previous command, it ensures you will use a sufficiently recent version of `lake` but has no impact on the version of `lean` your project will use. If you get an
78
+
`my_project`, and type `lake +v4.24.0 new my_project math`. Do not worry about the version in the previous command, it ensures you will use a sufficiently recent version of `lake` but has no impact on the version of `lean` your project will use. If you get an
79
79
error message saying `lake` is an unknown command and
80
80
you have not logged in since you installed Lean, then
81
81
you may need to first type `source ~/.profile` or `source ~/.bash_profile`.
0 commit comments