Zulip Chat Archive

Stream: new members

Topic: leanpkg build ... too fast?


view this post on Zulip Luis O'Shea (Nov 11 2019 at 00:41):

I've followed the instructions for installing mathlib, and just followed the "Working on an existing package" instructions from Creating a Lean project. The 7th step is "Type leanpkg build to compile everything, this will take some time.". When I executed leanpkg build it did not take much time (it took almost no time) and the output was

configuring tuto 0.1
mathlib: trying to update _target/deps/mathlib to revision 27515619bcd834006f2936b292021135496b4efb
> git checkout --detach 27515619bcd834006f2936b292021135496b4efb    # in directory _target/deps/mathlib
HEAD is now at 27515619 minor updates to the installation instructions (#1538)
> lean --make src
upper_bounds : set ?M_1 → set ?M_1
exact le_max_left (u N - x) (-(u N - x))
exact one_div_pos_of_pos this

Is everything ok? FWIW, first_proofs.lean seems to work fine in VSCode. Wasn't building mathlib supposed to take quite some time?

view this post on Zulip Koundinya Vajjha (Nov 11 2019 at 00:48):

Did you install and call the update-mathlib script?

view this post on Zulip Luis O'Shea (Nov 11 2019 at 01:20):

I did. It took about 30sec to run, and did so silently.

view this post on Zulip Scott Morrison (Nov 11 2019 at 01:21):

Then you're probably all good; you acquired a precompiled copy of mathlib, so lean --make had nothing to do.

view this post on Zulip Scott Morrison (Nov 11 2019 at 01:21):

(I'm a little surprised that update-mathlib was silent. Are you on windows?)

view this post on Zulip Luis O'Shea (Nov 11 2019 at 01:22):

Yes (Win10).

view this post on Zulip Luis O'Shea (Nov 11 2019 at 01:23):

Ooops -- it was almost silent. Output:

Info: No github section found in 'git config', we will use GitHub with no authentication
Querying GitHub...
Downloading nightly...
Extracting nightly...

view this post on Zulip Scott Morrison (Nov 11 2019 at 01:24):

Perfect!

view this post on Zulip Luis O'Shea (Nov 11 2019 at 01:29):

Thanks!

view this post on Zulip Luis O'Shea (Nov 11 2019 at 01:31):

By the way, is the output after lean --make src due to some stray #checks in the code?

view this post on Zulip Bryan Gin-ge Chen (Nov 11 2019 at 02:02):

Yep, you'll see them when you browse the source of first_proofs.lean in VS Code.

view this post on Zulip Kevin Buzzard (Nov 11 2019 at 06:40):

I think that some of these docs (where it warns you about a long wait) were written before the update-mathlib revolution


Last updated: May 13 2021 at 17:42 UTC