Zulip Chat Archive

Stream: new members

Topic: leanpkg build ... too fast?

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?

Koundinya Vajjha (Nov 11 2019 at 00:48):

Did you install and call the update-mathlib script?

Luis O'Shea (Nov 11 2019 at 01:20):

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

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.

Scott Morrison (Nov 11 2019 at 01:21):

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

Luis O'Shea (Nov 11 2019 at 01:22):

Yes (Win10).

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...

Scott Morrison (Nov 11 2019 at 01:24):


Luis O'Shea (Nov 11 2019 at 01:29):


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?

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.

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: Dec 20 2023 at 11:08 UTC