Intalling error

Stream: mathlib4

[Jordi Majó]

When I run

lake exe cache get

I get the following error

uncaught exception: unknown module prefix 'Mathlib'

No directory 'Mathlib' or file 'Mathlib.lean' in the search path entries:
C:\Users\Jordi Maj�\mathematics_in_lean\.lake\packages\Cli
C:\Users\Jordi Maj�\mathematics_in_lean\.lake\packages\batteries
C:\Users\Jordi Maj�\mathematics_in_lean\.lake\packages\batteries
C:\Users\Jordi Maj�\mathematics_in_lean\.lake\packages\Qq
C:\Users\Jordi Maj�\mathematics_in_lean\.lake\packages\aesop
C:\Users\Jordi Maj�\mathematics_in_lean\.lake\packages\aesop
C:\Users\Jordi Maj�\mathematics_in_lean\.lake\packages\proofwidgets
C:\Users\Jordi Maj�\mathematics_in_lean\.lake\packages\proofwidgets
C:\Users\Jordi Maj�\mathematics_in_lean\.lake\packages\importGraph
C:\Users\Jordi Maj�\mathematics_in_lean\.lake\packages\importGraph
C:\Users\Jordi Maj�\mathematics_in_lean\.lake\packages\LeanSearchClient
C:\Users\Jordi Maj�\mathematics_in_lean\.lake\packages\LeanSearchClient
C:\Users\Jordi Maj�\mathematics_in_lean\.lake\packages\plausible
C:\Users\Jordi Maj�\mathematics_in_lean\.lake\packages\plausible
C:\Users\Jordi Maj�\mathematics_in_lean\.lake\packages\mathlib
C:\Users\Jordi Maj�\mathematics_in_lean\.lake\packages\mathlib
C:\Users\Jordi Maj�\mathematics_in_lean\.lake\packages\mathlib
C:\Users\Jordi Maj�\mathematics_in_lean\.lake\packages\mathlib
C:\Users\Jordi Maj�\mathematics_in_lean\.lake\packages\mathlib
C:\Users\Jordi Maj�\mathematics_in_lean\.lake\packages\mathlib
C:\Users\Jordi Maj�\mathematics_in_lean\.lake\packages\mathlib
C:\Users\Jordi Maj�\mathematics_in_lean
c:\Users\Jordi Maj�\.elan\toolchains\leanprover--lean4---v4.21.0\src\lean\lake
.lake\packages\mathlib\.lake\build\bin\..\src\lean\lake
.lake\packages\mathlib\.lake\build\bin\..\src\lean

I'd appreciate it if anyone could provide suggestions for a fix.
Thanks

[Aaron Liu]

What does your mathematics_in_lean\.lake\packages\mathlib\ look like? Does it contain Mathlib.lean?

[Jordi Majó]

HI Aaron,

This is what the mathlib directory contains

 Volume in drive C is Windows
 Volume Serial Number is C09D-3259

 Directory of C:\Users\Jordi Majó\mathematics_in_lean\.lake\packages\mathlib

22/09/2025  20:07    <DIR>          .
22/09/2025  20:07    <DIR>          ..
22/09/2025  20:06    <DIR>          .devcontainer
22/09/2025  20:06    <DIR>          .docker
22/09/2025  20:06    <DIR>          .github
22/09/2025  20:06               162 .gitignore
22/09/2025  20:06               155 .gitpod.yml
22/09/2025  20:07    <DIR>          .lake
22/09/2025  20:06    <DIR>          .vscode
22/09/2025  20:06    <DIR>          Archive
22/09/2025  20:06             2.651 Archive.lean
22/09/2025  20:06               269 bors.toml
22/09/2025  20:06    <DIR>          Cache
22/09/2025  20:06             5.319 CODE_OF_CONDUCT.md
22/09/2025  20:06    <DIR>          Counterexamples
22/09/2025  20:06               936 Counterexamples.lean
22/09/2025  20:07    <DIR>          docs
22/09/2025  20:06                53 docs.lean
22/09/2025  20:06    <DIR>          DownstreamTest
22/09/2025  20:06               243 GNUmakefile
22/09/2025  20:07             2.786 lake-manifest.json
22/09/2025  20:07             5.543 lakefile.lean
22/09/2025  20:07                25 lean-toolchain
22/09/2025  20:06            11.357 LICENSE
22/09/2025  20:06    <DIR>          LongestPole
22/09/2025  20:07    <DIR>          Mathlib
22/09/2025  20:06           302.581 Mathlib.lean
22/09/2025  20:07    <DIR>          MathlibTest
22/09/2025  20:06             8.694 README.md
22/09/2025  20:07    <DIR>          scripts
22/09/2025  20:07    <DIR>          Shake
22/09/2025  20:06    <DIR>          widget
              14 File(s)        340.774 bytes
              18 Dir(s)  204.572.971.008 bytes free