lake exe cache get offline

Stream: mathlib4

[Eric Rodriguez]

Is it possible to make this have an offline fallback? It's sometimes nice to be able to switch between predownloaded oleans, but it seems to me it fails when fully offline because of the git fetch origin step:

error: > git fetch origin    # in directory ./lake-packages/std
error: stderr:
fatal: unable to access 'https://github.com/leanprover/std4/': Failed to connect to github.com port 443 after 7790 ms: Couldn't connect to server
error: external command `git` exited with code 128

[Eric Wieser]

hack: point origin at . instead so that fetching is a no-op

[Eric Rodriguez]

changing that back and forth all the time would be annoying though

[MohanadAhmed]

If the ltar files are already downloaded there shouldn't lake exe cache unpack! just work?

[MohanadAhmed]

https://github.com/leanprover-community/mathlib4/blob/07944c77adc653e2f348fc03e0e0671edc69777d/Cache/Main.lean#L20

[Eric Rodriguez]

Ah perfect, I'll try that out next time I'm on the tube

[Arthur Paulino]

Commands with exclamation mark are slower and meant to be used in case of error due to some corrupted file. lake exe cache unpack should do the job, not trying to decompress files that are already available and decompressed. If you notice that something is strange because some olean file is corrupted, then try the unpack! version