Side project importing mathlib branch

Stream: general

[Adam Topaz]

Suppose I have a lean project I'm working on, which I do not intend ever integrating with mathlib. Suppose also that I want to use a (non-master) branch of mathlib in this project. What's the preferred workflow to accomplish this? Does leanproject have a flag that will create a project based importing a non-master branch of mathlib?

[Johan Commelin]

Personally, I would just manually lump the commit hash of mathlib into the leanpkg.toml

[Rob Lewis]

And don't run leanproject up

[Adam Topaz]

Okay. So how would I use leanproject to get the oleans for the particular hash?

[Johan Commelin]

leanproject get-mathlib-cache

[Adam Topaz]

is it leanproject get-mathlib-cache?

[Rob Lewis]

leanproject get-mathlib-cache

[Adam Topaz]

:smile:

[Adam Topaz]

Thanks!

[Adam Topaz]

(cc: @Colter MacDonald )