1 | ELP Profiling Results: |
---|
2 | pg-autotest-test-process-wholefile 2 15.069724 7.534862 |
---|
3 | proof-shell-wait 12 14.891695 1.2409745833 |
---|
4 | pg-autotest-find-file-restart 2 0.7982279999 0.3991139999 |
---|
5 | proof-goto-point 2 0.554197 0.2770985 |
---|
6 | proof-retract-until-point 2 0.554181 0.2770905 |
---|
7 | proof-activate-scripting 4 0.5541750000 0.1385437500 |
---|
8 | proof-shell-invisible-command 6 0.487652 0.0812753333 |
---|
9 | proof-shell-filter 418 0.2987780000 0.0007147799 |
---|
10 | proof-shell-filter-manage-output 418 0.2802310000 0.0006704090 |
---|
11 | proof-unregister-buffer-file-name 2 0.270699 0.1353495 |
---|
12 | proof-shell-exec-loop 418 0.2542759999 0.0006083157 |
---|
13 | proof-inform-prover-file-retracted 2 0.2463370000 0.1231685000 |
---|
14 | proof-register-possibly-new-processed-file 4 0.2428369999 0.0607092499 |
---|
15 | proof-deactivate-scripting-auto 2 0.242364 0.121182 |
---|
16 | proof-deactivate-scripting 2 0.242204 0.121102 |
---|
17 | proof-cd-sync 2 0.227427 0.1137135 |
---|
18 | pg-autotest-message 4 0.1844549999 0.0461137499 |
---|
19 | proof-shell-invoke-callback 418 0.1797480000 0.0004300191 |
---|
20 | proof-done-advancing 408 0.1781130000 0.0004365514 |
---|
21 | pg-autotest-timetaken 2 0.095416 0.047708 |
---|
22 | proof-done-advancing-save 200 0.0933949999 0.0004669749 |
---|
23 | proof-process-buffer 2 0.092301 0.0461505 |
---|
24 | proof-assert-until-point-interactive 2 0.0921760000 0.0460880000 |
---|
25 | proof-assert-until-point 2 0.092171 0.0460855 |
---|
26 | proof-make-goalsave 200 0.0721499999 0.0003607499 |
---|
27 | pg-set-span-helphighlights 608 0.0703259999 0.0001156677 |
---|
28 | proof-shell-insert-action-item 418 0.0658640000 0.0001575693 |
---|
29 | proof-shell-insert 418 0.0643409999 0.0001539258 |
---|
30 | pg-add-proof-element 200 0.0568169999 0.0002840849 |
---|
31 | proof-segment-up-to-using-cache 2 0.051374 0.025687 |
---|
32 | proof-segment-up-to 2 0.051303 0.0256515 |
---|
33 | proof-segment-up-to-parser 2 0.051299 0.0256495 |
---|
34 | proof-script-generic-parse-cmdstart 408 0.0493449999 0.0001209436 |
---|
35 | proof-buffer-syntactic-context 822 0.0433680000 5.275...e-05 |
---|
36 | proof-buffer-syntactic-context-emulate 822 0.0418440000 5.090...e-05 |
---|
37 | proof-assert-semis 2 0.040736 0.020368 |
---|
38 | proof-semis-to-vanillas 2 0.0401360000 0.0200680000 |
---|
39 | pg-last-output-displayform 608 0.0241750000 3.976...e-05 |
---|
40 | proof-restart-buffers 4 0.0240470000 0.0060117500 |
---|
41 | proof-done-advancing-other 208 0.0236810000 0.0001138509 |
---|
42 | proof-set-locked-end 408 0.0221449999 5.427...e-05 |
---|
43 | proof-script-delete-spans 2 0.021876 0.010938 |
---|
44 | proof-shell-strip-output-markup 404 0.0214990000 5.321...e-05 |
---|
45 | proof-set-locked-endpoints 408 0.0206370000 5.058...e-05 |
---|
46 | proof-set-overlay-arrow 408 0.0144600000 3.544...e-05 |
---|
47 | proof-shell-handle-delayed-output 8 0.013599 0.001699875 |
---|
48 | pg-add-element 408 0.0122009999 2.990...e-05 |
---|
49 | proof-shell-process-urgent-messages 418 0.0087780000 2.100...e-05 |
---|
50 | proof-shell-handle-immediate-output 418 0.0081079999 1.939...e-05 |
---|
51 | proof-string-match 2234 0.0073080000 3.271...e-06 |
---|
52 | proof-next-element-id 408 0.0055589999 1.362...e-05 |
---|
53 | proof-re-search-forward-safe 1672 0.0038750000 2.317...e-06 |
---|
54 | pg-add-to-input-history 408 0.0036729999 9.002...e-06 |
---|
55 | proof-string-match-safe 408 0.0030939999 7.583...e-06 |
---|
56 | proof-element-id 408 0.0027950000 6.850...e-06 |
---|
57 | pg-autotest-find-file 6 0.002425 0.0004041666 |
---|
58 | proof-shell-process-urgent-message 10 0.002414 0.0002413999 |
---|
59 | proof-get-name-from-goal 200 0.0023580000 1.179...e-05 |
---|
60 | proof-script-delete-secondary-spans 4 0.002139 0.00053475 |
---|
61 | proof-shell-display-output-as-response 8 0.0018490000 0.0002311250 |
---|
62 | pg-response-display 8 0.0018119999 0.0002264999 |
---|
63 | proof-display-and-keep-buffer 8 0.0016699999 0.0002087499 |
---|
64 | pg-span-name 204 0.0016419999 8.049...e-06 |
---|
65 | proof-add-to-queue 8 0.001163 0.000145375 |
---|
66 | proof-next-element-count 408 0.0009510000 2.330...e-06 |
---|
67 | proof-start-queue 6 0.000919 0.0001531666 |
---|
68 | pg-autotest-test-assert-processed 2 0.0008799999 0.0004399999 |
---|
69 | proof-set-queue-start 408 0.0008750000 2.144...e-06 |
---|
70 | pg-processing-complete-hint 8 0.000814 0.00010175 |
---|
71 | pg-autotest-test-assert-unprocessed 2 0.0008049999 0.0004024999 |
---|
72 | proof-shell-slurp-comments 426 0.0007910000 1.856...e-06 |
---|
73 | proof-shell-process-urgent-message-default 6 0.0007710000 0.0001285 |
---|
74 | proof-cd 2 0.000539 0.0002695 |
---|
75 | proof-format-filename 6 0.000508 8.466...e-05 |
---|
76 | pg-remove-element 408 0.0005070000 1.242...e-06 |
---|
77 | proof-init-segmentation 4 0.000506 0.0001265 |
---|
78 | proof-shell-process-urgent-message-retract 2 0.000429 0.0002145 |
---|
79 | pg-response-display-with-face 14 0.0004220000 3.014...e-05 |
---|
80 | proof-span-read-only 8 0.000414 5.175e-05 |
---|
81 | proof-looking-at-safe 58 0.0003420000 5.896...e-06 |
---|
82 | proof-debug 204 0.0002869999 1.406...e-06 |
---|
83 | pg-response-maybe-erase 14 0.000281 2.007...e-05 |
---|
84 | proof-extend-queue 2 0.000277 0.0001385 |
---|
85 | proof-format 30 0.0002289999 7.633...e-06 |
---|
86 | proof-looking-at 52 0.0002049999 3.942...e-06 |
---|
87 | proof-shell-ready-prover 18 0.000156 8.666...e-06 |
---|
88 | proof-locked-region-full-p 8 0.0001040000 1.300...e-05 |
---|
89 | proof-shell-start 18 9.800...e-05 5.444...e-06 |
---|
90 | proof-grab-lock 8 7.999...e-05 9.999...e-06 |
---|
91 | proof-locked-region-empty-p 14 5.099...e-05 3.642...e-06 |
---|
92 | proof-shell-live-buffer 18 4.399...e-05 2.444...e-06 |
---|
93 | pg-autotest-test-assert-full 2 3.999...e-05 1.999...e-05 |
---|
94 | proof-maybe-follow-locked-end 2 3.700...e-05 1.850...e-05 |
---|
95 | proof-detach-queue 10 3.5e-05 3.499...e-06 |
---|
96 | proof-files-to-buffers 2 3.4e-05 1.7e-05 |
---|
97 | proof-only-whitespace-to-locked-region-p 2 3.4e-05 1.7e-05 |
---|
98 | proof-shell-strip-eager-annotations 6 3.4e-05 5.666...e-06 |
---|
99 | proof-unprocessed-begin 32 3.200...e-05 1.000...e-06 |
---|
100 | proof-complete-buffer-atomic 2 3.1e-05 1.55e-05 |
---|
101 | proof-re-search-forward 8 2.899...e-05 3.624...e-06 |
---|
102 | proof-get-window-for-buffer 8 2.600...e-05 3.250...e-06 |
---|
103 | pg-clear-script-portions 4 2.600...e-05 6.500...e-06 |
---|
104 | pg-autotest-timestart 2 2.600...e-05 1.300...e-05 |
---|
105 | proof-re-search-backward 2 1.999...e-05 9.999...e-06 |
---|
106 | proof-queue-or-locked-end 14 1.500...e-05 1.071...e-06 |
---|
107 | proof-shell-action-list-item 10 1.400...e-05 1.400...e-06 |
---|
108 | proof-shell-should-be-silent 8 1.400...e-05 1.750...e-06 |
---|
109 | proof-script-end 2 1.400...e-05 7.000...e-06 |
---|
110 | proof-shell-stop-silent-item 2 9e-06 4.5e-06 |
---|
111 | proof-shell-start-silent-item 2 6e-06 3e-06 |
---|
112 | proof-done-invisible 6 4.999...e-06 8.333...e-07 |
---|
113 | proof-release-lock 8 4.999...e-06 6.249...e-07 |
---|
114 | proof-set-queue-endpoints 2 4e-06 2e-06 |
---|
115 | proof-minibuffer-message 6 4e-06 6.666...e-07 |
---|
116 | proof-colour-locked-span 4 4e-06 1e-06 |
---|
117 | proof-pbp-focus-on-first-goal 8 4e-06 5e-07 |
---|
118 | pg-finish-tracing-display 8 4e-06 5e-07 |
---|
119 | proof-script-next-command-advance 2 3e-06 1.5e-06 |
---|
120 | pg-clear-input-ring 4 3e-06 7.5e-07 |
---|
121 | proof-auto-retract-dependencies 2 2e-06 1e-06 |
---|
122 | proof-detach-locked 2 2e-06 1e-06 |
---|
123 | proof-query-save-this-buffer-p 2 2e-06 1e-06 |
---|
124 | proof-shell-clear-silent 2 2e-06 1e-06 |
---|
125 | proof-shell-set-silent 2 1e-06 5e-07 |
---|
126 | |
---|
127 | |
---|
128 | TEST: (eval (proof-shell-ready-prover)) |
---|
129 | TEST: (eval (isar-tracing:auto-quickcheck-toggle 0)) |
---|
130 | TEST: (eval (isar-tracing:auto-solve-toggle 0)) |
---|
131 | TEST: (eval (proof-full-annotation-toggle 0)) |
---|
132 | TEST: (process-wholefile "etc/isar/AHundredTheorems.thy") |
---|
133 | TIME: 7.392437 (this test) |
---|
134 | TEST: (process-wholefile "etc/isar/AHundredTheorems.thy") |
---|
135 | TIME: 7.809447 (this test) |
---|
136 | TEST: (process-wholefile "etc/isar/AHundredTheorems.thy") |
---|
137 | TIME: 7.676066 (this test) |
---|
138 | TEST: (process-wholefile "etc/isar/AHundredTheorems.thy") |
---|
139 | TIME: 7.617290 (this test) |
---|
140 | TEST: (process-wholefile "etc/isar/AHundredTheorems.thy") |
---|
141 | TIME: 7.542135 (this test) |
---|