Zulip Chat Archive

Stream: general

Topic: leanproject get-cache --force


Chris Hughes (Sep 04 2021 at 17:17):

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 (Sep 04 2021 at 17:19):

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

Oliver Nash (Sep 04 2021 at 17:52):

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 (Sep 04 2021 at 17:56):

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

Eric Wieser (Sep 04 2021 at 19:24):

I have a PR that fixes this

Eric Wieser (Sep 04 2021 at 19:25):

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

Eric Wieser (Sep 04 2021 at 19:25):

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

Eric Wieser (Sep 04 2021 at 19:27):

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


Last updated: Dec 20 2023 at 11:08 UTC