Analyzing build logs

Stream: CI

[Gabriel Ebner]

I've found it interesting to aggregate the profiling outputs from Scott's build log.

#!/usr/bin/env perl

while (<>) {
  $cumtime{$2} += $1 if /^\s+(\d+)ms\s+[0-9.]+%\s+(.*)$/;
}

print "$cumtime{$_} $_\n" foreach sort { $cumtime{$a} <=> $cumtime{$b} } keys %cumtime;

This gives a nice blame-list for slow tactics (cumulative time is in milliseconds):

...
58073 auto.safe_core._main._lambda_4
67043 tactic.ext._main._lambda_1
68427 tactic.ext
70998 tactic.apply_core
73371 _interaction._lambda_7
74751 tactic.interactive.finish
78445 tactic.mk_mapp
78489 tactic.ring.lift
79648 tactic.interactive.ring1
79649 tactic.interactive.ring1._lambda_3
79650 tactic.interactive.ring
79650 tactic.interactive.ring._lambda_1
80756 tactic.ring.ring_m.run
84920 tactic.chain_iter._main._lambda_2
84920 tactic.chain_iter
85168 _private.1069121511.rw_goal._lambda_2
86784 _private.1069121511.rw_goal._lambda_4
88774 tactic.interactive.simpa._lambda_4
89521 _interaction._lambda_8
101443 rw_core
102461 tactic.dsimp_target
104491 simp_lemmas.dsimplify
114809 tactic.interactive.ext
117660 _interaction._lambda_6
119817 tactic.interactive.simp_core_aux._lambda_2
120007 tactic.interactive.simp_core_aux._lambda_4
122103 interaction_monad.orelse'
125459 tactic.interactive.simpa._lambda_3
126261 interactive.loc.apply
143214 user_attribute.get_param
143345 extensional_attribute._main._lambda_7
143676 tactic.eval_expr
143945 extensional_attribute._main._lambda_8
145009 tactic.interactive.have._lambda_1
157744 _interaction._lambda_5
160440 user_attribute.get_cache
162149 tactic.tidy.default_tactics._lambda_4
162667 tactic.refine
165736 tactic.ext1
182106 tactic.tidy.default_tactics._lambda_9
215667 tactic.interactive.propagate_tags._lambda_3
255084 tactic.tidy.default_tactics._lambda_8
270155 _interaction._lambda_4
399829 tactic.focus1
429593 tactic.interactive.simpa
445935 tactic.interactive.exact
474880 tactic.interactive.dsimp
481659 tactic.replacer_core
481659 tactic.replacer
481659 tactic.replacer_core._main._lambda_4
558587 tactic.interactive.simpa._lambda_6
613680 tactic.tidy.default_tactics._lambda_3
662713 tactic.chain_many._main._lambda_1
662856 tactic.chain_single
662857 tactic.first
662857 tactic.chain_many
662867 tactic.chain_core
662890 tactic.tidy
662890 tactic.tidy.core
669626 tactic.try
728163 tactic.try_core
837059 tactic.to_expr
884716 _interaction._lambda_3
925051 tactic.interactive.simp_core_aux._lambda_5
948162 tactic.simp_target
1045350 tactic.interactive.simp_core_aux
1056608 _private.1304821429.all_goals_core._main._lambda_2
1056647 all_goals_core
1056660 tactic.all_goals
1102715 tactic.simplify
1309747 tactic.seq
1506343 tactic.solve1
1520303 interaction_monad.monad._lambda_9
1998068 interaction_monad_orelse
3406500 tactic.mk_simp_set
3424549 tactic.join_user_simp_lemmas
3439367 simp_lemmas.mk_default
3449179 tactic.mk_simp_set_core
4135671 tactic.interactive.simp_core
4215137 tactic.interactive.propagate_tags
5029124 _interaction._lambda_2
5690358 tactic.istep._lambda_1
5690414 scope_trace
5690440 tactic.istep
5695842 _interaction
6126456 tactic.step

This is how I spotted the ext slowness (#2674). Unfortunately there are few other surprises, we all know that simp is slow.

[Gabriel Ebner]

Ok, I didn't realize just how slow simp is. The build spends one goddamn hour on just creating the simp set...

[Johan Commelin]

One hour out of?

[Gabriel Ebner]

Out of four hours (246m).

[Gabriel Ebner]

lean#234