elan default toolchain without network access

Stream: lean4

[Julian Berman]

I have my default toolchain set to beta but I don't want Lean constantly trying to reach the internet every time I run it.

Looking at the source code doesn't give me high hopes, there's no way to currently get the behavior I want right, which is "use the latest version installed but don't go looking for a new one"?

[Marc Huisinga]

I think the easiest way is to set a specific default toolchain that doesn't need to be resolved in this case.
Elan itself also supports --no-net, but invocations to the lean symlink don't.

You might also be interested in what we do in the VS Code extension to implement the mode that prompts users before installing new toolchains: https://github.com/leanprover/vscode-lean4/blob/master/vscode-lean4/src/utils/leanCmdRunner.ts