cpitclaudel
commented
8 years ago Can you try profiling and see if that shows interesting patterns? M-x profiler-start
Open JasonGross opened 8 years ago
cpitclaudel
commented
8 years ago Can you try profiling and see if that shows interesting patterns? M-x profiler-start
JasonGross
commented
8 years ago - command-execute 2637 68%
- call-interactively 2637 68%
- company-coq-proof-goto-point 854 22%
- apply 854 22%
- proof-goto-point 854 22%
- proof-assert-until-point 854 22%
- run-hooks 645 16%
- coq-adapt-printing-width 645 16%
- proof-shell-invisible-command 645 16%
+ proof-shell-ready-prover 345 8%
+ proof-shell-wait 300 7%
+ proof-activate-scripting 199 5%
+ proof-segment-up-to-using-cache 10 0%
- proof-shell-exit 703 18%
- kill-buffer 613 15%
- proof-shell-kill-function 613 15%
- byte-code 551 14%
- proof-deactivate-scripting-auto 532 13%
- byte-code 532 13%
- proof-deactivate-scripting 532 13%
- proof-protected-process-or-retract 532 13%
- proof-shell-wait 528 13%
- redisplay 521 13%
- timer-event-handler 446 11%
- byte-code 446 11%
- apply 446 11%
+ company-coq-maybe-reload-each 444 11%
+ proof-retract-buffer 4 0%
+ proof-shell-wait 19 0%
redisplay 62 1%
+ yes-or-no-p 83 2%
- byte-code 514 13%
+ read-extended-command 458 11%
+ find-file-read-args 56 1%
+ scroll-up-command 302 7%
scroll-down-command 157 4%
+ next-line 62 1%
+ previous-line 33 0%
+ execute-extended-command 12 0%
- timer-event-handler 960 24%
- byte-code 958 24%
- apply 958 24%
- company-coq-maybe-reload-each 857 22%
- company-coq-init-symbols 598 15%
- company-coq-reload-db 598 15%
- company-coq-get-symbols 598 15%
+ mapc 321 8%
+ company-coq-ask-prover-redirect 212 5%
+ company-coq-split-lines 29 0%
+ company-coq-union-sort 28 0%
- company-coq-init-tactics 160 4%
+ company-coq-reload-db 160 4%
+ company-coq-init-modules 99 2%
+ company-coq-features/spinner--spin 33 0%
+ timer-inc-time 2 0%
+ redisplay_internal (C function) 119 3%
+ ... 105 2%
+ scomint-output-filter 45 1%vs vanilla:
- command-execute 521 90%
- call-interactively 521 90%
- proof-goto-point 286 49%
- proof-assert-until-point 286 49%
- proof-activate-scripting 255 44%
- proof-shell-ready-prover 255 44%
- proof-shell-start 255 44%
- coq-shell-mode 116 20%
- coq-shell-mode-config 116 20%
+ proof-shell-config-done 116 20%
- coq-prog-args 83 14%
- coq-autodetect-version 64 11%
+ shell-command 64 11%
+ coq-load-project-file 15 2%
+ read-shell-command 52 9%
+ proof-multiple-frames-enable 4 0%
+ run-hooks 21 3%
+ proof-segment-up-to-using-cache 10 1%
- proof-shell-exit 112 19%
- kill-buffer 83 14%
- proof-shell-kill-function 83 14%
+ byte-code 51 8%
redisplay 29 5%
yes-or-no-p 16 2%
+ byte-code 68 11%
+ minibuffer-complete 35 6%
+ execute-extended-command 11 1%
+ next-line 9 1%
+ ... 41 7%
+ redisplay_internal (C function) 8 1%
+ scomint-output-filter 6 1%
+ timer-event-handler 1 0%Is there a way to get actual times out of this?
JasonGross
commented
8 years ago Here's the 20s that it takes to execute a proof-goto-point of 25 lines of code, and then another proof-goto-point that retracts the first one:
- timer-event-handler 790 76%
- byte-code 782 75%
- apply 782 75%
- company-coq-maybe-reload-each 670 64%
- company-coq-init-symbols 412 39%
- company-coq-reload-db 412 39%
- company-coq-get-symbols 412 39%
- mapc 230 22%
- company-coq-ask-prover 230 22%
- proof-shell-invisible-command 230 22%
- proof-shell-wait 230 22%
- redisplay 230 22%
+ timer-event-handler 4 0%
- company-coq-ask-prover-redirect 154 14%
- company-coq-ask-prover 154 14%
- proof-shell-invisible-command 154 14%
- proof-shell-wait 154 14%
- redisplay 151 14%
+ redisplay_internal (C function) 3 0%
+ timer-event-handler 2 0%
+ accept-process-output 3 0%
+ company-coq-split-lines 16 1%
+ company-coq-union-sort 12 1%
- company-coq-init-tactics 162 15%
- company-coq-reload-db 162 15%
- company-coq-get-tactics 162 15%
+ company-coq-get-ltacs 81 7%
+ company-coq-get-notations 81 7%
+ company-coq-init-modules 96 9%
+ company-coq-features/spinner--spin 5 0%
+ timer-inc-time 8 0%
+ command-execute 100 9%
+ redisplay_internal (C function) 80 7%
+ ... 56 5%
+ scomint-output-filter 12 1%In vanilla PG, it takes 3 seconds, and at least half of that time is time that I spent moving the cursor:
- command-execute 139 77%
- call-interactively 139 77%
- byte-code 78 43%
- read-extended-command 78 43%
- completing-read 78 43%
- completing-read-default 78 43%
- read-from-minibuffer 51 28%
+ redisplay_internal (C function) 4 2%
- previous-line 40 22%
- funcall 40 22%
- #<compiled 0xeb5d83> 40 22%
- line-move 40 22%
line-move-visual 31 17%
+ execute-extended-command 9 5%
scroll-down-command 8 4%
+ next-line 4 2%
+ redisplay_internal (C function) 16 8%
+ scomint-output-filter 13 7%
+ ... 11 6%Wait, I'm confused. Is this for the slow-down thing? Thanks for the profiles then :) But I was thinking of a memory profile, to diagnose your suspected leak.
cpitclaudel
commented
8 years ago Can you try making a performance profile without dynamic completion, too? I expect dynamic completion to be slow.
JasonGross
commented
8 years ago This is from after it's been running for a while. I have easy access to a slow one, less easy access to one that's slowing down fast enough.
Why is dynamic completion doing anything in the middle of proof-goto-point? Why is it doing anything in the middle of a retract? Most of the time is spent crawling through the individual lines.
In company-coq:
In vanilla PG:
JasonGross
commented
8 years ago Here's a memory profile: Company-coq:
- redisplay_internal (C function) 182,751,115 70%
- eval 162,578,898 62%
- list 160,988,079 61%
- company-coq--lighter-string 160,876,783 61%
- company-coq--ligther-image 80,480,629 30%
company-coq--icon 80,347,282 30%
company-coq--icon 80,306,362 30%
apply 89,792 0%
if 1,523,884 0%
unless 47,840 0%
+ tool-bar-make-keymap 17,874,928 6%
+ jit-lock-function 851,218 0%
+ keymap-canonicalize 452,592 0%
file-remote-p 136,980 0%
+ #<compiled 0x3f9111> 123,552 0%
+ x-gtk-map-stock 73,698 0%
proof-toolbar-next-enable-p 14,784 0%
proof-toolbar-use-enable-p 8,448 0%
- command-execute 74,622,285 28%
- call-interactively 74,622,285 28%
- company-coq-proof-goto-point 60,271,348 23%
- apply 60,266,164 23%
- proof-goto-point 60,266,164 23%
- proof-assert-until-point 60,264,116 23%
- proof-activate-scripting 57,536,875 22%
- proof-shell-ready-prover 56,506,909 21%
- proof-shell-start 56,506,909 21%
- coq-shell-mode 37,981,725 14%
- coq-shell-mode-config 37,978,621 14%
- proof-shell-config-done 37,974,477 14%
+ mapcar 28,490,615 10%
+ run-hooks 6,934,321 2%
+ mapc 1,371,348 0%
+ proof-shell-wait 608,853 0%
+ accept-process-output 39,876 0%
+ proof-assistant-settings-cmds 4,096 0%
coq-init-syntax-table 4,144 0%
+ proof-shell-mode 2,080 0%
+ run-mode-hooks 1,024 0%
+ coq-prog-args 9,072,376 3%
+ read-shell-command 6,266,327 2%
+ proof-multiple-frames-enable 2,145,076 0%
+ apply 927,075 0%
+ coq-goals-mode 76,776 0%
+ coq-response-mode 35,496 0%
proof-shell-make-associated-buffers 2,058 0%
+ proof-unregister-buffer-file-name 931,378 0%
+ run-hooks 98,588 0%
+ run-hooks 2,422,315 0%
+ proof-segment-up-to-using-cache 155,376 0%
+ proof-assert-semis 149,550 0%
proof-only-whitespace-to-locked-region-p 2,048 0%
+ company-abort 5,184 0%
+ byte-code 7,593,250 2%
+ execute-extended-command 4,325,037 1%
+ mouse-drag-region 1,287,915 0%
+ yank 867,839 0%
+ next-line 271,728 0%
+ handle-focus-in 2,080 0%
+ previous-line 2,048 0%
+ handle-focus-out 1,040 0%
+ scomint-output-filter 2,810,755 1%
+ timer-event-handler 808,372 0%
+ ... 8,188 0%
+ yas--post-command-handler 7,488 0%Vanilla PG:
- command-execute 5,773,883 67%
- call-interactively 5,773,883 67%
- execute-extended-command 3,890,006 45%
- command-execute 3,815,966 44%
- call-interactively 3,815,950 44%
- profiler-report 3,815,950 44%
+ profiler-report-cpu 1,965,990 23%
+ profiler-report-memory 1,849,960 21%
- byte-code 1,512,583 17%
- read-extended-command 1,512,583 17%
- completing-read 1,512,583 17%
- completing-read-default 1,512,583 17%
- read-from-minibuffer 1,510,957 17%
- redisplay_internal (C function) 1,480,346 17%
- tool-bar-make-keymap 1,312,760 15%
- tool-bar-make-keymap-1 1,312,760 15%
- mapcar 1,312,760 15%
- #<compiled 0x279b9b> 1,312,760 15%
- eval 1,312,760 15%
- find-image 1,312,760 15%
image-search-load-path 1,312,760 15%
+ jit-lock-function 167,586 1%
+ minibuffer-inactive-mode 1,024 0%
command-execute 64 0%
+ next-line 303,498 3%
+ proof-goto-point 67,796 0%
- scomint-output-filter 1,580,314 18%
- run-hook-with-args 1,580,314 18%
- proof-shell-filter-wrapper 1,580,314 18%
- byte-code 1,580,314 18%
- proof-shell-filter 1,580,314 18%
- proof-shell-filter-manage-output 1,550,072 18%
- proof-shell-exec-loop 1,530,452 17%
- proof-shell-insert 1,378,990 16%
scomint-send-input 1,378,990 16%
+ mapc 122,958 1%
+ pg-processing-complete-hint 28,504 0%
proof-shell-handle-immediate-output 16,548 0%
+ proof-shell-handle-delayed-output 3,072 0%
+ proof-shell-process-urgent-messages 22,660 0%
- redisplay_internal (C function) 1,160,200 13%
- tool-bar-make-keymap 1,124,348 13%
- tool-bar-make-keymap-1 1,124,348 13%
- mapcar 1,124,348 13%
- #<compiled 0x279b9b> 1,124,348 13%
- eval 1,124,348 13%
- find-image 1,124,348 13%
image-search-load-path 1,124,348 13%
file-remote-p 27,664 0%
+ eval 8,188 0%
+ ... 8,188 0%Is emacs unhappy with your spinning rooster icon?
cpitclaudel
commented
8 years ago Hmm. Let's look at this together :)
JasonGross
commented
8 years ago Sounds good. I'm in my office now and will be until 4.
cpitclaudel
commented
8 years ago Tomorrow will probably work better for me :)
cpitclaudel
commented
8 years ago Thanks for all your help, btw!
JasonGross
commented
8 years ago After in-person debugging with @cpitclaudel, this seems to be related to https://debbugs.gnu.org/cgi/bugreport.cgi?bug=21028.
I find that company-coq seems to get slower and slower the longer I've had emacs running, to the point where it can be many orders of magnitude slower than vanilla PG at executing statements like
Require Import ...andProof..