Mac Malone

Fixed by #138 (not sure why GitHub did not automatically close it already).

This issue is quite stale and suggested fixes have been generally implemented upstream (e.g.,, leanprover/lean4#2573), so I am closing this issue.

This issue is rather stale and some major performance improvements have landed ([lean4#2444](https://github.com/leanprover/lean4/pull/2444) and [lean4#2480](https://github.com/leanprover/lean4/pull/2480)), so I am closing this issue.

The Lake repository is being deprecated and its issues transferred to [leanprover/lean4](https://github.com/leanprover/lean4). As `meta if` did solve this problem initially and leanprover/lean4#2755 is a newer issue that tracks some problems...

@gebner I just pushed a commit that incorporated some of your changes. I am curious what benefit, if any, the update has on performance. Could you run your benchmark against...

@gebner In that case, I will consider the core issue of this PR reasonably addressed and close it now. Thanks for all your help!

> After #132, the biggest cost centers are `Lean.Elab.parseImports` (22%), `computeFileHash` (17%), and loading the lakefile (14%). With the old addition of [`parseImports'`](https://github.com/leanprover/lean4/commit/1704debcd02e2a847b89ca3366f32fc61b9fdb11), and the new file hash caching ([lean4#2444](https://github.com/leanprover/lean4/pull/2444))...

@digama0 As the benchmark machine is not Gabriel's or Sebastian's, we do not have exactly comparable benchmarks. However, [this analysis](http://speed.lean-fro.org/lean4/compare/bab50d33-13a1-40c4-85a0-fda5f93f8b22/to/c1e1b587-091f-47cc-8a69-871e5e90cbf0?hash1=8b5a0230052e4afdcff85c965741a4380c782219) compares the benchmarks before and after the new changes (where...

@digama0 It is also worth noting that hashing optimization [only significantly impacted](http://speed.lean-fro.org/lean4/compare/7ef02c1c-37bd-4a78-b8fb-bc3ab93f4670/to/bab50d33-13a1-40c4-85a0-fda5f93f8b22?hash2=143e265d24ce3ce0ad543e6dbb18683b533eaeb3) the task-clock, not the wall-clock time. Lake is already very efficient at hashing files with its massive parallelism...

@arthurpaulino Yeah. #152 has sufficiently addressed this.