installing mathlib problem

Stream: new members

[Souma Ray]

Hello, I am trying to install Lean 4 on Windows. I am persistently getting the error: unknown executable cache error. I have tried a complete reinstallation of elan, cleaning my PATH, and creating a fresh project with the toolchain pinned to v4.9.1, but the error remains. My Get-Command lake points to the correct .elan\bin directory. Can anyone help me troubleshoot what environmental issue on my PC could be causing this?

[Anthony Wang]

Did you forget to add mathlib as a dependency for your project? https://github.com/leanprover-community/mathlib4/wiki/Using-mathlib4-as-a-dependency

[Notification Bot]

This topic was moved here from #general > installing mathlib problem by Patrick Massot.