Zulip Chat Archive

Stream: new members

Topic: leanproject mathlib src confusion


view this post on Zulip 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

view this post on Zulip Yakov Pechersky (Jul 26 2020 at 21:21):

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

view this post on Zulip 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

view this post on Zulip Yakov Pechersky (Jul 26 2020 at 21:27):

Yeah, ended up doing that. Thanks!


Last updated: May 18 2021 at 17:44 UTC