search

leanprover-community / mathlib4

The math library of Lean 4
https://leanprover-community.github.io/mathlib4_docs
Apache License 2.0
1.21k stars 259 forks source link

Spikes in compilation + maximum resident set size #7103

Open mattrobball opened 10 months ago

mattrobball commented 10 months ago

Twice now, I've run into situations where the maximum resident set size has spiked due to increased compilation of one declaration.

6998 and #6499 with Zulip threads

https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Debugging.20procedure

https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/shortcut.20for.20.60Seminorm.2EinstMulAction.60.3F

eric-wieser commented 10 months ago

7223 too

mattrobball commented 10 months ago

7308

mattrobball commented 9 months ago

https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/instance.20construction.20patterns/near/396183797 with leanprover/lean4#2644 we have a huge jump in compilation for RingTheory.Kaehler