| 1 | ELP Profiling Results: |
|---|
| 2 | pg-autotest-test-process-wholefile 2 40.577944 20.288972 |
|---|
| 3 | proof-shell-wait 12 40.368700000 3.3640583333 |
|---|
| 4 | pg-autotest-find-file-restart 2 0.647197 0.3235985 |
|---|
| 5 | proof-shell-filter 418 0.443661 0.0010613899 |
|---|
| 6 | proof-goto-point 2 0.436492 0.218246 |
|---|
| 7 | proof-retract-until-point 2 0.436471 0.2182355 |
|---|
| 8 | proof-activate-scripting 4 0.4364670000 0.1091167500 |
|---|
| 9 | proof-shell-filter-manage-output 418 0.4234370000 0.0010130071 |
|---|
| 10 | proof-shell-invisible-command 6 0.409385 0.0682308333 |
|---|
| 11 | proof-shell-exec-loop 418 0.3895029999 0.0009318253 |
|---|
| 12 | proof-shell-invoke-callback 418 0.3208000000 0.0007674641 |
|---|
| 13 | proof-done-advancing 408 0.318907 0.0007816348 |
|---|
| 14 | proof-unregister-buffer-file-name 2 0.2325539999 0.1162769999 |
|---|
| 15 | proof-register-possibly-new-processed-file 4 0.209125 0.05228125 |
|---|
| 16 | proof-deactivate-scripting-auto 2 0.207721 0.1038605 |
|---|
| 17 | proof-deactivate-scripting 2 0.2075179999 0.1037589999 |
|---|
| 18 | proof-inform-prover-file-retracted 2 0.2040580000 0.1020290000 |
|---|
| 19 | proof-cd-sync 2 0.2030600000 0.1015300000 |
|---|
| 20 | proof-process-buffer 2 0.170764 0.085382 |
|---|
| 21 | proof-assert-until-point-interactive 2 0.170589 0.0852945 |
|---|
| 22 | proof-assert-until-point 2 0.1705809999 0.0852904999 |
|---|
| 23 | proof-segment-up-to-using-cache 2 0.116059 0.0580295 |
|---|
| 24 | proof-segment-up-to 2 0.1159709999 0.0579854999 |
|---|
| 25 | proof-segment-up-to-parser 2 0.1159649999 0.0579824999 |
|---|
| 26 | proof-script-generic-parse-cmdstart 408 0.1132090000 0.0002774730 |
|---|
| 27 | proof-done-advancing-save 200 0.1127790000 0.0005638950 |
|---|
| 28 | proof-buffer-syntactic-context 822 0.1040379999 0.0001265669 |
|---|
| 29 | proof-buffer-syntactic-context-emulate 822 0.1017650000 0.0001238017 |
|---|
| 30 | pg-set-span-helphighlights 608 0.0995989999 0.0001638141 |
|---|
| 31 | proof-make-goalsave 200 0.0791239999 0.0003956199 |
|---|
| 32 | proof-shell-insert-action-item 418 0.0549159999 0.0001313779 |
|---|
| 33 | proof-done-advancing-other 208 0.0546240000 0.0002626153 |
|---|
| 34 | proof-assert-semis 2 0.054451 0.0272255 |
|---|
| 35 | proof-semis-to-vanillas 2 0.053689 0.0268445 |
|---|
| 36 | proof-shell-insert 418 0.0528339999 0.0001263971 |
|---|
| 37 | pg-add-proof-element 200 0.0524450000 0.0002622250 |
|---|
| 38 | proof-set-locked-end 408 0.0417609999 0.0001023553 |
|---|
| 39 | proof-set-locked-endpoints 408 0.0397710000 9.747...e-05 |
|---|
| 40 | proof-set-overlay-arrow 408 0.0369940000 9.067...e-05 |
|---|
| 41 | pg-last-output-displayform 608 0.0328140000 5.397...e-05 |
|---|
| 42 | proof-shell-strip-output-markup 404 0.0291170000 7.207...e-05 |
|---|
| 43 | proof-shell-handle-immediate-output 418 0.0282280000 6.753...e-05 |
|---|
| 44 | proof-restart-buffers 4 0.027624 0.006906 |
|---|
| 45 | proof-script-delete-spans 2 0.02529 0.012645 |
|---|
| 46 | pg-add-element 408 0.0169669999 4.158...e-05 |
|---|
| 47 | pg-remove-element 408 0.0154180000 3.778...e-05 |
|---|
| 48 | proof-shell-process-urgent-messages 418 0.0100270000 2.398...e-05 |
|---|
| 49 | proof-string-match 2234 0.0096910000 4.337...e-06 |
|---|
| 50 | proof-next-element-id 408 0.0061479999 1.506...e-05 |
|---|
| 51 | proof-re-search-forward-safe 1672 0.0052360000 3.131...e-06 |
|---|
| 52 | pg-add-to-input-history 408 0.0046020000 1.127...e-05 |
|---|
| 53 | pg-autotest-find-file 6 0.0044599999 0.0007433333 |
|---|
| 54 | proof-shell-process-urgent-message 10 0.004364 0.0004364 |
|---|
| 55 | proof-string-match-safe 408 0.0037980000 9.308...e-06 |
|---|
| 56 | proof-set-queue-start 408 0.0037079999 9.088...e-06 |
|---|
| 57 | proof-get-name-from-goal 200 0.0033789999 1.689...e-05 |
|---|
| 58 | pg-processing-complete-hint 8 0.0032969999 0.0004121249 |
|---|
| 59 | proof-element-id 408 0.0024709999 6.056...e-06 |
|---|
| 60 | proof-script-delete-secondary-spans 4 0.002256 0.000564 |
|---|
| 61 | pg-span-name 204 0.0018739999 9.186...e-06 |
|---|
| 62 | pg-autotest-test-assert-processed 2 0.00168 0.00084 |
|---|
| 63 | pg-autotest-test-assert-unprocessed 2 0.001508 0.000754 |
|---|
| 64 | proof-add-to-queue 8 0.00142 0.0001775 |
|---|
| 65 | proof-start-queue 6 0.001105 0.0001841666 |
|---|
| 66 | proof-next-element-count 408 0.0010210000 2.502...e-06 |
|---|
| 67 | proof-shell-process-urgent-message-retract 2 0.000962 0.000481 |
|---|
| 68 | proof-shell-process-urgent-message-default 6 0.0009069999 0.0001511666 |
|---|
| 69 | proof-shell-slurp-comments 426 0.0008910000 2.091...e-06 |
|---|
| 70 | proof-shell-handle-delayed-output 8 0.0007970000 9.962...e-05 |
|---|
| 71 | proof-format-filename 6 0.000727 0.0001211666 |
|---|
| 72 | proof-init-segmentation 4 0.0007030000 0.0001757500 |
|---|
| 73 | proof-shell-display-output-as-response 8 0.0006689999 8.362...e-05 |
|---|
| 74 | proof-cd 2 0.0006670000 0.0003335000 |
|---|
| 75 | pg-autotest-message 4 0.000661 0.00016525 |
|---|
| 76 | pg-response-display 8 0.000631 7.8875e-05 |
|---|
| 77 | proof-span-read-only 8 0.000584 7.3e-05 |
|---|
| 78 | pg-response-display-with-face 14 0.000523 3.735...e-05 |
|---|
| 79 | proof-display-and-keep-buffer 8 0.00047 5.875e-05 |
|---|
| 80 | proof-locked-region-full-p 10 0.0004569999 4.569...e-05 |
|---|
| 81 | proof-looking-at-safe 58 0.0004520000 7.793...e-06 |
|---|
| 82 | pg-autotest-timetaken 2 0.000371 0.0001855 |
|---|
| 83 | proof-extend-queue 2 0.000356 0.000178 |
|---|
| 84 | proof-format 30 0.000322 1.073...e-05 |
|---|
| 85 | pg-response-maybe-erase 14 0.0002989999 2.135...e-05 |
|---|
| 86 | proof-debug 204 0.0002980000 1.460...e-06 |
|---|
| 87 | proof-looking-at 52 0.00028 5.384...e-06 |
|---|
| 88 | proof-get-window-for-buffer 8 0.000264 3.3e-05 |
|---|
| 89 | proof-shell-ready-prover 18 0.0001929999 1.072...e-05 |
|---|
| 90 | proof-shell-start 18 0.0001149999 6.388...e-06 |
|---|
| 91 | pg-autotest-test-assert-full 2 0.000107 5.35e-05 |
|---|
| 92 | proof-complete-buffer-atomic 2 0.000105 5.25e-05 |
|---|
| 93 | proof-grab-lock 8 0.0001040000 1.300...e-05 |
|---|
| 94 | pg-hint 2 9.6e-05 4.8e-05 |
|---|
| 95 | proof-script-end 2 8.7e-05 4.35e-05 |
|---|
| 96 | proof-locked-region-empty-p 16 7.000...e-05 4.375...e-06 |
|---|
| 97 | proof-maybe-follow-locked-end 2 5.2e-05 2.6e-05 |
|---|
| 98 | proof-shell-live-buffer 18 4.499...e-05 2.499...e-06 |
|---|
| 99 | proof-detach-queue 10 4.1e-05 4.1e-06 |
|---|
| 100 | proof-only-whitespace-to-locked-region-p 2 3.6e-05 1.8e-05 |
|---|
| 101 | proof-unprocessed-begin 36 3.6e-05 1e-06 |
|---|
| 102 | proof-shell-strip-eager-annotations 6 3.5e-05 5.833...e-06 |
|---|
| 103 | proof-re-search-forward 8 3.299...e-05 4.124...e-06 |
|---|
| 104 | pg-clear-script-portions 4 3e-05 7.5e-06 |
|---|
| 105 | proof-files-to-buffers 2 2.7e-05 1.35e-05 |
|---|
| 106 | proof-re-search-backward 2 2e-05 1e-05 |
|---|
| 107 | proof-shell-action-list-item 10 1.7e-05 1.7e-06 |
|---|
| 108 | proof-queue-or-locked-end 14 1.600...e-05 1.142...e-06 |
|---|
| 109 | proof-shell-stop-silent-item 2 1.300...e-05 6.500...e-06 |
|---|
| 110 | proof-shell-should-be-silent 8 1.300...e-05 1.625...e-06 |
|---|
| 111 | proof-shell-start-silent-item 2 1e-05 5e-06 |
|---|
| 112 | proof-associated-buffers 8 6.999...e-06 8.749...e-07 |
|---|
| 113 | proof-colour-locked-span 4 6.999...e-06 1.749...e-06 |
|---|
| 114 | pg-finish-tracing-display 8 6.999...e-06 8.749...e-07 |
|---|
| 115 | proof-minibuffer-message 6 4.999...e-06 8.333...e-07 |
|---|
| 116 | proof-pbp-focus-on-first-goal 8 4.999...e-06 6.249...e-07 |
|---|
| 117 | proof-done-invisible 6 4.999...e-06 8.333...e-07 |
|---|
| 118 | proof-set-queue-endpoints 2 4e-06 2e-06 |
|---|
| 119 | proof-detach-locked 2 4e-06 2e-06 |
|---|
| 120 | pg-autotest-timestart 2 4e-06 2e-06 |
|---|
| 121 | proof-query-save-this-buffer-p 2 3e-06 1.5e-06 |
|---|
| 122 | proof-script-next-command-advance 2 3e-06 1.5e-06 |
|---|
| 123 | proof-release-lock 8 3e-06 3.75e-07 |
|---|
| 124 | proof-auto-retract-dependencies 2 2e-06 1e-06 |
|---|
| 125 | proof-shell-clear-silent 2 2e-06 1e-06 |
|---|
| 126 | pg-clear-input-ring 4 2e-06 5e-07 |
|---|
| 127 | proof-shell-set-silent 2 0.0 0.0 |
|---|
| 128 | |
|---|
| 129 | |
|---|
| 130 | TEST: (eval (proof-shell-ready-prover)) |
|---|
| 131 | TEST: (eval (isar-tracing:auto-quickcheck-toggle 0)) |
|---|
| 132 | TEST: (eval (isar-tracing:auto-solve-toggle 0)) |
|---|
| 133 | TEST: (eval (proof-full-annotation-toggle 0)) |
|---|
| 134 | TEST: (process-wholefile "etc/isar/AHundredTheorems.thy") |
|---|
| 135 | TIME: 20.758037 (this test) |
|---|
| 136 | TEST: (process-wholefile "etc/isar/AHundredTheorems.thy") |
|---|
| 137 | TIME: 20.700929 (this test) |
|---|
| 138 | TEST: (process-wholefile "etc/isar/AHundredTheorems.thy") |
|---|
| 139 | TIME: 20.832824 (this test) |
|---|
| 140 | TEST: (process-wholefile "etc/isar/AHundredTheorems.thy") |
|---|
| 141 | TIME: 20.187454 (this test) |
|---|
| 142 | TEST: (process-wholefile "etc/isar/AHundredTheorems.thy") |
|---|
| 143 | TIME: 20.391642 (this test) |
|---|
