Stop lean automatically downloading things to my computer

Stream: lean4

[Patrick Nicodemus]

There are a lot of "conveniences" in the lean toolchain that I find pretty aggressive. I get pretty upset when things are downloaded or installed onto my computer without my consent.

I would like to get help with the following problems.
Number 1, how do I avoid the problem that lean --version tries to download and install lean? What on earth kind of behavior is that?
image.png

Number 2, when I open VSCode, it says 'Starting lean language server and cloning necessary repositories." No, thank you very much! How do I stop this behavior?

Please point me to everywhere else where this toolchain is downloading and installing things without my explicit direction so that I can disable this aggressive and absolutely unsolicited behavior. This is like the used car salesman of programming languages.

[Eric Wieser]

Regarding lean --version, this is invoking a shim provided by elan (which you presumably installed), which downloads the lean binary and runs that instead

[Eric Wieser]

If you want to see what toolchains elan has installed, rather than invoke one, you can use elan toolchain list

[Niels Voss]

I think there's two problems here: elan automatically downloads toolchains (what Eric Wieser mentioned), and lake automatically installs dependencies when it is run (which happens automatically when Lean is started up). For the former problem, it might be reasonable for elan to add a config option to allow prompting the user before installing new toolchains, though elan doesn't really seem to have a configuration right now. elan is a fork of rustup, so I'm wondering if anyone who uses Rust knows whether or not this same thing happens there, and how it has been resolved if so.

For the latter problem, there's at least two things that can be done: either have the Lean language server prompt the user before running lake build, or have lake build prompt before downloading repositories. It's not clear to me that either of these solutions is desirable. I think we could take inspiration from other programming languages, but as far as I know all other build tools (e.g. gradle with java, uv with python) I have worked with do the same thing that Lean does and just automatically download packages.

[Patrick Nicodemus]

How do I personally configure the Lean LSP or Lake build to behave differently with this regard?

[Patrick Nicodemus]

patrick@patrick-ThinkPad ~/c/l/double-categories (master) [1]> elan default leanprover/lean4:v4.26.0
info: default toolchain set to 'leanprover/lean4:v4.26.0'
patrick@patrick-ThinkPad ~/c/l/double-categories (master) [SIGINT]> lean --version
info: downloading https://releases.lean-lang.org/lean4/v4.27.0-rc1/lean-4.27.0-rc1-linux.tar.zst

[Patrick Nicodemus]

How do I stop lean from downloading the most recent version of lean? Obviously elan default isn't doing what I am looking for

[Patrick Nicodemus]

Oh, I see.

patrick@patrick-ThinkPad ~/c/l/double-categories (master)> lake update
info: leanprover-community/mathlib: checking out revision '950ff565938d137c026ab67af9dcd978a2ddd3be'
info: updating toolchain to 'leanprover/lean4:v4.27.0-rc1'

I didn't realize lake update was going to edit my project-local configuration files. Is there a way to pin the Lean version to a project? What is the command to update only those projects which don't already have a version pinned?

[Patrick Nicodemus]

For example I just installed Lean 4.26, and I want to install any version of mathlib which is compatible with this, say the most recent compatible version. How do I install a compatible version of mathlib?

[Ruben Van de Velde]

Do you want an independent clone of mathlib or do you have a project that depends on mathlib, and you want it to use a compatible version?

[Patrick Nicodemus]

Ruben Van de Velde said:

Do you want an independent clone of mathlib or do you have a project that depends on mathlib, and you want it to use a compatible version?

Right now I have a project that depends on mathlib and I'd like to use a compatible version. However, I'd be interested in hearing about the first one.

[Ruben Van de Velde]

If you have a lakefile.lean, you can use

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

or with a lakefile.toml

[[require]]
name = "mathlib"
scope = "leanprover-community"
rev = "v4.26.0"

and within an independent clone of mathlib, you can do git checkout v4.26.0

[Patrick Nicodemus]

Okay, thank you. That's very helpful. Is rev = "v.4.26.0" a tag in the Mathlib git repo?

[Ruben Van de Velde]

Yes, exactly