Getting olean cache for Mathlib branch

Stream: new members

[Daniel Packer]

Hi all,
Currently, I have a branch of mathlib that I'm building upon in a different project. (That is, the branch of mathlib is the _target of this other project). However, I've currently done it in the super hacky way of copy/pasting the stuff in my mathlib branch into the _target of my other project. Is there a way to get a specific branch of mathlib along with its oleans when I'm not on that branch?
I'm imaging something like $ leanproject get-cache master/orthonormal_basis but I don't know what the right syntax would be.

[Anne Baanen]

You should be able to specify the mathlib commit id you want in the _target in the leanpkg.toml.

[Daniel Packer]

Awesome! And then I just run $ leanproject get-mathlib-cache?

[Anne Baanen]

So the dependencies should look something like:

[dependencies]
mathlib = {git = "https://github.com/leanprover-community/mathlib", rev = "d6d2d7e5017f89b0ca8e9fe18e61980efdbd6e0b"}

[Anne Baanen]

Yes, I believe leanproject will detect that the dependency version changed and update the _target folder automatically