Closed rwst closed 3 months ago
About updating the lean-toolchain file: If the project depends on Mathlib and the old version of lake is able to parse the new lakefiles of all dependencies, then this happens automatically, IIUC. Maybe this should be mentioned, because in most cases nothing has to be done by the user.
@fpvandoorn You mean it's not necessary to lake update
, just change lean-toolchain
? And maybe lake exe cache get
?
I see, there is also e.g. elan toolchain install leanprover/lean4:stable
.
I only was talking about manually updating lean-toolchain
.
I don't think these instructions are very good, users don't have to directly interact with elan
themselves. This page assumes your project depends on Mathlib, and then you also always have to update Mathlib, and doing that will automatically install the right version of Lean.
I added my own version of these instructions here: #487
No problem. I don't have much experience with lean. I'm glad that you are taking over, and that there will be good instructions on that page. Closing.
Thanks for taking the initiative in writing these instructions. They were indeed needed!
Please add/change if inaccurate.