leanpkg build ... too fast?

Stream: new members

[Luis O'Shea]

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]

Did you install and call the update-mathlib script?

[Luis O'Shea]

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

[Scott Morrison]

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

[Scott Morrison]

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

[Luis O'Shea]

Yes (Win10).

[Luis O'Shea]

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]

Perfect!

[Luis O'Shea]

Thanks!

[Luis O'Shea]

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

[Bryan Gin-ge Chen]

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

[Kevin Buzzard]

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