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
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322

Wed Aug 18 2010.  See Trac #324.

-----------------------------------------------------------------

Interactive:  C-c C-n

### 12.461s elapsed time, 0.514s cpu time, 0.108s GC time

scomint-output-filter                                           206         3.6426039999  0.0176825436
proof-shell-filter                                              206         3.629433      0.0176186067
proof-shell-filter-manage-output                                206         3.6140779999  0.0175440679
proof-shell-exec-loop                                           206         3.5814560000  0.0173857087
mapc                                                            208         3.4833689999  0.0167469663
proof-shell-invoke-callback                                     206         3.4798549999  0.0168924999
proof-done-advancing                                            204         3.4786709999  0.0170523088
proof-done-advancing-other                                      104         3.2460199999  0.0312117307
pg-add-element                                                  204         3.2301699999  0.0158341666
proof-debug                                                     99          3.2140250000  0.0324648989
pg-autotest-message                                             99          3.211558      0.0324399797
redisplay                                                       99          3.140468      0.0317218989
proof-done-advancing-save                                       100         0.107982      0.00107982
proof-process-buffer                                            1           0.103025      0.103025
proof-assert-until-point-interactive                            1           0.102849      0.102849
proof-assert-until-point                                        1           0.102845      0.102845
proof-make-goalsave                                             100         0.0734089999  0.0007340899
proof-assert-semis                                              1           0.0729        0.0729
proof-semis-to-vanillas                                         1           0.069353      0.069353
span-at-before                                                  200         0.0607209999  0.0003036049
proof-shell-insert-action-item                                  206         0.0561400000  0.0002725242
proof-shell-insert                                              206         0.0552149999  0.0002680339
pg-set-span-helphighlights                                      304         0.0523910000  0.0001723388
pg-add-proof-element                                            100         0.0507439999  0.0005074399
isar-global-save-command-p                                      100         0.0403249999  0.0004032499
isar-command-wrapping                                           204         0.0389439999  0.0001909019
isar-positions-of                                               204         0.0342390000  0.0001678382
proof-segment-up-to-using-cache                                 1           0.029667      0.029667
proof-segment-up-to                                             1           0.029599      0.029599
proof-segment-up-to-parser                                      1           0.02959       0.02959
proof-script-generic-parse-cmdstart                             204         0.0265809999  0.0001302990
span-live-p                                                     408         0.0245460000  6.016...e-05
span-property                                                   2226        0.0242540000  1.089...e-05
proof-set-locked-end                                            204         0.0179210000  8.784...e-05
proof-set-locked-endpoints                                      204         0.0169129999  8.290...e-05
goto-char                                                       3401        0.0159649999  4.694...e-06
replace-regexp-in-string                                        613         0.0154579999  2.521...e-05
pg-processing-complete-hint                                     1           0.014814      0.014814
proof-buffer-syntactic-context                                  411         0.0145479999  3.539...e-05
pg-last-output-displayform                                      304         0.0140980000  4.637...e-05
proof-buffer-syntactic-context-emulate                          411         0.0135870000  3.305...e-05
span-set-property                                               4968        0.0131570000  2.648...e-06
proof-shell-strip-output-markup                                 202         0.0121529999  6.016...e-05
isar-strip-output-markup                                        202         0.0115120000  5.699...e-05
proof-set-overlay-arrow                                         204         0.0110750000  5.428...e-05
pg-hint                                                         1           0.010877      0.010877
scomint-send-input                                              206         0.0096710000  4.694...e-05
skip-chars-forward                                              917         0.0088720000  9.675...e-06
string-match                                                    3879        0.0085580000  2.206...e-06
proof-string-match                                              1114        0.0083859999  7.527...e-06
re-search-forward                                               1084        0.0076900000  7.094...e-06
proof-shell-process-urgent-messages                             206         0.0072959999  3.541...e-05
proof-shell-handle-immediate-output                             206         0.0069180000  3.358...e-05
span-set-endpoints                                              409         0.0060590000  1.481...e-05
isar-preprocessing                                              206         0.0057689999  2.800...e-05
isar-string-wrapping                                            408         0.0057090000  1.399...e-05
move-overlay                                                    410         0.0048900000  1.192...e-05
insert                                                          718         0.0043259999  6.025...e-06
proof-set-queue-start                                           204         0.0039419999  1.932...e-05
proof-next-element-id                                           204         0.0038919999  1.907...e-05
proof-re-search-forward-safe                                    824         0.0038370000  4.656...e-06
proof-script-delete-secondary-spans                             1           0.003218      0.003218
span-delete-spans                                               1           0.003215      0.003215
span-mapc-spans                                                 1           0.003214      0.003214
span-set-start                                                  204         0.003181      1.559...e-05
pg-add-to-input-history                                         204         0.0030040000  1.472...e-05
isar-goal-command-p                                             204         0.0029059999  1.424...e-05
span-make                                                       608         0.0029059999  4.779...e-06
span-end                                                        928         0.0026819999  2.890...e-06
proof-get-name-from-goal                                        100         0.0024339999  2.433...e-05
proof-string-match-safe                                         204         0.0024330000  1.192...e-05
overlay-put                                                     4970        0.0023869999  4.802...e-07
span-delete                                                     304         0.002174      7.151...e-06
pg-span-name                                                    102         0.00199       1.950...e-05
proof-element-id                                                204         0.0019369999  9.495...e-06
span-start                                                      604         0.0018080000  2.993...e-06
replace-match                                                   1009        0.0016779999  1.663...e-06
skip-chars-backward                                             207         0.0015489999  7.483...e-06
make-overlay                                                    609         0.0014599999  2.397...e-06
proof-shell-slurp-comments                                      207         0.0012420000  6.000...e-06
delete-overlay                                                  306         0.0011619999  3.797...e-06
font-lock-fontify-region                                        2           0.000982      0.000491
font-lock-default-fontify-region                                2           0.0009649999  0.0004824999
set-marker                                                      1853        0.0009280000  5.008...e-07
proof-shell-handle-delayed-output                               1           0.000917      0.000917
proof-shell-display-output-as-response                          1           0.000892      0.000892
pg-response-display                                             1           0.000888      0.000888
font-lock-fontify-keywords-region                               2           0.000882      0.000441
proof-display-and-keep-buffer                                   1           0.00087       0.00087
kill-buffer                                                     4           0.000787      0.00019675
proof-next-element-count                                        204         0.0006769999  3.318...e-06
spans-at-region-prop                                            1           0.000641      0.000641
overlay-end                                                     1129        0.0004920000  4.357...e-07
match-string                                                    308         0.0004569999  1.483...e-06
marker-position                                                 1237        0.0004520000  3.654...e-07
buffer-live-p                                                   723         0.0003860000  5.338...e-07
isar-shell-adjust-line-width                                    206         0.0003380000  1.640...e-06
get-buffer-process                                              212         0.0002819999  1.330...e-06
proof-extend-queue                                              1           0.000254      0.000254
proof-shell-process-urgent-message                              1           0.00024       0.00024
overlay-start                                                   605         0.0002349999  3.884...e-07
proof-add-to-queue                                              1           0.000231      0.000231
proof-only-whitespace-to-locked-region-p                        1           0.000192      0.000192
isar-font-lock-fontify-syntactically-region                     2           0.000184      9.2e-05
nreverse                                                        209         0.0001679999  8.038...e-07
proof-shell-process-urgent-message-default                      1           0.000163      0.000163
proof-get-window-for-buffer                                     1           0.000161      0.000161
proof-re-search-backward                                        1           0.000157      0.000157
re-search-backward                                              1           8.5e-05       8.5e-05
pg-response-display-with-face                                   2           7.999...e-05  3.999...e-05
proof-queue-or-locked-end                                       6           7.2e-05       1.2e-05
pg-response-maybe-erase                                         2           5.9e-05       2.95e-05
proof-shell-ready-prover                                        2           5.3e-05       2.65e-05
proof-looking-at-safe                                           8           5.1e-05       6.375e-06
proof-shell-start                                               2           4.6e-05       2.3e-05
proof-unprocessed-begin                                         5           4.3e-05       8.6e-06
isar-match-nesting                                              1           4.3e-05       4.3e-05
proof-activate-scripting                                        1           4.2e-05       4.2e-05
proof-shell-live-buffer                                         2           3.9e-05       1.95e-05
proof-looking-at                                                7           3.6e-05       5.142...e-06
proof-re-search-forward                                         2           3.500...e-05  1.750...e-05
proof-detach-queue                                              1           3.1e-05       3.1e-05
scomint-check-proc                                              2           2.9e-05       1.45e-05
span-detach                                                     1           2.8e-05       2.8e-05
proof-maybe-follow-locked-end                                   1           2.7e-05       2.7e-05
proof-locked-region-full-p                                      1           2.7e-05       2.7e-05
proof-grab-lock                                                 1           2.4e-05       2.4e-05
font-lock-fontify-syntactically-region                          1           2.3e-05       2.3e-05
font-lock-mode                                                  1           2e-05         2e-05
font-lock-unfontify-region                                      2           1.7e-05       8.5e-06
font-lock-extend-jit-lock-region-after-change                   3           1.1e-05       3.666...e-06
proof-locked-region-empty-p                                     1           1e-05         1e-05
proof-set-queue-endpoints                                       1           1e-05         1e-05
proof-shell-strip-eager-annotations                             1           1e-05         1e-05
font-lock-default-unfontify-region                              2           7.000...e-06  3.500...e-06
proof-associated-windows                                        1           7e-06         7e-06
proof-shell-should-be-silent                                    1           6e-06         6e-06
font-lock-default-function                                      1           5e-06         5e-06
proof-shell-stop-silent-item                                    1           4e-06         4e-06
proof-shell-start-silent-item                                   1           4e-06         4e-06
proof-script-next-command-advance                               1           4e-06         4e-06
proof-shell-action-list-item                                    2           3e-06         1.5e-06
font-lock-set-defaults                                          2           3e-06         1.5e-06
proof-associated-buffers                                        2           2e-06         1e-06
font-lock-extend-region-wholelines                              2           2e-06         1e-06
font-lock-extend-region-multiline                               2           2e-06         1e-06
proof-minibuffer-message                                        1           1e-06         1e-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-release-lock                                              1           1e-06         1e-06
pg-finish-tracing-display                                       1           1e-06         1e-06
nconc                                                           1           1e-06         1e-06
process-status                                                  2           0.0           0.0


-----------------------------------------------------------------

Non-interactive:  (progn (proof-process-buffer) (proof-shell-wait))

### 4.368s elapsed time, 0.457s cpu time, 0.094s GC time

proof-shell-wait                                                1           4.484316      4.484316
accept-process-output                                           73          3.8998559999  0.0534226849
redisplay                                                       172         3.7155909999  0.0216022732
scomint-output-filter                                           206         3.5921849999  0.0174377912
proof-shell-filter                                              206         3.5562370000  0.0172632864
proof-shell-filter-manage-output                                206         3.5167620000  0.0170716601
proof-shell-exec-loop                                           206         3.5079160000  0.0170287184
mapc                                                            208         3.4532319999  0.0166020769
proof-shell-invoke-callback                                     206         3.4492200000  0.0167437864
proof-done-advancing                                            204         3.4481900000  0.0169028921
proof-done-advancing-other                                      104         3.2636610000  0.0313813557
pg-add-element                                                  204         3.2225049999  0.0157965931
proof-debug                                                     99          3.1809079999  0.0321303838
pg-autotest-message                                             99          3.1785960000  0.0321070303
proof-process-buffer                                            1           0.098653      0.098653
proof-assert-until-point-interactive                            1           0.098513      0.098513
proof-assert-until-point                                        1           0.098508      0.098508
proof-done-advancing-save                                       100         0.0861289999  0.0008612899
pg-set-span-helphighlights                                      304         0.0751920000  0.0002473421
proof-make-goalsave                                             100         0.074799      0.00074799
proof-assert-semis                                              1           0.072791      0.072791
proof-shell-insert-action-item                                  206         0.0508700000  0.0002469417
proof-shell-insert                                              206         0.0500239999  0.0002428349
proof-set-locked-end                                            204         0.0447420000  0.0002193235
proof-semis-to-vanillas                                         1           0.043912      0.043912
proof-set-locked-endpoints                                      204         0.0438019999  0.0002147156
proof-set-overlay-arrow                                         204         0.039986      0.0001960098
span-set-property                                               4968        0.0389520000  7.840...e-06
isar-command-wrapping                                           204         0.0359119999  0.0001760392
isar-global-save-command-p                                      100         0.0357419999  0.0003574199
span-at-before                                                  200         0.033411      0.0001670550
proof-script-delete-secondary-spans                             1           0.02853       0.02853
span-delete-spans                                               1           0.028527      0.028527
span-mapc-spans                                                 1           0.028523      0.028523
pg-add-proof-element                                            100         0.0274090000  0.0002740900
proof-segment-up-to-using-cache                                 1           0.025547      0.025547
proof-segment-up-to                                             1           0.025512      0.025512
proof-segment-up-to-parser                                      1           0.025509      0.025509
proof-script-generic-parse-cmdstart                             204         0.023117      0.0001133186
replace-regexp-in-string                                        612         0.0151239999  2.471...e-05
pg-last-output-displayform                                      304         0.0137170000  4.512...e-05
goto-char                                                       3399        0.0134079999  3.944...e-06
proof-buffer-syntactic-context                                  411         0.0133350000  3.244...e-05
proof-buffer-syntactic-context-emulate                          411         0.0125479999  3.053...e-05
proof-shell-strip-output-markup                                 202         0.0118950000  5.888...e-05
isar-strip-output-markup                                        202         0.01126       5.574...e-05
scomint-send-input                                              206         0.0089030000  4.321...e-05
skip-chars-forward                                              917         0.0077629999  8.465...e-06
proof-string-match                                              1114        0.0076579999  6.874...e-06
string-match                                                    3859        0.0065880000  1.707...e-06
isar-positions-of                                               204         0.0063140000  3.095...e-05
proof-shell-handle-immediate-output                             206         0.0061669999  2.993...e-05
proof-shell-process-urgent-messages                             206         0.006087      2.954...e-05
re-search-forward                                               1048        0.0060810000  5.802...e-06
isar-string-wrapping                                            408         0.0055940000  1.371...e-05
isar-preprocessing                                              206         0.0048040000  2.332...e-05
insert                                                          718         0.0036899999  5.139...e-06
proof-re-search-forward-safe                                    824         0.0034060000  4.133...e-06
proof-next-element-id                                           204         0.0033579999  1.646...e-05
span-set-endpoints                                              409         0.0031649999  7.738...e-06
proof-set-queue-start                                           204         0.0029729999  1.457...e-05
span-delete                                                     304         0.0027480000  9.039...e-06
isar-goal-command-p                                             204         0.0027019999  1.324...e-05
span-make                                                       608         0.0026310000  4.327...e-06
span-end                                                        926         0.0024999999  2.699...e-06
overlay-put                                                     4977        0.0024500000  4.922...e-07
pg-add-to-input-history                                         204         0.002432      1.192...e-05
proof-string-match-safe                                         204         0.0024030000  1.177...e-05
proof-get-name-from-goal                                        100         0.0022690000  2.269...e-05
span-set-start                                                  204         0.0022479999  1.101...e-05
move-overlay                                                    413         0.0020689999  5.009...e-06
pg-span-name                                                    102         0.0019750000  1.936...e-05
span-start                                                      604         0.0016740000  2.771...e-06
replace-match                                                   1008        0.0015839999  1.571...e-06
span-live-p                                                     408         0.0015820000  3.877...e-06
proof-element-id                                                204         0.0015369999  7.534...e-06
span-property                                                   2226        0.0014979999  6.729...e-07
make-overlay                                                    609         0.0012819999  2.105...e-06
delete-overlay                                                  309         0.0012420000  4.019...e-06
skip-chars-backward                                             206         0.0011609999  5.635...e-06
proof-shell-slurp-comments                                      207         0.0011250000  5.434...e-06
set-marker                                                      1853        0.0009220000  4.975...e-07
pg-processing-complete-hint                                     1           0.000625      0.000625
proof-next-element-count                                        204         0.0005830000  2.857...e-06
spans-at-region-prop                                            1           0.000573      0.000573
proof-shell-handle-delayed-output                               1           0.000495      0.000495
proof-shell-display-output-as-response                          1           0.000478      0.000478
pg-response-display                                             1           0.000474      0.000474
proof-display-and-keep-buffer                                   1           0.000463      0.000463
overlay-end                                                     1126        0.0004170000  3.703...e-07
marker-position                                                 1236        0.0004100000  3.317...e-07
match-string                                                    308         0.0003959999  1.285...e-06
buffer-live-p                                                   725         0.0003580000  4.937...e-07
isar-shell-adjust-line-width                                    206         0.0003170000  1.538...e-06
proof-extend-queue                                              1           0.000293      0.000293
proof-add-to-queue                                              1           0.000266      0.000266
get-buffer-process                                              209         0.0002369999  1.133...e-06
overlay-start                                                   604         0.0002369999  3.923...e-07
proof-shell-process-urgent-message                              1           0.000232      0.000232
proof-shell-process-urgent-message-default                      1           0.000169      0.000169
font-lock-fontify-region                                        1           0.000167      0.000167
font-lock-default-fontify-region                                1           0.00016       0.00016
nreverse                                                        209         0.0001489999  7.129...e-07
proof-get-window-for-buffer                                     1           0.000124      0.000124
font-lock-fontify-keywords-region                               1           0.000117      0.000117
proof-only-whitespace-to-locked-region-p                        1           0.000108      0.000108
proof-re-search-backward                                        1           8.2e-05       8.2e-05
pg-response-display-with-face                                   2           8.2e-05       4.1e-05
re-search-backward                                              1           6.7e-05       6.7e-05
pg-response-maybe-erase                                         2           5.900...e-05  2.950...e-05
font-lock-mode                                                  3           5.8e-05       1.933...e-05
proof-queue-or-locked-end                                       6           5.600...e-05  9.333...e-06
proof-shell-ready-prover                                        2           4.6e-05       2.3e-05
proof-looking-at-safe                                           8           4.2e-05       5.25e-06
proof-shell-start                                               2           3.700...e-05  1.850...e-05
proof-maybe-follow-locked-end                                   1           3.5e-05       3.5e-05
proof-shell-live-buffer                                         2           3.1e-05       1.55e-05
proof-activate-scripting                                        1           2.8e-05       2.8e-05
proof-looking-at                                                7           2.8e-05       4e-06
proof-grab-lock                                                 1           2.7e-05       2.7e-05
proof-unprocessed-begin                                         3           2.399...e-05  8e-06
proof-shell-should-be-silent                                    1           2.2e-05       2.2e-05
proof-detach-queue                                              1           1.8e-05       1.8e-05
scomint-check-proc                                              2           1.7e-05       8.5e-06
font-lock-fontify-syntactically-region                          1           1.7e-05       1.7e-05
isar-font-lock-fontify-syntactically-region                     1           1.6e-05       1.6e-05
span-detach                                                     1           1.5e-05       1.5e-05
font-lock-default-function                                      3           1.400...e-05  4.666...e-06
proof-shell-strip-eager-annotations                             1           1.1e-05       1.1e-05
font-lock-extend-jit-lock-region-after-change                   3           1e-05         3.333...e-06
proof-set-queue-endpoints                                       1           8e-06         8e-06
font-lock-unfontify-region                                      1           7e-06         7e-06
proof-re-search-forward                                         1           6e-06         6e-06
proof-associated-windows                                        1           6e-06         6e-06
proof-script-next-command-advance                               1           6e-06         6e-06
proof-shell-stop-silent-item                                    1           4e-06         4e-06
proof-shell-start-silent-item                                   1           4e-06         4e-06
proof-shell-action-list-item                                    2           3e-06         1.5e-06
proof-shell-clear-silent                                        1           3e-06         3e-06
process-status                                                  2           2e-06         1e-06
font-lock-set-defaults                                          1           2e-06         2e-06
proof-associated-buffers                                        2           1e-06         5e-07
proof-minibuffer-message                                        1           1e-06         1e-06
proof-shell-set-silent                                          1           1e-06         1e-06
proof-release-lock                                              1           1e-06         1e-06
pg-finish-tracing-display                                       1           1e-06         1e-06
nconc                                                           1           1e-06         1e-06
font-lock-extend-region-wholelines                              1           1e-06         1e-06
font-lock-default-unfontify-region                              1           1e-06         1e-06
proof-pbp-focus-on-first-goal                                   1           0.0           0.0
font-lock-extend-region-multiline                               1           0.0           0.0