import bottleneck

Stream: lean4

[Alexander Bentkamp]

Hi! On our web interface https://lean.math.hhu.de/#code=import%20Mathlib, importing mathlib takes more than 20s. On my laptop, it only takes 3s. What is the bottleneck here? Is it hard disk speed?

[Locria Cyber]

that doesn't seem like an official Lean website

[Alexander Bentkamp]

No, it's ours, and I would like to make it faster if possible.

[Martin Dvořák]

OT: I really appreciate your efforts! I want to use https://lean.math.hhu.de/ for my students (as one of the options).

[Sebastian Ullrich]

Here is the timing on my laptop:

$ echo 'import Mathlib' | lake env time lean --stdin --profile
interpretation of Mathlib.Prelude.Rename.binportTag took 318ms
interpretation of Lean.mkStateFromImportedEntries._at.Mathlib.Prelude.Rename.initFn._@.Mathlib.Mathport.Rename._hyg.251._spec_1 took 299ms
import took 852ms
cumulative profiling times:
    elaboration 0.0386ms
    import 852ms
    initialization 22.5ms
    interpretation 784ms
    linting 0.0482ms
    parsing 0.00384ms
1.25user 0.35system 0:01.72elapsed 93%CPU (0avgtext+0avgdata 1690552maxresident)k
253160inputs+0outputs (439major+70565minor)pagefaults 0swaps

If the CPU time doesn't scale up on your server, disk bottleneck seems likely, yes

[Notification Bot]

14 messages were moved from this topic to #mathlib4 > Problems building mathlib4 by Sebastian Ullrich.