1 | ELP Profiling Results: |
---|
2 | pg-autotest-test-process-wholefile 2 5.165872 2.582936 |
---|
3 | proof-shell-wait 12 5.024099 0.4186749166 |
---|
4 | proof-shell-filter 419 0.2695630000 0.0006433484 |
---|
5 | proof-shell-filter-manage-output 418 0.2489370000 0.0005955430 |
---|
6 | proof-shell-exec-loop 418 0.2271960000 0.0005435311 |
---|
7 | pg-autotest-find-file-restart 2 0.155834 0.077917 |
---|
8 | proof-shell-invoke-callback 418 0.1538019999 0.0003679473 |
---|
9 | proof-done-advancing 408 0.1525409999 0.0003738749 |
---|
10 | proof-process-buffer 2 0.112509 0.0562545 |
---|
11 | proof-assert-until-point-interactive 2 0.112292 0.056146 |
---|
12 | proof-assert-until-point 2 0.112288 0.056144 |
---|
13 | proof-shell-invisible-command 6 0.0962000000 0.0160333333 |
---|
14 | proof-activate-scripting 4 0.093024 0.023256 |
---|
15 | proof-goto-point 2 0.093013 0.0465065 |
---|
16 | proof-retract-until-point 2 0.09301 0.046505 |
---|
17 | proof-segment-up-to-using-cache 2 0.067206 0.033603 |
---|
18 | proof-segment-up-to 2 0.067169 0.0335845 |
---|
19 | proof-segment-up-to-parser 2 0.067163 0.0335815 |
---|
20 | proof-script-generic-parse-cmdstart 408 0.0655719999 0.0001607156 |
---|
21 | proof-register-possibly-new-processed-file 4 0.062253 0.01556325 |
---|
22 | proof-deactivate-scripting-auto 2 0.0619269999 0.0309634999 |
---|
23 | proof-deactivate-scripting 2 0.0619269999 0.0309634999 |
---|
24 | proof-unregister-buffer-file-name 2 0.0605119999 0.0302559999 |
---|
25 | proof-done-advancing-save 200 0.0558869999 0.0002794349 |
---|
26 | proof-shell-insert-action-item 418 0.0468400000 0.0001120574 |
---|
27 | proof-assert-semis 2 0.04504 0.02252 |
---|
28 | proof-shell-insert 418 0.0449620000 0.0001075645 |
---|
29 | proof-semis-to-vanillas 2 0.044723 0.0223615 |
---|
30 | proof-buffer-syntactic-context 822 0.0442250000 5.380...e-05 |
---|
31 | proof-done-advancing-other 208 0.0432040000 0.0002077115 |
---|
32 | pg-set-span-helphighlights 608 0.0420460000 6.915...e-05 |
---|
33 | proof-buffer-syntactic-context-emulate 822 0.0412470000 5.017...e-05 |
---|
34 | proof-inform-prover-file-retracted 2 0.037103 0.0185515 |
---|
35 | proof-make-goalsave 200 0.0331550000 0.0001657750 |
---|
36 | proof-toolbar-next-enable-p 832 0.0315920000 3.797...e-05 |
---|
37 | proof-cd-sync 2 0.031373 0.0156865 |
---|
38 | proof-toolbar-use-enable-p 416 0.0267579999 6.432...e-05 |
---|
39 | pg-add-proof-element 200 0.025211 0.000126055 |
---|
40 | pg-add-element 408 0.024243 5.941...e-05 |
---|
41 | proof-restart-buffers 4 0.023409 0.00585225 |
---|
42 | proof-locked-region-full-p 840 0.0188870000 2.248...e-05 |
---|
43 | pg-last-output-displayform 608 0.0174579999 2.871...e-05 |
---|
44 | proof-shell-handle-immediate-output 418 0.0173019999 4.139...e-05 |
---|
45 | proof-shell-strip-output-markup 404 0.015164 3.753...e-05 |
---|
46 | proof-script-delete-secondary-spans 4 0.01449 0.0036225 |
---|
47 | pg-span-name 204 0.0140400000 6.882...e-05 |
---|
48 | proof-shell-available-p 2912 0.0122319999 4.200...e-06 |
---|
49 | proof-toolbar-undo-enable-p 416 0.0099360000 2.388...e-05 |
---|
50 | proof-set-locked-end 408 0.0090480000 2.217...e-05 |
---|
51 | proof-script-delete-spans 2 0.009024 0.004512 |
---|
52 | proof-toolbar-retract-enable-p 416 0.0083189999 1.999...e-05 |
---|
53 | proof-set-locked-endpoints 408 0.0078690000 1.928...e-05 |
---|
54 | proof-toolbar-delete-enable-p 416 0.0076840000 1.847...e-05 |
---|
55 | proof-set-overlay-arrow 408 0.005549 1.360...e-05 |
---|
56 | proof-string-match 2234 0.0051529999 2.306...e-06 |
---|
57 | proof-toolbar-state-enable-p 416 0.0047509999 1.142...e-05 |
---|
58 | proof-next-element-id 408 0.004011 9.830...e-06 |
---|
59 | proof-shell-live-buffer 2930 0.0032549999 1.110...e-06 |
---|
60 | proof-toolbar-command-enable-p 416 0.0031299999 7.524...e-06 |
---|
61 | proof-format-filename 6 0.002797 0.0004661666 |
---|
62 | proof-toolbar-interrupt-enable-p 416 0.0027889999 6.704...e-06 |
---|
63 | proof-toolbar-info-enable-p 416 0.002784 6.692...e-06 |
---|
64 | proof-toolbar-find-enable-p 416 0.0026969999 6.483...e-06 |
---|
65 | proof-shell-process-urgent-messages 419 0.0023110000 5.515...e-06 |
---|
66 | pg-autotest-message 4 0.002248 0.000562 |
---|
67 | proof-re-search-forward-safe 1672 0.0021379999 1.278...e-06 |
---|
68 | proof-string-match-safe 408 0.002084 5.107...e-06 |
---|
69 | pg-remove-element 408 0.0018470000 4.526...e-06 |
---|
70 | proof-toolbar-context-enable-p 416 0.0018379999 4.418...e-06 |
---|
71 | pg-add-to-input-history 408 0.0016629999 4.075...e-06 |
---|
72 | proof-get-name-from-goal 200 0.0014020000 7.010...e-06 |
---|
73 | proof-locked-region-empty-p 430 0.0013809999 3.211...e-06 |
---|
74 | proof-unprocessed-begin 1304 0.0013060000 1.001...e-06 |
---|
75 | proof-shell-slurp-comments 426 0.0010179999 2.389...e-06 |
---|
76 | proof-add-to-queue 8 0.0009320000 0.0001165000 |
---|
77 | pg-autotest-test-assert-unprocessed 2 0.000887 0.0004435 |
---|
78 | pg-autotest-find-file 6 0.000871 0.0001451666 |
---|
79 | proof-element-id 408 0.0008580000 2.102...e-06 |
---|
80 | proof-start-queue 6 0.000793 0.0001321666 |
---|
81 | proof-set-queue-start 408 0.0007539999 1.848...e-06 |
---|
82 | proof-format 30 0.000688 2.293...e-05 |
---|
83 | proof-shell-display-output-as-response 8 0.000501 6.2625e-05 |
---|
84 | proof-shell-handle-delayed-output 8 0.000501 6.2625e-05 |
---|
85 | proof-display-and-keep-buffer 8 0.000501 6.2625e-05 |
---|
86 | pg-response-display 8 0.000501 6.2625e-05 |
---|
87 | proof-next-element-count 408 0.0004190000 1.026...e-06 |
---|
88 | proof-shell-process-urgent-message 10 0.000326 3.26e-05 |
---|
89 | proof-toolbar-goto-enable-p 416 0.0002959999 7.115...e-07 |
---|
90 | proof-debug 204 0.0002349999 1.151...e-06 |
---|
91 | proof-extend-queue 2 0.000154 7.7e-05 |
---|
92 | proof-shell-action-list-item 10 0.000117 1.17e-05 |
---|
93 | proof-shell-ready-prover 18 0.000109 6.055...e-06 |
---|
94 | proof-shell-start 18 6.9e-05 3.833...e-06 |
---|
95 | proof-grab-lock 8 5.8e-05 7.25e-06 |
---|
96 | proof-maybe-follow-locked-end 2 2.8e-05 1.4e-05 |
---|
97 | proof-only-whitespace-to-locked-region-p 2 2.3e-05 1.15e-05 |
---|
98 | proof-queue-or-locked-end 14 1.499...e-05 1.071...e-06 |
---|
99 | proof-re-search-backward 2 1.3e-05 6.5e-06 |
---|
100 | proof-shell-start-silent-item 2 6e-06 3e-06 |
---|
101 | proof-script-next-command-advance 2 4e-06 2e-06 |
---|
102 | proof-set-queue-endpoints 2 3e-06 1.5e-06 |
---|
103 | proof-shell-should-be-silent 8 3e-06 3.75e-07 |
---|
104 | proof-shell-set-silent 2 2e-06 1e-06 |
---|
105 | proof-re-search-forward 8 0.0 0.0 |
---|
106 | proof-files-to-buffers 2 0.0 0.0 |
---|
107 | proof-cd 2 0.0 0.0 |
---|
108 | proof-looking-at-safe 58 0.0 0.0 |
---|
109 | proof-auto-retract-dependencies 2 0.0 0.0 |
---|
110 | proof-minibuffer-message 6 0.0 0.0 |
---|
111 | proof-complete-buffer-atomic 2 0.0 0.0 |
---|
112 | proof-get-window-for-buffer 8 0.0 0.0 |
---|
113 | proof-shell-stop-silent-item 2 0.0 0.0 |
---|
114 | proof-detach-locked 2 0.0 0.0 |
---|
115 | proof-query-save-this-buffer-p 2 0.0 0.0 |
---|
116 | proof-shell-process-urgent-message-retract 2 0.0 0.0 |
---|
117 | proof-detach-queue 10 0.0 0.0 |
---|
118 | proof-colour-locked-span 4 0.0 0.0 |
---|
119 | proof-span-read-only 8 0.0 0.0 |
---|
120 | proof-shell-clear-silent 2 0.0 0.0 |
---|
121 | proof-script-end 2 0.0 0.0 |
---|
122 | proof-pbp-focus-on-first-goal 8 0.0 0.0 |
---|
123 | proof-shell-process-urgent-message-default 6 0.0 0.0 |
---|
124 | proof-init-segmentation 4 0.0 0.0 |
---|
125 | proof-done-invisible 6 0.0 0.0 |
---|
126 | proof-looking-at 52 0.0 0.0 |
---|
127 | proof-release-lock 8 0.0 0.0 |
---|
128 | proof-shell-strip-eager-annotations 6 0.0 0.0 |
---|
129 | pg-autotest-timetaken 2 0.0 0.0 |
---|
130 | pg-clear-script-portions 4 0.0 0.0 |
---|
131 | pg-autotest-test-assert-processed 2 0.0 0.0 |
---|
132 | pg-finish-tracing-display 8 0.0 0.0 |
---|
133 | pg-autotest-test-assert-full 2 0.0 0.0 |
---|
134 | pg-processing-complete-hint 8 0.0 0.0 |
---|
135 | pg-autotest-timestart 2 0.0 0.0 |
---|
136 | pg-clear-input-ring 4 0.0 0.0 |
---|
137 | pg-response-display-with-face 14 0.0 0.0 |
---|
138 | pg-response-maybe-erase 14 0.0 0.0 |
---|
139 | |
---|
140 | |
---|
141 | TEST: (eval (proof-shell-ready-prover)) |
---|
142 | TEST: (eval (isar-tracing:auto-quickcheck-toggle 0)) |
---|
143 | TEST: (eval (isar-tracing:auto-solve-toggle 0)) |
---|
144 | TEST: (eval (proof-full-annotation-toggle 0)) |
---|
145 | TEST: (process-wholefile "etc/isar/AHundredTheorems.thy") |
---|
146 | TIME: 3.270711 (this test) |
---|
147 | TEST: (process-wholefile "etc/isar/AHundredTheorems.thy") |
---|
148 | TIME: 2.591389 (this test) |
---|
149 | TEST: (process-wholefile "etc/isar/AHundredTheorems.thy") |
---|
150 | TIME: 2.452165 (this test) |
---|
151 | TEST: (process-wholefile "etc/isar/AHundredTheorems.thy") |
---|
152 | TIME: 2.619878 (this test) |
---|
153 | TEST: (process-wholefile "etc/isar/AHundredTheorems.thy") |
---|
154 | TIME: 2.548242 (this test) |
---|