Gabriel Ebner

I think all you need to do is: ``` cd lean/library lean --make ```

This could be a difference between macOS and Linux. From what I can tell the git password prompt goes to extreme lengths so that it is shown (and accepts input!)...

Thanks! This is very interesting. So Nix's advantage is really mostly due to the flake eval cache! For comparison, could you also post how long `lake print-paths Inundation` takes on...

> this implies that Lake has a 3-4x overhead over Nix (w/o the cache). How much of that do you think is likely just due to the differences in language...

> My originally question (which is now essentially moot due to actual difference being smaller than I though) was simply what percent of overhead, if any, should one expect from...

After #132, the biggest cost centers are `Lean.Elab.parseImports` (22%), `computeFileHash` (17%), and loading the lakefile (14%).

Oooh, there are some low-hanging fruit in `Lean.Elab.parseImports`. We actually initialize a new empty environment every single time we parse the imports....

> if you turned on precompiled modules Yeah, turning on precompiled modules will still cause the quadratic behavior at the moment. But we will only use them in mathlib if...

> since it will recompute the transitive imports for a module each time it is visited As far as I can tell, all of the `recBuild*` functions where `transImports` is...

Okay, I've tried to understand the logic behind the precompiled modules code so that I can fix it properly. One thing that confuses me is that we treat direct and...