diff options
| author | David Aspinall | 2009-08-17 13:10:17 +0000 |
|---|---|---|
| committer | David Aspinall | 2009-08-17 13:10:17 +0000 |
| commit | 660bf86b2aee99b6a8f0005e26c2e7efe7a41d32 (patch) | |
| tree | effc3fa9aa9aad633a95da9cc1fedeb546ecce36 | |
| parent | 7c44e8472d020385d59254e6b88de3dfdc96ae63 (diff) | |
New files.
| -rw-r--r-- | etc/profiling.txt | 408 |
1 files changed, 408 insertions, 0 deletions
diff --git a/etc/profiling.txt b/etc/profiling.txt new file mode 100644 index 00000000..8348c7ad --- /dev/null +++ b/etc/profiling.txt @@ -0,0 +1,408 @@ +Notes on Profiling Proof General in XEmacs [da] +------------------------------------------------ + +Usage of Elisp profiler: + + M-x elp-instrument-package RET proof RET + +< do something now > + + M-x elp-results + +To display results. + + +M-x clear-profiling-info +Eval: (profile (proof-toolbar-next) (proof-shell-wait)) +M-x profile-results + +NB: Must ignore calls to accept-process-output and sit-for, these + are from proof-shell-wait (only). + + +Testing by processing first line of src/HOL/Real/ROOT.ML (i.e. loading +RealDef) + +Best case scenarios: + + * Running Isabelle in ordinary shell buffer in Emacs, PIII: + ~8% Emacs (PIII), ~90% SML if shell hidden + ~15% X, ~25% xemacs, ~60% SML if shell displayed! + + * Running Isabelle in xterm: + ~3% xterm, ~2% X, 95% SML if xterm hidden + ~4% xterm, ~16% X, 90% SML if xterm revealed + + +Before optimization: + + * CPU time split about 70%/30% (Cel 366) or 65%/35% (PIII 500) SML/xemacs + + + + + + + + +Sample Runs. Tue Oct 5 +----------------------- + +[On Cel 366 64M] + + +Function Name Ticks %/Total Call Count +=================================== ===== ======= ========== +(in redisplay) 1183 44.947 +re-search-forward 901 34.233 8061 +sit-for 159 6.041 11919 +comint-output-filter 93 3.533 3596 +accept-process-output 43 1.634 11919 +string-match 34 1.292 7300 +font-lock-pre-idle-hook 30 1.140 25261 +insert-before-markers 28 1.064 3597 +let 14 0.532 10853 +map-extents 13 0.494 539 +(in garbage collection) 10 0.380 +byte-code 9 0.342 25376 +while 8 0.304 3648 +setq 7 0.266 8299 +comint-postoutput-scroll-to-bottom 7 0.266 3597 +next-window 6 0.228 7194 +put-nonduplicable-text-property 5 0.190 1166 +marker-position 5 0.190 14389 +goto-char 5 0.190 14097 +walk-windows 4 0.152 3597 +window-minibuffer-p 4 0.152 3597 +proof-toolbar-refresh 4 0.152 3686 +and 4 0.152 11162 +selected-window 3 0.114 14390 +window-start 3 0.114 3596 +proof-shell-filter 3 0.114 3597 +itimer-time-difference 3 0.114 546 +#<compiled-function (window) "...(134)" [window-buffer window current window-point process-mark process scroll t all this selected others string set-window-point comint-scroll-show-maximum-output pos-visible-in-window-p recenter floatp floor window-height 1 -1 sit-for 0] 4> 3 0.114 7194 +#<compiled-function (place &optional x) "...(29)" [place setq x + 1+ callf 1] 5 553442> 3 0.114 1298 +process-buffer 3 0.114 3596 +point 3 0.114 7382 +or 3 0.114 7256 +comint-watch-for-password-prompt 3 0.114 3597 +save-excursion 2 0.076 3655 +proof-shell-process-urgent-messages 2 0.076 3597 +marker-buffer 2 0.076 3596 +font-lock-fontify-keywords-region 2 0.076 45 +process-mark 2 0.076 7208 +redisplay-echo-area 2 0.076 23 +if 2 0.076 18901 +buffer-name 1 0.038 3650 +erase-buffer 1 0.038 26 +pos-visible-in-window-p 1 0.038 1 +window-buffer 1 0.038 7195 +self-insert-command 1 0.038 14 +< 1 0.038 4300 +itimer-timer-driver 1 0.038 182 +font-lock-fontify-glumped-region 1 0.038 31 +get-buffer-process 1 0.038 3633 +char-to-string 1 0.038 3597 +save-current-buffer 1 0.038 17 +insert-string 1 0.038 23 +-------------------------------------------------------------------- +Total 2632 100.00 + + +One tick = 1 ms + + +[On PIII 256M] top shows roughly 65% SML / 35% xemacs. + +Function Name Ticks %/Total Call Count +====================================== ===== ======= ========== +(in redisplay) 3529 55.166 +re-search-forward 1520 23.761 31627 +sit-for 356 5.565 33870 +comint-output-filter 265 4.143 12980 +accept-process-output 125 1.954 33870 +font-lock-pre-idle-hook 67 1.047 73094 +insert-before-markers 51 0.797 12981 +(in garbage collection) 46 0.719 +string-match 44 0.688 27686 +byte-code 27 0.422 74822 +let 23 0.360 39724 +#<compiled-function (window) "...(134)" [window-buffer window current window-point process-mark process scroll t all this selected others string set-window-point comint-scroll-show-maximum-output pos-visible-in-window-p recenter floatp floor window-height 1 -1 sit-for 0] 4> 21 0.328 25962 +selected-window 20 0.313 51951 +comint-postoutput-scroll-to-bottom 19 0.297 12981 +setq 15 0.234 39971 +if 15 0.234 72709 +walk-windows 13 0.203 12981 +proof-toolbar-refresh 13 0.203 14429 +marker-position 12 0.188 51925 +proof-shell-filter 12 0.188 12981 +goto-char 12 0.188 53685 +run-hook-with-args 12 0.188 13219 +next-window 11 0.172 25962 +and 9 0.141 40761 +save-excursion 8 0.125 13756 +buffer-name 7 0.109 13783 +window-buffer 7 0.109 26077 +log-message 7 0.109 237 +process-mark 7 0.109 26208 +point 7 0.109 27554 +while 7 0.109 13727 +#<compiled-function (place &optional x) "...(29)" [place setq x + 1+ callf 1] 5 553442> 6 0.094 11268 +char-to-string 6 0.094 12981 +force-mode-line-update 6 0.094 12980 +< 5 0.078 19216 +itimer-run-expired-timers 4 0.063 415 +aref 4 0.063 11953 +get-buffer-process 4 0.063 13290 +proof-shell-process-urgent-messages 4 0.063 12981 +redisplay-echo-area 4 0.063 238 +insert-string 4 0.063 238 +font-lock-fontify-keywords-region 4 0.063 740 +window-minibuffer-p 3 0.047 12981 +window-start 3 0.047 12980 +marker-buffer 3 0.047 12980 +process-buffer 3 0.047 12980 +featurep 3 0.047 2120 +comint-watch-for-password-prompt 3 0.047 12981 +set-buffer 2 0.031 259 +or 2 0.031 26285 +font-lock-after-change-function-1 2 0.031 494 +font-lock-default-fontify-region 2 0.031 740 +event-over-toolbar-p 1 0.016 107 +get-buffer 1 0.016 433 +extent-object 1 0.016 988 +itimerp 1 0.016 9136 +itimer-is-idle 1 0.016 3735 +set-extent-property 1 0.016 1024 +make-string 1 0.016 247 +next-single-property-change 1 0.016 246 +expand-file-name 1 0.016 96 +incf 1 0.016 11268 +center-to-window-line 1 0.016 9 +proof-done-advancing 1 0.016 2 +itimer-time-difference 1 0.016 1660 +itimer-timer-driver 1 0.016 415 +1+ 1 0.016 11268 +length 1 0.016 249 +append-message 1 0.016 238 +concat 1 0.016 246 +proof-shell-strip-special-annotations 1 0.016 246 +proof-shell-process-urgent-message 1 0.016 246 +buffer-substring 1 0.016 493 +save-current-buffer 1 0.016 248 +newline 1 0.016 246 +insert 1 0.016 249 +current-time 1 0.016 831 +match-beginning 1 0.016 247 +font-lock-append-text-property 1 0.016 246 +progn 1 0.016 1034 +proof-response-buffer-display 1 0.016 246 +font-lock-fontify-syntactically-region 1 0.016 740 +font-lock-fontify-glumped-region 1 0.016 494 +#<compiled-function (buffer &rest body) "...(8)" [save-current-buffer set-buffer buffer body] 3 540150> 1 0.016 248 +font-lock-after-change-function 1 0.016 494 +----------------------------------------------------------------------- +Total 6397 100.00 + + +One tick = 1 ms + + +*** After some optimization attempt in proof-shell-process-urgent-messages, + to remove re-search-forward hog: + +[Cel 366] + +Function Name Ticks %/Total Call Count +=================================== ===== ======= ========== +accept-process-output 3279 62.374 1047436 +(in redisplay) 919 17.481 +sit-for 547 10.405 1047435 +re-search-forward 134 2.549 8950 +while 110 2.092 3648 +comint-output-filter 65 1.236 3347 +(in garbage collection) 24 0.457 +font-lock-pre-idle-hook 18 0.342 14166 +insert-before-markers 15 0.285 3348 +string-match 10 0.190 7376 +let 9 0.171 7010 +#<compiled-function (window) "...(134)" [window-buffer window current window-point process-mark process scroll t all this selected others string set-window-point comint-scroll-show-maximum-output pos-visible-in-window-p recenter floatp floor window-height 1 -1 sit-for 0] 4> 9 0.171 6696 +setq 6 0.114 12598 +byte-code 5 0.095 14879 +#<compiled-function (place &optional x) "...(29)" [place setq x + 1+ callf 1] 5 553442> 5 0.095 4762 +and 5 0.095 10936 +comint-postoutput-scroll-to-bottom 5 0.095 3348 +log-message 4 0.076 98 +save-excursion 3 0.057 3655 +itimerp 3 0.057 14128 +selected-window 3 0.057 13403 +next-window 3 0.057 6696 +point 3 0.057 10722 +proof-toolbar-refresh 3 0.057 3942 +if 3 0.057 23233 +font-lock-default-unfontify-region 3 0.057 295 +walk-windows 2 0.038 3348 +event-window 2 0.038 658 +buffer-name 2 0.038 3670 +erase-buffer 2 0.038 105 +put-nonduplicable-text-property 2 0.038 590 +window-start 2 0.038 3347 +null 2 0.038 3352 +marker-position 2 0.038 13393 +marker-buffer 2 0.038 3347 +itimer-time-difference 2 0.038 2223 +- 2 0.038 3350 +font-lock-fontify-keywords-region 2 0.038 295 +goto-char 2 0.038 14092 +buffer-substring 2 0.038 196 +redisplay-echo-area 2 0.038 104 +run-hook-with-args 2 0.038 3447 +comint-watch-for-password-prompt 2 0.038 3348 +event-over-vertical-divider-p 1 0.019 254 +event-glyph-extent 1 0.019 329 +get-buffer 1 0.019 255 +pointer-image-instance-p 1 0.019 985 +barf-if-buffer-read-only 1 0.019 98 +extent-at 1 0.019 87 +itimer-value 1 0.019 6175 +pos-visible-in-window-p 1 0.019 4 +expand-file-name 1 0.019 192 +file-truename 1 0.019 104 +center-to-window-line 1 0.019 4 +proof-shell-process-urgent-messages 1 0.019 3348 +proof-shell-filter 1 0.019 3348 +set-marker 1 0.019 3429 +itimer-run-expired-timers 1 0.019 247 +< 1 0.019 5950 +min 1 0.019 3428 +1- 1 0.019 3428 +display-message 1 0.019 99 +font-lock-fontify-glumped-region 1 0.019 197 +get-buffer-process 1 0.019 6791 +process-mark 1 0.019 10124 +default-mouse-motion-handler 1 0.019 329 +char-to-string 1 0.019 3348 +save-current-buffer 1 0.019 99 +newline 1 0.019 98 +or 1 0.019 3490 +#<compiled-function (buffer &rest body) "...(8)" [save-current-buffer set-buffer buffer body] 3 540150> 1 0.019 99 +font-lock-unfontify-region 1 0.019 295 +specifier-instance 1 0.019 329 +-------------------------------------------------------------------- +Total 5257 100.00 + + +One tick = 1 ms + + +[PIII] split now about 70%/30% + +Function Name Ticks %/Total Call Count +====================================== ===== ======= ========== +(in redisplay) 3638 72.082 +sit-for 358 7.093 34176 +comint-output-filter 247 4.894 12963 +accept-process-output 132 2.615 34176 +font-lock-pre-idle-hook 70 1.387 74389 +insert-before-markers 67 1.328 12964 +string-match 50 0.991 27655 +(in garbage collection) 43 0.852 +#<compiled-function (window) "...(134)" [window-buffer window current window-point process-mark process scroll t all this selected others string set-window-point comint-scroll-show-maximum-output pos-visible-in-window-p recenter floatp floor window-height 1 -1 sit-for 0] 4> 29 0.575 25928 +re-search-forward 25 0.495 18630 +comint-postoutput-scroll-to-bottom 24 0.476 12964 +byte-code 22 0.436 76129 +selected-window 20 0.396 51883 +walk-windows 19 0.376 12964 +let 18 0.357 13746 +next-window 16 0.317 25928 +proof-toolbar-refresh 13 0.258 14445 +while 13 0.258 13710 +proof-shell-filter 11 0.218 12964 +process-mark 11 0.218 39137 +save-excursion 10 0.198 13741 +setq 10 0.198 27010 +and 9 0.178 27701 +goto-char 8 0.159 27695 +run-hook-with-args 8 0.159 13211 +if 7 0.139 33491 +font-lock-fontify-keywords-region 6 0.119 740 +#<compiled-function (place &optional x) "...(29)" [place setq x + 1+ callf 1] 5 553442> 6 0.119 11268 +get-buffer-process 6 0.119 26242 +char-to-string 6 0.119 12964 +redisplay-echo-area 6 0.119 253 +specifier-instance 6 0.119 656 +itimerp 5 0.099 5713 +1- 5 0.099 13209 +point 5 0.099 27523 +buffer-name 4 0.079 13766 +current-buffer 4 0.079 13210 +window-start 4 0.079 12963 +< 4 0.079 6236 +itimer-timer-driver 4 0.079 380 +default-mouse-motion-handler 4 0.079 656 +featurep 4 0.079 2693 +force-mode-line-update 4 0.079 12963 +comint-watch-for-password-prompt 4 0.079 12964 +proof-shell-process-urgent-messages 3 0.059 12964 +font-lock-fontify-syntactically-region 3 0.059 740 +incf 3 0.059 11268 +marker-position 3 0.059 12968 +set-marker 3 0.059 13210 +itimer-time-difference 3 0.059 1140 +process-buffer 3 0.059 12963 +event-window 2 0.040 1312 +window-minibuffer-p 2 0.040 12964 +window-buffer 2 0.040 26524 +- 2 0.040 12967 +move-to-left-margin 2 0.040 246 +remove-message 2 0.040 253 +event-buffer 2 0.040 656 +font-lock-default-unfontify-region 2 0.040 740 +font-lock-after-change-function 2 0.040 494 +buffer-substring 2 0.040 493 +insert-string 2 0.040 253 +event-over-modeline-p 1 0.020 537 +event-glyph-extent 1 0.020 656 +set-syntax-table 1 0.020 740 +pointer-image-instance-p 1 0.020 1913 +extent-start-position 1 0.020 494 +make-extent 1 0.020 527 +detach-extent 1 0.020 495 +extent-at 1 0.020 363 +itimer-value 1 0.020 2660 +itimer-is-idle 1 0.020 2280 +set-extent-property 1 0.020 1024 +highlight-extent 1 0.020 656 +pos-visible-in-window-p 1 0.020 9 +glyph-property-instance 1 0.020 656 +get-text-property 1 0.020 492 +put-nonduplicable-text-property 1 0.020 1480 +next-single-property-change 1 0.020 246 +quote 1 0.020 13798 +marker-buffer 1 0.020 12963 +itimer-run-expired-timers 1 0.020 380 +aset 1 0.020 5280 +log-message 1 0.020 246 +min 1 0.020 13209 +current-left-margin 1 0.020 246 +display-message 1 0.020 246 +fw-frame 1 0.020 656 +font-lock-fontify-region 1 0.020 740 +font-lock-append-text-property 1 0.020 246 +substring 1 0.020 247 +proof-response-buffer-display 1 0.020 246 +delq 1 0.020 246 +syntactically-sectionize 1 0.020 740 +format 1 0.020 238 +proof-file-truename 1 0.020 88 +newline 1 0.020 246 +store-match-data 1 0.020 742 +proof-zap-commas-region 1 0.020 494 +specifierp 1 0.020 656 +log-message-filter 1 0.020 246 +----------------------------------------------------------------------- +Total 5047 100.00 + + +One tick = 1 ms + |