Zulip Chat Archive

Stream: new members

Topic: leanproject mathlib src confusion

Yakov Pechersky (Jul 26 2020 at 21:20):

I switched from a recent mathlib commit to an older one in my leanpkg.toml, but now am getting the following error on the first line of importing:
image.png

Yakov Pechersky (Jul 26 2020 at 21:21):

Do I have to purge my _target folder to fix this?

Kenny Lau (Jul 26 2020 at 21:27):

if leanproject doesn't work:

  1. go to the mathlib inside the _target folder
  2. git reset --hard [commit SHA]
  3. leanproject get-cache
  4. profit

Yakov Pechersky (Jul 26 2020 at 21:27):

Yeah, ended up doing that. Thanks!

Last updated: Dec 20 2023 at 11:08 UTC