etc/isar/profiling.txt


1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217

Profiling of hundred theorems:

proof-shell-filter                                              206         0.5755520000  0.0027939417
proof-shell-filter-manage-output                                206         0.4828650000  0.0023440048
proof-shell-exec-loop                                           206         0.479615      0.0023282281
proof-done-advancing                                            204         0.3241909999  0.0015891715
proof-done-advancing-save                                       100         0.2885119999  0.0028851199
proof-make-goalsave                                             100         0.2780209999  0.0027802099
pg-add-proof-element                                            100         0.2667299999  0.0026672999
proof-next-element-id                                           100         0.2568640000  0.0025686400
proof-element-id                                                100         0.2559739999  0.0025597399
proof-shell-insert                                              206         0.1490790000  0.0007236844
scomint-send-input                                              206         0.0973649999  0.0004726456
scomint-send-string                                             206         0.0899980000  0.0004368834
pg-remove-specials                                              206         0.0822929999  0.0003994805
isar-preprocessing                                              206         0.0361179999  0.0001753300
proof-toolbar-next-enable-p                                     638         0.0286260000  4.486...e-05
isar-command-wrapping                                           206         0.0269059999  0.0001306116
proof-locked-region-full-p                                      639         0.0268030000  4.194...e-05
pg-set-span-helphighlights                                      304         0.0225119999  7.405...e-05
isar-positions-of                                               206         0.0202500000  9.830...e-05
proof-toolbar-use-enable-p                                      319         0.0138090000  4.328...e-05
proof-set-overlay-arrow                                         204         0.0115210000  5.647...e-05
proof-string-match                                              1526        0.0104410000  6.842...e-06
proof-shell-available-p                                         2233        0.0092940000  4.162...e-06
proof-done-advancing-other                                      104         0.007964      7.657...e-05
pg-last-output-displayform                                      304         0.0075990000  2.499...e-05
isar-string-wrapping                                            412         0.0063830000  1.549...e-05
proof-shell-strip-output-markup                                 304         0.0059760000  1.965...e-05
isar-strip-output-markup                                        305         0.0048359999  1.585...e-05
proof-replace-regexp-in-string                                  412         0.0047720000  1.158...e-05
isar-shell-adjust-line-width                                    206         0.00416       2.019...e-05
isar-global-save-command-p                                      100         0.0038479999  3.847...e-05
proof-shell-process-urgent-messages                             206         0.003735      1.813...e-05
proof-string-match-safe                                         204         0.0032319999  1.584...e-05
proof-toolbar-state-enable-p                                    319         0.0031699999  9.937...e-06
pg-processing-complete-hint                                     1           0.002853      0.002853
scomint-check-proc                                              2441        0.0028120000  1.151...e-06
proof-get-name-from-goal                                        100         0.0026769999  2.676...e-05
proof-toolbar-retract-enable-p                                  319         0.0025379999  7.956...e-06
proof-toolbar-undo-enable-p                                     319         0.0024359999  7.636...e-06
proof-toolbar-delete-enable-p                                   319         0.0023529999  7.376...e-06
isar-goal-command-p                                             204         0.0021389999  1.048...e-05
proof-toolbar-find-enable-p                                     319         0.0020489999  6.423...e-06
proof-toolbar-context-enable-p                                  319         0.0018939999  5.937...e-06
proof-toolbar-info-enable-p                                     319         0.0018169999  5.695...e-06
proof-toolbar-command-enable-p                                  319         0.0017689999  5.545...e-06
pg-add-element                                                  100         0.0016860000  1.686...e-05
proof-shell-classify-output                                     206         0.0016479999  7.999...e-06
proof-locked-region-empty-p                                     320         0.0014510000  4.534...e-06
pg-span-name                                                    304         0.0012320000  4.052...e-06
proof-process-buffer                                            1           0.001196      0.001196
pg-add-to-input-history                                         104         0.0011950000  1.149...e-05
proof-assert-until-point-interactive                            1           0.001159      0.001159
proof-assert-until-point                                        1           0.001155      0.001155
proof-unprocessed-begin                                         1126        0.0010770000  9.564...e-07
proof-shell-live-buffer                                         206         0.0010610000  5.150...e-06
proof-assert-semis                                              1           0.001013      0.001013
proof-splice-separator                                          206         0.0007109999  3.451...e-06
proof-extend-queue                                              1           0.000638      0.000638
proof-append-alist                                              1           0.00063       0.00063
proof-semis-to-vanillas                                         1           0.000347      0.000347
proof-next-element-count                                        100         0.0002829999  2.829...e-06
proof-shell-process-urgent-message                              1           0.00025       0.00025
proof-toolbar-goto-enable-p                                     319         0.0002259999  7.084...e-07
proof-toolbar-interrupt-enable-p                                319         0.0001709999  5.360...e-07
proof-debug                                                     100         0.0001189999  1.189...e-06
proof-segment-up-to-using-cache                                 1           9.6e-05       9.6e-05
proof-segment-cache-contents-for                                1           8.4e-05       8.4e-05
pg-response-display-with-face                                   2           7.5e-05       3.75e-05
proof-shell-message                                             1           7e-05         7e-05
pg-response-maybe-erase                                         2           5e-05         2.5e-05
pg-hint                                                         1           3.9e-05       3.9e-05
proof-re-search-backward                                        1           3e-05         3e-05
proof-shell-ready-prover                                        2           2.100...e-05  1.050...e-05
proof-shell-handle-delayed-output                               1           2.1e-05       2.1e-05
proof-activate-scripting                                        1           1.7e-05       1.7e-05
proof-maybe-follow-locked-end                                   1           1.6e-05       1.6e-05
proof-shell-start                                               2           1.5e-05       7.5e-06
pg-response-display                                             1           1.4e-05       1.4e-05
proof-grab-lock                                                 1           1.2e-05       1.2e-05
proof-script-next-command-advance                               1           7e-06         7e-06
proof-shell-strip-eager-annotations                             1           7e-06         7e-06
proof-shell-start-silent-item                                   1           6e-06         6e-06
proof-shell-action-list-item                                    2           4e-06         2e-06
proof-shell-stop-silent-item                                    1           4e-06         4e-06
proof-queue-or-locked-end                                       4           3e-06         7.5e-07
proof-shell-should-be-silent                                    1           2e-06         2e-06
proof-shell-set-silent                                          1           1e-06         1e-06
proof-shell-clear-silent                                        1           1e-06         1e-06
proof-pbp-focus-on-first-goal                                   1           1e-06         1e-06
proof-display-and-keep-buffer                                   1           1e-06         1e-06
proof-release-lock                                              1           1e-06         1e-06
pg-finish-tracing-display                                       1           1e-06         1e-06


Profiling AThousandTheorems:

proof-shell-filter                                              2009        4.2185289999  0.0020998153
proof-shell-filter-manage-output                                2008        3.7156680000  0.0018504322
proof-process-buffer                                            1           3.681492      3.681492
proof-assert-until-point-interactive                            1           3.681391      3.681391
proof-assert-until-point                                        1           3.681388      3.681388
proof-shell-exec-loop                                           2008        3.6569860000  0.0018212081
proof-assert-semis                                              1           2.165613      2.165613
proof-activate-scripting                                        1           2.1626339999  2.1626339999
proof-shell-wait                                                3           2.157879      0.719293
proof-shell-insert                                              2008        1.8324589999  0.0009125791
proof-done-advancing                                            2004        1.7108090000  0.0008536971
proof-segment-up-to-using-cache                                 1           1.515725      1.515725
proof-segment-up-to                                             1           1.5153910000  1.5153910000
proof-segment-up-to-cmdstart                                    1           1.515388      1.515388
proof-looking-at-syntactic-context                              2012        1.2962439999  0.0006442564
isar-syntactic-context                                          2012        1.2880049999  0.0006401615
proof-looking-at-syntactic-context-default                      2012        1.283686      0.0006380149
proof-buffer-syntactic-context                                  2013        1.2504469999  0.0006211857
proof-register-possibly-new-processed-file                      2           1.147767      0.5738835
proof-deactivate-scripting                                      1           1.146929      1.146929
proof-shell-invisible-command                                   2           1.144748      0.572374
proof-cd-sync                                                   1           1.014265      1.014265
scomint-send-input                                              2008        1.0111659999  0.0005035687
proof-toolbar-next-enable-p                                     7434        0.6904569999  9.287...e-05
proof-done-advancing-save                                       1000        0.6694850000  0.0006694850
proof-locked-region-full-p                                      7437        0.6680110000  8.982...e-05
isar-preprocessing                                              2008        0.5888010000  0.0002932275
scomint-send-string                                             2008        0.5238210000  0.0002608670
isar-command-wrapping                                           2008        0.4266709999  0.0002124855
isar-positions-of                                               2008        0.2837250000  0.0001412973
proof-make-goalsave                                             1000        0.2802490000  0.0002802490
pg-set-span-helphighlights                                      3004        0.2778229999  9.248...e-05
pg-remove-specials                                              2008        0.2700440000  0.0001344840
proof-toolbar-use-enable-p                                      3717        0.2482730000  6.679...e-05
proof-shell-available-p                                         26019       0.1759880000  6.763...e-06
proof-re-search-forward                                         2064        0.1741260000  8.436...e-05
pg-add-proof-element                                            1000        0.1635090000  0.0001635090
proof-string-match                                              15032       0.1542850000  1.026...e-05
proof-done-advancing-other                                      1004        0.1512260000  0.0001506235
isar-string-wrapping                                            4015        0.1382279999  3.442...e-05
proof-get-name-from-goal                                        1000        0.1235100000  0.0001235100
proof-replace-regexp-in-string                                  4015        0.1221689999  3.042...e-05
isar-global-save-command-p                                      1000        0.1135740000  0.0001135740
proof-string-match-safe                                         2004        0.1066289999  5.320...e-05
proof-toolbar-command-enable-p                                  3717        0.0918040000  2.469...e-05
proof-set-overlay-arrow                                         2004        0.0877379999  4.378...e-05
pg-add-to-input-history                                         1004        0.0811079999  8.078...e-05
pg-last-output-displayform                                      3004        0.0799419999  2.661...e-05
pg-add-element                                                  1000        0.0758799999  7.587...e-05
proof-shell-process-urgent-messages                             2009        0.0691360000  3.441...e-05
proof-shell-strip-output-markup                                 3006        0.0621240000  2.066...e-05
isar-strip-output-markup                                        3008        0.0508979999  1.692...e-05
isar-shell-adjust-line-width                                    2008        0.0436570000  2.174...e-05
proof-shell-classify-output                                     2008        0.0423230000  2.107...e-05
proof-toolbar-state-enable-p                                    3717        0.0384680000  1.034...e-05
scomint-check-proc                                              28033       0.0319450000  1.139...e-06
proof-toolbar-retract-enable-p                                  3717        0.0305389999  8.216...e-06
isar-goal-command-p                                             2004        0.026745      1.334...e-05
proof-cmdstart-add-segment-for-cmd                              2004        0.0246840000  1.231...e-05
proof-toolbar-delete-enable-p                                   3717        0.0242569999  6.525...e-06
proof-toolbar-undo-enable-p                                     3717        0.0241040000  6.484...e-06
proof-toolbar-context-enable-p                                  3717        0.0233320000  6.277...e-06
proof-toolbar-find-enable-p                                     3717        0.0226730000  6.099...e-06
proof-toolbar-info-enable-p                                     3717        0.0210330000  5.658...e-06
proof-locked-region-empty-p                                     3722        0.0176580000  4.744...e-06
proof-looking-at-safe                                           4012        0.0171930000  4.285...e-06
proof-next-element-id                                           1000        0.0129890000  1.298...e-05
pg-span-name                                                    3004        0.0127430000  4.242...e-06
proof-shell-live-buffer                                         2008        0.0114760000  5.715...e-06
proof-unprocessed-begin                                         11480       0.0112319999  9.783...e-07
proof-looking-at                                                4012        0.0082560000  2.057...e-06
proof-splice-separator                                          2008        0.0070060000  3.489...e-06
pg-processing-complete-hint                                     3           0.0058870000  0.0019623333
proof-element-id                                                1000        0.0039640000  3.964...e-06
proof-next-element-count                                        1000        0.0028809999  2.880...e-06
proof-toolbar-goto-enable-p                                     3717        0.0027980000  7.527...e-07
proof-semis-to-vanillas                                         1           0.002604      0.002604
proof-toolbar-interrupt-enable-p                                3717        0.0022529999  6.061...e-07
proof-shell-process-urgent-message                              3           0.001543      0.0005143333
proof-debug                                                     1003        0.0012860000  1.282...e-06
proof-append-alist                                              3           0.000957      0.000319
isar-match-nesting                                              51          0.000897      1.758...e-05
proof-start-queue                                               2           0.000614      0.000307
proof-unregister-buffer-file-name                               1           0.000609      0.000609
proof-cd                                                        1           0.000429      0.000429
proof-extend-queue                                              1           0.00036       0.00036
proof-shell-message                                             2           0.000257      0.0001285
pg-response-display-with-face                                   5           0.0001839999  3.679...e-05
proof-format-filename                                           2           0.000173      8.65e-05
pg-response-maybe-erase                                         5           0.000124      2.48e-05
proof-shell-handle-delayed-output                               3           0.000117      3.9e-05
pg-response-display                                             3           9.5e-05       3.166...e-05
pg-hint                                                         1           7.1e-05       7.1e-05
proof-format                                                    10          6.1e-05       6.1e-06
proof-shell-ready-prover                                        6           5.899...e-05  9.833...e-06
proof-shell-start                                               6           3.8e-05       6.333...e-06
proof-grab-lock                                                 3           3.5e-05       1.166...e-05
proof-re-search-backward                                        1           3.3e-05       3.3e-05
proof-init-segmentation                                         1           2.4e-05       2.4e-05
proof-shell-strip-eager-annotations                             2           1.5e-05       7.5e-06
proof-complete-buffer-atomic                                    1           1.4e-05       1.4e-05
proof-maybe-follow-locked-end                                   1           1.1e-05       1.1e-05
proof-shell-action-list-item                                    4           1.099...e-05  2.749...e-06
proof-queue-or-locked-end                                       4           8e-06         2e-06
proof-script-end                                                1           7e-06         7e-06
proof-shell-stop-silent-item                                    1           6e-06         6e-06
proof-shell-should-be-silent                                    3           6e-06         2e-06
proof-shell-start-silent-item                                   1           6e-06         6e-06
proof-span-read-only                                            2           4e-06         2e-06
proof-display-and-keep-buffer                                   3           4e-06         1.333...e-06
proof-pbp-focus-on-first-goal                                   3           3e-06         1e-06
proof-release-lock                                              3           3e-06         1e-06
pg-finish-tracing-display                                       3           3e-06         1e-06
proof-done-invisible                                            2           2e-06         1e-06
proof-script-next-command-advance                               1           2e-06         2e-06
pg-clear-script-portions                                        1           2e-06         2e-06
proof-shell-set-silent                                          1           1e-06         1e-06
proof-shell-clear-silent                                        1           1e-06         1e-06
pg-clear-input-ring                                             1           1e-06         1e-06