help with 'mathematics in lean'

Stream: lean4

[LizBonn]

Hi, I'm new to lean and trying to fetch 'mathematics in lean' repository on my PC. I followed this instruction and reach Step 5, but then I meet something wrong when running command 'lake exe cache get'. The errors are below. Could anyone help with this case?
Thanks in advance.
Errors.png

[LizBonn]

When I first ran this command, it really worked and showed info 'downloading component 'lean' '. After a while the info became 'installing component 'lean' ', but then such errors came out. I have no idea what happened. :-(

[Mauricio Collares]

What does git status say?

[LizBonn]

git-status.jpg

[LizBonn]

It shows like this.

[Alex J. Best]

How did you install Lean? What does lean -v say?

[LizBonn]

I installed lean following this.
This is what 'lean -v' shows.
leanv.png

[Alex J. Best]

That looks good. What happens if you type lake build?

[LizBonn]

btw, there's also something wrong with my vscode. I cannot start the lean server. When I try to open a .lean file, it reminds me that 'The lean4 server crashed...'.
vscodeproblem.jpg

[LizBonn]

'lake build' actually results in the same errors as above...

[Ruben Van de Velde]

What happens if you "go to output"?

[LizBonn]

This is the output, some similar error messages.
ouput.jpg

[Sebastian Ullrich]

Something seems to be seriously wrong with your installation of Lean. Try removing all of ~/.elan and then reinstalling it

[LizBonn]

ok, I'll have a try.

[Alex J. Best]

It looks like people had similar issues before maybe due to non ascii characters in their username, is that the case for your setups?

[Sebastian Ullrich]

Oh! If lake build fails but lean lakefile.lean works, that would more or less confirm that.

[LizBonn]

There's truly non ascii characters in my username. I don't know if it influences this...

[LizBonn]

Unluckily, the latter one doesn't work either :-(

[Yaël Dillies]

LizBonn said:

There's truly non ascii characters in my username. I don't know if it influences this...

I had the same problem with my ë. I resorted to fully reinstall my computer and change my username to Yael. It fixed it.

[Sebastian Ullrich]

I would have loved to hear about this issue earlier!

[MohanadAhmed]

Hello @LizBonn
I notice from the screenshots you are using windows. Before going with the drastic option of reinstalling your computer perhaps you can try the TryLean4Bundle located at https://github.com/MohanadAhmed/TryLean4Bundle/releases/tag/latest
The steps are very simple:

1. Download the exe from the link above.
2. Run the exe for it to unpack. It will create a folder called TryLean4Bundle.
3. Inside the TryLean4Bundle you will find a file called RunLean.bat. Double click on it and it will open the mathematics_in_lean folder in VSCodium directly.

[MohanadAhmed]

If non-ascii characters are the source of the problem you can put the bundle in a folder out of your user account for example in C:\MyLeanStuff or other location.

[Sebastian Ullrich]

Yaël Dillies said:

LizBonn said:

There's truly non ascii characters in my username. I don't know if it influences this...

I had the same problem with my ë. I resorted to fully reinstall my computer and change my username to Yael. It fixed it.

Fixed in lean4#2633, for people called aü¤ and likely others as well

[Eric Wieser]

I'm very confused by that PR, the windows documentation says that the alternative to (wide) unicode is ASCII, which also sounds wrong

[Eric Wieser]

https://stackoverflow.com/a/8831181/102441 suggests that we should be using the W API, then converting to utf8

[Eric Wieser]

Ah, the answer below says that it's fine after all!