Zulip Chat Archive
Stream: new members
Topic: getting cache in windows
Adam (Nov 27 2025 at 15:54):
Hi everyone. I'm one of the LSGNT student's working on a computing project in Lean. I have trouble setting up Lean environment on Windows (see the terminal of VS attached).
Screenshot 2025-11-27.png
Aaron Liu (Nov 27 2025 at 15:56):
That doesn't look like a normal Lean project it seems to be a normal Lean project?, how did you set it up?
Edison Xie (Nov 27 2025 at 16:01):
we were doing a project with verso so this lean_content contains everything about lean and some bnlueprints which is under v4.26.rc2 and verso is under v4.25.2 but I don't think that's the issue?
Aaron Liu (Nov 27 2025 at 16:04):
what's the rest of that error message?
Adam (Nov 27 2025 at 16:12):
Aaron Liu (Nov 27 2025 at 16:14):
What's in .lake\packages\mathlib?
Adam (Nov 27 2025 at 16:17):
Aaron Liu (Nov 27 2025 at 16:23):
try removing the .lake directory and they again?
Adam (Nov 27 2025 at 16:30):
Aaron Liu (Nov 27 2025 at 16:53):
Maybe the weird line break in your file path is causing a problem?
Adam (Nov 27 2025 at 16:57):
Yes, that was it! Thank you so much for your help!!
Last updated: Dec 20 2025 at 21:32 UTC