Problem installing "mechanics of proof"

Stream: new members

[Martin Krastev]

I'm trying to clone a repository called "mechanics-of-proof" and I received this error message after VS code told me to restart the code. Please help: c:\Users\Martin\.elan\toolchains\leanprover--lean4---v4.3.0\bin\lake.exe print-paths Init Mathlib.Data.Real.Basic Library.Basic failed:

stderr:
error: compiled configuration is invalid; run with -R to reconfigure
Invalid Lake configuration. Please restart the server after fixing the Lake configuration file.

[Notification Bot]

A message was moved here from #new members > Hypothesis names with `split` by Kevin Buzzard.

[Kevin Buzzard]

@Martin Krastev how did you install the repo? I have Lean installed already, I typed git clone https://github.com/hrmacbeth/math2001.git on the command line, then cd math2001 then lake exe cache get and it looks like it's all working fine. Maybe explain more clearly exactly which instructions you followed to try to get things working?

[Kevin Buzzard]

Actually parts of it are not quite working fine but I think that this is because the repo is unfortunately on an absurdly old version of Lean. But I am not getting the error you're getting, I just have some of the exercise sheets not quite working properly.

[Martin Krastev]

Hello @Kevin Buzzard , just to let you know that the issue has been resolved by disabling the antivirus software on my PC and running the setup.bat file again. Thank you for your support