leanproject get-cache looks further back?

Stream: general

[Scott Morrison]

Would anyone be interested in modifying leanproject get-cache so that if oleans aren't available it looks further back in the git history and tries again?

[Scott Morrison]

I very often merge a proposed edit on github and then realise that this blocks me from working on the branch for a while, until oleans are available again.

[Scott Morrison]

We already do this during CI: in scripts/fetch_olean_cache.sh the relevant line is

for new_git_sha in $(git log -$GIT_HISTORY_DEPTH --first-parent --pretty=format:%H)

[Scott Morrison]

Hopefully we could just reproduce the same behaviour in leanproject. However I know my python-fu is weak enough that I am not the person with comparative advantage implementing this. :-)

[Bryan Gin-ge Chen]

The PR that added this feature to mathlib's CI is #2278. I suppose it would be natural for me to take this on, but it'll take me some time to understand how mathlibtools currently works, so I won't make any promises. More than happy to help out if someone else wants to jump on this in the near future though!

[Yakov Pechersky]

When I'm on a branch, I do leanproject get-c --rev origin to get that branch's oleans, or at least the most recent thing that's been pushed and cached upstream

[Scott Morrison]

Can we just make this the default behavior?

[Bryan Gin-ge Chen]

Yakov Pechersky said:

When I'm on a branch, I do leanproject get-c --rev origin to get that branch's oleans, or at least the most recent thing that's been pushed and cached upstream

This still fails if someone's pushed to the branch recently though, right?

edit: (Granted, this is still an improvement over the current behavior.)

[Eric Wieser]

I think there's a longer thread about this elsewhere

[Eric Wieser]

Here's a relevant message in the old thread: https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/get-mathlib-at-commit/near/213010027

[Eric Wieser]

PR'd the behavior described in the thread I link above as leanprover-community/mathlib-tools#106