| 1 | ELP Profiling Results: |
|---|
| 2 | pg-autotest-test-process-wholefile 2 9.037719 4.5188595 |
|---|
| 3 | proof-shell-wait 12 8.8928889999 0.7410740833 |
|---|
| 4 | proof-shell-filter 418 0.2528340000 0.0006048660 |
|---|
| 5 | proof-shell-filter-manage-output 418 0.2292829999 0.0005485239 |
|---|
| 6 | proof-shell-exec-loop 418 0.209148 0.0005003540 |
|---|
| 7 | proof-shell-invoke-callback 418 0.1595800000 0.0003817703 |
|---|
| 8 | proof-toolbar-next-enable-p 844 0.1575169999 0.0001866315 |
|---|
| 9 | proof-done-advancing 408 0.1571190000 0.0003850955 |
|---|
| 10 | pg-autotest-find-file-restart 2 0.151516 0.075758 |
|---|
| 11 | proof-process-buffer 2 0.122839 0.0614195 |
|---|
| 12 | proof-assert-until-point-interactive 2 0.1226599999 0.0613299999 |
|---|
| 13 | proof-assert-until-point 2 0.1226500000 0.0613250000 |
|---|
| 14 | proof-toolbar-delete-enable-p 422 0.1134290000 0.0002687890 |
|---|
| 15 | proof-goto-point 2 0.105531 0.0527655 |
|---|
| 16 | proof-retract-until-point 2 0.105504 0.052752 |
|---|
| 17 | proof-activate-scripting 4 0.105484 0.026371 |
|---|
| 18 | proof-segment-up-to-using-cache 2 0.1026509999 0.0513254999 |
|---|
| 19 | proof-segment-up-to 2 0.1025389999 0.0512694999 |
|---|
| 20 | proof-segment-up-to-parser 2 0.1025280000 0.0512640000 |
|---|
| 21 | proof-script-generic-parse-cmdstart 408 0.099814 0.0002446421 |
|---|
| 22 | proof-toolbar-use-enable-p 422 0.0916920000 0.0002172796 |
|---|
| 23 | proof-buffer-syntactic-context 822 0.0881740000 0.0001072676 |
|---|
| 24 | proof-shell-invisible-command 6 0.087902 0.0146503333 |
|---|
| 25 | proof-buffer-syntactic-context-emulate 822 0.085143 0.0001035802 |
|---|
| 26 | proof-toolbar-retract-enable-p 422 0.0671890000 0.0001592156 |
|---|
| 27 | proof-toolbar-undo-enable-p 422 0.0649750000 0.0001539691 |
|---|
| 28 | proof-unregister-buffer-file-name 2 0.059778 0.029889 |
|---|
| 29 | proof-done-advancing-save 200 0.0592889999 0.0002964449 |
|---|
| 30 | proof-register-possibly-new-processed-file 4 0.0447889999 0.0111972499 |
|---|
| 31 | proof-inform-prover-file-retracted 2 0.0447150000 0.0223575000 |
|---|
| 32 | proof-cd-sync 2 0.044489 0.0222445 |
|---|
| 33 | proof-deactivate-scripting-auto 2 0.044286 0.022143 |
|---|
| 34 | proof-deactivate-scripting 2 0.044139 0.0220695 |
|---|
| 35 | proof-make-goalsave 200 0.0435589999 0.0002177949 |
|---|
| 36 | pg-set-span-helphighlights 608 0.0397900000 6.544...e-05 |
|---|
| 37 | proof-shell-insert-action-item 418 0.0370909999 8.873...e-05 |
|---|
| 38 | proof-shell-insert 418 0.0347310000 8.308...e-05 |
|---|
| 39 | proof-done-advancing-other 208 0.0308109999 0.0001481298 |
|---|
| 40 | proof-set-locked-end 408 0.028179 6.906...e-05 |
|---|
| 41 | proof-locked-region-empty-p 436 0.0262720000 6.025...e-05 |
|---|
| 42 | proof-set-locked-endpoints 408 0.0256880000 6.296...e-05 |
|---|
| 43 | pg-add-proof-element 200 0.0236599999 0.0001182999 |
|---|
| 44 | proof-shell-available-p 2954 0.0201330000 6.815...e-06 |
|---|
| 45 | proof-assert-semis 2 0.019893 0.0099465 |
|---|
| 46 | proof-semis-to-vanillas 2 0.019066 0.009533 |
|---|
| 47 | proof-set-overlay-arrow 408 0.0166099999 4.071...e-05 |
|---|
| 48 | proof-restart-buffers 4 0.0147050000 0.0036762500 |
|---|
| 49 | pg-add-element 408 0.0143920000 3.527...e-05 |
|---|
| 50 | pg-autotest-message 4 0.0143329999 0.0035832499 |
|---|
| 51 | proof-shell-handle-immediate-output 418 0.0124590000 2.980...e-05 |
|---|
| 52 | pg-last-output-displayform 608 0.0114860000 1.889...e-05 |
|---|
| 53 | proof-string-match 2234 0.0111520000 4.991...e-06 |
|---|
| 54 | proof-script-delete-spans 2 0.010645 0.0053225 |
|---|
| 55 | proof-shell-process-urgent-messages 418 0.0106349999 2.544...e-05 |
|---|
| 56 | proof-locked-region-full-p 852 0.0104840000 1.230...e-05 |
|---|
| 57 | proof-next-element-id 408 0.0083910000 2.056...e-05 |
|---|
| 58 | pg-autotest-timetaken 2 0.007594 0.003797 |
|---|
| 59 | proof-shell-strip-output-markup 404 0.0075280000 1.863...e-05 |
|---|
| 60 | proof-shell-live-buffer 2972 0.0072400000 2.436...e-06 |
|---|
| 61 | proof-toolbar-state-enable-p 422 0.0069010000 1.635...e-05 |
|---|
| 62 | pg-add-to-input-history 408 0.0062320000 1.527...e-05 |
|---|
| 63 | proof-re-search-forward-safe 1672 0.0060230000 3.602...e-06 |
|---|
| 64 | proof-get-name-from-goal 200 0.0047499999 2.374...e-05 |
|---|
| 65 | proof-string-match-safe 408 0.0044190000 1.083...e-05 |
|---|
| 66 | proof-toolbar-find-enable-p 422 0.0040839999 9.677...e-06 |
|---|
| 67 | proof-toolbar-info-enable-p 422 0.0039859999 9.445...e-06 |
|---|
| 68 | proof-script-delete-secondary-spans 4 0.003892 0.000973 |
|---|
| 69 | proof-toolbar-context-enable-p 422 0.0038829999 9.201...e-06 |
|---|
| 70 | proof-toolbar-command-enable-p 422 0.0038529999 9.130...e-06 |
|---|
| 71 | proof-element-id 408 0.0037529999 9.198...e-06 |
|---|
| 72 | proof-shell-process-urgent-message 10 0.00278 0.000278 |
|---|
| 73 | proof-unprocessed-begin 1322 0.0024009999 1.816...e-06 |
|---|
| 74 | pg-autotest-find-file 6 0.0023580000 0.0003930000 |
|---|
| 75 | proof-shell-handle-delayed-output 8 0.002277 0.000284625 |
|---|
| 76 | proof-shell-display-output-as-response 8 0.002133 0.000266625 |
|---|
| 77 | pg-response-display 8 0.0020859999 0.0002607499 |
|---|
| 78 | pg-span-name 204 0.0019179999 9.401...e-06 |
|---|
| 79 | proof-display-and-keep-buffer 8 0.0018720000 0.0002340000 |
|---|
| 80 | proof-next-element-count 408 0.0015630000 3.830...e-06 |
|---|
| 81 | proof-shell-slurp-comments 426 0.0014759999 3.464...e-06 |
|---|
| 82 | proof-set-queue-start 408 0.0014730000 3.610...e-06 |
|---|
| 83 | proof-add-to-queue 8 0.001384 0.000173 |
|---|
| 84 | proof-start-queue 6 0.001029 0.0001715 |
|---|
| 85 | pg-processing-complete-hint 8 0.000967 0.000120875 |
|---|
| 86 | pg-remove-element 408 0.0009090000 2.227...e-06 |
|---|
| 87 | pg-autotest-test-assert-unprocessed 2 0.00088 0.00044 |
|---|
| 88 | pg-autotest-test-assert-processed 2 0.0008500000 0.0004250000 |
|---|
| 89 | proof-shell-process-urgent-message-default 6 0.000824 0.0001373333 |
|---|
| 90 | proof-init-segmentation 4 0.000737 0.00018425 |
|---|
| 91 | proof-toolbar-goto-enable-p 422 0.0006700000 1.587...e-06 |
|---|
| 92 | proof-cd 2 0.000615 0.0003075 |
|---|
| 93 | proof-span-read-only 8 0.000578 7.225e-05 |
|---|
| 94 | proof-format-filename 6 0.000568 9.466...e-05 |
|---|
| 95 | proof-toolbar-interrupt-enable-p 422 0.0005470000 1.296...e-06 |
|---|
| 96 | proof-looking-at-safe 58 0.0004890000 8.431...e-06 |
|---|
| 97 | proof-shell-process-urgent-message-retract 2 0.000479 0.0002395 |
|---|
| 98 | pg-response-display-with-face 14 0.0004449999 3.178...e-05 |
|---|
| 99 | proof-debug 204 0.0004299999 2.107...e-06 |
|---|
| 100 | proof-extend-queue 2 0.00042 0.00021 |
|---|
| 101 | pg-response-maybe-erase 14 0.0003250000 2.321...e-05 |
|---|
| 102 | proof-format 30 0.0002660000 8.866...e-06 |
|---|
| 103 | proof-shell-ready-prover 18 0.0002659999 1.477...e-05 |
|---|
| 104 | proof-looking-at 52 0.0002489999 4.788...e-06 |
|---|
| 105 | proof-shell-start 18 0.0001699999 9.444...e-06 |
|---|
| 106 | proof-grab-lock 8 0.0001449999 1.812...e-05 |
|---|
| 107 | pg-autotest-test-assert-full 2 5.8e-05 2.9e-05 |
|---|
| 108 | proof-maybe-follow-locked-end 2 5.6e-05 2.8e-05 |
|---|
| 109 | proof-only-whitespace-to-locked-region-p 2 5.4e-05 2.7e-05 |
|---|
| 110 | pg-clear-script-portions 4 4.6e-05 1.15e-05 |
|---|
| 111 | proof-detach-queue 10 4.3e-05 4.3e-06 |
|---|
| 112 | proof-complete-buffer-atomic 2 3.8e-05 1.9e-05 |
|---|
| 113 | proof-files-to-buffers 2 3.700...e-05 1.850...e-05 |
|---|
| 114 | proof-re-search-backward 2 3.2e-05 1.6e-05 |
|---|
| 115 | proof-re-search-forward 8 3.1e-05 3.875e-06 |
|---|
| 116 | proof-queue-or-locked-end 14 3.1e-05 2.214...e-06 |
|---|
| 117 | proof-shell-strip-eager-annotations 6 3.1e-05 5.166...e-06 |
|---|
| 118 | proof-get-window-for-buffer 8 2.999...e-05 3.749...e-06 |
|---|
| 119 | proof-shell-action-list-item 10 2.600...e-05 2.6e-06 |
|---|
| 120 | proof-shell-should-be-silent 8 2.5e-05 3.125e-06 |
|---|
| 121 | proof-shell-stop-silent-item 2 1.7e-05 8.5e-06 |
|---|
| 122 | proof-script-end 2 1.499...e-05 7.499...e-06 |
|---|
| 123 | proof-shell-start-silent-item 2 1.499...e-05 7.499...e-06 |
|---|
| 124 | proof-release-lock 8 1.300...e-05 1.625...e-06 |
|---|
| 125 | pg-finish-tracing-display 8 1.3e-05 1.625e-06 |
|---|
| 126 | proof-pbp-focus-on-first-goal 8 1.299...e-05 1.624...e-06 |
|---|
| 127 | proof-done-invisible 6 1.199...e-05 2e-06 |
|---|
| 128 | proof-minibuffer-message 6 9.999...e-06 1.666...e-06 |
|---|
| 129 | pg-clear-input-ring 4 9e-06 2.25e-06 |
|---|
| 130 | proof-colour-locked-span 4 8e-06 2e-06 |
|---|
| 131 | proof-set-queue-endpoints 2 7e-06 3.5e-06 |
|---|
| 132 | pg-autotest-timestart 2 7e-06 3.5e-06 |
|---|
| 133 | proof-detach-locked 2 6e-06 3e-06 |
|---|
| 134 | proof-auto-retract-dependencies 2 4e-06 2e-06 |
|---|
| 135 | proof-shell-clear-silent 2 4e-06 2e-06 |
|---|
| 136 | proof-script-next-command-advance 2 4e-06 2e-06 |
|---|
| 137 | proof-shell-set-silent 2 3e-06 1.5e-06 |
|---|
| 138 | proof-query-save-this-buffer-p 2 3e-06 1.5e-06 |
|---|
| 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: 4.521919 (this test) |
|---|
| 147 | TEST: (process-wholefile "etc/isar/AHundredTheorems.thy") |
|---|
| 148 | TIME: 4.618779 (this test) |
|---|
| 149 | TEST: (process-wholefile "etc/isar/AHundredTheorems.thy") |
|---|
| 150 | TIME: 4.463783 (this test) |
|---|
| 151 | TEST: (process-wholefile "etc/isar/AHundredTheorems.thy") |
|---|
| 152 | TIME: 4.480727 (this test) |
|---|
| 153 | TEST: (process-wholefile "etc/isar/AHundredTheorems.thy") |
|---|
| 154 | TIME: 4.564446 (this test) |
|---|
