installation issues on windows

Stream: lean4

[Floris van Doorn]

I'm helping someone installing Lean on Windows:

• We've downloaded mathematics_in_lean and we're running into the error "no such file or directory (error code 2)".
• We've already deleted the Lean toolchain multiple times
• We've already disabled the antivirus scanner
• We've already deleted mathematics_in_lean/.lake
• We've already ran lake clean

The problem persist.
Any further ideas?

One potential issue: he had Lean 3 installed before, and we manually deleted the Lean 3 ~/.elan directory at some point (the automatic installation instructions was unable to delete it, probably because a Lean 3 file was open at the same time).

[Julian Berman]

I don't suppose the error says which path it claims to not exist then?

[Floris van Doorn]

nope...

[Floris van Doorn]

when running it, it seems to correctly compile the ~10 files needed to run Mathlib.Cache.

[Julian Berman]

(I'm only brainstorming as I know not much about Lean's install and even less about Windows) -- what's the command you're running that produces the error then? Just opening it in VSCode? If you run lake build you get the same error I assume?

[Julian Berman]

Also, does the username look special at all? In particular does it have anything non-ASCII and/or have spaces in it?

[Floris van Doorn]

lake exe cache get! via the terminal.

[Julian Berman]

I vaguely recall an earlier thread saying spaces in usernames on Windows was causing some issue.

[Floris van Doorn]

Username is normal, computer is German

[Floris van Doorn]

(we first tried to have the extension run set up mathematics_in_lean, and that seemed to succeed, but when opening a Lean file it started compiling everything, starting with Batteries.)

[Floris van Doorn]

There is no .cache subfolder in the user directory, which is surprising...

[Floris van Doorn]

(there is an .elan subfolder with the expected toolchains, which we tried to delete a couple of times, since that was an issue elsewhere sometimes)

[Julian Berman]

I think a first guess scanning through what cache does and comparing it to your list of things you tried is maybe it's something curl related?

[Julian Berman]

Can you find curl on the machine and/or can the user successfully execute it?

[Julian Berman]

Uninstalling/reinstalling elan itself may also be another random idea if you haven't already tried that.

[Floris van Doorn]

I think we used curl in the install script, but let me try that...

[Floris van Doorn]

curl --version gives version 7.55.1, and running a single random curl command indeed works...

[Floris van Doorn]

We can try reinstalling elan, but Lean does successfully compile a few files, so that's unlikely to be it...

[Sebastian Ullrich]

In other threads it usually said that bin/leanc.exe was missing, can you check it's there? That would explain at least why it succeeded partially

[Sebastian Ullrich]

(if it makes sense to take a look at it in person tomorrow, that would be worth a bike detour...)