lake exe cache get failure with no internet

Stream: general

[Kevin Buzzard]

The last hour of the train journey from mainland Europe back to London is famous for its poor WiFi. From the moment you enter the Channel Tunnel (the undersea part of the journey) until arrival in central London you spend most of your time either in very long tunnels or in parts of the UK which have poor mobile reception. Basically you're offline for an hour.

I just did this journey. I was working on a project which depended on mathlib and I was working on two branches of this project which depended on two different versions of mathlib because there had been a very recent mathlib bump. I had all of the websites open which I needed and I had mathlib cache for both branches -- I was prepared. Five minutes into the hour of no connectivity I had finished working on main and wanted to switch to the second branch kenny-lemma-80-statement to review a PR. All the mathlib oleans were present on my computer, and I was happy to build the project files on my local machine. But my plan was foiled:

buzzard@IC-HWDXTW69VR ClassFieldTheory % # pre-tunnel preparations
buzzard@IC-HWDXTW69VR ClassFieldTheory % git checkout kenny-lemma-80-statement
Switched to branch 'kenny-lemma-80-statement'
buzzard@IC-HWDXTW69VR ClassFieldTheory % lake exe cache get
info: mathlib: checking out revision '0a052585de2cfc95e94c373033fe24df36ca7c0e'
info: aesop: checking out revision '1da2f2d2945f8740802cc38c48d2ce6723ef6154'
info: batteries: checking out revision '5da171049c81931a2110303c9d547f5ab2955b06'
Current branch: HEAD
Using cache (Azure) from origin: leanprover-community/mathlib4
No files to download
Decompressing 7442 file(s)
Unpacked in 5126 ms
Completed successfully!
buzzard@IC-HWDXTW69VR ClassFieldTheory % git checkout main
Switched to branch 'main'
Your branch is up to date with 'origin/main'.
buzzard@IC-HWDXTW69VR ClassFieldTheory % lake exe cache get
info: mathlib: checking out revision 'e551247794a13557744c7c61cf10625fb940db09'
info: aesop: checking out revision 'ca519018e8bdc34d7bb4ecf0c8d39634a8c15300'
info: batteries: checking out revision 'dd3edb3aa6b4de87f96f2c3998881ef95ba24ed7'
Current branch: HEAD
Using cache (Azure) from origin: leanprover-community/mathlib4
No files to download
Decompressing 7456 file(s)
Unpacked in 5034 ms
Completed successfully!
buzzard@IC-HWDXTW69VR ClassFieldTheory % # enter Channel tunnel
buzzard@IC-HWDXTW69VR ClassFieldTheory % # finish working on `main`
buzzard@IC-HWDXTW69VR ClassFieldTheory % git checkout kenny-lemma-80-statement
Switched to branch 'kenny-lemma-80-statement'
buzzard@IC-HWDXTW69VR ClassFieldTheory % lake exe cache get
error: external command 'git' exited with code 128
buzzard@IC-HWDXTW69VR ClassFieldTheory % # gaargh
buzzard@IC-HWDXTW69VR ClassFieldTheory %

I am 99.9% sure that my computer, even without internet access, is in theory capable of doing exactly what I want to do at this point, which is to just look at which version of mathlib (and whatever else) I want using the project's lake-manifest.json, check out those branches (which certainly exist locally), and then get oleans from local cache (which also definitely exist). But in practice I had no idea how to do this so I lost an hour of work (although I did compose this message so all was not lost; hello from under the sea, by the way). Is there some hack whereby I can get around this? This has also happened to me on other occasions but today it was particularly annoying because I lost an hour.

[Aaron Liu]

What about lake exe unpack? Does that do anything?

[Andrew Yang]

My experience with this is that lake itself wants internet access somehow. So while lake exe cache unpack does not download cache, it might still fail without internet.

[Kevin Buzzard]

I can simulate my undersea adventures on my laptop by switching WiFi off:

buzzard@IC-HWDXTW69VR ClassFieldTheory % lake exe unpack
error: external command 'git' exited with code 128
buzzard@IC-HWDXTW69VR ClassFieldTheory % lake exe cache unpack
error: external command 'git' exited with code 128
buzzard@IC-HWDXTW69VR ClassFieldTheory %

[Ruben Van de Velde]

I guess this is a side effect of writing all our tooling in lean

[Arthur Paulino]

Ruben Van de Velde said:

I guess this is a side effect of writing all our tooling in lean

That shouldn't be an issue. Lake (or any other build tool) relies on internet connectivity whenever a project has non-local dependencies. The same would happen with Python+Pip, Rust+Cargo, Node+Npm etc.

Now, Lake trying to access the internet for an operation that doesn't need it is strange. @Kevin Buzzard do you know if that issue happens before or after the Cache binary is built?

[Ruben Van de Velde]

Definitely before, from the logs

[Ruben Van de Velde]

And I mean that you generally wouldn't need to rebuild a rust tool when switching between branches that have a different version of mathlib

[Arthur Paulino]

Even when the version of mathlib changes, Cache should not be rebuilt because it doesn't have mathlib as a dependency. What I'm hinting at is that diversifying the language is a tangential workaround. The ideal solution would allow per-subpackage dependencies, like Cargo accepts subcrates with self-contained Cargo.toml files.

[Arthur Paulino]

In other words, I would advocate in favor of a "more expressive Lake" solution rather than a "less Lean" solution

[Ruben Van de Velde]

Oh, I'm not advocating for anything

[Kevin Buzzard]

Is someone who understands what's going on (so, not me!) able to turn this advocating into something which could be raised on #lean4 ? I didn't post there because I thought my question might be too mathlib-specific but of course I had no idea about what was actually going on.

[Arthur Paulino]

@Mac Malone is this something that's already in your mind/roadmap?

[Mac Malone]

@Arthur Paulino I am not 100% sure what went wrong here. I think the prpblem is this:

Kevin Buzzard said:

check out those branches (which certainly exist locally)

This is not a safe assumption. Lake does not really make any guarantees on what tags or branches are availble offline in its checkout. That is, it does not promise to maintain previously checkout references (and there are performance reasons why this can be undesirable). As currenlty implemented, the branch probably does exist, but lake always performs a fetch before attempting a checkout, so it unfortunately does not matter. I am hesistent to fix this and make this a supported feature for the aformentioned reasons.

[Mac Malone]

Independently, one thing what would definitely be good to improve here is Lake's error messages.

[Ruben Van de Velde]

Even if there's no guarantees, if I'm offline, I'd like lake to make a best effort at doing its job. If it fails, it fails, but it seems silly to me to block me if there's no need to

[Arthur Paulino]

What I'm proposing is along the lines of there should be no checkout because Cache doesn't have dependencies. Right now Lake assumes it does because mathlib does.

[Kevin Buzzard]

Yes let me be clear, I am not suggesting that lake has to be changed, I am asking what the hack is which will enable me to change branches on the london subway and get cache.

[Julian Berman]

Kevin when you do this do you know before your train hits the tunnel that you have these N branches and you want to be able to look at all N of them and move back and forth? I.e. you know ahead of time which branches you want to look at?

[Julian Berman]

If so maybe your hack is "use git work trees when this happens, and have N work trees you set up and run lake exe cache get in in each one before you dive underwater"

[Kevin Buzzard]

I guess in this particular case I did know, and I also knew that I had got this timeout error before with no internet on my mac, but I incorrectly conjectured that my recent experience with Microsoft Defender might have fixed this problem too.

[Julian Berman]

Is that helpful to try then? Maybe you want to try git worktree add kenny-lemma-80-statement and lake exe cache get in that directory ahead of time, and do that for each branch you want locally available offline, and then rather than switching branches now you just end up with one folder per branch

[Julian Berman]

(Undoubtedly this is doable from within VSCode as well if you prefer that.)

[Aaron Liu]

Just ran into this, lake exe cache get didn't with offline, lake build doesn't work either so I don't think it's specifically a cache problem

[Jireh Loreaux]

Kevin, if you just want a hack, and because your shiny new computer has plenty of space, just have multiple copies of Mathlib (like, literally multiple folders) with each checked out to the appropriate branch and having the correct cache already unpacked.

This is a stupid hack, but it will prevent you from losing an hour next time.

[Julian Berman]

(That's the same hack as worktrees, the only advantage of the latter is they do "copy + checkout branch" in one step, and also they track all the copies you have made via git worktree list)