Zulip Chat Archive

Stream: general

Topic: Changing the default behavior of leanproject get-cache

Eric Wieser (Jul 01 2022 at 08:30):

Right now, leanproject get-cache has a somewhat underused --fallback argument for when no exact cache is available but when caches might be available for parent commits. The options available are:

  • --fallback=none: do not even detect the presence of inexact caches
    use-case: to avoid unnecessary network access

  • --fallback=show (default): detect but do not download inexact caches
    use-case: to not surprise users by succeeding but providing an incomplete cache, but also inform them that they can recover

  • --fallback=download-first: download and apply the first available cache, following first git parents
    use-case: any cache is better than no cache. This is better than get-cache --rev origin/master, because it doesn't pick up an incompatible cache if origin/master is ahead of $(git merge-base HEAD origin/master)

  • --fallback=download-all: like download-first, but also download caches found by following non-first git parents
    use-case: you just merged master after doing a big refactor, and don't know whether the master cache or your branches old cache will be better. Download both upfront so that you can try switching with --rev later, even if offline.

In probably 90% of use-cases --fallback=download-first is the right thing to do, but it's also long to type so I suspect it's severely underused.

Should we change this to be the default, or at least to have a shorter spelling?

Eric Wieser (Jul 01 2022 at 08:33):

/poll Do you use the --fallback option?

  • Yes, with --fallback=download-first
  • No, I use get-cache --rev origin/master
  • No, I use git switch master; get-cache; git switch my-branch
  • No, I just wait for github to have the latest cache
  • No, I didn't know it existed!

Eric Wieser (Jul 01 2022 at 08:39):

(before deciding whether to change anything, let's find out how it's currently used!)

Damiano Testa (Jul 01 2022 at 10:07):

Eric, I am very grateful that you keep reminding me (and the community!) of all these commands! My strategy is to use leanproject get-cache and then run leanproject get-cache --rev <commit found with earlier get-cache>: a very inefficient way of doing leanproject get-cache --fallback=download-first!

If the name does not change, I will probably create an alias

alias firstcache='leanproject get-cache --fallback=download-first'

Kevin Buzzard (Jul 01 2022 at 10:21):

I can't ever remember the options so I just type leanproject get-cache and then if it says "this doesn't work, try this instead" I tend to just cut and paste what it suggests. I think that in practice I am usually in one of two situations: (1) I'm editing a leaf file, so I just want to merge master, get master oleans and then continue; (2) I've edited data.nat.basic or whatever, so I'm probably doomed but perhaps the best bet is the most recent oleans available for my branch.

Eric Wieser (Jul 01 2022 at 10:43):

Regarding not remember the options, if you put

eval "$(_LEANPROJECT_COMPLETE=bash_source leanproject)"

in your ~/.bashrc, then tab-completion will remind you of the options

Yury G. Kudryashov (Jul 01 2022 at 20:06):

I look at github, then use explicit --rev

Alex J. Best (Jul 01 2022 at 21:40):

I always use download-all...

Alex J. Best (Jul 01 2022 at 21:41):

Having a user configurable default would be great I think.

Last updated: Aug 03 2023 at 10:10 UTC