Error: unknown package 'Init' with Chinese characters

Stream: general

[Floris van Doorn]

I just installed a fresh copy of Lean for one of my students. This is a Chinese student with Chinese characters in their username.
When we open a Lean file outside a project in VSCode, and write #eval 1 + 1, Lean is working correctly.
When we open a Lean file with just #eval 1 + 1 in a repository (this repository, on lean v4.2-rc1), then we get the error "unknown package 'Init'" when compiling the lakefile. This happens both in VSCode and on the command line.

Related:
https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/error.3A.20file.20'init'.20not.20found.20in.20the.20search.20path

[Mauricio Collares]

4.2.0-rc1 does not contain lean4#2633

[Mauricio Collares]

So probably upgrading to 4.2.0 helps

[Mauricio Collares]

(there is a "v4.2.0" mathlib tag which may help a bit with the upgrade)

[Mauricio Collares]

By the way, the repo contains a file named lecture1.lean (lowercase L) so Linux users will probably have trouble

[Mario Carneiro]

lowercased files aren't a problem AFAIK, except for lake init

[Floris van Doorn]

oh, lowercase filenames cause issues? I tried to uppercase my file names indeed.

[Mauricio Collares]

They don't cause issues by themselves, but I think you refer to LeanCourse.Lectures.Lecture1 (uppercase L) in your repo

[Floris van Doorn]

Ok, thanks!

[Floris van Doorn]

Mauricio Collares said:

So probably upgrading to 4.2.0 helps

We're now running lake exe cache get, that indeed seems to work correctly! Thanks a lot.

[Floris van Doorn]

Now I have the difficult decision: ask everyone to upgrade, or have my students work on two different versions of Lean/mathlib... Neither option is great.

[Eric Wieser]

At least you weren't on rc2 or rc3...