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

Stream: general

[Eric Wieser]

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]

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