Zulip Chat Archive

Stream: general

Topic: What is `leanproject mk-cache --force` for

Eric Wieser (Aug 22 2021 at 11:59):

I'm struggling to see why this command would ever be a good idea; it essentially builds a cache labelled as being for commit A that actually contains lean and olean files for some changes which were never assigned a sha. Some options that I think would be better:

  • Just remove it, require users to run git commit
  • Have it run git stash -k first to actual create a real commit B, and then store the cache under that name

The reason I ask is because I can't work out what the correct behavior of leanproject get-cache --rev HEAD^ (when not in mathlib) should be; right now it essentially resets the entire working tree to whatever state it was in when mk-cache was run, which may or may not correspond to the contents off the git commit HEAD^.

Eric Wieser (Sep 01 2021 at 13:40):

I implemented the git stash version at leanprover-community/mathlib-tools#115

Last updated: Dec 20 2023 at 11:08 UTC