blob: 49b378bac61a85d3381c192c364ef26cfa6eb437 (
plain)
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
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
|
Notes on Profiling Proof General in Emacs
-----------------------------------------
Usage of Elisp profiler:
M-x elp-instrument-package RET proof RET
< do something now >
M-x elp-results
To display results.
M-x clear-profiling-info
Eval: (profile (proof-toolbar-next) (proof-shell-wait))
M-x profile-results
NB: Must ignore calls to accept-process-output and sit-for, these
are from proof-shell-wait (only).
Testing by processing first line of src/HOL/Real/ROOT.ML (i.e. loading
RealDef)
Best case scenarios:
* Running Isabelle in ordinary shell buffer in Emacs, PIII:
~8% Emacs (PIII), ~90% SML if shell hidden
~15% X, ~25% xemacs, ~60% SML if shell displayed!
* Running Isabelle in xterm:
~3% xterm, ~2% X, 95% SML if xterm hidden
~4% xterm, ~16% X, 90% SML if xterm revealed
Before optimization:
* CPU time split about 70%/30% (Cel 366) or 65%/35% (PIII 500) SML/xemacs
Sample Runs. Tue Oct 5
-----------------------
[On Cel 366 64M]
Function Name Ticks %/Total Call Count
=================================== ===== ======= ==========
(in redisplay) 1183 44.947
re-search-forward 901 34.233 8061
sit-for 159 6.041 11919
comint-output-filter 93 3.533 3596
accept-process-output 43 1.634 11919
string-match 34 1.292 7300
font-lock-pre-idle-hook 30 1.140 25261
insert-before-markers 28 1.064 3597
let 14 0.532 10853
map-extents 13 0.494 539
(in garbage collection) 10 0.380
byte-code 9 0.342 25376
while 8 0.304 3648
setq 7 0.266 8299
comint-postoutput-scroll-to-bottom 7 0.266 3597
next-window 6 0.228 7194
put-nonduplicable-text-property 5 0.190 1166
marker-position 5 0.190 14389
goto-char 5 0.190 14097
walk-windows 4 0.152 3597
window-minibuffer-p 4 0.152 3597
proof-toolbar-refresh 4 0.152 3686
and 4 0.152 11162
selected-window 3 0.114 14390
window-start 3 0.114 3596
proof-shell-filter 3 0.114 3597
itimer-time-difference 3 0.114 546
#<compiled-function (window) "...(134)" [window-buffer window current window-point process-mark process scroll t all this selected others string set-window-point comint-scroll-show-maximum-output pos-visible-in-window-p recenter floatp floor window-height 1 -1 sit-for 0] 4> 3 0.114 7194
#<compiled-function (place &optional x) "...(29)" [place setq x + 1+ callf 1] 5 553442> 3 0.114 1298
process-buffer 3 0.114 3596
point 3 0.114 7382
or 3 0.114 7256
comint-watch-for-password-prompt 3 0.114 3597
save-excursion 2 0.076 3655
proof-shell-process-urgent-messages 2 0.076 3597
marker-buffer 2 0.076 3596
font-lock-fontify-keywords-region 2 0.076 45
process-mark 2 0.076 7208
redisplay-echo-area 2 0.076 23
if 2 0.076 18901
buffer-name 1 0.038 3650
erase-buffer 1 0.038 26
pos-visible-in-window-p 1 0.038 1
window-buffer 1 0.038 7195
self-insert-command 1 0.038 14
< 1 0.038 4300
itimer-timer-driver 1 0.038 182
font-lock-fontify-glumped-region 1 0.038 31
get-buffer-process 1 0.038 3633
char-to-string 1 0.038 3597
save-current-buffer 1 0.038 17
insert-string 1 0.038 23
--------------------------------------------------------------------
Total 2632 100.00
One tick = 1 ms
[On PIII 256M] top shows roughly 65% SML / 35% xemacs.
Function Name Ticks %/Total Call Count
====================================== ===== ======= ==========
(in redisplay) 3529 55.166
re-search-forward 1520 23.761 31627
sit-for 356 5.565 33870
comint-output-filter 265 4.143 12980
accept-process-output 125 1.954 33870
font-lock-pre-idle-hook 67 1.047 73094
insert-before-markers 51 0.797 12981
(in garbage collection) 46 0.719
string-match 44 0.688 27686
byte-code 27 0.422 74822
let 23 0.360 39724
#<compiled-function (window) "...(134)" [window-buffer window current window-point process-mark process scroll t all this selected others string set-window-point comint-scroll-show-maximum-output pos-visible-in-window-p recenter floatp floor window-height 1 -1 sit-for 0] 4> 21 0.328 25962
selected-window 20 0.313 51951
comint-postoutput-scroll-to-bottom 19 0.297 12981
setq 15 0.234 39971
if 15 0.234 72709
walk-windows 13 0.203 12981
proof-toolbar-refresh 13 0.203 14429
marker-position 12 0.188 51925
proof-shell-filter 12 0.188 12981
goto-char 12 0.188 53685
run-hook-with-args 12 0.188 13219
next-window 11 0.172 25962
and 9 0.141 40761
save-excursion 8 0.125 13756
buffer-name 7 0.109 13783
window-buffer 7 0.109 26077
log-message 7 0.109 237
process-mark 7 0.109 26208
point 7 0.109 27554
while 7 0.109 13727
#<compiled-function (place &optional x) "...(29)" [place setq x + 1+ callf 1] 5 553442> 6 0.094 11268
char-to-string 6 0.094 12981
force-mode-line-update 6 0.094 12980
< 5 0.078 19216
itimer-run-expired-timers 4 0.063 415
aref 4 0.063 11953
get-buffer-process 4 0.063 13290
proof-shell-process-urgent-messages 4 0.063 12981
redisplay-echo-area 4 0.063 238
insert-string 4 0.063 238
font-lock-fontify-keywords-region 4 0.063 740
window-minibuffer-p 3 0.047 12981
window-start 3 0.047 12980
marker-buffer 3 0.047 12980
process-buffer 3 0.047 12980
featurep 3 0.047 2120
comint-watch-for-password-prompt 3 0.047 12981
set-buffer 2 0.031 259
or 2 0.031 26285
font-lock-after-change-function-1 2 0.031 494
font-lock-default-fontify-region 2 0.031 740
event-over-toolbar-p 1 0.016 107
get-buffer 1 0.016 433
extent-object 1 0.016 988
itimerp 1 0.016 9136
itimer-is-idle 1 0.016 3735
set-extent-property 1 0.016 1024
make-string 1 0.016 247
next-single-property-change 1 0.016 246
expand-file-name 1 0.016 96
incf 1 0.016 11268
center-to-window-line 1 0.016 9
proof-done-advancing 1 0.016 2
itimer-time-difference 1 0.016 1660
itimer-timer-driver 1 0.016 415
1+ 1 0.016 11268
length 1 0.016 249
append-message 1 0.016 238
concat 1 0.016 246
proof-shell-strip-special-annotations 1 0.016 246
proof-shell-process-urgent-message 1 0.016 246
buffer-substring 1 0.016 493
save-current-buffer 1 0.016 248
newline 1 0.016 246
insert 1 0.016 249
current-time 1 0.016 831
match-beginning 1 0.016 247
font-lock-append-text-property 1 0.016 246
progn 1 0.016 1034
proof-response-buffer-display 1 0.016 246
font-lock-fontify-syntactically-region 1 0.016 740
font-lock-fontify-glumped-region 1 0.016 494
#<compiled-function (buffer &rest body) "...(8)" [save-current-buffer set-buffer buffer body] 3 540150> 1 0.016 248
font-lock-after-change-function 1 0.016 494
-----------------------------------------------------------------------
Total 6397 100.00
One tick = 1 ms
*** After some optimization attempt in proof-shell-process-urgent-messages,
to remove re-search-forward hog:
[Cel 366]
Function Name Ticks %/Total Call Count
=================================== ===== ======= ==========
accept-process-output 3279 62.374 1047436
(in redisplay) 919 17.481
sit-for 547 10.405 1047435
re-search-forward 134 2.549 8950
while 110 2.092 3648
comint-output-filter 65 1.236 3347
(in garbage collection) 24 0.457
font-lock-pre-idle-hook 18 0.342 14166
insert-before-markers 15 0.285 3348
string-match 10 0.190 7376
let 9 0.171 7010
#<compiled-function (window) "...(134)" [window-buffer window current window-point process-mark process scroll t all this selected others string set-window-point comint-scroll-show-maximum-output pos-visible-in-window-p recenter floatp floor window-height 1 -1 sit-for 0] 4> 9 0.171 6696
setq 6 0.114 12598
byte-code 5 0.095 14879
#<compiled-function (place &optional x) "...(29)" [place setq x + 1+ callf 1] 5 553442> 5 0.095 4762
and 5 0.095 10936
comint-postoutput-scroll-to-bottom 5 0.095 3348
log-message 4 0.076 98
save-excursion 3 0.057 3655
itimerp 3 0.057 14128
selected-window 3 0.057 13403
next-window 3 0.057 6696
point 3 0.057 10722
proof-toolbar-refresh 3 0.057 3942
if 3 0.057 23233
font-lock-default-unfontify-region 3 0.057 295
walk-windows 2 0.038 3348
event-window 2 0.038 658
buffer-name 2 0.038 3670
erase-buffer 2 0.038 105
put-nonduplicable-text-property 2 0.038 590
window-start 2 0.038 3347
null 2 0.038 3352
marker-position 2 0.038 13393
marker-buffer 2 0.038 3347
itimer-time-difference 2 0.038 2223
- 2 0.038 3350
font-lock-fontify-keywords-region 2 0.038 295
goto-char 2 0.038 14092
buffer-substring 2 0.038 196
redisplay-echo-area 2 0.038 104
run-hook-with-args 2 0.038 3447
comint-watch-for-password-prompt 2 0.038 3348
event-over-vertical-divider-p 1 0.019 254
event-glyph-extent 1 0.019 329
get-buffer 1 0.019 255
pointer-image-instance-p 1 0.019 985
barf-if-buffer-read-only 1 0.019 98
extent-at 1 0.019 87
itimer-value 1 0.019 6175
pos-visible-in-window-p 1 0.019 4
expand-file-name 1 0.019 192
file-truename 1 0.019 104
center-to-window-line 1 0.019 4
proof-shell-process-urgent-messages 1 0.019 3348
proof-shell-filter 1 0.019 3348
set-marker 1 0.019 3429
itimer-run-expired-timers 1 0.019 247
< 1 0.019 5950
min 1 0.019 3428
1- 1 0.019 3428
display-message 1 0.019 99
font-lock-fontify-glumped-region 1 0.019 197
get-buffer-process 1 0.019 6791
process-mark 1 0.019 10124
default-mouse-motion-handler 1 0.019 329
char-to-string 1 0.019 3348
save-current-buffer 1 0.019 99
newline 1 0.019 98
or 1 0.019 3490
#<compiled-function (buffer &rest body) "...(8)" [save-current-buffer set-buffer buffer body] 3 540150> 1 0.019 99
font-lock-unfontify-region 1 0.019 295
specifier-instance 1 0.019 329
--------------------------------------------------------------------
Total 5257 100.00
One tick = 1 ms
[PIII] split now about 70%/30%
Function Name Ticks %/Total Call Count
====================================== ===== ======= ==========
(in redisplay) 3638 72.082
sit-for 358 7.093 34176
comint-output-filter 247 4.894 12963
accept-process-output 132 2.615 34176
font-lock-pre-idle-hook 70 1.387 74389
insert-before-markers 67 1.328 12964
string-match 50 0.991 27655
(in garbage collection) 43 0.852
#<compiled-function (window) "...(134)" [window-buffer window current window-point process-mark process scroll t all this selected others string set-window-point comint-scroll-show-maximum-output pos-visible-in-window-p recenter floatp floor window-height 1 -1 sit-for 0] 4> 29 0.575 25928
re-search-forward 25 0.495 18630
comint-postoutput-scroll-to-bottom 24 0.476 12964
byte-code 22 0.436 76129
selected-window 20 0.396 51883
walk-windows 19 0.376 12964
let 18 0.357 13746
next-window 16 0.317 25928
proof-toolbar-refresh 13 0.258 14445
while 13 0.258 13710
proof-shell-filter 11 0.218 12964
process-mark 11 0.218 39137
save-excursion 10 0.198 13741
setq 10 0.198 27010
and 9 0.178 27701
goto-char 8 0.159 27695
run-hook-with-args 8 0.159 13211
if 7 0.139 33491
font-lock-fontify-keywords-region 6 0.119 740
#<compiled-function (place &optional x) "...(29)" [place setq x + 1+ callf 1] 5 553442> 6 0.119 11268
get-buffer-process 6 0.119 26242
char-to-string 6 0.119 12964
redisplay-echo-area 6 0.119 253
specifier-instance 6 0.119 656
itimerp 5 0.099 5713
1- 5 0.099 13209
point 5 0.099 27523
buffer-name 4 0.079 13766
current-buffer 4 0.079 13210
window-start 4 0.079 12963
< 4 0.079 6236
itimer-timer-driver 4 0.079 380
default-mouse-motion-handler 4 0.079 656
featurep 4 0.079 2693
force-mode-line-update 4 0.079 12963
comint-watch-for-password-prompt 4 0.079 12964
proof-shell-process-urgent-messages 3 0.059 12964
font-lock-fontify-syntactically-region 3 0.059 740
incf 3 0.059 11268
marker-position 3 0.059 12968
set-marker 3 0.059 13210
itimer-time-difference 3 0.059 1140
process-buffer 3 0.059 12963
event-window 2 0.040 1312
window-minibuffer-p 2 0.040 12964
window-buffer 2 0.040 26524
- 2 0.040 12967
move-to-left-margin 2 0.040 246
remove-message 2 0.040 253
event-buffer 2 0.040 656
font-lock-default-unfontify-region 2 0.040 740
font-lock-after-change-function 2 0.040 494
buffer-substring 2 0.040 493
insert-string 2 0.040 253
event-over-modeline-p 1 0.020 537
event-glyph-extent 1 0.020 656
set-syntax-table 1 0.020 740
pointer-image-instance-p 1 0.020 1913
extent-start-position 1 0.020 494
make-extent 1 0.020 527
detach-extent 1 0.020 495
extent-at 1 0.020 363
itimer-value 1 0.020 2660
itimer-is-idle 1 0.020 2280
set-extent-property 1 0.020 1024
highlight-extent 1 0.020 656
pos-visible-in-window-p 1 0.020 9
glyph-property-instance 1 0.020 656
get-text-property 1 0.020 492
put-nonduplicable-text-property 1 0.020 1480
next-single-property-change 1 0.020 246
quote 1 0.020 13798
marker-buffer 1 0.020 12963
itimer-run-expired-timers 1 0.020 380
aset 1 0.020 5280
log-message 1 0.020 246
min 1 0.020 13209
current-left-margin 1 0.020 246
display-message 1 0.020 246
fw-frame 1 0.020 656
font-lock-fontify-region 1 0.020 740
font-lock-append-text-property 1 0.020 246
substring 1 0.020 247
proof-response-buffer-display 1 0.020 246
delq 1 0.020 246
syntactically-sectionize 1 0.020 740
format 1 0.020 238
proof-file-truename 1 0.020 88
newline 1 0.020 246
store-match-data 1 0.020 742
proof-zap-commas-region 1 0.020 494
specifierp 1 0.020 656
log-message-filter 1 0.020 246
-----------------------------------------------------------------------
Total 5047 100.00
One tick = 1 ms
|
