`elan` is unusable offline (behind VPN)

[omentic]

Prerequisites

• Check that your issue is not already filed:
  https://github.com/leanprover/lean4/issues
• Reduce the issue to a minimal, self-contained, reproducible test case.
  Avoid dependencies to Mathlib or Batteries.
• Test your test case against the latest nightly release, for example on
  https://live.lean-lang.org/#project=lean-nightly
  (You can also use the settings there to switch to “Lean nightly”)

Description

The lake cli checks and pulls down the latest version of Lean, whenever it can, before being run. This makes it unusable offline. I'd like to request that lake checks for network connectivity before attempting to download Lean -- though, this would still be an issue over slow networks.

Context

N/A

Steps to Reproduce

1. Install lake. Do whatever with it, install a toolchain or something.
2. Disconnect from the internet.
3. Run lake --help.

Expected behavior:
lake should recognize it is offline / on a slow network and immediately function with the existing toolchain.

Actual behavior:
lake stalls out.

Versions

Lake version 5.0.0-src+d8204c9 (Lean version 4.26.0)

Additional Information

N/A

Impact

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.

[nomeata]

What is the content of your lean-toolchain?

[omentic]

Ah, I should have mentioned, this is running lake outside any project context. I usually hit this when I spawn a new terminal to run lake --help, or when I'm trying to create a new project with lake new or lake init.

Is there a global lean-toolchain file somewhere?

[nomeata]

It may be that it's actually elan that gets in your way here? What if you use lake +already_installed_toolchain --help? That hopefully runs locally.

[omentic]

Hrm, elan appears to have the same problem. elan show stalls out when offline.

lake +already_installed_toolchain --help does run locally.

[nomeata]

Well, note that if you invoke lake, you are actually invoking elan which resolves the toolchain and then invokes the lake of that toolchain. So the issue is actually a lake issue and should be reported there.

[nomeata]

Ah, these days it's possible to transfer issues

[Kha]

Cannot reproduce.

$ nmcli connection down ...
$ lake --version
warning: failed to query latest release, using existing version 'leanprover/lean4:v4.26.0'
Lake version 5.0.0-src+d8204c9 (Lean version 4.26.0)

[nomeata]

Since OP says that lake stalls out, maybe there are different ways of being “offline” that have different symptoms. Maybe @omentic can say more.

[omentic]

Interesting. This appears to be due to being behind a VPN.

[~]$ nmcli connection down eduroam
Connection 'eduroam' successfully deactivated (D-Bus active path: /org/freedesktop/NetworkManager/ActiveConnection/27)
[~]$ lake --version
^C⏎                                 # (stalls)
[~]$ tailscale down
[~]$ lake --version
warning: failed to query latest release, using existing version 'leanprover/lean4:v4.26.0'
Lake version 5.0.0-src+d8204c9 (Lean version 4.26.0)