fail in updating matlib

Stream: general

[Chengyan Hu]

When I trying to update matlib, something strange happens and it fails. Can anyone help me with that?
image.png

[Chengyan Hu]

The error message is:

info: mathlib: running post-update hooks
uncaught exception: unknown module prefix 'Mathlib'

No directory 'Mathlib' or file 'Mathlib.lean' in the search path entries:
C:\Users\����\Desktop\cyclo_project\.lake\packages\Cli
C:\Users\����\Desktop\cyclo_project\.lake\packages\batteries
C:\Users\����\Desktop\cyclo_project\.lake\packages\batteries
C:\Users\����\Desktop\cyclo_project\.lake\packages\Qq
C:\Users\����\Desktop\cyclo_project\.lake\packages\aesop
C:\Users\����\Desktop\cyclo_project\.lake\packages\aesop
C:\Users\����\Desktop\cyclo_project\.lake\packages\proofwidgets
C:\Users\����\Desktop\cyclo_project\.lake\packages\proofwidgets
C:\Users\����\Desktop\cyclo_project\.lake\packages\importGraph
C:\Users\����\Desktop\cyclo_project\.lake\packages\importGraph
C:\Users\����\Desktop\cyclo_project\.lake\packages\LeanSearchClient
C:\Users\����\Desktop\cyclo_project\.lake\packages\LeanSearchClient
C:\Users\����\Desktop\cyclo_project\.lake\packages\plausible
C:\Users\����\Desktop\cyclo_project\.lake\packages\plausible
C:\Users\����\Desktop\cyclo_project\.lake\packages\mathlib
C:\Users\����\Desktop\cyclo_project\.lake\packages\mathlib
C:\Users\����\Desktop\cyclo_project\.lake\packages\mathlib
C:\Users\����\Desktop\cyclo_project\.lake\packages\mathlib
C:\Users\����\Desktop\cyclo_project\.lake\packages\mathlib
C:\Users\����\Desktop\cyclo_project\.lake\packages\mathlib
C:\Users\����\Desktop\cyclo_project\.lake\packages\mathlib
C:\Users\����\Desktop\cyclo_project
c:\Users\����\.elan\toolchains\leanprover--lean4---v4.21.0-rc3\src\lean\lake
.lake\packages\mathlib\.lake\build\bin\..\src\lean\lake
.lake\packages\mathlib\.lake\build\bin\..\src\lean
error: mathlib: failed to fetch cache

白衣@LAPTOP-QCFVN1RJ MINGW64 ~/Desktop/cyclo_project (master)
$

[Andrew Yang]

We try to help him during Xena and we tried reinstalling everything but we couldn't fix the problem.

[Kevin Buzzard]

We've deleted .elan, switched off windows defender (which blocks .elan install, so it seems), deleted and recreated the project, we cannot even begin to use Lean + mathlib on this windows machine.

[Yaël Dillies]

Our suspicion is that the issue is triggered by the Chinese characters

[Jz Pan]

Our suspicion is that the issue is triggered by the Chinese characters

That's possible. Try a path with only ASCII character and without spaces. Maybe you need to setup environment variable manually (just like TryLean4 bundle) in cast that the default user path already contains Chinese characters...

[Eric Wieser]

Can you ls .lake\packages\mathlib?

[Kevin Buzzard]

This user still cannot install Lean + mathlib on their Windows laptop and they're supposed to be starting a project with me on Monday.

The directory .lake/packages/mathlib looks normal to me.

[Chengyan Hu]

白衣@LAPTOP-QCFVN1RJ MINGW64 ~/Desktop/cyclo_project/.lake/packages/mathlib ((d5f3cef44b...))
$ ls
Archive/            Cache/                DownstreamTest/  LongestPole/  MathlibTest/  bors.toml  lake-manifest.json  scripts/
Archive.lean        Counterexamples/      GNUmakefile      Mathlib/      README.md     docs/      lakefile.lean       widget/
CODE_OF_CONDUCT.md  Counterexamples.lean  LICENSE          Mathlib.lean  Shake/        docs.lean  lean-toolchain

[Jz Pan]

Kevin Buzzard said:

This user still cannot install Lean + mathlib on their Windows laptop and they're supposed to be starting a project with me on Monday.

The directory .lake/packages/mathlib looks normal to me.

Can you give my TryLean4 Windows bundle a try?

[Jz Pan]

Since your ~ directory already contains Chinese characters, I suspect the usual installation doesn't work. Maybe you can try to unpack TryLean4 Windows bundle to C:\TryLean4 or D:\TryLean4 or whatever folder without Chinese characters and spaces.

[Kevin Buzzard]

Where is this bundle?

[Jz Pan]

https://github.com/acmepjz/TryLean4Bundle1/releases/tag/nightly

[Jz Pan]

Currently it is almost only tested on my computer...

[Jz Pan]

Feedback can go here #general > My version of offline mathlib help and TryLean4 Windows @ 💬

[Jz Pan]

Oh, another possible fix without using TryLean4 Windows bundle:

Can you try to move the project to a directory without Chinese characters? For example C:\LeanProjects\cyclo_project\

[Eric Wieser]

Another suggestion: try the same thing not in git bash

[Eric Wieser]

That is, use cmd or powershell

[Eric Wieser]

Confusingly, in your screenshot you're using powershell but in the code you're using git bash

[Eric Wieser]

Jz Pan said:

Can you try to move the project to a directory without Chinese characters?

This is likely to help, but ideally we would track down the bug first

[Chengyan Hu]

Jz Pan said:

https://github.com/acmepjz/TryLean4Bundle1/releases/tag/nightly

Seems it doesn't work. It reported the same error as before. I think again due to Chinese Character.

[Chengyan Hu]

Eric Wieser said:

Jz Pan said:

Can you try to move the project to a directory without Chinese characters?

This is likely to help, but ideally we would track down the bug first

I think this might be helpful.

[Chengyan Hu]

It seems like it's neccesary to edit environmental variable to do it, otherwise VS code might not able to find where the project is?

[Kevin Buzzard]

There is something wrong with the machine in general I think. We created a new account and attempted to install VS Code and the process hung at the point where we attempted to run the installer.

[Justin Asher]

Just to throw out some ideas that would fix it:

• WSL
• Set up a server if you really need something working (4 shared vCPU + 8gb of RAM through Hetzner is $15 per month)

Both of these would feel nearly identical to you, since you can just open Lean in VS Code in either case + hook up your GitHub.

I have no clue if the Chinese characters are causing the problem. If that is indeed the case, WSL should fix this because you can just create files in a path without those special characters.

[Jz Pan]

Chengyan Hu said:

Jz Pan said:

https://github.com/acmepjz/TryLean4Bundle1/releases/tag/nightly

Seems it doesn't work. It reported the same error as before. I think again due to Chinese Character.

Oh I mean you should extract it to somewhere without Chinese character, e.g. C:\LeanProjects\TryLean4Bundle

[Chengyan Hu]

Hi! I set up a new account without Chinese character and tried to redownload everything like VsCode and Git again to make it work. Now I successfully downloaded VsCode and Git, but it still gave me an error message saying Git is missed.

[Chengyan Hu]

image.png

[Chengyan Hu]

image.png

[Chengyan Hu]

The error message looks like this.

[Aaron Liu]

Chengyan Hu said:

image.png

I see "Git GUI" here, can you confirm that you also have Git?

[Chengyan Hu]

image.png

[Chengyan Hu]

I just followed all instructions of installing there, and this folder is all I have about ''git

[Aaron Liu]

Try typing git --version on the command line. What do you get?

[Chengyan Hu]

git version 2.50.0.windows.1

[Aaron Liu]

Try restarting VSCode.

[Chengyan Hu]

It works now!

[Chengyan Hu]

May I ask that how can I download mathlib and tell lean to automatically update it?

[Aaron Liu]

What are you going to be using mathlib for?

[Kevin Buzzard]

Working with me on various projects

[Chengyan Hu]

Hi! I ask Edison to help me install mathlib, but something wrong occured again.

info: Qq: checking out revision '56047303fce0d07dcae7e3e91b17eef67d11f6f4'
info: batteries: cloning https://github.com/leanprover-community/batteries
info: batteries: checking out revision '3613427d66262c4e25e19b40a6a49242e94ba072
'
info: Cli: cloning https://github.com/leanprover/lean4-cli
info: Cli: checking out revision '1604206fcd0462da9a241beeac0e2df471647435'
info: mathlib: running post-update hooks
installing leantar 0.1.15
  % Total    % Received % Xferd  Average Speed   Time    Time     Time  Current
                                 Dload  Upload   Total   Spent    Left  Speed
  0     0    0     0    0     0      0      0 --:--:-- --:--:-- --:--:--     0
100  706k  100  706k    0     0   810k      0 --:--:-- --:--:-- --:--:--  810k

✖ [2/2] Running proofwidgets:release
error: failed to fetch GitHub release (run with '-v' for details)
Some required builds logged failures:
- proofwidgets:release
error: build failed
uncaught exception: Failed to fetch ProofWidgets cloud release: lake failed with
 error code 1
error: mathlib: failed to fetch cache

bourbaki@LAPTOP-QCFVN1RJ MINGW64 ~/desktop
$

[Jz Pan]

Try run lake update again, it is transient error.

[Chengyan Hu]

$ lake exe cache get -v
uncaught exception: unknown module prefix '[anonymous]'

No directory '[anonymous]' or file '[anonymous].lean' in the search path entries
:
C:\Users\bourbaki\Desktop\kb_minion\.lake\packages\Cli
C:\Users\bourbaki\Desktop\kb_minion\.lake\packages\batteries
C:\Users\bourbaki\Desktop\kb_minion\.lake\packages\batteries
C:\Users\bourbaki\Desktop\kb_minion\.lake\packages\Qq
C:\Users\bourbaki\Desktop\kb_minion\.lake\packages\aesop
C:\Users\bourbaki\Desktop\kb_minion\.lake\packages\aesop
C:\Users\bourbaki\Desktop\kb_minion\.lake\packages\proofwidgets
C:\Users\bourbaki\Desktop\kb_minion\.lake\packages\proofwidgets
C:\Users\bourbaki\Desktop\kb_minion\.lake\packages\importGraph
C:\Users\bourbaki\Desktop\kb_minion\.lake\packages\importGraph
C:\Users\bourbaki\Desktop\kb_minion\.lake\packages\LeanSearchClient
C:\Users\bourbaki\Desktop\kb_minion\.lake\packages\LeanSearchClient
C:\Users\bourbaki\Desktop\kb_minion\.lake\packages\plausible
C:\Users\bourbaki\Desktop\kb_minion\.lake\packages\plausible
C:\Users\bourbaki\Desktop\kb_minion\.lake\packages\mathlib
C:\Users\bourbaki\Desktop\kb_minion\.lake\packages\mathlib
C:\Users\bourbaki\Desktop\kb_minion\.lake\packages\mathlib
C:\Users\bourbaki\Desktop\kb_minion\.lake\packages\mathlib
C:\Users\bourbaki\Desktop\kb_minion\.lake\packages\mathlib
C:\Users\bourbaki\Desktop\kb_minion\.lake\packages\mathlib
C:\Users\bourbaki\Desktop\kb_minion\.lake\packages\mathlib
C:\Users\bourbaki\Desktop\kb_minion
c:\Users\bourbaki\.elan\toolchains\leanprover--lean4---v4.22.0-rc2\src\lean\lake
.lake\packages\mathlib\.lake\build\bin\..\src\lean\lake
.lake\packages\mathlib\.lake\build\bin\..\src\lean

[Chengyan Hu]

I tried to redownload it instead.

[Chengyan Hu]

I'm now running again by lake-update

[Chengyan Hu]

Fantastic! Now after lake-update, we got an error that nobody on the table now ever seen before:

PS D:\kb_minion> lake exe cache get
error: D:\kb_minion\.lake/packages\mathlib: could not resolve 'HEAD' to a commit; the repository may be corrupt, so you may need to remove it and try again
PS D:\kb_minion>

[Chengyan Hu]

Does anyone have any idea about this

[Julian Berman]

Fun. The mix of directory separators looks mildly suspicious there? I don't have any specific idea but if no one else chimes in, I'd try:

• run rm -rf .lake && lake exe cache get, does the error still occur?
• run git --git-dir D:\kb_minion\.lake\packages\mathlib\.git show-ref HEAD -- do you get output? how about git --git-dir D:\kb_minion\.lake/packages\mathlib\.git show-ref HEAD? Also have you intentionally switched which drive you have your Mathlib on (from C:\ to D:\)?
• are you in git bash? Try powershell instead, maybe that somehow is related to whatever being confused by what the right separator is for Windows

[Chengyan Hu]

bourbaki@LAPTOP-QCFVN1RJ MINGW64 ~
$ rm -rf .lake && lake exe cache get
error: [root]: no configuration file with a supported extension:
C:\Users\bourbaki\lakefile.lean
C:\Users\bourbaki\lakefile.toml

after run rm -rf .lake && lake exe cache get

[Julian Berman]

You're in the wrong directory

[Julian Berman]

Run that from the directory you cloned your project to

[Julian Berman]

The above makes it seem like maybe that's D:\kb_minion -- is that where you think you cloned it to (tell me if I'm not being specific enough of course!)

[Chengyan Hu]

Ahh yes it should be in D:\

[Chengyan Hu]

Sorry I'm really an idiot in computer science

[Julian Berman]

Don't worry we all are, each in our own fun ways...

[Chengyan Hu]

How can I make git to believe I wanna use D:\?

[Chengyan Hu]

I have no idea how to set up

[Julian Berman]

I haven't followed the whole thread, sorry -- probably you should be opening VSCode, then doing File > Open Folder and choosing that directory (D:\kb_minion)

[Julian Berman]

And then:

Screenshot 2025-07-01 at 17.20.00.png

in this menu, clicking Project: Clean Project followed by Project: Fetch Mathlib Cache should be the equivalent of what I asked in that line.

[Chengyan Hu]

You mean Fetch Mathlib Build Cache right?

[Chengyan Hu]

image.png

[Chengyan Hu]

image.png

[Julian Berman]

Yes -- ok -- are those screenshots from after running Clean Project first, right?

[Julian Berman]

If so, in that command line window that popped up there try running git --git-dir D:\kb_minion\.lake\packages\mathlib\.git show-ref HEAD

[Chengyan Hu]

image.png

[Julian Berman]

OK, so far so good, can you try the second one as well? git --git-dir D:\kb_minion\.lake/packages\mathlib\.git show-ref HEAD

[Chengyan Hu]

This seems exactly the same as the previous one you sent me?

[Chengyan Hu]

modulo the direction of \

[Chengyan Hu]

image.png

[Chengyan Hu]

I tried the other direction of \, it gives the same output as before

[Julian Berman]

Yes -- ok, interesting

[Julian Berman]

OK the command lake runs looks actually to be this: git --git-dir D:\kb_minion\.lake/packages\mathlib\.git rev-parse --verify --end-of-options HEAD can you try that just to be totally sure

[Julian Berman]

But it does so via specifying the working directory of the git process, not using --git-dir. I suspect this means nothing to you, but basically my guess is that's the issue.

[Julian Berman]

Specifically (and I'm still guessing), I think the "wrong" directory separator is not OK for that. I still don't know why it's wrong.

[Julian Berman]

If the above succeeds (which I think it will) -- can you open a blank Lean file and tell me what #eval System.FilePath.pathSeparator says?

[Chengyan Hu]

I want to share a fantastic news! I finally done this.

[Chengyan Hu]

I don't know how, Kenny used some magic

[Chengyan Hu]

But now everything works.