Zulip Chat Archive

Stream: general

Topic: Side project importing mathlib branch


view this post on Zulip Adam Topaz (Jan 22 2021 at 16:00):

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?

view this post on Zulip Johan Commelin (Jan 22 2021 at 16:01):

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

view this post on Zulip Rob Lewis (Jan 22 2021 at 16:01):

And don't run leanproject up

view this post on Zulip Adam Topaz (Jan 22 2021 at 16:01):

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

view this post on Zulip Johan Commelin (Jan 22 2021 at 16:02):

leanproject get-mathlib-cache

view this post on Zulip Adam Topaz (Jan 22 2021 at 16:02):

is it leanproject get-mathlib-cache?

view this post on Zulip Rob Lewis (Jan 22 2021 at 16:02):

leanproject get-mathlib-cache

view this post on Zulip Adam Topaz (Jan 22 2021 at 16:02):

:smile:

view this post on Zulip Adam Topaz (Jan 22 2021 at 16:02):

Thanks!

view this post on Zulip Adam Topaz (Jan 22 2021 at 16:03):

(cc: @Colter MacDonald )


Last updated: May 15 2021 at 00:39 UTC