Skip to content

Instantly share code, notes, and snippets.

@Kha

Kha/mathlib4.nixprof Secret

Created January 12, 2023 09:27
Show Gist options
  • Save Kha/564dcf3461ac8cb5715cda63dbea4f92 to your computer and use it in GitHub Desktop.
Save Kha/564dcf3461ac8cb5715cda63dbea4f92 to your computer and use it in GitHub Desktop.
Download ZIP
Raw
mathlib4.nixprof
$ nix run github:Kha/nixprof -- report --all --tred --merge-into-succ '-depRoot'
Critical path
time [s] [cum] drv
---------- ---- ------- ------ -------------------------------------
0.3 0.1% 0.3 0.1% Std.Lean.TagAttribute
0.6 0.2% 0.9 0.2% Std.Lean.AttributeExtra
1.8 0.5% 2.6 0.7% Std.Linter.UnnecessarySeqFocus
0.2 0.1% 2.8 0.8% Std.Linter
1.9 0.5% 4.8 1.3% Std.Tactic.Basic
1.3 0.4% 6.1 1.7% Std.Logic
1.5 0.4% 7.6 2.1% Std.Classes.LawfulMonad
2.1 0.6% 9.7 2.7% Std.Data.Array.Init.Lemmas
7.8 2.2% 17.5 4.9% Std.Data.List.Basic
6.6 1.9% 24.1 6.8% Std.Data.List.Lemmas
3.9 1.1% 28.1 7.9% Std.Data.Array.Lemmas
3.5 1.0% 31.6 8.9% Std.Data.HashMap.WF
0.2 0.1% 31.8 8.9% Std.Data.HashMap
0.5 0.1% 32.3 9.1% Std
1.3 0.4% 33.6 9.4% Mathlib.Tactic.Basic
1.5 0.4% 35.1 9.9% Mathlib.Init.Logic
1.5 0.4% 36.7 10.3% Mathlib.Init.Algebra.Order
0.7 0.2% 37.4 10.5% Mathlib.Init.Algebra.Functions
2.2 0.6% 39.6 11.1% Mathlib.Init.Data.Nat.Lemmas
3.6 1.0% 43.2 12.1% Mathlib.Logic.Function.Basic
5.5 1.6% 48.7 13.7% Mathlib.Algebra.Group.Defs
2.3 0.7% 51.0 14.3% Mathlib.Data.Nat.Cast.Defs
4.5 1.3% 55.5 15.6% Mathlib.Tactic.NormCast.Tactic
0.5 0.1% 56.0 15.7% Mathlib.Tactic.NormCast
0.6 0.2% 56.6 15.9% Mathlib.Data.FunLike.Basic
0.5 0.1% 57.1 16.0% Mathlib.Data.FunLike.Embedding
0.6 0.2% 57.8 16.2% Mathlib.Data.FunLike.Equiv
4.9 1.4% 62.6 17.6% Mathlib.Logic.Equiv.Defs
1.6 0.5% 64.3 18.0% Mathlib.Order.Synonym
1.7 0.5% 66.0 18.5% Mathlib.Order.Compare
3.2 0.9% 69.2 19.4% Mathlib.Order.Monotone.Basic
5.7 1.6% 74.9 21.0% Mathlib.Order.Lattice
4.0 1.1% 78.9 22.1% Mathlib.Order.BoundedOrder
10.8 3.0% 89.7 25.2% Mathlib.Order.WithBot
8.9 2.5% 98.6 27.7% Mathlib.Order.Hom.Basic
10.2 2.9% 108.8 30.5% Mathlib.Algebra.Order.Group.Defs
33.2 9.3% 142.0 39.8% Mathlib.Algebra.Order.Ring.Defs
2.8 0.8% 144.8 40.6% Mathlib.Algebra.Order.Ring.Canonical
8.0 2.2% 152.8 42.9% Mathlib.Data.Nat.Order.Basic
14.5 4.1% 167.3 47.0% Mathlib.Algebra.GroupPower.Ring
16.4 4.6% 183.7 51.6% Mathlib.Algebra.GroupPower.Order
2.8 0.8% 186.5 52.3% Mathlib.Data.Nat.Pow
27.3 7.7% 213.8 60.0% Mathlib.Algebra.GroupPower.Lemmas
5.6 1.6% 219.4 61.6% Mathlib.Tactic.NormNum.Basic
0.8 0.2% 220.2 61.8% Mathlib.Tactic.NormNum
1.3 0.4% 221.5 62.2% Mathlib.Util.AtomM
27.6 7.8% 249.1 69.9% Mathlib.Tactic.Ring.Basic
4.7 1.3% 253.8 71.3% Mathlib.Tactic.Ring.RingNF
0.8 0.2% 254.7 71.5% Mathlib.Tactic.Ring
3.4 1.0% 258.1 72.4% Mathlib.Tactic.Linarith.Datatypes
22.6 6.4% 280.7 78.8% Mathlib.Tactic.Linarith.Preprocessing
2.8 0.8% 283.5 79.6% Mathlib.Tactic.Linarith.Frontend
0.7 0.2% 284.1 79.8% Mathlib.Tactic.Linarith
26.4 7.4% 310.5 87.2% Mathlib.Algebra.Order.Floor
5.5 1.6% 316.1 88.7% Mathlib.Data.Rat.Floor
33.5 9.4% 349.6 98.1% Mathlib.Algebra.Order.Archimedean
3.9 1.1% 353.5 99.2% Mathlib
2.8 0.8% 356.2 100.0% Mathlib-depRoot
Average contribution to critical paths
time [s] [cum] drv
---------- ----- ------- ------ ------------------------------------------------
18.2 12.0% 18.2 12.0% Mathlib.Algebra.Order.Archimedean
14.1 9.2% 32.2 21.2% Mathlib.Algebra.Order.Floor
13.5 8.9% 45.8 30.1% Mathlib.Tactic.Ring.Basic
13.2 8.7% 59.0 38.8% Mathlib.Algebra.GroupPower.Lemmas
11.3 7.4% 70.3 46.2% Mathlib.Tactic.Linarith.Preprocessing
9.5 6.2% 79.7 52.5% Mathlib.Algebra.Order.Ring.Defs
7.6 5.0% 87.4 57.5% Mathlib.Algebra.GroupPower.Order
6.5 4.3% 93.9 61.8% Mathlib.Algebra.GroupPower.Ring
3.9 2.6% 97.7 64.3% Mathlib
3.0 2.0% 100.7 66.3% Mathlib.Data.Rat.Floor
2.8 1.8% 103.5 68.1% Mathlib-depRoot
2.7 1.8% 106.2 69.9% Mathlib.Tactic.NormNum.Basic
2.7 1.8% 108.9 71.7% Mathlib.Algebra.Star.Basic
2.6 1.7% 111.5 73.4% Mathlib.Algebra.Order.Group.Defs
2.5 1.6% 114.0 75.0% Mathlib.Order.WithBot
2.4 1.6% 116.4 76.6% Mathlib.Data.Nat.Order.Basic
2.3 1.5% 118.7 78.1% Mathlib.Tactic.Ring.RingNF
2.2 1.5% 121.0 79.6% Mathlib.Order.Hom.Basic
1.7 1.1% 122.7 80.7% Mathlib.Tactic.Linarith.Datatypes
1.4 0.9% 124.0 81.6% Mathlib.Tactic.Linarith.Frontend
1.4 0.9% 125.4 82.5% Mathlib.Algebra.Hom.Ring
1.3 0.9% 126.7 83.4% Mathlib.Data.Rat.Cast
1.3 0.8% 128.0 84.2% Mathlib.Data.Nat.Pow
1.3 0.8% 129.2 85.0% Mathlib.Order.Lattice
1.2 0.8% 130.4 85.8% Mathlib.Data.Set.Basic
1.0 0.6% 131.4 86.4% Mathlib.Logic.Equiv.Defs
0.9 0.6% 132.3 87.0% Mathlib.Algebra.Group.Defs
0.9 0.6% 133.2 87.6% Mathlib.Order.BoundedOrder
0.8 0.6% 134.0 88.2% Mathlib.Algebra.Order.Ring.Canonical
0.8 0.5% 134.8 88.7% Mathlib.Tactic.NormCast.Tactic
0.7 0.5% 135.5 89.2% Mathlib.Order.Monotone.Basic
0.7 0.4% 136.2 89.6% Mathlib.Order.SymmDiff
0.6 0.4% 136.8 90.0% Aesop.Search.Main
0.6 0.4% 137.4 90.4% Mathlib.Util.AtomM
0.6 0.4% 138.0 90.8% Mathlib.Logic.Function.Basic
0.6 0.4% 138.6 91.2% Mathlib.Data.Set.Image
0.5 0.4% 139.1 91.5% Mathlib.Order.BooleanAlgebra
0.5 0.3% 139.6 91.9% Aesop.Search.Expansion
0.4 0.3% 140.0 92.1% Mathlib.Tactic.Ring
0.4 0.3% 140.4 92.4% Mathlib.Data.Nat.Cast.Defs
0.4 0.2% 140.8 92.6% Mathlib.Tactic.NormNum
0.4 0.2% 141.2 92.9% Mathlib.Order.Compare
0.3 0.2% 141.5 93.1% Std.Data.List.Lemmas
0.3 0.2% 141.9 93.3% Mathlib.Order.Synonym
0.3 0.2% 142.2 93.6% Mathlib.Tactic.Linarith
0.3 0.2% 142.5 93.8% Mathlib.Init.Data.Nat.Lemmas
0.3 0.2% 142.9 94.0% Mathlib.Algebra.Star.Unitary
0.3 0.2% 143.1 94.2% Std.Data.List.Basic
0.3 0.2% 143.4 94.4% Mathlib.Algebra.Order.Field.Basic
0.2 0.1% 143.6 94.5% Mathlib.Order.CompleteBooleanAlgebra
0.2 0.1% 143.9 94.6% Std.Data.Array.Lemmas
0.2 0.1% 144.1 94.8% Std.Data.HashMap.WF
0.2 0.1% 144.3 94.9% Mathlib.Init.Algebra.Order
0.2 0.1% 144.5 95.0% Mathlib.Init.Logic
0.2 0.1% 144.6 95.2% Mathlib.Data.Real.CauSeq
0.2 0.1% 144.8 95.3% Mathlib.Algebra.Order.Field.InjSurj
0.2 0.1% 145.0 95.4% Mathlib.CategoryTheory.Whiskering
0.2 0.1% 145.2 95.5% Mathlib.GroupTheory.Perm.Basic
0.2 0.1% 145.4 95.6% Mathlib.Algebra.Ring.Prod
0.2 0.1% 145.5 95.7% Mathlib.Data.Set.Lattice
0.2 0.1% 145.7 95.8% Mathlib.Tactic.Basic
0.1 0.1% 145.8 95.9% Mathlib.Mathport.Syntax
0.1 0.1% 145.9 96.0% Mathlib.Algebra.Order.WithZero
0.1 0.1% 146.0 96.1% Mathlib.Data.FunLike.Equiv
0.1 0.1% 146.2 96.2% Mathlib.Order.Atoms
0.1 0.1% 146.3 96.2% Mathlib.Data.FunLike.Basic
0.1 0.1% 146.4 96.3% Aesop.Main
0.1 0.1% 146.5 96.4% Mathlib.Algebra.Ring.Aut
0.1 0.1% 146.6 96.4% Aesop.Tree.Check
0.1 0.1% 146.7 96.5% Mathlib.Data.FunLike.Embedding
0.1 0.1% 146.7 96.5% Mathlib.Logic.Equiv.Basic
0.1 0.1% 146.8 96.6% Mathlib.Init.Algebra.Functions
0.1 0.1% 146.9 96.7% Mathlib.Tactic.ToAdditive
0.1 0.1% 147.0 96.7% Mathlib.GroupTheory.Submonoid.Operations
0.1 0.1% 147.1 96.8% Aesop.RuleSet
0.1 0.1% 147.2 96.8% Mathlib.GroupTheory.GroupAction.Group
0.1 0.1% 147.3 96.9% Mathlib.Tactic.NormCast
0.1 0.1% 147.4 97.0% Aesop.Search.SearchM
0.1 0.1% 147.4 97.0% Aesop.Search.ExpandSafePrefix
0.1 0.1% 147.5 97.1% Mathlib.Data.Int.AbsoluteValue
0.1 0.1% 147.6 97.1% Aesop.Test.Persistence1
0.1 0.1% 147.7 97.2% Aesop
0.1 0.0% 147.8 97.2% Mathlib.Order.CompleteLattice
0.1 0.0% 147.8 97.3% Mathlib.Algebra.Hom.Aut
0.1 0.0% 147.9 97.3% Std.Data.Array.Init.Lemmas
0.1 0.0% 148.0 97.4% Mathlib.Data.List.Basic
0.1 0.0% 148.0 97.4% Mathlib.Algebra.Group.Units
0.1 0.0% 148.1 97.4% Mathlib.Algebra.Module.Basic
0.1 0.0% 148.2 97.5% Mathlib.GroupTheory.GroupAction.Defs
0.1 0.0% 148.2 97.5% Std.Data.RBMap.WF
0.1 0.0% 148.3 97.6% Mathlib.Data.List.BigOperators.Basic
0.1 0.0% 148.4 97.6% Aesop.Test.Persistence3
0.1 0.0% 148.4 97.7% Aesop.Search.RuleSelection
0.1 0.0% 148.5 97.7% Mathlib.Algebra.GCDMonoid.Basic
0.1 0.0% 148.6 97.8% Aesop.Test
0.1 0.0% 148.6 97.8% Aesop.Tree.Data
0.1 0.0% 148.7 97.8% Mathlib.Order.ModularLattice
0.1 0.0% 148.8 97.9% Mathlib.Order.RelIso.Basic
0.1 0.0% 148.8 97.9% Std
0.1 0.0% 148.9 98.0% Mathlib.Data.Rat.Order
0.1 0.0% 148.9 98.0% Mathlib.Algebra.Order.Ring.InjSurj
0.1 0.0% 149.0 98.0% Mathlib.Order.Heyting.Basic
0.1 0.0% 149.0 98.1% Mathlib.Data.List.Zip
0.1 0.0% 149.1 98.1% Mathlib.CategoryTheory.Functor.Category
0.1 0.0% 149.1 98.1% Mathlib.Order.ConditionallyCompleteLattice.Basic
0.1 0.0% 149.2 98.2% Mathlib.Tactic.Simps.Basic
0.0 0.0% 152.0 100.0% [total]
Simulated build times by processor count up optimal power of two
#CPUs time [s] CPU% [avg]
------- ----------- ------------
1 3254.840521 100%
2 1649.018548 197%
4 862.331974 377%
8 492.543853 661%
16 367.825029 885%
32 359.791283 905%
64 358.219489 909%
128 357.863204 910%
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment