From d91448ac7e56302cb5dd5b1386a79b14f647c26f Mon Sep 17 00:00:00 2001 From: Jon Eugster Date: Fri, 2 Aug 2024 13:28:44 +0200 Subject: [PATCH 01/10] doc: add tips about lake usage --- templates/install/project.md | 11 ++- templates/install/tricks.md | 143 +++++++++++++++++++++++++++++++++++ 2 files changed, 153 insertions(+), 1 deletion(-) create mode 100644 templates/install/tricks.md diff --git a/templates/install/project.md b/templates/install/project.md index 1de220c62..8cb99fb0d 100644 --- a/templates/install/project.md +++ b/templates/install/project.md @@ -19,7 +19,7 @@ a portmanteau of `lean` and `make`). This page describes the basic use of this tool, and should be sufficient for everyday use. If this is not enough for your purposes, you can read the -full [lake documentation](https://github.com/leanprover/lake/blob/master/README.md). +full [lake documentation](https://github.com/leanprover/lean4/tree/master/src/lake#readme). ## Working on an existing project @@ -123,6 +123,15 @@ More information about Lake can be found [here](https://github.com/leanprover/le See [How to contribute to mathlib](https://leanprover-community.github.io/contribute/index.html). +## Further Tips and Tricks + +If you are interested in a custom setup, +you can read [Tips and Tricks](tricks.html). + +This contains some notes about +* Setting up a shared, *global/centralised* mathlib installation. +* Automatically follow stable versions of dependencies. + ## Troubleshooting * Some Windows users have reported an error like this when running `lake exe cache get`: diff --git a/templates/install/tricks.md b/templates/install/tricks.md new file mode 100644 index 000000000..8d98a7a55 --- /dev/null +++ b/templates/install/tricks.md @@ -0,0 +1,143 @@ +# Tips and Tricks about Lean Projects + +These tips and tricks about managing Lean projects should be considered workarounds or common practice. Some care is adviced when trying these non-standard setups. + +*Note:* Things here might change as `lake` is being developed, as features described here are not necessarily officially supported by `lake`. This file has been written for Lean `v4.10.0`. If in doubt, ask for help on [Zulip](https://leanprover.zulipchat.com). + +## Shared Mathlib + +If you start many projects which all use the latest stable version of mathlib, e.g. because you have little +disk space available, it might be worth setting them up using one centralised mathlib instead of +letting every project download there own clone. + +Here is a guide on best practise on how to achieve that. + +1) First, clone the version of mathlib somewhere on your computer: + ```bash + git clone --branch v4.10.0 git@github.com:leanprover-community/mathlib4.git + ``` + Note that `v4.10.0` is the tag of the latest release, you can look at [mathlib's tags](https://github.com/leanprover-community/mathlib4/tags) to find out which is the most recent release version. + + (If you don't have git setup correctly using an SSH key, you might want to use `git clone --branch v4.10.0 https://github.com/leanprover-community/mathlib4.git` instead.) +2) Go inside your mathlib and download cache: + ```bash + cd mathlib + lake exe cache get + ``` +3) If you ever want to **update** your global mathlib, come back to the mathlib directory and call + ```bash + git checkout v4.11.0 + lake exe cache get + ``` + with the [version](https://github.com/leanprover-community/mathlib4/tags) you'd like to update to. +4) Now if you don't already have a Lean project, create it + ```bash + lake new MyProject math.lean + cd MyProject + ``` +5) In the project `MyProject` you need to modify two things: + + * In `lakefile.lean`, replace the line `require "leanprover-community" / "mathlib"` with + ``` + require mathlib from ".." / "relative" / "path" / "to" / "mathlib4" + ``` + * Now inside `MyProject` you need to clean up lake: + ```bash + rm -rf .lake # because `lake clean` does not remove `.lake/packages/mathlib` which might have been downloaded by `lake new`. + lake clean + ```` + *(note: it looks like a bug that with a simple `lake clean`, there might still be a folder `.lake/packages/mathlib` floating around from before you changed the `lakefile.lean`. However, deleting `.lake/` is a reasonably save action as it only contains build artifacts that are fully recovered by the next `lake` call.)* + * Your project should be ready and when you add `import Mathlib` in a file and click "Restart File" in VSCode, it should be reasonably quick without rebuilding mathlib. +6) When you updated your global mathlib it might be enough to call + ``` + lake update -R mathlib + ``` + which would in theory update everything automatically. + However, if there are breaking changes to the `lakefile` parsing, you might need to + * edit `lean-toolchain` to be the same as your global mathlib. + * make sure `lakefile.lean` parses without error in the new version. + * try `lake update -R mathlib` again. + +## Following stable versions of packages + +If your Lean project only wants to following the stable releases of packages (i.e. `v4.10.0`, `v4.11.0`, etc.) you could do the following trick: + +In your `lakefile.lean`, add + +```lean +def leanVersion : String := s!"v{Lean.versionString}" +``` + +and then suffix all `require`s with `@ leanVersion`: + +``` +require "leanprover-community" / "mathlib" @ leanVersion +``` + +*Note:* for this to work, the corresponding repository needs to have a tag (or branch) for the corresponding Lean version, see e.g. [the mathlib tags](https://github.com/leanprover-community/mathlib4/tags). + +If you specified the version for all packages in your project, you can then update your project simply by + +* Edit `lean-toolchain` to have the new toolchain `leanprover/lean4:v4.11.0`. +* Call `lake update -R`. + + *(note: a blank `lake update -R` is only reasonable if **all** required packages in your project have a version specified with `@`)* + + + +## Using local dev version of a dependency + +In rare circumstances you might want to use a local copy of a dependency (e.g. `mathlib`) when developing, i.e. to test changes immediately. + +You could do this by using a local dependency while developing +``` +require mathlib from ".." / "mathlib4" +``` +and then change it back to the remote dependency before pushing changes: +``` +require "leanprover-community" / "mathlib" +``` + +However, if you want to do this frequently, here might be a better setup. With the suggested modifications to the `lakefile.lean` below, you get the following behaviour: + +* To use the local dependency, call + ``` + lake update -R -Kmathlib.useDev mathlib + ``` +* To switch back to the remote dependency, call + ``` + lake update -R mathlib + ``` +* Anybody `require`-ing your package in there own project will automatically get the remote version of the packages. + +(*Note:* make sure to read the chapter above about specifying versions when using `lake update`). + +For this you need to replace `require "leanprover-community" / "mathlib"` in your `lakefile.lean` with the following instructions: + +```lean +/-- The local dependency. Using a relative path. -/ +def LocalMathlib : Dependency := { + name := `mathlib + src? := some <| .path (".." / "mathlib4") + scope := "" + version? := none + opts := {} +} + +/-- The remote dependency. Note that "master" is the version you want. -/ +def RemoteMathlib : Dependency := { + name := `mathlib + src? := some <| .git "https://github.com/leanprover-community/mathlib4.git" "master" none + scope := "leanprover-community" + version? := none + opts := {} +} + +/- Choose `mathlib` dependency locally if `-Kmathlib.useDev` is provided. -/ +open Lean in +#eval (do + let depName := if get_config? mathlib.useDev |>.isSome then + ``LocalMathlib else ``RemoteMathlib + modifyEnv (fun env => Lake.packageDepAttr.ext.addEntry env depName) + : Elab.Command.CommandElabM Unit) +``` \ No newline at end of file From 4eee3238c64a87de94632caa785c7adfe389b239 Mon Sep 17 00:00:00 2001 From: Jon Eugster Date: Fri, 2 Aug 2024 13:30:50 +0200 Subject: [PATCH 02/10] update lake doc link --- templates/install/project.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/templates/install/project.md b/templates/install/project.md index 8cb99fb0d..8ab9a5729 100644 --- a/templates/install/project.md +++ b/templates/install/project.md @@ -19,7 +19,7 @@ a portmanteau of `lean` and `make`). This page describes the basic use of this tool, and should be sufficient for everyday use. If this is not enough for your purposes, you can read the -full [lake documentation](https://github.com/leanprover/lean4/tree/master/src/lake#readme). +full [lake documentation](https://github.com/leanprover/lean4/blob/master/src/lake/README.md). ## Working on an existing project From 5086492966d650d8620eecb5ae6e5f5504d40b4c Mon Sep 17 00:00:00 2001 From: Jon Eugster Date: Fri, 2 Aug 2024 13:32:09 +0200 Subject: [PATCH 03/10] update text --- templates/install/project.md | 1 + 1 file changed, 1 insertion(+) diff --git a/templates/install/project.md b/templates/install/project.md index 8ab9a5729..779e012e9 100644 --- a/templates/install/project.md +++ b/templates/install/project.md @@ -131,6 +131,7 @@ you can read [Tips and Tricks](tricks.html). This contains some notes about * Setting up a shared, *global/centralised* mathlib installation. * Automatically follow stable versions of dependencies. +* Using build options to switch to local package versions. ## Troubleshooting From c22f5d4bf395a63a0ed778e1987b88b10dd20fe5 Mon Sep 17 00:00:00 2001 From: Jon Eugster Date: Fri, 2 Aug 2024 13:34:16 +0200 Subject: [PATCH 04/10] add comment --- templates/install/tricks.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/templates/install/tricks.md b/templates/install/tricks.md index 8d98a7a55..1460fb4b4 100644 --- a/templates/install/tricks.md +++ b/templates/install/tricks.md @@ -44,7 +44,7 @@ Here is a guide on best practise on how to achieve that. * Now inside `MyProject` you need to clean up lake: ```bash rm -rf .lake # because `lake clean` does not remove `.lake/packages/mathlib` which might have been downloaded by `lake new`. - lake clean + lake clean # or potentially `lake update -R mathlib` instead ```` *(note: it looks like a bug that with a simple `lake clean`, there might still be a folder `.lake/packages/mathlib` floating around from before you changed the `lakefile.lean`. However, deleting `.lake/` is a reasonably save action as it only contains build artifacts that are fully recovered by the next `lake` call.)* * Your project should be ready and when you add `import Mathlib` in a file and click "Restart File" in VSCode, it should be reasonably quick without rebuilding mathlib. From 04f87feb493c9bb37d90cb612314305ca95ef445 Mon Sep 17 00:00:00 2001 From: Jon Eugster Date: Fri, 2 Aug 2024 13:45:31 +0200 Subject: [PATCH 05/10] use word dependency instead of package --- templates/install/tricks.md | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/templates/install/tricks.md b/templates/install/tricks.md index 1460fb4b4..36be68a5e 100644 --- a/templates/install/tricks.md +++ b/templates/install/tricks.md @@ -58,9 +58,9 @@ Here is a guide on best practise on how to achieve that. * make sure `lakefile.lean` parses without error in the new version. * try `lake update -R mathlib` again. -## Following stable versions of packages +## Following stable versions of dependencies -If your Lean project only wants to following the stable releases of packages (i.e. `v4.10.0`, `v4.11.0`, etc.) you could do the following trick: +If your Lean project only wants to following the stable releases of dependencies (i.e. `v4.10.0`, `v4.11.0`, etc.) you could do the following trick: In your `lakefile.lean`, add @@ -76,12 +76,12 @@ require "leanprover-community" / "mathlib" @ leanVersion *Note:* for this to work, the corresponding repository needs to have a tag (or branch) for the corresponding Lean version, see e.g. [the mathlib tags](https://github.com/leanprover-community/mathlib4/tags). -If you specified the version for all packages in your project, you can then update your project simply by +If you specified the version for all dependencies in your project, you can then update your project simply by * Edit `lean-toolchain` to have the new toolchain `leanprover/lean4:v4.11.0`. * Call `lake update -R`. - *(note: a blank `lake update -R` is only reasonable if **all** required packages in your project have a version specified with `@`)* + *(note: a blank `lake update -R` is only reasonable if **all** required dependencies in your project have a version specified with `@`)* @@ -108,7 +108,7 @@ However, if you want to do this frequently, here might be a better setup. With t ``` lake update -R mathlib ``` -* Anybody `require`-ing your package in there own project will automatically get the remote version of the packages. +* Anybody `require`-ing your project as dependency in there own project will automatically get the remote version of the dependencies. (*Note:* make sure to read the chapter above about specifying versions when using `lake update`). From 0af416f49c377ac7eb8c615d0bb3c77cef71fbcd Mon Sep 17 00:00:00 2001 From: Jon Eugster Date: Fri, 2 Aug 2024 13:54:32 +0200 Subject: [PATCH 06/10] wording --- templates/install/tricks.md | 9 +++++++-- 1 file changed, 7 insertions(+), 2 deletions(-) diff --git a/templates/install/tricks.md b/templates/install/tricks.md index 36be68a5e..e425e2a34 100644 --- a/templates/install/tricks.md +++ b/templates/install/tricks.md @@ -74,7 +74,7 @@ and then suffix all `require`s with `@ leanVersion`: require "leanprover-community" / "mathlib" @ leanVersion ``` -*Note:* for this to work, the corresponding repository needs to have a tag (or branch) for the corresponding Lean version, see e.g. [the mathlib tags](https://github.com/leanprover-community/mathlib4/tags). +*Note:* for this to work, the repository of each dependency needs to have a tag (or branch) for the Lean version you're using, e.g. look at [the mathlib tags](https://github.com/leanprover-community/mathlib4/tags). If you specified the version for all dependencies in your project, you can then update your project simply by @@ -124,9 +124,14 @@ def LocalMathlib : Dependency := { opts := {} } -/-- The remote dependency. Note that "master" is the version you want. -/ +/-- The remote dependency. Note that "master" is the tag/branch you want to clone from. -/ def RemoteMathlib : Dependency := { name := `mathlib + /-- + You can also write `src? := none` to get the package from Reservoir instead + (if `scope` is specified correctly), + or you can replace `"master"` with `none` to not specify the input branch/tag. + -/ src? := some <| .git "https://github.com/leanprover-community/mathlib4.git" "master" none scope := "leanprover-community" version? := none From b658096ad49dac1ee7e7e504a0d021070c34dccc Mon Sep 17 00:00:00 2001 From: Jon Eugster Date: Thu, 5 Sep 2024 16:48:14 +0200 Subject: [PATCH 07/10] Apply suggestions from code review Co-authored-by: grunweg --- templates/install/tricks.md | 14 +++++++------- 1 file changed, 7 insertions(+), 7 deletions(-) diff --git a/templates/install/tricks.md b/templates/install/tricks.md index e425e2a34..d6fe50b9d 100644 --- a/templates/install/tricks.md +++ b/templates/install/tricks.md @@ -8,11 +8,11 @@ These tips and tricks about managing Lean projects should be considered workarou If you start many projects which all use the latest stable version of mathlib, e.g. because you have little disk space available, it might be worth setting them up using one centralised mathlib instead of -letting every project download there own clone. +letting every project download their own clone. -Here is a guide on best practise on how to achieve that. +Here is the current best practice to achieve this. -1) First, clone the version of mathlib somewhere on your computer: +1) First, clone a version of mathlib somewhere on your computer: ```bash git clone --branch v4.10.0 git@github.com:leanprover-community/mathlib4.git ``` @@ -30,7 +30,7 @@ Here is a guide on best practise on how to achieve that. lake exe cache get ``` with the [version](https://github.com/leanprover-community/mathlib4/tags) you'd like to update to. -4) Now if you don't already have a Lean project, create it +4) If you don't already have a Lean project, create it. ```bash lake new MyProject math.lean cd MyProject @@ -45,9 +45,9 @@ Here is a guide on best practise on how to achieve that. ```bash rm -rf .lake # because `lake clean` does not remove `.lake/packages/mathlib` which might have been downloaded by `lake new`. lake clean # or potentially `lake update -R mathlib` instead - ```` - *(note: it looks like a bug that with a simple `lake clean`, there might still be a folder `.lake/packages/mathlib` floating around from before you changed the `lakefile.lean`. However, deleting `.lake/` is a reasonably save action as it only contains build artifacts that are fully recovered by the next `lake` call.)* - * Your project should be ready and when you add `import Mathlib` in a file and click "Restart File" in VSCode, it should be reasonably quick without rebuilding mathlib. + ``` + *(note: it looks like a bug that with a simple `lake clean`, there might still be a folder `.lake/packages/mathlib` floating around from before you changed the `lakefile.lean`. However, deleting `.lake/` is a reasonably safe action as it only contains build artifacts that are fully recovered by the next `lake` call.)* + * Your project should be ready: when you add `import Mathlib` in a file and click "Restart File" in VSCode, it should be reasonably quick, without rebuilding mathlib. 6) When you updated your global mathlib it might be enough to call ``` lake update -R mathlib From 30140c57d3676ead8e1cc825149a5bc7d9b14383 Mon Sep 17 00:00:00 2001 From: Jon Eugster Date: Thu, 5 Sep 2024 16:59:39 +0200 Subject: [PATCH 08/10] address suggestions --- templates/install/tricks.md | 30 ++++++++++++++++++++++-------- 1 file changed, 22 insertions(+), 8 deletions(-) diff --git a/templates/install/tricks.md b/templates/install/tricks.md index d6fe50b9d..ba7dedecf 100644 --- a/templates/install/tricks.md +++ b/templates/install/tricks.md @@ -1,14 +1,25 @@ # Tips and Tricks about Lean Projects -These tips and tricks about managing Lean projects should be considered workarounds or common practice. Some care is adviced when trying these non-standard setups. +These tips and tricks about managing Lean projects should be considered workarounds. +Some care is adviced when trying these non-standard setups. *Note:* Things here might change as `lake` is being developed, as features described here are not necessarily officially supported by `lake`. This file has been written for Lean `v4.10.0`. If in doubt, ask for help on [Zulip](https://leanprover.zulipchat.com). +*Note:* Whenever this guide talks of the `lakefile.lean` + ## Shared Mathlib -If you start many projects which all use the latest stable version of mathlib, e.g. because you have little -disk space available, it might be worth setting them up using one centralised mathlib instead of -letting every project download their own clone. +If you start many projects which all use the latest stable version of mathlib +by default each project will download its own clone. +If you, for example, have little disk space available, +it might be worth setting them up using one centralised copy of mathlib instead. + +*Note*: This means additional effort when upgrading the mathlib version, +as you need to update all your projects at once. + +*Note*: Whenever this tutorial mentions the `lakefile.lean`, you should make the mentioned +modifications to your `lakefile.toml` if you have this instead. Every Lean project +has exactly one of these two configuration files. Here is the current best practice to achieve this. @@ -18,8 +29,11 @@ Here is the current best practice to achieve this. ``` Note that `v4.10.0` is the tag of the latest release, you can look at [mathlib's tags](https://github.com/leanprover-community/mathlib4/tags) to find out which is the most recent release version. - (If you don't have git setup correctly using an SSH key, you might want to use `git clone --branch v4.10.0 https://github.com/leanprover-community/mathlib4.git` instead.) -2) Go inside your mathlib and download cache: + The above line assumes you have set up git using an SSH key. + If you have not set this up correctly, you may want to + use `git clone --branch v4.10.0 https://github.com/leanprover-community/mathlib4.git` instead. + +2) Go inside your mathlib and download the current cache: ```bash cd mathlib lake exe cache get @@ -35,8 +49,8 @@ Here is the current best practice to achieve this. lake new MyProject math.lean cd MyProject ``` -5) In the project `MyProject` you need to modify two things: - +5) In the project `MyProject` you need to modify the following things: + * Make sure `lean-toolchain` contains the string `leanprover/lean4:v4.10.0` with the same version your shared mathlib is at. * In `lakefile.lean`, replace the line `require "leanprover-community" / "mathlib"` with ``` require mathlib from ".." / "relative" / "path" / "to" / "mathlib4" From b402afcc4dff4b6caff82eb62638c8bbcf4bfaf1 Mon Sep 17 00:00:00 2001 From: Jon Eugster Date: Thu, 5 Sep 2024 17:00:48 +0200 Subject: [PATCH 09/10] fix --- templates/install/tricks.md | 2 -- 1 file changed, 2 deletions(-) diff --git a/templates/install/tricks.md b/templates/install/tricks.md index ba7dedecf..85190ba48 100644 --- a/templates/install/tricks.md +++ b/templates/install/tricks.md @@ -5,8 +5,6 @@ Some care is adviced when trying these non-standard setups. *Note:* Things here might change as `lake` is being developed, as features described here are not necessarily officially supported by `lake`. This file has been written for Lean `v4.10.0`. If in doubt, ask for help on [Zulip](https://leanprover.zulipchat.com). -*Note:* Whenever this guide talks of the `lakefile.lean` - ## Shared Mathlib If you start many projects which all use the latest stable version of mathlib From 605b4119356d29e34ab2e3b1fb6b8f57f3453a96 Mon Sep 17 00:00:00 2001 From: Jon Eugster Date: Thu, 5 Sep 2024 17:03:16 +0200 Subject: [PATCH 10/10] whitespace --- templates/install/tricks.md | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/templates/install/tricks.md b/templates/install/tricks.md index 85190ba48..da4d0490c 100644 --- a/templates/install/tricks.md +++ b/templates/install/tricks.md @@ -27,9 +27,9 @@ Here is the current best practice to achieve this. ``` Note that `v4.10.0` is the tag of the latest release, you can look at [mathlib's tags](https://github.com/leanprover-community/mathlib4/tags) to find out which is the most recent release version. - The above line assumes you have set up git using an SSH key. - If you have not set this up correctly, you may want to - use `git clone --branch v4.10.0 https://github.com/leanprover-community/mathlib4.git` instead. + The above line assumes you have set up git using an SSH key. + If you have not set this up correctly, you may want to + use `git clone --branch v4.10.0 https://github.com/leanprover-community/mathlib4.git` instead. 2) Go inside your mathlib and download the current cache: ```bash