error: file 'init' not found in the search path

Stream: general

[Kevin Buzzard]

A student on a new Windows machine gets error: file 'init' not found in the search path whatever Lean file they open. This also happens on the command line. I suspected that they'd corrupted their local Lean install (which was 3.45) so I told them to run leanproject up on the project they were working on (which then caused an install of 3.48), which I hoped would fix the problem, but it didn't. I have no idea what to suggest next.

[Kevin Buzzard]

The student has the Lean 3 extension installed. I just got them to rm -rf .elan and then open the project again; Lean was downloaded again and the error was still there. I am totally lost. You wouldn't believe what I've seen, dealing with undergraduate mathematicians. People accidentally edit core.lean or whatever, and I can always solve their problems (unless they're python-related, in which case I know people who can solve them). But this one really has me stumped. Any ideas? The laptop is new and the installation is new. I got the student to make a new one-line file just containing def n := 37 and running Lean it on still gave the error about init not found. And lean --version produced a sensible output.

The student gave me a cryptic comment about how the system had asked them about a file with a very long weird name (probably a hash) and asked if they wanted to replace it, or something odd happened or something; anyway I'm out of ideas.

[Mauricio Collares]

Is there something uncommon about the user's home directory/user name? Length, special characters, or the like. Windows has a path length limit and some weird restrictions.

[Mauricio Collares]

Would be nice to know where this hash-named file was located and what it was, too

[Kevin Buzzard]

Yes! This is a Chinese user with a unicode username!

[Mauricio Collares]

I wonder if the "hash" is a mangled representation of the codepoints contained in the username. I also wonder if there's a particular character causing trouble, because I would guess Chinese users would have faced this earlier (unless it's common to use generic placeholders or romanized usernames).