lake exe cache get no such file or directory

Stream: lean4

[Floris van Doorn]

I am trying to help someone to set up Lean on Windows. Lean is installed correctly, and when running lake exe cache get in a project we get the error no such file or directory. The cache.exe file is correctly generated, but once it starts executing, before any message is printed, we get the aforementioned error.
The folder ~/.cache does not exist after running this command (so leantar is presumably not downloaded). He seems to have an internet connection.

Any ideas? Any way to run in debug mode to print more info where it is going wrong? Can we print the path that we're trying to access?

Potential issue: It is a laptop using a Japanese locale - but no unicode appears in any relevant folder.

[Mario Carneiro]

try putting a println! "hi" command in Cache/Main.lean

[Sebastian Ullrich]

Complete guess: does running curl in the terminal work?

[Mario Carneiro]

+1 to the curl guess, that's the first thing that cache does IO-wise other than reading files it has already checked for existence

[Mario Carneiro]

Unfortunately it seems https://github.com/leanprover-community/static-curl/releases only has releases for linux, not windows

[Sebastian Ullrich]

It should be a Windows built-in nowadays

[Floris van Doorn]

curl and tar do exist in the terminal. I'll try some print-debugging.

[Floris van Doorn]

Thanks for the suggestions so far.

[Mauricio Collares]

Any antivirus software? AVG and Kaspersky does some MiTM to scan https connections, and that interferes with curl. There's another thread about it: https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/lake.20exe.20cache.20get.20errors/near/388953502

[Floris van Doorn]

I believe the antivirus errors were curl errors, but here we didn't even reach the Attempting to download ... file(s) output yet.

[Floris van Doorn]

But it might still be a good thing to try.

[Mauricio Collares]

I thought leantar itself was downloaded using curl

[Mauricio Collares]

The antivirus could be quarantining the leantar binary too, of course

[Mario Carneiro]

unlikely. The first message you would expect to see is leantar is too old, so if you haven't seen that then cache hasn't even started the download yet