Required Internet Connection

Stream: lean4

[Marcus Rossel]

I'm guessing this is just user error, but I've recently started having problems when trying to use Lean in VS Code when not connected to the internet.
I habitually use Lean 4: Restart File. When not connected to the internet, this results in:

`/Users/marcus/.elan/toolchains/leanprover--lean4---nightly-2022-08-11/bin/lake print-paths Init ReactorModel.Execution.State` failed:

stderr:
error: stderr:
fatal: unable to access 'https://github.com/leanprover-community/mathlib4.git/': Could not resolve host: github.com
error: git exited with code 128

I declare Mathlib as a dependency in lakefile.lean:

import Lake
open Lake DSL

package reactor_model
lean_lib ReactorModel
require mathlib from git "https://github.com/leanprover-community/mathlib4.git"@"876d9cc42ccbfea023752e40e6edb7279d9c6b5a"

Is there something other than Lean 4: Restart File I should be using when I want to force Lean to recheck a file?

[Henrik Böving]

No this is an inherent thing of lake that VScode cannot influence, I think this has been brought up before though I cannot recall the topic name anymore.

[Marcus Rossel]

Hmm, that's a bummer. Is there a way to work around this? I tend to work while traveling, but this kinda throws a wrench in it.

[Tomas Skrivan]

Here is the previous GitHub issue https://github.com/leanprover/lake/issues/104

It should be fixed, what is your lean version?