Kevin Buzzard (Sep 06 2022 at 18:21):
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 (Sep 06 2022 at 18:35):
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 (Sep 06 2022 at 18:55):
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 (Sep 06 2022 at 18:56):
Would be nice to know where this hash-named file was located and what it was, too
Kevin Buzzard (Sep 06 2022 at 19:01):
Yes! This is a Chinese user with a unicode username!
Mauricio Collares (Sep 06 2022 at 19:14):
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).
Last updated: Aug 03 2023 at 10:10 UTC