Eric Wieser (Jul 01 2022 at 08:30):
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/masteris ahead of
$(git merge-base HEAD origin/master)
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
--revlater, 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
- Yes, with
- 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)"
~/.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
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