Using a mathlib branch in a project

Stream: general

[Bolton Bailey]

Is there a way to tell my mathlib-using lean project to use a particular branch of mathlib, as I might want to do if I were developing a project in parallel to some changes to mathlib that hadn't been accepted yet? I sort of expected there to be a leanproject get-mathlib-cache --rev my_branch command, but it seems there is not.

[Jason Rute]

To do this, I manually edit the leanpkg.toml file with the exact version of mathlib I've needed. The tricky thing then is figuring out the exact invocations of leanpkg and/or leanproject to download the oleans and build the project without upgrading mathlib. Let me look back at my notes...

[Eric Wieser]

I think leanpkg configure; leanproject get-mathlib-cache should do the trick

[Jason Rute]

Does anyone know how frequently the oleans are saved for a commit? Can you do leanproject get-mathlib-cache for basically any commit on github, or only on select releases?

[Yaël Dillies]

Any commit

[Jason Rute]

Also, I've only ever done this for specific commit hashes? (I just looked at the leanpkg.toml file and replaced the rev with the commit I want.) Can you use branch names instead of commits?

[Eric Wieser]

IIRC, Not every commit has a cache

[Eric Wieser]

Only the one at the head of each bors batch

[Eric Wieser]

Using a branch name is a bad idea, because then no one can reproduce your build if the branch moves

[Bryan Gin-ge Chen]

My recollection is the following: on the master branch, we keep a cache for every commit at the head of every bors batch (more or less the commits with a green checkmark next to them here). We create a cache for every commit to any branch pushed to the repo, but they are deleted after ~3 days if they are not at the head of a branch.

The precise details are in this script.

[Yaël Dillies]

Oh sorry, I had branches in mind.

[Eric Wieser]

Even on a branch, CI only ever builds the head commit

[Eric Wieser]

If you commit twice and push both simultaneously, only the second commit gets built

[Yaël Dillies]

Ah, is that what you call the head commit? Then sure. Sorry for the terminology confusion.

[Johan Commelin]

HEAD has a well-defined meaning in the gitiverse (-;

[Kyle Miller]

Not answering anyone's questions, but here's a git trick I use sometimes: HEAD refers to what commit is currently checked out (I think it's just whatever .git/HEAD is referring to), and you can refer to its parents by repeatedly suffixing it with ^. So for example if you've checked out a branch and you know CI hasn't finished, but still the oleans of its parent commit should be good enough, you can do

leanproject get-cache --rev=HEAD^

[Eric Wieser]

get-cache --fallback=download-first iteratively does that for you @Kyle Miller.