Zulip Chat Archive

Stream: mathlib4

Topic: How to clone mathlib4

Eric Rodriguez (Nov 18 2022 at 17:06):

Is the correct way to use mathlib4 just to clone it as a git repo and use it as-is? I can't seem to find anything in the README about this

Floris van Doorn (Nov 18 2022 at 17:13):

Generally people ask for permission here to be able to push to non-master branches, just like with mathlib3.

Eric Rodriguez (Nov 18 2022 at 17:17):

I actually meant to do things locally - I've never used a Lean4 project and don't know what the equivalent of leanproject is

Jireh Loreaux (Nov 18 2022 at 17:18):

Yes just clone and run lake build

Jireh Loreaux (Nov 18 2022 at 17:19):

There are no cached oleans yet.

Floris van Doorn (Nov 18 2022 at 17:35):

What README were you looking at? On https://github.com/leanprover-community/mathlib4 you see the full build instructions for mathlib4, which work if you have not used Lean 4 before.

Floris van Doorn (Nov 18 2022 at 17:36):

but indeed, for now we're building mathlib4 ourselves.

Yaël Dillies (Nov 18 2022 at 17:43):

Another option is to use gitpod. It's already set up.

Adam Topaz (Nov 18 2022 at 18:07):

How far are we from the point where lake build (in a freshly cloned mathlib4) takes too long?

Jireh Loreaux (Nov 18 2022 at 19:35):

It depends on what you mean by too long. On one hand, it's still less than 5 minutes on my not very powerful laptop, but if you're constantly switching branches (including nightly versions of Lean 4) while porting, it is already arguably too long. However, there was some discussion of this yesterday at the meeting, and we'll be looking into what we should do (soon).

Adam Topaz (Nov 18 2022 at 21:17):

Sure, it's great that it only takes 5 minutes to compile std4+mathlib4, as porting picks up I can imagine that number will grow VERY quickly.

Jireh Loreaux (Nov 18 2022 at 21:54):

Yes, hence the reason for the discussion about it yesterday. :smiley:

Adam Topaz (Nov 18 2022 at 22:10):

Is the plan for these meetings to always be on Thursdays at the time mentioned above? I wanted to attend the last one, but completely missed the announcement

Mario Carneiro (Nov 18 2022 at 22:12):

yes, they are weekly at 2022-11-17T16:00:00-05:00 . Not next week though since it's a holiday here (or at least, I won't be around)

Adam Topaz (Nov 18 2022 at 22:14):

Oh, the so-called "American" thanksgiving eh?

Mario Carneiro (Nov 18 2022 at 22:15):

Yes, thanks to everyone who has donated their time to assisting in the port!

Moritz Doll (Nov 18 2022 at 22:20):

so you are having an octopus instead of a turkey?

Last updated: Dec 20 2023 at 11:08 UTC