leanproject get-cache --force

Stream: general

[Chris Hughes]

The behaviour of leanproject get-cache --force surprised me a little. It undid all my changes since the last commit, whereas the behaviour I expected would be to get oleans that matched my last commit while keeping the lean files the same. Maybe the help file should include a warning that it will overwrite uncommitted changes.

[Johan Commelin]

Would it make sense that leanproject does a git stash ... git stash pop if it detects a dirty directory?

[Oliver Nash]

This happened to me ages ago and IIRC I then PR’d the feature that a dirty repo requires —force.

I think one could argue that the behaviour is fine but the user deserves a stronger hint to be sure they know what they’re doing. e.g., rename —force to —dangerous and move on?

[Ruben Van de Velde]

Or just --destroy-my-changes? :)

[Eric Wieser]

I have a PR that fixes this

[Eric Wieser]

IMO leanproject get-cache has no right to touch the working tree; it should get the cache and only the cache

[Eric Wieser]

If you want the working tree, use git to get it first, then get the cache for that

[Eric Wieser]

Relatedly, mk-cache --force poisons the cache for future cache requests