diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 2009-09-04 16:50:32 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 2009-09-04 16:50:32 +0000 |
| commit | 45d5c186ade7b26404a9652d462e6c3940382419 (patch) | |
| tree | 1efd7a318a416aa480c70740532e8cb676603cfa /etc/isar | |
| parent | 17460bf8b246b7f26b390ca67145c11ee230de9d (diff) | |
some profiling records
Diffstat (limited to 'etc/isar')
| -rw-r--r-- | etc/isar/profiling.txt | 217 |
1 files changed, 217 insertions, 0 deletions
diff --git a/etc/isar/profiling.txt b/etc/isar/profiling.txt new file mode 100644 index 00000000..d732b4f5 --- /dev/null +++ b/etc/isar/profiling.txt @@ -0,0 +1,217 @@ +Profiling of hundred theorems: + +proof-shell-filter 206 0.5755520000 0.0027939417 +proof-shell-filter-manage-output 206 0.4828650000 0.0023440048 +proof-shell-exec-loop 206 0.479615 0.0023282281 +proof-done-advancing 204 0.3241909999 0.0015891715 +proof-done-advancing-save 100 0.2885119999 0.0028851199 +proof-make-goalsave 100 0.2780209999 0.0027802099 +pg-add-proof-element 100 0.2667299999 0.0026672999 +proof-next-element-id 100 0.2568640000 0.0025686400 +proof-element-id 100 0.2559739999 0.0025597399 +proof-shell-insert 206 0.1490790000 0.0007236844 +scomint-send-input 206 0.0973649999 0.0004726456 +scomint-send-string 206 0.0899980000 0.0004368834 +pg-remove-specials 206 0.0822929999 0.0003994805 +isar-preprocessing 206 0.0361179999 0.0001753300 +proof-toolbar-next-enable-p 638 0.0286260000 4.486...e-05 +isar-command-wrapping 206 0.0269059999 0.0001306116 +proof-locked-region-full-p 639 0.0268030000 4.194...e-05 +pg-set-span-helphighlights 304 0.0225119999 7.405...e-05 +isar-positions-of 206 0.0202500000 9.830...e-05 +proof-toolbar-use-enable-p 319 0.0138090000 4.328...e-05 +proof-set-overlay-arrow 204 0.0115210000 5.647...e-05 +proof-string-match 1526 0.0104410000 6.842...e-06 +proof-shell-available-p 2233 0.0092940000 4.162...e-06 +proof-done-advancing-other 104 0.007964 7.657...e-05 +pg-last-output-displayform 304 0.0075990000 2.499...e-05 +isar-string-wrapping 412 0.0063830000 1.549...e-05 +proof-shell-strip-output-markup 304 0.0059760000 1.965...e-05 +isar-strip-output-markup 305 0.0048359999 1.585...e-05 +proof-replace-regexp-in-string 412 0.0047720000 1.158...e-05 +isar-shell-adjust-line-width 206 0.00416 2.019...e-05 +isar-global-save-command-p 100 0.0038479999 3.847...e-05 +proof-shell-process-urgent-messages 206 0.003735 1.813...e-05 +proof-string-match-safe 204 0.0032319999 1.584...e-05 +proof-toolbar-state-enable-p 319 0.0031699999 9.937...e-06 +pg-processing-complete-hint 1 0.002853 0.002853 +scomint-check-proc 2441 0.0028120000 1.151...e-06 +proof-get-name-from-goal 100 0.0026769999 2.676...e-05 +proof-toolbar-retract-enable-p 319 0.0025379999 7.956...e-06 +proof-toolbar-undo-enable-p 319 0.0024359999 7.636...e-06 +proof-toolbar-delete-enable-p 319 0.0023529999 7.376...e-06 +isar-goal-command-p 204 0.0021389999 1.048...e-05 +proof-toolbar-find-enable-p 319 0.0020489999 6.423...e-06 +proof-toolbar-context-enable-p 319 0.0018939999 5.937...e-06 +proof-toolbar-info-enable-p 319 0.0018169999 5.695...e-06 +proof-toolbar-command-enable-p 319 0.0017689999 5.545...e-06 +pg-add-element 100 0.0016860000 1.686...e-05 +proof-shell-classify-output 206 0.0016479999 7.999...e-06 +proof-locked-region-empty-p 320 0.0014510000 4.534...e-06 +pg-span-name 304 0.0012320000 4.052...e-06 +proof-process-buffer 1 0.001196 0.001196 +pg-add-to-input-history 104 0.0011950000 1.149...e-05 +proof-assert-until-point-interactive 1 0.001159 0.001159 +proof-assert-until-point 1 0.001155 0.001155 +proof-unprocessed-begin 1126 0.0010770000 9.564...e-07 +proof-shell-live-buffer 206 0.0010610000 5.150...e-06 +proof-assert-semis 1 0.001013 0.001013 +proof-splice-separator 206 0.0007109999 3.451...e-06 +proof-extend-queue 1 0.000638 0.000638 +proof-append-alist 1 0.00063 0.00063 +proof-semis-to-vanillas 1 0.000347 0.000347 +proof-next-element-count 100 0.0002829999 2.829...e-06 +proof-shell-process-urgent-message 1 0.00025 0.00025 +proof-toolbar-goto-enable-p 319 0.0002259999 7.084...e-07 +proof-toolbar-interrupt-enable-p 319 0.0001709999 5.360...e-07 +proof-debug 100 0.0001189999 1.189...e-06 +proof-segment-up-to-using-cache 1 9.6e-05 9.6e-05 +proof-segment-cache-contents-for 1 8.4e-05 8.4e-05 +pg-response-display-with-face 2 7.5e-05 3.75e-05 +proof-shell-message 1 7e-05 7e-05 +pg-response-maybe-erase 2 5e-05 2.5e-05 +pg-hint 1 3.9e-05 3.9e-05 +proof-re-search-backward 1 3e-05 3e-05 +proof-shell-ready-prover 2 2.100...e-05 1.050...e-05 +proof-shell-handle-delayed-output 1 2.1e-05 2.1e-05 +proof-activate-scripting 1 1.7e-05 1.7e-05 +proof-maybe-follow-locked-end 1 1.6e-05 1.6e-05 +proof-shell-start 2 1.5e-05 7.5e-06 +pg-response-display 1 1.4e-05 1.4e-05 +proof-grab-lock 1 1.2e-05 1.2e-05 +proof-script-next-command-advance 1 7e-06 7e-06 +proof-shell-strip-eager-annotations 1 7e-06 7e-06 +proof-shell-start-silent-item 1 6e-06 6e-06 +proof-shell-action-list-item 2 4e-06 2e-06 +proof-shell-stop-silent-item 1 4e-06 4e-06 +proof-queue-or-locked-end 4 3e-06 7.5e-07 +proof-shell-should-be-silent 1 2e-06 2e-06 +proof-shell-set-silent 1 1e-06 1e-06 +proof-shell-clear-silent 1 1e-06 1e-06 +proof-pbp-focus-on-first-goal 1 1e-06 1e-06 +proof-display-and-keep-buffer 1 1e-06 1e-06 +proof-release-lock 1 1e-06 1e-06 +pg-finish-tracing-display 1 1e-06 1e-06 + + +Profiling AThousandTheorems: + +proof-shell-filter 2009 4.2185289999 0.0020998153 +proof-shell-filter-manage-output 2008 3.7156680000 0.0018504322 +proof-process-buffer 1 3.681492 3.681492 +proof-assert-until-point-interactive 1 3.681391 3.681391 +proof-assert-until-point 1 3.681388 3.681388 +proof-shell-exec-loop 2008 3.6569860000 0.0018212081 +proof-assert-semis 1 2.165613 2.165613 +proof-activate-scripting 1 2.1626339999 2.1626339999 +proof-shell-wait 3 2.157879 0.719293 +proof-shell-insert 2008 1.8324589999 0.0009125791 +proof-done-advancing 2004 1.7108090000 0.0008536971 +proof-segment-up-to-using-cache 1 1.515725 1.515725 +proof-segment-up-to 1 1.5153910000 1.5153910000 +proof-segment-up-to-cmdstart 1 1.515388 1.515388 +proof-looking-at-syntactic-context 2012 1.2962439999 0.0006442564 +isar-syntactic-context 2012 1.2880049999 0.0006401615 +proof-looking-at-syntactic-context-default 2012 1.283686 0.0006380149 +proof-buffer-syntactic-context 2013 1.2504469999 0.0006211857 +proof-register-possibly-new-processed-file 2 1.147767 0.5738835 +proof-deactivate-scripting 1 1.146929 1.146929 +proof-shell-invisible-command 2 1.144748 0.572374 +proof-cd-sync 1 1.014265 1.014265 +scomint-send-input 2008 1.0111659999 0.0005035687 +proof-toolbar-next-enable-p 7434 0.6904569999 9.287...e-05 +proof-done-advancing-save 1000 0.6694850000 0.0006694850 +proof-locked-region-full-p 7437 0.6680110000 8.982...e-05 +isar-preprocessing 2008 0.5888010000 0.0002932275 +scomint-send-string 2008 0.5238210000 0.0002608670 +isar-command-wrapping 2008 0.4266709999 0.0002124855 +isar-positions-of 2008 0.2837250000 0.0001412973 +proof-make-goalsave 1000 0.2802490000 0.0002802490 +pg-set-span-helphighlights 3004 0.2778229999 9.248...e-05 +pg-remove-specials 2008 0.2700440000 0.0001344840 +proof-toolbar-use-enable-p 3717 0.2482730000 6.679...e-05 +proof-shell-available-p 26019 0.1759880000 6.763...e-06 +proof-re-search-forward 2064 0.1741260000 8.436...e-05 +pg-add-proof-element 1000 0.1635090000 0.0001635090 +proof-string-match 15032 0.1542850000 1.026...e-05 +proof-done-advancing-other 1004 0.1512260000 0.0001506235 +isar-string-wrapping 4015 0.1382279999 3.442...e-05 +proof-get-name-from-goal 1000 0.1235100000 0.0001235100 +proof-replace-regexp-in-string 4015 0.1221689999 3.042...e-05 +isar-global-save-command-p 1000 0.1135740000 0.0001135740 +proof-string-match-safe 2004 0.1066289999 5.320...e-05 +proof-toolbar-command-enable-p 3717 0.0918040000 2.469...e-05 +proof-set-overlay-arrow 2004 0.0877379999 4.378...e-05 +pg-add-to-input-history 1004 0.0811079999 8.078...e-05 +pg-last-output-displayform 3004 0.0799419999 2.661...e-05 +pg-add-element 1000 0.0758799999 7.587...e-05 +proof-shell-process-urgent-messages 2009 0.0691360000 3.441...e-05 +proof-shell-strip-output-markup 3006 0.0621240000 2.066...e-05 +isar-strip-output-markup 3008 0.0508979999 1.692...e-05 +isar-shell-adjust-line-width 2008 0.0436570000 2.174...e-05 +proof-shell-classify-output 2008 0.0423230000 2.107...e-05 +proof-toolbar-state-enable-p 3717 0.0384680000 1.034...e-05 +scomint-check-proc 28033 0.0319450000 1.139...e-06 +proof-toolbar-retract-enable-p 3717 0.0305389999 8.216...e-06 +isar-goal-command-p 2004 0.026745 1.334...e-05 +proof-cmdstart-add-segment-for-cmd 2004 0.0246840000 1.231...e-05 +proof-toolbar-delete-enable-p 3717 0.0242569999 6.525...e-06 +proof-toolbar-undo-enable-p 3717 0.0241040000 6.484...e-06 +proof-toolbar-context-enable-p 3717 0.0233320000 6.277...e-06 +proof-toolbar-find-enable-p 3717 0.0226730000 6.099...e-06 +proof-toolbar-info-enable-p 3717 0.0210330000 5.658...e-06 +proof-locked-region-empty-p 3722 0.0176580000 4.744...e-06 +proof-looking-at-safe 4012 0.0171930000 4.285...e-06 +proof-next-element-id 1000 0.0129890000 1.298...e-05 +pg-span-name 3004 0.0127430000 4.242...e-06 +proof-shell-live-buffer 2008 0.0114760000 5.715...e-06 +proof-unprocessed-begin 11480 0.0112319999 9.783...e-07 +proof-looking-at 4012 0.0082560000 2.057...e-06 +proof-splice-separator 2008 0.0070060000 3.489...e-06 +pg-processing-complete-hint 3 0.0058870000 0.0019623333 +proof-element-id 1000 0.0039640000 3.964...e-06 +proof-next-element-count 1000 0.0028809999 2.880...e-06 +proof-toolbar-goto-enable-p 3717 0.0027980000 7.527...e-07 +proof-semis-to-vanillas 1 0.002604 0.002604 +proof-toolbar-interrupt-enable-p 3717 0.0022529999 6.061...e-07 +proof-shell-process-urgent-message 3 0.001543 0.0005143333 +proof-debug 1003 0.0012860000 1.282...e-06 +proof-append-alist 3 0.000957 0.000319 +isar-match-nesting 51 0.000897 1.758...e-05 +proof-start-queue 2 0.000614 0.000307 +proof-unregister-buffer-file-name 1 0.000609 0.000609 +proof-cd 1 0.000429 0.000429 +proof-extend-queue 1 0.00036 0.00036 +proof-shell-message 2 0.000257 0.0001285 +pg-response-display-with-face 5 0.0001839999 3.679...e-05 +proof-format-filename 2 0.000173 8.65e-05 +pg-response-maybe-erase 5 0.000124 2.48e-05 +proof-shell-handle-delayed-output 3 0.000117 3.9e-05 +pg-response-display 3 9.5e-05 3.166...e-05 +pg-hint 1 7.1e-05 7.1e-05 +proof-format 10 6.1e-05 6.1e-06 +proof-shell-ready-prover 6 5.899...e-05 9.833...e-06 +proof-shell-start 6 3.8e-05 6.333...e-06 +proof-grab-lock 3 3.5e-05 1.166...e-05 +proof-re-search-backward 1 3.3e-05 3.3e-05 +proof-init-segmentation 1 2.4e-05 2.4e-05 +proof-shell-strip-eager-annotations 2 1.5e-05 7.5e-06 +proof-complete-buffer-atomic 1 1.4e-05 1.4e-05 +proof-maybe-follow-locked-end 1 1.1e-05 1.1e-05 +proof-shell-action-list-item 4 1.099...e-05 2.749...e-06 +proof-queue-or-locked-end 4 8e-06 2e-06 +proof-script-end 1 7e-06 7e-06 +proof-shell-stop-silent-item 1 6e-06 6e-06 +proof-shell-should-be-silent 3 6e-06 2e-06 +proof-shell-start-silent-item 1 6e-06 6e-06 +proof-span-read-only 2 4e-06 2e-06 +proof-display-and-keep-buffer 3 4e-06 1.333...e-06 +proof-pbp-focus-on-first-goal 3 3e-06 1e-06 +proof-release-lock 3 3e-06 1e-06 +pg-finish-tracing-display 3 3e-06 1e-06 +proof-done-invisible 2 2e-06 1e-06 +proof-script-next-command-advance 1 2e-06 2e-06 +pg-clear-script-portions 1 2e-06 2e-06 +proof-shell-set-silent 1 1e-06 1e-06 +proof-shell-clear-silent 1 1e-06 1e-06 +pg-clear-input-ring 1 1e-06 1e-06 |