Changing the default behavior of leanproject get-cache

Stream: general

[Eric Wieser]

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]

/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]

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

[Damiano Testa]

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]

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]

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]

I look at github, then use explicit --rev

[Alex J. Best]

I always use download-all...

[Alex J. Best]

Having a user configurable default would be great I think.