What makes set-window-buffer slow?

What makes set-window-buffer slow?

[Clément Pit--Claudel]

[-- Attachment #1.1: Type: text/plain, Size: 1168 bytes --]

Hi emacs-devel,

This is a rather ill-defined question. I've just been through a round of 20 emails with a user, trying to understand which part of one of my packages made Proof General horribly slow. We progressively narrowed it down to this:

    (set-window-buffer win buf)

... which is definitely not what I expected. Note that:

* This happens in emacs -Q with just Proof General loaded
* The two hooks that set-window-buffer calls are nil (window-hscroll-functions and window-configuration-change-hook)
* This is called about 200 times (once for each full message received from a subprocess).
* Commenting out this line makes processing of these ~200 messages from the subprocess take 5 seconds instead of 50.

The (most) surprising part here is that the following change makes it fast again:

    (unless (eq (window-buffer win) buf)
       (set-window-buffer win buf))

IOW, in most cases, the window in question already displays buf; yet, the calls are extremely slow.

Is anyone familiar with such an issue? This is in GNU Emacs 24.4.1; I can't reproduce it myself, but I can ask for more information if needed.

Cheers,
Clément.


[-- Attachment #2: OpenPGP digital signature --]
[-- Type: application/pgp-signature, Size: 836 bytes --]

Re: What makes set-window-buffer slow?

[Andreas Schwab]

Perhaps it's because set-window-buffer marks the window for redisplay.

Andreas.

-- 
Andreas Schwab, SUSE Labs, schwab@suse.de
GPG Key fingerprint = 0196 BAD8 1CE9 1970 F4BE  1748 E4D4 88E3 0EEA B9D7
"And now for something completely different."

Re: What makes set-window-buffer slow?

[Clément Pit--Claudel]

[-- Attachment #1.1: Type: text/plain, Size: 398 bytes --]

Thanks for this suggestion! I probably have to investigate why redisplay is slow, then; that's bound to be rather tricky :/

Is there a reason for set-window-buffer to trigger redisplay if the window was already displaying that same buffer?

Clément.

On 2016-06-23 12:01, Andreas Schwab wrote:
> Perhaps it's because set-window-buffer marks the window for redisplay.
> 
> Andreas.
> 


[-- Attachment #2: OpenPGP digital signature --]
[-- Type: application/pgp-signature, Size: 836 bytes --]

Re: What makes set-window-buffer slow?

[Alan Mackenzie]

Hello, Clément.

On Thu, Jun 23, 2016 at 01:45:56PM -0400, Clément Pit--Claudel wrote:
> Thanks for this suggestion! I probably have to investigate why
> redisplay is slow, then; that's bound to be rather tricky :/

Redisplay is NOT slow.  It's written in C and is heavily optimised.

> Is there a reason for set-window-buffer to trigger redisplay if the window was already displaying that same buffer?

I can't answer your exact question, but should redisplay get triggered
in these circumstances, its optimisations would ensure that the reusable
part of the display would, in fact, get reused.

> Clément.

-- 
Alan Mackenzie (Nuremberg, Germany).

Re: What makes set-window-buffer slow?

[Clément Pit--Claudel]

[-- Attachment #1.1: Type: text/plain, Size: 804 bytes --]

On 2016-06-23 14:12, Alan Mackenzie wrote:
> Hello, Clément.
Hi Alan,

> On Thu, Jun 23, 2016 at 01:45:56PM -0400, Clément Pit--Claudel wrote:
>> Thanks for this suggestion! I probably have to investigate why
>> redisplay is slow, then; that's bound to be rather tricky :/
> 
> Redisplay is NOT slow.  It's written in C and is heavily optimised.

Thanks for the clarification! Do you know what else might make set-window-buffer slow?

>> Is there a reason for set-window-buffer to trigger redisplay if the window was already displaying that same buffer?
> 
> I can't answer your exact question, but should redisplay get triggered
> in these circumstances, its optimisations would ensure that the reusable
> part of the display would, in fact, get reused.

Nifty. Thanks!

Clément.


[-- Attachment #2: OpenPGP digital signature --]
[-- Type: application/pgp-signature, Size: 836 bytes --]

Re: What makes set-window-buffer slow?

[Eli Zaretskii]

> From: Clément Pit--Claudel <clement.pit@gmail.com>
> Date: Thu, 23 Jun 2016 14:30:02 -0400
> Cc: Andreas Schwab <schwab@suse.de>, Emacs developers <emacs-devel@gnu.org>
> 
> > On Thu, Jun 23, 2016 at 01:45:56PM -0400, Clément Pit--Claudel wrote:
> >> Thanks for this suggestion! I probably have to investigate why
> >> redisplay is slow, then; that's bound to be rather tricky :/
> > 
> > Redisplay is NOT slow.  It's written in C and is heavily optimised.
> 
> Thanks for the clarification! Do you know what else might make set-window-buffer slow?
> 
> >> Is there a reason for set-window-buffer to trigger redisplay if the window was already displaying that same buffer?
> > 
> > I can't answer your exact question, but should redisplay get triggered
> > in these circumstances, its optimisations would ensure that the reusable
> > part of the display would, in fact, get reused.
> 
> Nifty. Thanks!

Instead of hypothesizing, I suggest to profile your code with
profiler.el.  If indeed redisplay is taking the time, you should see
that in the profile.

Re: What makes set-window-buffer slow?

[Clément Pit--Claudel]

[-- Attachment #1.1: Type: text/plain, Size: 944 bytes --]

On 2016-06-23 15:11, Eli Zaretskii wrote:
> Instead of hypothesizing, I suggest to profile your code with
> profiler.el.  If indeed redisplay is taking the time, you should see
> that in the profile.

The profile doesn't show that, unfortunately; in fact, we spent a significant amount of time trying to understand what was taking all that time by looking at the profile, but nothing in there was taking more than 30% of the time, and even optimizing away a function that according to the profile took 28% of the time didn't yield a measurable runtime difference.

Commenting out the call to set-window-buffer (or predicating it on the window not already displaying the buffer), on the other hand, does yield a 95% performance gain.  set-window-buffer does not appear in the profile; redisplay_internal does appear, but it only is credited with 30% of the execution time.

I wonder what might explain these results...
Clément.




[-- Attachment #2: OpenPGP digital signature --]
[-- Type: application/pgp-signature, Size: 836 bytes --]

Re: What makes set-window-buffer slow?

[Eli Zaretskii]

> From: Clément Pit--Claudel <clement.pit@gmail.com>
> Cc: acm@muc.de, schwab@suse.de, emacs-devel@gnu.org
> Date: Thu, 23 Jun 2016 17:23:54 -0400
> 
> On 2016-06-23 15:11, Eli Zaretskii wrote:
> > Instead of hypothesizing, I suggest to profile your code with
> > profiler.el.  If indeed redisplay is taking the time, you should see
> > that in the profile.
> 
> The profile doesn't show that, unfortunately; in fact, we spent a significant amount of time trying to understand what was taking all that time by looking at the profile, but nothing in there was taking more than 30% of the time, and even optimizing away a function that according to the profile took 28% of the time didn't yield a measurable runtime difference.
> 
> Commenting out the call to set-window-buffer (or predicating it on the window not already displaying the buffer), on the other hand, does yield a 95% performance gain.  set-window-buffer does not appear in the profile; redisplay_internal does appear, but it only is credited with 30% of the execution time.
> 
> I wonder what might explain these results...

Any hope of seeing the profile, fully expanded?

Re: What makes set-window-buffer slow?

[Clément Pit--Claudel]

[-- Attachment #1.1.1: Type: text/plain, Size: 1283 bytes --]

On 2016-06-24 02:54, Eli Zaretskii wrote:
>> From: Clément Pit--Claudel <clement.pit@gmail.com> Cc: acm@muc.de,
>> schwab@suse.de, emacs-devel@gnu.org Date: Thu, 23 Jun 2016 17:23:54
>> -0400
>> 
>> On 2016-06-23 15:11, Eli Zaretskii wrote:
>>> Instead of hypothesizing, I suggest to profile your code with 
>>> profiler.el.  If indeed redisplay is taking the time, you should
>>> see that in the profile.
>> 
>> The profile doesn't show that, unfortunately; in fact, we spent a
>> significant amount of time trying to understand what was taking all
>> that time by looking at the profile, but nothing in there was
>> taking more than 30% of the time, and even optimizing away a
>> function that according to the profile took 28% of the time didn't
>> yield a measurable runtime difference.
>> 
>> Commenting out the call to set-window-buffer (or predicating it on
>> the window not already displaying the buffer), on the other hand,
>> does yield a 95% performance gain.  set-window-buffer does not
>> appear in the profile; redisplay_internal does appear, but it only
>> is credited with 30% of the execution time.
>> 
>> I wonder what might explain these results...
> 
> Any hope of seeing the profile, fully expanded?

Absolutely. I've attached it.


[-- Attachment #1.1.2: mergesort-profile2 --]
[-- Type: text/plain, Size: 13830 bytes --]


[profiler-profile "24.3" cpu #s(hash-table size 97 test equal rehash-size 1.5 rehash-threshold 0.8 data ([nil nil nil nil nil nil nil nil nil nil nil nil nil nil nil nil] 3308 ["#<compiled 0x261fc9>" funcall with-no-warnings setq let ad-Advice-font-lock-fontify-keywords-region apply font-lock-fontify-keywords-region font-lock-default-fontify-region font-lock-fontify-region run-hook-with-args "#<compiled 0xdcd5b5>" funcall jit-lock-fontify-now jit-lock-function recenter] 20 [end-of-buffer call-interactively command-execute nil nil nil nil nil nil nil nil nil nil nil nil nil] 9 [font-lock-fontify-region run-hook-with-args "#<compiled 0xdcd765>" funcall jit-lock-fontify-now jit-lock-function recenter end-of-buffer call-interactively command-execute nil nil nil nil nil nil] 3 [read-event "#<compiled 0x9782d9>" funcall track-mouse eval mouse-drag-track mouse-drag-region call-interactively command-execute nil nil nil nil nil nil nil] 8 [byte-code tooltip-show tooltip-help-tips run-hook-with-args-until-success tooltip-timeout apply byte-code timer-event-handler nil nil nil nil nil nil nil nil] 6 [coq-script-parse-cmdend-forward coq-script-parse-function proof-segment-up-to proof-segment-up-to-using-cache proof-assert-until-point proof-toolbar-goto call-interactively command-execute nil nil nil nil nil nil nil nil] 14 ["#<compiled 0x45ce3b>" funcall syntax-ppss proof-buffer-syntactic-context coq-script-parse-cmdend-forward coq-script-parse-function proof-segment-up-to proof-segment-up-to-using-cache proof-assert-until-point proof-toolbar-goto call-interactively command-execute nil nil nil nil] 43 [proof-segment-up-to proof-segment-up-to-using-cache proof-assert-until-point proof-toolbar-goto call-interactively command-execute nil nil nil nil nil nil nil nil nil nil] 4 [proof-buffer-syntactic-context proof-inside-comment coq-looking-at-comment coq-find-comment-start coq-find-not-in-comment-backward coq-empty-command-p coq-script-parse-cmdend-forward coq-script-parse-function proof-segment-up-to proof-segment-up-to-using-cache proof-assert-until-point proof-toolbar-goto call-interactively command-execute nil nil] 5 ["#<compiled 0xe3cf8f>" funcall syntax-ppss proof-buffer-syntactic-context proof-inside-comment coq-looking-at-comment coq-find-not-in-comment-backward coq-empty-command-p coq-empty-command-p coq-empty-command-p coq-script-parse-cmdend-forward coq-script-parse-function proof-segment-up-to proof-segment-up-to-using-cache proof-assert-until-point proof-toolbar-goto] 3 [coq-empty-command-p coq-script-parse-cmdend-forward coq-script-parse-function proof-segment-up-to proof-segment-up-to-using-cache proof-assert-until-point proof-toolbar-goto call-interactively command-execute nil nil nil nil nil nil nil] 4 [proof-segment-up-to-using-cache proof-assert-until-point proof-toolbar-goto call-interactively command-execute nil nil nil nil nil nil nil nil nil nil nil] 4 ["#<compiled 0x974991>" funcall syntax-ppss proof-buffer-syntactic-context proof-inside-comment coq-looking-at-comment coq-find-not-in-comment-backward coq-empty-command-p coq-script-parse-cmdend-forward coq-script-parse-function proof-segment-up-to proof-segment-up-to-using-cache proof-assert-until-point proof-toolbar-goto call-interactively command-execute] 11 ["#<compiled 0x9928ad>" funcall syntax-ppss proof-buffer-syntactic-context proof-inside-comment coq-looking-at-comment coq-find-comment-start coq-find-not-in-comment-backward coq-empty-command-p coq-script-parse-cmdend-forward coq-script-parse-function proof-segment-up-to proof-segment-up-to-using-cache proof-assert-until-point proof-toolbar-goto call-interactively] 8 [syntax-ppss proof-buffer-syntactic-context coq-script-parse-cmdend-forward coq-script-parse-function proof-segment-up-to proof-segment-up-to-using-cache proof-assert-until-point proof-toolbar-goto call-interactively command-execute nil nil nil nil nil nil] 4 [redisplay proof-shell-wait proof-shell-invisible-command coq-adapt-printing-width run-hooks proof-assert-until-point proof-toolbar-goto call-interactively command-execute nil nil nil nil nil nil nil] 2 [proof-script-delete-secondary-spans proof-assert-semis proof-assert-until-point proof-toolbar-goto call-interactively command-execute nil nil nil nil nil nil nil nil nil nil] 8 [apply coq-seq-get-library-dependencies coq-seq-map-module-id-to-obj-file coq-seq-check-module coq-seq-preprocess-require-commands run-hooks byte-code proof-extend-queue proof-assert-semis proof-assert-until-point proof-toolbar-goto call-interactively command-execute nil nil nil] 7 [coq-seq-preprocess-require-commands run-hooks byte-code proof-extend-queue proof-assert-semis proof-assert-until-point proof-toolbar-goto call-interactively command-execute nil nil nil nil nil nil nil] 3 [proof-done-advancing byte-code proof-shell-invoke-callback mapc proof-add-to-queue proof-extend-queue proof-assert-semis proof-assert-until-point proof-toolbar-goto call-interactively command-execute nil nil nil nil nil] 2 [proof-done-advancing-other proof-done-advancing byte-code proof-shell-invoke-callback mapc proof-shell-exec-loop proof-shell-filter-manage-output proof-shell-filter byte-code proof-shell-filter-wrapper run-hook-with-args scomint-output-filter nil nil nil nil] 4 [proof-set-overlay-arrow proof-done-advancing byte-code proof-shell-invoke-callback mapc proof-shell-exec-loop proof-shell-filter-manage-output proof-shell-filter byte-code proof-shell-filter-wrapper run-hook-with-args scomint-output-filter nil nil nil nil] 13 [proof-toolbar-next-enable-p redisplay_internal\ \(C\ function\) nil nil nil nil nil nil nil nil nil nil nil nil nil nil] 19 [run-hooks proof-done-advancing byte-code proof-shell-invoke-callback mapc proof-shell-exec-loop proof-shell-filter-manage-output proof-shell-filter byte-code proof-shell-filter-wrapper run-hook-with-args scomint-output-filter nil nil nil nil] 17 [proof-done-advancing byte-code proof-shell-invoke-callback mapc proof-shell-exec-loop proof-shell-filter-manage-output proof-shell-filter byte-code proof-shell-filter-wrapper run-hook-with-args scomint-output-filter nil nil nil nil nil] 25 [redisplay--update-region-highlight "#<compiled 0xe6722f>" funcall redisplay--update-region-highlights apply "#<compiled 0x406067>" redisplay_internal\ \(C\ function\) nil nil nil nil nil nil nil nil nil] 2 [proof-shell-filter-manage-output proof-shell-filter byte-code proof-shell-filter-wrapper run-hook-with-args scomint-output-filter nil nil nil nil nil nil nil nil nil nil] 7 [scomint-send-input proof-shell-insert proof-shell-exec-loop proof-shell-filter-manage-output proof-shell-filter byte-code proof-shell-filter-wrapper run-hook-with-args scomint-output-filter nil nil nil nil nil nil nil] 11 [proof-shell-handle-immediate-output proof-shell-filter-manage-output proof-shell-filter byte-code proof-shell-filter-wrapper run-hook-with-args scomint-output-filter nil nil nil nil nil nil nil nil nil] 7 [company-coq-state-change run-hooks proof-done-advancing byte-code proof-shell-invoke-callback mapc proof-shell-exec-loop proof-shell-filter-manage-output proof-shell-filter byte-code proof-shell-filter-wrapper run-hook-with-args scomint-output-filter nil nil nil] 4 [proof-unprocessed-begin proof-locked-region-full-p proof-toolbar-use-enable-p redisplay_internal\ \(C\ function\) nil nil nil nil nil nil nil nil nil nil nil nil] 1 [run-hook-with-args scomint-output-filter nil nil nil nil nil nil nil nil nil nil nil nil nil nil] 4 [menu-bar-update-buffers redisplay_internal\ \(C\ function\) nil nil nil nil nil nil nil nil nil nil nil nil nil nil] 14 [redisplay_internal\ \(C\ function\) nil nil nil nil nil nil nil nil nil nil nil nil nil nil nil] 8 [proof-shell-filter byte-code proof-shell-filter-wrapper run-hook-with-args scomint-output-filter nil nil nil nil nil nil nil nil nil nil nil] 19 [proof-done-advancing-save proof-done-advancing byte-code proof-shell-invoke-callback mapc proof-shell-exec-loop proof-shell-filter-manage-output proof-shell-filter byte-code proof-shell-filter-wrapper run-hook-with-args scomint-output-filter nil nil nil nil] 9 [file-remote-p redisplay_internal\ \(C\ function\) nil nil nil nil nil nil nil nil nil nil nil nil nil nil] 17 [display-graphic-p if eval redisplay_internal\ \(C\ function\) nil nil nil nil nil nil nil nil nil nil nil nil] 6 [proof-get-name-from-goal proof-done-advancing-save proof-done-advancing byte-code proof-shell-invoke-callback mapc proof-shell-exec-loop proof-shell-filter-manage-output proof-shell-filter byte-code proof-shell-filter-wrapper run-hook-with-args scomint-output-filter nil nil nil] 2 [tool-bar-make-keymap redisplay_internal\ \(C\ function\) nil nil nil nil nil nil nil nil nil nil nil nil nil nil] 14 [image-search-load-path find-image eval "#<compiled 0x279bef>" mapcar tool-bar-make-keymap-1 tool-bar-make-keymap redisplay_internal\ \(C\ function\) nil nil nil nil nil nil nil nil] 3 [coq-set-state-infos run-hooks proof-done-advancing byte-code proof-shell-invoke-callback mapc proof-shell-exec-loop proof-shell-filter-manage-output proof-shell-filter byte-code proof-shell-filter-wrapper run-hook-with-args scomint-output-filter nil nil nil] 2 [if company-coq-state-change run-hooks proof-done-advancing byte-code proof-shell-invoke-callback mapc proof-shell-exec-loop proof-shell-filter-manage-output proof-shell-filter byte-code proof-shell-filter-wrapper run-hook-with-args scomint-output-filter nil nil] 1 [eval redisplay_internal\ \(C\ function\) nil nil nil nil nil nil nil nil nil nil nil nil nil nil] 7 [proof-shell-exec-loop proof-shell-filter-manage-output proof-shell-filter byte-code proof-shell-filter-wrapper run-hook-with-args scomint-output-filter nil nil nil nil nil nil nil nil nil] 2 [coq-count-match coq-module-opening-p coq-goal-command-p proof-done-advancing-other proof-done-advancing byte-code proof-shell-invoke-callback mapc proof-shell-exec-loop proof-shell-filter-manage-output proof-shell-filter byte-code proof-shell-filter-wrapper run-hook-with-args scomint-output-filter nil] 4 [coq-search-urgent-message proof-shell-process-urgent-messages proof-shell-filter byte-code proof-shell-filter-wrapper run-hook-with-args scomint-output-filter nil nil nil nil nil nil nil nil nil] 4 [if eval redisplay_internal\ \(C\ function\) nil nil nil nil nil nil nil nil nil nil nil nil nil] 19 [keymap-canonicalize redisplay_internal\ \(C\ function\) nil nil nil nil nil nil nil nil nil nil nil nil nil nil] 5 [proof-shell-insert proof-shell-exec-loop proof-shell-filter-manage-output proof-shell-filter byte-code proof-shell-filter-wrapper run-hook-with-args scomint-output-filter nil nil nil nil nil nil nil nil] 2 [mapc proof-shell-exec-loop proof-shell-filter-manage-output proof-shell-filter byte-code proof-shell-filter-wrapper run-hook-with-args scomint-output-filter nil nil nil nil nil nil nil nil] 2 [proof-element-id proof-next-element-id proof-done-advancing-other proof-done-advancing byte-code proof-shell-invoke-callback mapc proof-shell-exec-loop proof-shell-filter-manage-output proof-shell-filter byte-code proof-shell-filter-wrapper run-hook-with-args scomint-output-filter nil nil] 1 [unless eval redisplay_internal\ \(C\ function\) nil nil nil nil nil nil nil nil nil nil nil nil nil] 4 [byte-code proof-shell-filter-wrapper run-hook-with-args scomint-output-filter nil nil nil nil nil nil nil nil nil nil nil nil] 9 [progn if let if let company-coq-state-change run-hooks proof-done-advancing byte-code proof-shell-invoke-callback mapc proof-shell-exec-loop proof-shell-filter-manage-output proof-shell-filter byte-code proof-shell-filter-wrapper] 5 [coq-last-prompt-info coq-last-prompt-info-safe coq-set-state-infos run-hooks proof-done-advancing byte-code proof-shell-invoke-callback mapc proof-shell-exec-loop proof-shell-filter-manage-output proof-shell-filter byte-code proof-shell-filter-wrapper run-hook-with-args scomint-output-filter nil] 4 [coq-count-match coq-module-opening-p coq-goal-command-p proof-done-advancing-save proof-done-advancing byte-code proof-shell-invoke-callback mapc proof-shell-exec-loop proof-shell-filter-manage-output proof-shell-filter byte-code proof-shell-filter-wrapper run-hook-with-args scomint-output-filter nil] 2 [and company-coq-boundp-string-match-p and let* if company-coq-maybe-proof-input-reload-things run-hooks proof-shell-insert proof-shell-exec-loop proof-shell-filter-manage-output proof-shell-filter byte-code proof-shell-filter-wrapper run-hook-with-args scomint-output-filter nil] 2 [run-hooks proof-shell-insert proof-shell-exec-loop proof-shell-filter-manage-output proof-shell-filter byte-code proof-shell-filter-wrapper run-hook-with-args scomint-output-filter nil nil nil nil nil nil nil] 5 [pg-processing-complete-hint proof-shell-exec-loop proof-shell-filter-manage-output proof-shell-filter byte-code proof-shell-filter-wrapper run-hook-with-args scomint-output-filter nil nil nil nil nil nil nil nil] 6 ["#<compiled 0x261fc9>" funcall with-no-warnings setq let ad-Advice-font-lock-fontify-keywords-region apply font-lock-fontify-keywords-region font-lock-default-fontify-region font-lock-fontify-region run-hook-with-args "#<compiled 0xe64a05>" funcall jit-lock-fontify-now jit-lock-function pos-visible-in-window-p] 4 [completing-read-default completing-read read-extended-command byte-code call-interactively command-execute nil nil nil nil nil nil nil nil nil nil] 38 [read-from-minibuffer completing-read-default completing-read read-extended-command byte-code call-interactively command-execute nil nil nil nil nil nil nil nil nil] 78 [profiler-cpu-profile profiler-report-cpu profiler-report call-interactively command-execute execute-extended-command call-interactively command-execute nil nil nil nil nil nil nil nil] 10 [Automatic\ GC] 53)) (22380 15820 895462 621000) nil]

[-- Attachment #2: OpenPGP digital signature --]
[-- Type: application/pgp-signature, Size: 836 bytes --]

Re: What makes set-window-buffer slow?

[Eli Zaretskii]

> Cc: acm@muc.de, schwab@suse.de, emacs-devel@gnu.org
> From: Clément Pit--Claudel <clement.pit@gmail.com>
> Date: Fri, 24 Jun 2016 08:33:25 -0400
> 
> >> On 2016-06-23 15:11, Eli Zaretskii wrote:
> >>> Instead of hypothesizing, I suggest to profile your code with 
> >>> profiler.el.  If indeed redisplay is taking the time, you should
> >>> see that in the profile.
> >> 
> >> The profile doesn't show that, unfortunately; in fact, we spent a
> >> significant amount of time trying to understand what was taking all
> >> that time by looking at the profile, but nothing in there was
> >> taking more than 30% of the time, and even optimizing away a
> >> function that according to the profile took 28% of the time didn't
> >> yield a measurable runtime difference.
> >> 
> >> Commenting out the call to set-window-buffer (or predicating it on
> >> the window not already displaying the buffer), on the other hand,
> >> does yield a 95% performance gain.  set-window-buffer does not
> >> appear in the profile; redisplay_internal does appear, but it only
> >> is credited with 30% of the execution time.
> >> 
> >> I wonder what might explain these results...
> > 
> > Any hope of seeing the profile, fully expanded?
> 
> Absolutely. I've attached it.

Looks like redisplay is indeed an important factor here.

In addition, it looks like you have some subprocess from which you
read input?  What's the part of profile below about?

  - scomint-output-filter                                           173  26%
   - run-hook-with-args                                             173  26%
    - proof-shell-filter-wrapper                                    169  26%
     - byte-code                                                    169  26%
      - proof-shell-filter                                          160  24%
       - proof-shell-filter-manage-output                           137  21%
	- proof-shell-exec-loop                                     123  19%
	 - mapc                                                      95  14%
	  - proof-shell-invoke-callback                              93  14%
	   - byte-code                                               93  14%
	    - proof-done-advancing                                   93  14%

Can you write some high-level overview of what the inner loop of your
code does, including what is being redisplayed, and how input from
subprocesses enters the picture?

In addition, I suggest to run your benchmark several times, so as to
eliminate the significant portion of time execute-extended-command and
its subroutines, and the profiler itself, show in the profile?  Also,
load all the Lisp libraries as *.el files, so that the profile is more
detailed.

Re: What makes set-window-buffer slow?

[Clément Pit--Claudel]

[-- Attachment #1.1: Type: text/plain, Size: 2380 bytes --]

On 2016-06-24 09:56, Eli Zaretskii wrote:
> Looks like redisplay is indeed an important factor here.
> 
> In addition, it looks like you have some subprocess from which you
> read input?  What's the part of profile below about?
> 
>   - scomint-output-filter                                           173  26%
>    - run-hook-with-args                                             173  26%
>     - proof-shell-filter-wrapper                                    169  26%
>      - byte-code                                                    169  26%
>       - proof-shell-filter                                          160  24%
>        - proof-shell-filter-manage-output                           137  21%
> 	- proof-shell-exec-loop                                     123  19%
> 	 - mapc                                                      95  14%
> 	  - proof-shell-invoke-callback                              93  14%
> 	   - byte-code                                               93  14%
> 	    - proof-done-advancing                                   93  14%
> 
> Can you write some high-level overview of what the inner loop of your
> code does, including what is being redisplayed, and how input from
> subprocesses enters the picture?

This is in the context of a package called proof general. It's an interface for proof assistants. Essentially you write a sequence of commands, and ask the proof assistant to process them one by one.

The proof-shell functions do this: they handle communication with the subprocess. The main loop looks like this:

* Fetch one command from the buffer
* Send it to the subprocess
* When a response arrives, call a hook
* Send the next command

My code adds a functioon into that hook that calls set-window-buffer; when I remove that call, everything is snappy. When I add it back in, everything gets much slower (at least that's what I understand; this isn't happening on my machine).

> In addition, I suggest to run your benchmark several times, so as to
> eliminate the significant portion of time execute-extended-command and
> its subroutines, and the profiler itself, show in the profile?  Also,
> load all the Lisp libraries as *.el files, so that the profile is more
> detailed.

OK, I'll ask the person who's seeing that bug to generate this report.

Thanks for your help!
Clément.


[-- Attachment #2: OpenPGP digital signature --]
[-- Type: application/pgp-signature, Size: 836 bytes --]

Re: What makes set-window-buffer slow?

[Clément Pit--Claudel]

[-- Attachment #1.1.1: Type: text/plain, Size: 148 bytes --]

On 2016-06-24 10:19, Clément Pit--Claudel wrote:
> OK, I'll ask the person who's seeing that bug to generate this report.

New report attached.

[-- Attachment #1.1.2: mergesort-profile4 --]
[-- Type: text/plain, Size: 56672 bytes --]


[profiler-profile "24.3" cpu #s(hash-table size 487 test equal rehash-size 1.5 rehash-threshold 0.8 data ([let* proof-shell-kill-function kill-buffer let progn if if proof-shell-exit progn condition-case progn if if save-current-buffer pg-profile-1 apply] 22 [redisplay let* proof-shell-kill-function kill-buffer let progn if if proof-shell-exit progn condition-case progn if if save-current-buffer pg-profile-1] 46 [menu-bar-update-buffers redisplay_internal\ \(C\ function\) redisplay progn if let* proof-shell-wait catch progn if let* proof-shell-kill-function kill-buffer let progn if] 2 [message display-message-or-buffer "#<compiled 0x44d6bf>" funcall shell-command-on-region shell-command if let* progn unwind-protect save-current-buffer let coq-autodetect-version coq-prog-args funcall cons] 54 [redisplay progn if let* proof-shell-wait if progn if proof-shell-invisible-command let* progn unwind-protect let unwind-protect progn if] 601 [progn if let* proof-shell-wait if progn if proof-shell-invisible-command let* progn unwind-protect let unwind-protect progn if progn] 27 [while progn if let* proof-shell-wait if progn if proof-shell-invisible-command let* progn unwind-protect let unwind-protect progn if] 78 [replace-regexp-in-string company-coq-trim progn unwind-protect let unwind-protect progn if progn if company-coq-ask-prover company-coq-unless-error company-coq-ask-prover-swallow-errors let company-coq-get-all-notations company-coq--list-to-table] 2 [list let cond let* cond cond let* if company-coq-tg--parse-tactic-part mapcar company-coq-tg--parse-tactic-subs cons company-coq-tg--parse-tactic mapcar let if] 4 [let* company-coq-tg--find-tactics mapcar apply let cond let* if let* company-coq-tg--find-tactics mapcar apply let if let* cond] 4 [progn if company-coq-tg--format-tactic let* reverse nconc setq while let* condition-case let* company-coq-tg--extract-notations and let company-coq-get-all-notations company-coq--list-to-table] 8 [redisplay progn if let* proof-shell-wait if progn if proof-shell-invisible-command proof-shell-invisible-command-invisible-result mapc if progn if progn unwind-protect] 111 [eval redisplay_internal\ \(C\ function\) redisplay progn if let* proof-shell-wait if progn if proof-shell-invisible-command "#<lambda 0x1ff2a7ca4a7ea4d5>" mapcar if progn unwind-protect] 3 [redisplay progn if let* proof-shell-wait if progn if proof-shell-invisible-command "#<lambda 0x1ff2a7ca4a7ea4d5>" mapcar if progn unwind-protect progn if] 355 [progn if let* proof-shell-wait if progn if proof-shell-invisible-command "#<lambda 0x1ff2a7ca4a7ea4d5>" mapcar if progn unwind-protect progn if let] 26 [message if pg-hint if pg-response-buffers-hint pg-hint proof-layout-windows proof-multiple-frames-enable progn unwind-protect let progn unwind-protect save-current-buffer let if] 5 ["#<compiled 0xbdb0dd>" funcall syntax-ppss let save-excursion proof-buffer-syntactic-context eq save-excursion proof-inside-comment or coq-looking-at-comment if coq-find-comment-start coq-find-not-in-comment-backward let coq-empty-command-p] 16 [and setq and while let if coq-script-parse-cmdend-forward coq-script-parse-function funcall let* while let* save-excursion proof-segment-up-to let if] 22 ["#<compiled 0xd6d3c3>" funcall syntax-ppss let save-excursion proof-buffer-syntactic-context eq save-excursion proof-inside-comment or coq-looking-at-comment if progn if while let] 7 ["#<compiled 0xf7ff65>" funcall syntax-ppss let save-excursion proof-buffer-syntactic-context and or and while let if coq-script-parse-cmdend-forward coq-script-parse-function funcall let*] 9 ["#<compiled 0x1032f7b>" funcall syntax-ppss let save-excursion proof-buffer-syntactic-context not and if let if coq-script-parse-cmdend-forward coq-script-parse-function funcall let* while] 10 [save-excursion proof-inside-comment or coq-looking-at-comment if coq-find-comment-start coq-find-not-in-comment-backward let coq-empty-command-p not save-excursion and or and while let] 4 [redisplay progn if let* proof-shell-wait if progn if proof-shell-invisible-command progn if let coq-adapt-printing-width run-hooks let proof-assert-until-point] 574 [let and proof-re-search-forward-safe cond proof-shell-handle-immediate-output let proof-shell-filter-manage-output progn if let if if let save-excursion proof-shell-filter progn] 45 [while progn if let* proof-shell-wait if progn if proof-shell-invisible-command progn if let coq-adapt-printing-width run-hooks let proof-assert-until-point] 35 [progn if let* proof-shell-wait if progn if proof-shell-invisible-command progn if let coq-adapt-printing-width run-hooks let proof-assert-until-point if] 28 [while let progn unwind-protect let let proof-semis-to-vanillas let proof-assert-semis let proof-assert-until-point if save-excursion proof-goto-point progn if] 12 [message map-y-or-n-p save-some-buffers let coq-compile-save-some-buffers let progn if let while let let if coq-seq-preprocess-require-commands run-hooks condition-case] 688 [save-some-buffers let coq-compile-save-some-buffers let progn if let while let let if coq-seq-preprocess-require-commands run-hooks condition-case proof-extend-queue let] 16 [save-current-buffer prog1 unwind-protect let progn unwind-protect let coq-seq-map-module-id-to-obj-file let coq-seq-check-module while let progn if let while] 18 ["#<compiled 0x1013545>" funcall make-temp-file let coq-seq-map-module-id-to-obj-file let coq-seq-check-module while let progn if let while let let if] 19 [nil nil nil nil nil nil nil nil nil nil nil nil nil nil nil nil] 64563 [redisplay_internal\ \(C\ function\) nil nil nil nil nil nil nil nil nil nil nil nil nil nil nil] 133 [redisplay--update-region-highlights apply "#<compiled 0x406067>" redisplay_internal\ \(C\ function\) nil nil nil nil nil nil nil nil nil nil nil nil] 44 [save-current-buffer proof-shell-insert proof-shell-insert-action-item if let* save-excursion if proof-shell-exec-loop if if let proof-shell-filter-manage-output progn if let if] 18 [if let coq-last-prompt-info coq-last-prompt-info-safe or let if coq-set-state-infos run-hooks proof-done-advancing funcall condition-case proof-shell-invoke-callback mapc let* save-excursion] 53 [proof-done-advancing-comment cond let proof-done-advancing funcall condition-case proof-shell-invoke-callback mapc let* save-excursion if proof-shell-exec-loop if if let proof-shell-filter-manage-output] 3 ["#<compiled 0x3ee67d>" redisplay--update-region-highlight "#<compiled 0xbd6387>" funcall redisplay--update-region-highlights apply "#<compiled 0x406067>" redisplay_internal\ \(C\ function\) nil nil nil nil nil nil nil nil] 15 [and company-coq-boundp-string-match-p and let* if company-coq-maybe-proof-input-reload-things run-hooks let save-current-buffer proof-shell-insert proof-shell-insert-action-item if let* save-excursion if proof-shell-exec-loop] 47 [menu-bar-update-buffers redisplay_internal\ \(C\ function\) nil nil nil nil nil nil nil nil nil nil nil nil nil nil] 95 [if eval redisplay_internal\ \(C\ function\) nil nil nil nil nil nil nil nil nil nil nil nil nil] 242 [condition-case proof-shell-invoke-callback mapc let* save-excursion if proof-shell-exec-loop if if let proof-shell-filter-manage-output progn if let if if] 6 ["#<compiled 0x10bdbfb>" funcall redisplay--update-region-highlights apply "#<compiled 0x406067>" redisplay_internal\ \(C\ function\) nil nil nil nil nil nil nil nil nil nil] 24 [span-set-end if proof-make-goalsave if let proof-done-advancing-save cond let proof-done-advancing funcall condition-case proof-shell-invoke-callback mapc let* save-excursion if] 6 [apply "#<compiled 0x406067>" redisplay_internal\ \(C\ function\) nil nil nil nil nil nil nil nil nil nil nil nil nil] 149 [eval redisplay_internal\ \(C\ function\) nil nil nil nil nil nil nil nil nil nil nil nil nil nil] 235 [proof-set-locked-endpoints if proof-set-locked-end let proof-done-advancing funcall condition-case proof-shell-invoke-callback mapc let* save-excursion if proof-shell-exec-loop if if let] 439 [let proof-string-match and cond progn if while let proof-done-advancing-save cond let proof-done-advancing funcall condition-case proof-shell-invoke-callback mapc] 90 [if let* let scomint-send-input let save-current-buffer proof-shell-insert proof-shell-insert-action-item if let* save-excursion if proof-shell-exec-loop if if let] 83 [progn if let if let company-coq-state-change run-hooks proof-done-advancing funcall condition-case proof-shell-invoke-callback mapc let* save-excursion if proof-shell-exec-loop] 60 [file-remote-p redisplay_internal\ \(C\ function\) nil nil nil nil nil nil nil nil nil nil nil nil nil nil] 476 [keymap-canonicalize redisplay_internal\ \(C\ function\) nil nil nil nil nil nil nil nil nil nil nil nil nil nil] 45 [proof-shell-handle-immediate-output let proof-shell-filter-manage-output progn if let if if let save-excursion proof-shell-filter progn condition-case while let if] 7 [proof-shell-live-buffer and proof-toolbar-command-enable-p redisplay_internal\ \(C\ function\) nil nil nil nil nil nil nil nil nil nil nil nil] 4 [and setq while let coq-search-urgent-message setq and while let proof-shell-process-urgent-messages and save-excursion proof-shell-filter progn condition-case while] 47 [save-excursion set-marker and proof-set-overlay-arrow proof-set-locked-endpoints if proof-set-locked-end let proof-done-advancing funcall condition-case proof-shell-invoke-callback mapc let* save-excursion if] 361 [if save-excursion set-marker and proof-set-overlay-arrow proof-set-locked-endpoints if proof-set-locked-end let proof-done-advancing funcall condition-case proof-shell-invoke-callback mapc let* save-excursion] 51 [proof-shell-insert proof-shell-insert-action-item if let* save-excursion if proof-shell-exec-loop if if let proof-shell-filter-manage-output progn if let if if] 42 [let progn if let span-at-before prev-span setq while let proof-done-advancing-save cond let proof-done-advancing funcall condition-case proof-shell-invoke-callback] 12 [if save-excursion if proof-shell-exec-loop if if let proof-shell-filter-manage-output progn if let if if let save-excursion proof-shell-filter] 27 [run-hooks let save-current-buffer proof-shell-insert proof-shell-insert-action-item if let* save-excursion if proof-shell-exec-loop if if let proof-shell-filter-manage-output progn if] 2 [proof-shell-filter-wrapper run-hook-with-args let save-current-buffer progn if let scomint-output-filter nil nil nil nil nil nil nil nil] 3 [facep or if let* pg-set-span-helphighlights let proof-done-advancing-other cond let proof-done-advancing funcall condition-case proof-shell-invoke-callback mapc let* save-excursion] 5 [if let if if let save-excursion proof-shell-filter progn condition-case while let if proof-shell-filter-wrapper run-hook-with-args let save-current-buffer] 28 [span-delete if while let proof-done-advancing-save cond let proof-done-advancing funcall condition-case proof-shell-invoke-callback mapc let* save-excursion if proof-shell-exec-loop] 101 [map-keymap keymap-canonicalize redisplay_internal\ \(C\ function\) nil nil nil nil nil nil nil nil nil nil nil nil nil] 14 [funcall condition-case proof-shell-invoke-callback mapc let* save-excursion if proof-shell-exec-loop if if let proof-shell-filter-manage-output progn if let if] 12 [and proof-shell-live-buffer and proof-shell-available-p and progn cond proof-toolbar-undo-enable-p redisplay_internal\ \(C\ function\) nil nil nil nil nil nil nil] 6 [if let if coq-set-state-infos run-hooks proof-done-advancing funcall condition-case proof-shell-invoke-callback mapc let* save-excursion if proof-shell-exec-loop if if] 40 [let if build-list-id-from-string let progn if let coq-last-prompt-info coq-last-prompt-info-safe or let if coq-set-state-infos run-hooks proof-done-advancing funcall] 12 [image-search-load-path find-image eval "#<compiled 0x279bef>" mapcar tool-bar-make-keymap-1 tool-bar-make-keymap redisplay_internal\ \(C\ function\) nil nil nil nil nil nil nil nil] 19 [and proof-toolbar-context-enable-p redisplay_internal\ \(C\ function\) nil nil nil nil nil nil nil nil nil nil nil nil nil] 13 [set-marker and proof-set-overlay-arrow proof-set-locked-endpoints if proof-set-locked-end let proof-done-advancing funcall condition-case proof-shell-invoke-callback mapc let* save-excursion if proof-shell-exec-loop] 13 [let* pg-set-span-helphighlights let proof-done-advancing-other cond let proof-done-advancing funcall condition-case proof-shell-invoke-callback mapc let* save-excursion if proof-shell-exec-loop if] 16 [setq let* save-excursion if proof-shell-exec-loop if if let proof-shell-filter-manage-output progn if let if if let save-excursion] 11 [save-excursion proof-locked-region-full-p not progn cond proof-toolbar-next-enable-p redisplay_internal\ \(C\ function\) nil nil nil nil nil nil nil nil nil] 4 [let proof-string-match and while let coq-count-match let* coq-module-opening-p or let or coq-goal-command-p funcall cond let proof-done-advancing-other] 9 [string-equal not or if pg-add-to-input-history if let proof-done-advancing funcall condition-case proof-shell-invoke-callback mapc let* save-excursion if proof-shell-exec-loop] 17 [proof-done-advancing funcall condition-case proof-shell-invoke-callback mapc let* save-excursion if proof-shell-exec-loop if if let proof-shell-filter-manage-output progn if let] 21 [redisplay--update-region-highlight "#<compiled 0x117a507>" funcall redisplay--update-region-highlights apply "#<compiled 0x406067>" redisplay_internal\ \(C\ function\) nil nil nil nil nil nil nil nil nil] 28 [let* save-excursion if proof-shell-exec-loop if if let proof-shell-filter-manage-output progn if let if if let save-excursion proof-shell-filter] 11 [let proof-done-advancing funcall condition-case proof-shell-invoke-callback mapc let* save-excursion if proof-shell-exec-loop if if let proof-shell-filter-manage-output progn if] 33 [eq if let span-at-before prev-span setq while let proof-done-advancing-save cond let proof-done-advancing funcall condition-case proof-shell-invoke-callback mapc] 5 [not and if let* save-excursion if proof-shell-exec-loop if if let proof-shell-filter-manage-output progn if let if if] 2 [+ let* coq-module-opening-p or let or coq-goal-command-p funcall cond progn if while let proof-done-advancing-save cond let] 3 [and if let if pg-processing-complete-hint if if let* save-excursion if proof-shell-exec-loop if if let proof-shell-filter-manage-output progn] 254 [cond proof-retract-buffer funcall progn unwind-protect let if save-current-buffer let proof-protected-process-or-retract if let* save-current-buffer if proof-deactivate-scripting progn] 8 [if progn if progn if let progn unwind-protect save-current-buffer let save-excursion if proof-display-and-keep-buffer pg-response-display if proof-shell-display-output-as-response] 4 [redisplay progn if let* proof-shell-wait progn unwind-protect let if save-current-buffer let proof-protected-process-or-retract if let* save-current-buffer if] 1928 [progn if let* proof-shell-wait progn unwind-protect let if save-current-buffer let proof-protected-process-or-retract if let* save-current-buffer if proof-deactivate-scripting] 131 [redisplay progn if let* proof-shell-wait catch progn if let* proof-shell-kill-function kill-buffer let progn if if proof-shell-exit] 57 [span-delete-spans proof-script-delete-spans save-current-buffer if save-excursion "#<lambda 0x291590e159b71182>" mapcar proof-restart-buffers proof-script-remove-all-spans-and-deactivate let* proof-shell-kill-function kill-buffer let progn if if] 2 [span-delete mapc span-mapc-spans span-delete-spans proof-script-delete-secondary-spans save-current-buffer if save-excursion "#<lambda 0x291590e159b71182>" mapcar proof-restart-buffers proof-script-remove-all-spans-and-deactivate let* proof-shell-kill-function kill-buffer let] 22 [while let save-current-buffer proof-shell-config-done coq-shell-mode-config let progn delay-mode-hooks coq-shell-mode funcall save-current-buffer let if proof-shell-start proof-shell-ready-prover condition-case] 20 [unwind-protect let unwind-protect progn if progn if company-coq-ask-prover let* progn if company-coq-ask-prover-redirect car let* progn if] 7 [while while let* progn unwind-protect save-current-buffer let company-coq-tg--preprocess-tactics-grammar let* company-coq-tg--extract-notations and let company-coq-get-all-notations company-coq--list-to-table setq company-coq-tactic-initialize-notations-filter] 30 [if company-coq-tg--parse-tactic-part mapcar company-coq-tg--parse-tactic-subs cons company-coq-tg--parse-tactic mapcar let if let* if company-coq-tg--parse-group cons let cond let*] 92 [setq if while let* company-coq--split-seq mapcar company-coq-tg--parse-tactic-subs cons company-coq-tg--parse-tactic mapcar let if let* if company-coq-tg--parse-group cons] 4 [let "#<lambda 0x20d7ceb9ed959acf>" funcall cond let* cond let* company-coq-tg--format-tactic-rec progn if company-coq-tg--format-tactic let* reverse nconc setq while] 4 [setq while let progn unwind-protect let let proof-semis-to-vanillas let proof-assert-semis let proof-assert-until-point if save-excursion proof-goto-point progn] 11 [apply setq progn unwind-protect save-current-buffer let let coq-seq-get-library-dependencies setq progn unwind-protect let coq-seq-map-module-id-to-obj-file let coq-seq-check-module while] 8 [and unwind-protect save-current-buffer let let coq-seq-get-library-dependencies setq progn unwind-protect let coq-seq-map-module-id-to-obj-file let coq-seq-check-module while let progn] 83 [if let* let scomint-send-input let save-current-buffer proof-shell-insert proof-shell-insert-action-item progn if progn if let proof-add-to-queue proof-extend-queue let] 3 [tool-bar-make-keymap redisplay_internal\ \(C\ function\) nil nil nil nil nil nil nil nil nil nil nil nil nil nil] 72 [coq-last-prompt-info coq-last-prompt-info-safe or let if coq-set-state-infos run-hooks proof-done-advancing funcall condition-case proof-shell-invoke-callback mapc let* save-excursion if proof-shell-exec-loop] 15 [display-graphic-p if eval redisplay_internal\ \(C\ function\) nil nil nil nil nil nil nil nil nil nil nil nil] 25 [let* pg-add-element cond let proof-done-advancing-other cond let proof-done-advancing funcall condition-case proof-shell-invoke-callback mapc let* save-excursion if proof-shell-exec-loop] 18 [if proof-shell-exec-loop if if let proof-shell-filter-manage-output progn if let if if let save-excursion proof-shell-filter progn condition-case] 30 ["#<compiled 0x279bef>" mapcar tool-bar-make-keymap-1 tool-bar-make-keymap redisplay_internal\ \(C\ function\) nil nil nil nil nil nil nil nil nil nil nil] 4 [list list let* pg-add-element cond let proof-done-advancing-other cond let proof-done-advancing funcall condition-case proof-shell-invoke-callback mapc let* save-excursion] 1 [save-excursion if proof-shell-exec-loop if if let proof-shell-filter-manage-output progn if let if if let save-excursion proof-shell-filter progn] 14 [setq if let save-current-buffer proof-shell-insert proof-shell-insert-action-item if let* save-excursion if proof-shell-exec-loop if if let proof-shell-filter-manage-output progn] 13 [ring-index ring-ref string-equal not or if pg-add-to-input-history if let proof-done-advancing funcall condition-case proof-shell-invoke-callback mapc let* save-excursion] 3 [let progn if let coq-last-prompt-info coq-last-prompt-info-safe or let if coq-set-state-infos run-hooks proof-done-advancing funcall condition-case proof-shell-invoke-callback mapc] 22 [let save-current-buffer progn if let scomint-output-filter nil nil nil nil nil nil nil nil nil nil] 40 [let if let spans-at-point-prop car-safe span-at save-current-buffer proof-last-locked-span if let if coq-set-state-infos run-hooks proof-done-advancing funcall condition-case] 23 [if let if build-list-id-from-string let progn if let coq-last-prompt-info coq-last-prompt-info-safe or let if coq-set-state-infos run-hooks proof-done-advancing] 5 [or if pg-add-to-input-history if let proof-done-advancing funcall condition-case proof-shell-invoke-callback mapc let* save-excursion if proof-shell-exec-loop if if] 4 [save-excursion let* pg-set-span-helphighlights let proof-done-advancing-other cond let proof-done-advancing funcall condition-case proof-shell-invoke-callback mapc let* save-excursion if proof-shell-exec-loop] 53 [and cond progn if while let proof-done-advancing-save cond let proof-done-advancing funcall condition-case proof-shell-invoke-callback mapc let* save-excursion] 5 [let proof-shell-process-urgent-messages and save-excursion proof-shell-filter progn condition-case while let if proof-shell-filter-wrapper run-hook-with-args let save-current-buffer progn if] 10 [let scomint-check-proc and proof-shell-live-buffer and proof-toolbar-state-enable-p redisplay_internal\ \(C\ function\) nil nil nil nil nil nil nil nil nil] 7 [save-current-buffer progn if let scomint-output-filter nil nil nil nil nil nil nil nil nil nil nil] 14 [and proof-shell-live-buffer and proof-toolbar-state-enable-p redisplay_internal\ \(C\ function\) nil nil nil nil nil nil nil nil nil nil nil] 13 [set-marker if let save-current-buffer proof-shell-insert proof-shell-insert-action-item if let* save-excursion if proof-shell-exec-loop if if let proof-shell-filter-manage-output progn] 8 [coq-get-span-proofnum or if let if coq-set-state-infos run-hooks proof-done-advancing funcall condition-case proof-shell-invoke-callback mapc let* save-excursion if proof-shell-exec-loop] 3 [mode-line-eol-desc eval redisplay_internal\ \(C\ function\) nil nil nil nil nil nil nil nil nil nil nil nil nil] 8 [cond proof-toolbar-next-enable-p redisplay_internal\ \(C\ function\) nil nil nil nil nil nil nil nil nil nil nil nil nil] 167 [every or and let* save-excursion if proof-shell-exec-loop if if let proof-shell-filter-manage-output progn if let if if] 6 [or proof-unprocessed-begin - span-at save-current-buffer proof-last-locked-span if let if coq-set-state-infos run-hooks proof-done-advancing funcall condition-case proof-shell-invoke-callback mapc] 15 [coq-section-command-p or let or coq-goal-command-p funcall cond progn if while let proof-done-advancing-save cond let proof-done-advancing funcall] 9 [concat proof-element-id proof-next-element-id let proof-done-advancing-other cond let proof-done-advancing funcall condition-case proof-shell-invoke-callback mapc let* save-excursion if proof-shell-exec-loop] 17 [let if coq-show-first-goal run-hooks let proof-shell-handle-delayed-output setq if if let proof-shell-filter-manage-output progn if let if if] 3 [progn unwind-protect let if save-current-buffer let proof-protected-process-or-retract if let* save-current-buffer if proof-deactivate-scripting progn condition-case proof-deactivate-scripting-auto catch] 3 [progn condition-case setq progn while let* progn unwind-protect save-current-buffer let company-coq-tg--preprocess-tactics-grammar let* company-coq-tg--extract-notations and let company-coq-get-all-notations] 110 [let* company-coq--split-seq mapcar company-coq-tg--parse-tactic-subs cons company-coq-tg--parse-tactic mapcar let if let* if company-coq-tg--parse-group cons let cond let*] 4 [let "#<lambda 0x2e6c5da14cf86a6c>" funcall cond let* cond let* company-coq-tg--format-tactic-rec let* let "#<lambda 0x29f8fbec6106a6f>" funcall cond let* cond let*] 8 [while progn if let* proof-shell-wait if progn if proof-shell-invisible-command "#<lambda 0x1ff2a7ca4a7ea4d5>" mapcar if progn unwind-protect progn if] 2 [window--pixel-to-total byte-code split-window split-window-horizontally cond progn unwind-protect save-current-buffer let let proof-select-three-b save-excursion progn if proof-display-three-b cond] 3 [menu-bar-update-buffers redisplay_internal\ \(C\ function\) message map-y-or-n-p save-some-buffers let coq-compile-save-some-buffers let progn if let while let let if coq-seq-preprocess-require-commands] 5 [proof-string-match and while let coq-count-match let* coq-module-opening-p or let or coq-goal-command-p funcall cond let proof-done-advancing-other cond] 6 [if if let save-excursion proof-shell-filter progn condition-case while let if proof-shell-filter-wrapper run-hook-with-args let save-current-buffer progn if] 1 [proof-locked-region-full-p not progn cond proof-toolbar-next-enable-p redisplay_internal\ \(C\ function\) nil nil nil nil nil nil nil nil nil nil] 56 [null or and if let* save-excursion if proof-shell-exec-loop if if let proof-shell-filter-manage-output progn if let if] 6 [let proof-string-match and let proof-get-name-from-goal or setq if let proof-done-advancing-save cond let proof-done-advancing funcall condition-case proof-shell-invoke-callback] 18 [if let span-at-before prev-span setq while let proof-done-advancing-save cond let proof-done-advancing funcall condition-case proof-shell-invoke-callback mapc let*] 15 [proof-re-search-forward-safe cond proof-shell-handle-immediate-output let proof-shell-filter-manage-output progn if let if if let save-excursion proof-shell-filter progn condition-case while] 6 [let coq-last-prompt-info coq-last-prompt-info-safe or let if coq-set-state-infos run-hooks proof-done-advancing funcall condition-case proof-shell-invoke-callback mapc let* save-excursion if] 8 [framep-on-display display-graphic-p if eval redisplay_internal\ \(C\ function\) nil nil nil nil nil nil nil nil nil nil nil] 8 [progn if let coq-last-prompt-info coq-last-prompt-info-safe or let if coq-set-state-infos run-hooks proof-done-advancing funcall condition-case proof-shell-invoke-callback mapc let*] 19 [unless eval redisplay_internal\ \(C\ function\) nil nil nil nil nil nil nil nil nil nil nil nil nil] 236 [eq proof-locked-region-empty-p not progn cond proof-toolbar-retract-enable-p redisplay_internal\ \(C\ function\) nil nil nil nil nil nil nil nil nil] 7 [if proof-set-locked-end let proof-done-advancing funcall condition-case proof-shell-invoke-callback mapc let* save-excursion if proof-shell-exec-loop if if let proof-shell-filter-manage-output] 32 [company-coq-state-change run-hooks proof-done-advancing funcall condition-case proof-shell-invoke-callback mapc let* save-excursion if proof-shell-exec-loop if if let proof-shell-filter-manage-output progn] 2 [let coq-count-match let* coq-module-opening-p or let or coq-goal-command-p funcall cond let proof-done-advancing-other cond let proof-done-advancing funcall] 7 [let* coq-module-opening-p or let or coq-goal-command-p funcall cond progn if while let proof-done-advancing-save cond let proof-done-advancing] 5 [progn pg-add-element cond let proof-done-advancing-other cond let proof-done-advancing funcall condition-case proof-shell-invoke-callback mapc let* save-excursion if proof-shell-exec-loop] 2 [let proof-done-advancing-other cond let proof-done-advancing funcall condition-case proof-shell-invoke-callback mapc let* save-excursion if proof-shell-exec-loop if if let] 8 [let proof-string-match if proof-string-match-safe and cond let proof-done-advancing funcall condition-case proof-shell-invoke-callback mapc let* save-excursion if proof-shell-exec-loop] 17 [proof-string-match and while let coq-count-match let* coq-module-opening-p or let or coq-goal-command-p funcall cond progn if while] 17 [eq cond let proof-done-advancing funcall condition-case proof-shell-invoke-callback mapc let* save-excursion if proof-shell-exec-loop if if let proof-shell-filter-manage-output] 5 [proof-element-id proof-next-element-id let proof-done-advancing-other cond let proof-done-advancing funcall condition-case proof-shell-invoke-callback mapc let* save-excursion if proof-shell-exec-loop if] 10 [- max if set-marker let proof-shell-process-urgent-messages and save-excursion proof-shell-filter progn condition-case while let if proof-shell-filter-wrapper run-hook-with-args] 5 [cond proof-shell-handle-immediate-output let proof-shell-filter-manage-output progn if let if if let save-excursion proof-shell-filter progn condition-case while let] 3 [let proof-string-match and while let coq-count-match + let* coq-module-opening-p or let or coq-goal-command-p funcall cond progn] 4 [pg-remove-element "#<lambda 0x5a29898b7185a3a>" funcall "#<lambda 0xa4306fd6cb>" mapc span-delete if while let proof-done-advancing-save cond let proof-done-advancing funcall condition-case proof-shell-invoke-callback] 6 [internal--after-with-selected-window unwind-protect save-current-buffer let let progn if progn unwind-protect let let progn if if coq-optimise-resp-windows progn] 7 [if while let if let spans-at-region-prop mapc span-mapc-spans span-delete-spans proof-script-delete-spans let if proof-done-retracting funcall condition-case proof-shell-invoke-callback] 4 [apply let* tramp-completion-run-real-handler if let tramp-completion-file-name-handler file-symlink-p file-truename apply let* tramp-completion-run-real-handler if let tramp-completion-file-name-handler file-truename file-truename] 2 [byte-code delete-window delete-windows-on progn if while let let let* proof-shell-kill-function kill-buffer let progn if if proof-shell-exit] 13 [if coq-set-state-infos run-hooks proof-grab-lock progn if progn if let proof-add-to-queue proof-start-queue let* progn if proof-shell-invisible-command let*] 3 [cond let* cond cond let* if company-coq-tg--parse-tactic-part mapcar company-coq-tg--parse-tactic-subs cons company-coq-tg--parse-tactic mapcar let if let* if] 4 [company-coq--split-seq mapcar company-coq-tg--parse-tactic-subs cons company-coq-tg--parse-tactic mapcar let if let* if company-coq-tg--parse-group cons let cond let* if] 153 [cond let* if company-coq-tg--parse-tactic-part mapcar company-coq-tg--parse-tactic-subs cons company-coq-tg--parse-tactic mapcar let if let* if company-coq-tg--parse-group cons let] 2 [cons setq while let* reverse nconc setq while let* let "#<lambda 0x1b3266d91da89abb>" funcall cond let* cond let*] 5 [company-coq-tg--format-tactic-rec let "#<lambda 0x320f583b014d5ebf>" funcall cond let* cond let* company-coq-tg--format-tactic-rec progn if company-coq-tg--format-tactic let* reverse nconc setq] 4 [let coq-last-prompt-info coq-last-prompt-info-safe or let if coq-set-state-infos run-hooks proof-done-invisible funcall condition-case proof-shell-invoke-callback mapc let* save-excursion if] 7 [let* progn if while let progn unwind-protect let let proof-semis-to-vanillas let proof-assert-semis let proof-assert-until-point if save-excursion] 9 [while let let if coq-seq-preprocess-require-commands run-hooks condition-case proof-extend-queue let proof-assert-semis let proof-assert-until-point if save-excursion proof-goto-point progn] 150 [file-name-sans-extension x-gtk-map-stock redisplay_internal\ \(C\ function\) nil nil nil nil nil nil nil nil nil nil nil nil nil] 5 [eq if save-excursion set-marker and proof-set-overlay-arrow proof-set-locked-endpoints if proof-set-locked-end let proof-done-advancing funcall condition-case proof-shell-invoke-callback mapc let*] 1 [progn if let scomint-output-filter nil nil nil nil nil nil nil nil nil nil nil nil] 18 [or if let if coq-set-state-infos run-hooks proof-done-advancing funcall condition-case proof-shell-invoke-callback mapc let* save-excursion if proof-shell-exec-loop if] 5 [or coq-goal-command-p funcall cond let proof-done-advancing-other cond let proof-done-advancing funcall condition-case proof-shell-invoke-callback mapc let* save-excursion if] 3 [let* if company-coq-maybe-proof-input-reload-things run-hooks let save-current-buffer proof-shell-insert proof-shell-insert-action-item if let* save-excursion if proof-shell-exec-loop if if let] 9 [let* let scomint-send-input let save-current-buffer proof-shell-insert proof-shell-insert-action-item if let* save-excursion if proof-shell-exec-loop if if let proof-shell-filter-manage-output] 6 [proof-debug if proof-done-advancing-save cond let proof-done-advancing funcall condition-case proof-shell-invoke-callback mapc let* save-excursion if proof-shell-exec-loop if if] 9 [if progn if pg-add-to-input-history if let proof-done-advancing funcall condition-case proof-shell-invoke-callback mapc let* save-excursion if proof-shell-exec-loop if] 12 [mapc let* save-excursion if proof-shell-exec-loop if if let proof-shell-filter-manage-output progn if let if if let save-excursion] 4 [and while let coq-count-match let* coq-module-opening-p or let or coq-goal-command-p funcall cond let proof-done-advancing-other cond let] 1 [let proof-string-match and while let coq-count-match + let* coq-module-opening-p or let or coq-goal-command-p funcall cond let] 12 [let* coq-module-opening-p or let or coq-goal-command-p funcall cond let proof-done-advancing-other cond let proof-done-advancing funcall condition-case proof-shell-invoke-callback] 6 [let proof-done-advancing-save cond let proof-done-advancing funcall condition-case proof-shell-invoke-callback mapc let* save-excursion if proof-shell-exec-loop if if let] 4 [proof-shell-filter-manage-output progn if let if if let save-excursion proof-shell-filter progn condition-case while let if proof-shell-filter-wrapper run-hook-with-args] 9 [timer-relative-time timer-inc-time timer-event-handler nil nil nil nil nil nil nil nil nil nil nil nil nil] 13 [if if let* let scomint-send-input let save-current-buffer proof-shell-insert proof-shell-insert-action-item if let* save-excursion if proof-shell-exec-loop if if] 8 [progn cond proof-toolbar-qed-enable-p redisplay_internal\ \(C\ function\) nil nil nil nil nil nil nil nil nil nil nil nil] 2 [let* pg-remove-element "#<lambda 0x5a29898b7185af8>" funcall "#<lambda 0xa4306fd6cb>" mapc span-delete if while let proof-done-advancing-save cond let proof-done-advancing funcall condition-case] 8 [let coq-count-match let* coq-module-opening-p or let or coq-goal-command-p funcall cond progn if while let proof-done-advancing-save cond] 4 [and let* if company-coq-maybe-proof-input-reload-things run-hooks let save-current-buffer proof-shell-insert proof-shell-insert-action-item if let* save-excursion if proof-shell-exec-loop if if] 6 [while progn if let* proof-shell-wait progn unwind-protect let if save-current-buffer let proof-protected-process-or-retract if let* save-current-buffer if] 7 [while let catch progn if let* proof-shell-kill-function kill-buffer let progn if if proof-shell-exit progn condition-case progn] 21 [apply start-file-process apply setq let let scomint-exec-1 if let save-current-buffer scomint-exec if scomint-make-in-buffer apply scomint-make apply] 2 [let progn condition-case company-coq-read-and-delete cons let* progn if company-coq-ask-prover-redirect car let* progn if company-coq-detect-capabilities progn if] 5 [setq while let* company-coq--split-seq mapcar let if let* if company-coq-tg--parse-group cons let cond let* if cond] 4 [progn if while let* company-coq--split-seq mapcar company-coq-tg--parse-tactic-subs cons company-coq-tg--parse-tactic mapcar let if let* if company-coq-tg--parse-group cons] 3 [company-coq-tg--mk-placeholder list list cond let cond let* company-coq-tg--format-tactic-rec let "#<lambda 0x1f80a3a0ab95240d>" funcall cond let* cond let* company-coq-tg--format-tactic-rec] 13 [setq while let* let company-coq--list-to-table setq company-coq-tactic-initialize-notations-filter progn if company-coq-prover-init run-hooks progn unwind-protect progn if let] 4 [menu-bar-update-buffers-1 menu-bar-update-buffers redisplay_internal\ \(C\ function\) redisplay progn if let* proof-shell-wait if progn if proof-shell-invisible-command "#<lambda 0x1ff2a7ca4a7ea4d5>" mapcar if progn] 2 [internal--after-with-selected-window unwind-protect save-current-buffer let + - let progn if progn unwind-protect let let progn if if] 3 [map-y-or-n-p save-some-buffers let coq-compile-save-some-buffers let progn if let while let let if coq-seq-preprocess-require-commands run-hooks condition-case proof-extend-queue] 29 [mapconcat let while let let if coq-seq-preprocess-require-commands run-hooks condition-case proof-extend-queue let proof-assert-semis let proof-assert-until-point if save-excursion] 4 [apply if let save-current-buffer proof-shell-insert proof-shell-insert-action-item if let* save-excursion if proof-shell-exec-loop if if let proof-shell-filter-manage-output progn] 4 [cond proof-toolbar-qed-enable-p redisplay_internal\ \(C\ function\) nil nil nil nil nil nil nil nil nil nil nil nil nil] 3 [if let proof-done-advancing funcall condition-case proof-shell-invoke-callback mapc let* save-excursion if proof-shell-exec-loop if if let proof-shell-filter-manage-output progn] 6 [save-excursion let* pg-set-span-helphighlights proof-make-goalsave if let proof-done-advancing-save cond let proof-done-advancing funcall condition-case proof-shell-invoke-callback mapc let* save-excursion] 18 [proof-toolbar-goto-enable-p redisplay_internal\ \(C\ function\) nil nil nil nil nil nil nil nil nil nil nil nil nil nil] 10 [if proof-make-goalsave if let proof-done-advancing-save cond let proof-done-advancing funcall condition-case proof-shell-invoke-callback mapc let* save-excursion if proof-shell-exec-loop] 3 [proof-string-match if proof-string-match-safe and cond let proof-done-advancing funcall condition-case proof-shell-invoke-callback mapc let* save-excursion if proof-shell-exec-loop if] 9 [coq-search-urgent-message setq and while let proof-shell-process-urgent-messages and save-excursion proof-shell-filter progn condition-case while let if proof-shell-filter-wrapper run-hook-with-args] 9 [if let save-current-buffer proof-shell-insert proof-shell-insert-action-item if let* save-excursion if proof-shell-exec-loop if if let proof-shell-filter-manage-output progn if] 9 [if while let progn if let span-at-before prev-span setq while let proof-done-advancing-save cond let proof-done-advancing funcall] 8 [if coq-set-state-infos run-hooks proof-done-advancing funcall condition-case proof-shell-invoke-callback mapc let* save-excursion if proof-shell-exec-loop if if let proof-shell-filter-manage-output] 7 [let company-coq-state-change run-hooks proof-done-advancing funcall condition-case proof-shell-invoke-callback mapc let* save-excursion if proof-shell-exec-loop if if let proof-shell-filter-manage-output] 6 [condition-case while let if proof-shell-filter-wrapper run-hook-with-args let save-current-buffer progn if let scomint-output-filter nil nil nil nil] 1 [apply byte-code timer-event-handler nil nil nil nil nil nil nil nil nil nil nil nil nil] 6 [cons if let if build-list-id-from-string let progn if let coq-last-prompt-info coq-last-prompt-info-safe or let if coq-set-state-infos run-hooks] 16 [and or let company-coq-get-goals-window let if let company-coq-state-change run-hooks proof-done-advancing funcall condition-case proof-shell-invoke-callback mapc let* save-excursion] 10 [+ let* coq-module-opening-p or let or coq-goal-command-p funcall cond let proof-done-advancing-other cond let proof-done-advancing funcall condition-case] 7 [goto-char let save-current-buffer progn if let scomint-output-filter nil nil nil nil nil nil nil nil nil] 4 [and let* pg-remove-element "#<lambda 0x5a2f0505ccd5515>" funcall "#<lambda 0xa4306fd6cb>" mapc span-delete if while let proof-done-advancing-save cond let proof-done-advancing funcall] 7 [span-delete mapc span-mapc-spans span-delete-spans proof-script-delete-spans let if proof-done-retracting funcall condition-case proof-shell-invoke-callback mapc let* save-excursion if proof-shell-exec-loop] 4 [file-name-sans-extension x-gtk-map-stock redisplay_internal\ \(C\ function\) redisplay progn if let* proof-shell-wait progn unwind-protect let if save-current-buffer let proof-protected-process-or-retract if] 4 [replace-regexp-in-string progn if company-coq--last-output-without-eager-annotation-markers company-coq-trim progn unwind-protect let unwind-protect progn if progn if company-coq-ask-prover company-coq-unless-error company-coq-ask-prover-swallow-errors] 7 [if while let* company-coq--split-seq mapcar let if let* if company-coq-tg--parse-group cons let cond let* if cond] 4 [last car concat company-coq-tg--mk-placeholder list list cond let cond let* company-coq-tg--format-tactic-rec let "#<lambda 0x20fcd9722e2a51ce>" funcall cond let*] 4 [while let* let company-coq--list-to-table setq company-coq-tactic-initialize-notations-filter progn if company-coq-prover-init run-hooks progn unwind-protect progn if let save-current-buffer] 4 [split-window-sensibly funcall window--try-to-split-window display-buffer-pop-up-window display-buffer--maybe-pop-up-frame-or-window display-buffer if if proof-get-window-for-buffer let progn unwind-protect save-current-buffer let save-excursion if] 6 [pg-add-element let proof-done-advancing-comment cond let proof-done-advancing funcall condition-case proof-shell-invoke-callback mapc let progn if let proof-add-to-queue proof-extend-queue] 6 [cond let proof-done-advancing-other cond let proof-done-advancing funcall condition-case proof-shell-invoke-callback mapc let* save-excursion if proof-shell-exec-loop if if] 3 [let span-make-modifying-removing-span let* pg-set-span-helphighlights let proof-done-advancing-other cond let proof-done-advancing funcall condition-case proof-shell-invoke-callback mapc let* save-excursion if] 3 [timer-event-handler nil nil nil nil nil nil nil nil nil nil nil nil nil nil nil] 4 [coq-set-span-proofstack if let if coq-set-state-infos run-hooks proof-done-advancing funcall condition-case proof-shell-invoke-callback mapc let* save-excursion if proof-shell-exec-loop if] 6 [while let if let spans-at-point-prop car-safe span-at save-current-buffer proof-last-locked-span if let if coq-set-state-infos run-hooks proof-done-advancing funcall] 3 [memq and let scomint-check-proc and proof-shell-live-buffer and proof-toolbar-find-enable-p redisplay_internal\ \(C\ function\) nil nil nil nil nil nil nil] 3 [time-add timer-relative-time timer-inc-time timer-event-handler nil nil nil nil nil nil nil nil nil nil nil nil] 1 [and proof-re-search-forward-safe cond proof-shell-handle-immediate-output let proof-shell-filter-manage-output progn if let if if let save-excursion proof-shell-filter progn condition-case] 26 [let scomint-check-proc and proof-shell-live-buffer and proof-toolbar-find-enable-p redisplay_internal\ \(C\ function\) nil nil nil nil nil nil nil nil nil] 10 [progn condition-case while let if proof-shell-filter-wrapper run-hook-with-args let save-current-buffer progn if let scomint-output-filter nil nil nil] 3 [let if if let save-excursion proof-shell-filter progn condition-case while let if proof-shell-filter-wrapper run-hook-with-args let save-current-buffer progn] 3 [let save-current-buffer proof-shell-insert proof-shell-insert-action-item if let* save-excursion if proof-shell-exec-loop if if let proof-shell-filter-manage-output progn if let] 15 [let proof-shell-filter-manage-output progn if let if if let save-excursion proof-shell-filter progn condition-case while let if proof-shell-filter-wrapper] 9 [or let or coq-goal-command-p funcall cond let proof-done-advancing-other cond let proof-done-advancing funcall condition-case proof-shell-invoke-callback mapc let*] 5 [while let proof-done-advancing-save cond let proof-done-advancing funcall condition-case proof-shell-invoke-callback mapc let* save-excursion if proof-shell-exec-loop if if] 6 [save-current-buffer proof-last-locked-span if let if coq-set-state-infos run-hooks proof-done-advancing funcall condition-case proof-shell-invoke-callback mapc let* save-excursion if proof-shell-exec-loop] 1 [span-set-property let span-make-modifying-removing-span let* pg-set-span-helphighlights proof-make-goalsave if let proof-done-advancing-save cond let proof-done-advancing funcall condition-case proof-shell-invoke-callback mapc] 10 [let progn if let coq-last-prompt-info coq-last-prompt-info-safe or let if coq-set-state-infos run-hooks proof-done-retracting funcall condition-case proof-shell-invoke-callback mapc] 9 [let* progn unwind-protect save-current-buffer let company-coq-tg--preprocess-tactics-grammar let* company-coq-tg--extract-notations and let company-coq-get-all-notations company-coq--list-to-table setq company-coq-tactic-initialize-notations-filter progn if] 4 [company-coq-tg--parse-tactic-part let cond let* if company-coq-tg--parse-tactic-part mapcar company-coq-tg--parse-tactic-subs cons company-coq-tg--parse-tactic mapcar let if let* if company-coq-tg--parse-group] 4 [while let* reverse nconc setq while let* condition-case let* company-coq-tg--extract-notations and let company-coq-get-all-notations company-coq--list-to-table setq company-coq-tactic-initialize-notations-filter] 4 [split-string last car concat company-coq-tg--mk-placeholder list list cond let cond let* company-coq-tg--format-tactic-rec let "#<lambda 0x24ee59938e2aaeb7>" funcall cond] 8 [nconc setq while let* let "#<lambda 0x24ef14fd14aa9352>" funcall cond let* cond let* company-coq-tg--format-tactic-rec progn if company-coq-tg--format-tactic let*] 4 [progn if coq-update-minor-mode-alist run-hooks let proof-shell-handle-delayed-output setq if if let proof-shell-filter-manage-output progn if let if if] 2 [redisplay_internal\ \(C\ function\) redisplay progn if let* proof-shell-wait if progn if proof-shell-invisible-command "#<lambda 0x1ff2a7ca4a7ea4d5>" mapcar if progn unwind-protect progn] 11 [progn if let if let company-coq-state-change run-hooks proof-grab-lock progn if progn if let proof-add-to-queue proof-start-queue let*] 5 [file-remote-p redisplay_internal\ \(C\ function\) message map-y-or-n-p save-some-buffers let coq-compile-save-some-buffers let progn if let while let let if coq-seq-preprocess-require-commands] 4 [let if coq-set-state-infos run-hooks proof-done-advancing funcall condition-case proof-shell-invoke-callback mapc let* save-excursion if proof-shell-exec-loop if if let] 4 [save-excursion proof-locked-region-full-p not progn cond proof-toolbar-use-enable-p redisplay_internal\ \(C\ function\) nil nil nil nil nil nil nil nil nil] 3 [and company-coq-boundp-equal let* if company-coq-maybe-proof-input-reload-things run-hooks let save-current-buffer proof-shell-insert proof-shell-insert-action-item if let* save-excursion if proof-shell-exec-loop if] 9 [let* pg-remove-element "#<lambda 0x5a29898b71869e0>" funcall "#<lambda 0xa4306fd6cb>" mapc span-delete if while let proof-done-advancing-save cond let proof-done-advancing funcall condition-case] 7 [and let* pg-remove-element "#<lambda 0x5a29898b7186907>" funcall "#<lambda 0xa4306fd6cb>" mapc span-delete if while let proof-done-advancing-save cond let proof-done-advancing funcall] 7 [span-property eq cond progn if while let proof-done-advancing-save cond let proof-done-advancing funcall condition-case proof-shell-invoke-callback mapc let*] 9 [internal--after-save-selected-window unwind-protect save-current-buffer let save-excursion if proof-display-and-keep-buffer pg-response-display if proof-shell-display-output-as-response cond let proof-shell-handle-delayed-output setq if if] 173 [redisplay sit-for progn unwind-protect let if save-current-buffer let proof-protected-process-or-retract if let* save-current-buffer if proof-deactivate-scripting progn condition-case] 1 [global-font-lock-mode-cmhh kill-all-local-variables let progn scomint-mode if save-current-buffer if scomint-make-in-buffer apply scomint-make apply let* let if proof-shell-start] 3 [eq cond let* cond let* company-coq-tg--format-tactic-rec progn if company-coq-tg--format-tactic let* reverse nconc setq while let* condition-case] 4 [coq-find-threeb-frames and if if coq-optimise-resp-windows progn if coq-optimise-resp-windows-if-option run-hooks let proof-shell-handle-delayed-output setq if if let proof-shell-filter-manage-output] 3 [setq progn unwind-protect save-current-buffer let let coq-seq-get-library-dependencies setq progn unwind-protect let coq-seq-map-module-id-to-obj-file let coq-seq-check-module while let] 4 [proof-shell-insert-action-item if let* save-excursion if proof-shell-exec-loop if if let proof-shell-filter-manage-output progn if let if if let] 11 [- span-at save-current-buffer proof-last-locked-span if let if coq-set-state-infos run-hooks proof-done-advancing funcall condition-case proof-shell-invoke-callback mapc let* save-excursion] 4 [1+ if let proof-next-element-count proof-element-id proof-next-element-id let proof-done-advancing-other cond let proof-done-advancing funcall condition-case proof-shell-invoke-callback mapc let*] 2 [list eval redisplay_internal\ \(C\ function\) nil nil nil nil nil nil nil nil nil nil nil nil nil] 4 [coq-get-span-statenum or if let if coq-set-state-infos run-hooks proof-done-advancing funcall condition-case proof-shell-invoke-callback mapc let* save-excursion if proof-shell-exec-loop] 3 [save-excursion let* pg-set-span-helphighlights let let proof-done-advancing-comment cond let proof-done-advancing funcall condition-case proof-shell-invoke-callback mapc let* save-excursion if] 4 [if pg-last-output-displayform let* pg-set-span-helphighlights let proof-done-advancing-other cond let proof-done-advancing funcall condition-case proof-shell-invoke-callback mapc let* save-excursion if] 5 [and let scomint-check-proc and proof-shell-live-buffer and proof-toolbar-context-enable-p redisplay_internal\ \(C\ function\) nil nil nil nil nil nil nil nil] 2 [while let coq-search-urgent-message setq and while let proof-shell-process-urgent-messages and save-excursion proof-shell-filter progn condition-case while let if] 1 [proof-shell-live-buffer and proof-toolbar-context-enable-p redisplay_internal\ \(C\ function\) nil nil nil nil nil nil nil nil nil nil nil nil] 8 [proof-string-match coq-section-command-p or let or coq-goal-command-p funcall cond let proof-done-advancing-other cond let proof-done-advancing funcall condition-case proof-shell-invoke-callback] 6 [memq and let scomint-check-proc and proof-shell-live-buffer and proof-toolbar-state-enable-p redisplay_internal\ \(C\ function\) nil nil nil nil nil nil nil] 3 [cond proof-toolbar-undo-enable-p redisplay_internal\ \(C\ function\) nil nil nil nil nil nil nil nil nil nil nil nil nil] 3 [coq-last-prompt-info-safe or let if coq-set-state-infos run-hooks proof-done-advancing funcall condition-case proof-shell-invoke-callback mapc let* save-excursion if proof-shell-exec-loop if] 6 [proof-set-overlay-arrow proof-set-locked-endpoints if proof-set-locked-end let proof-done-advancing funcall condition-case proof-shell-invoke-callback mapc let* save-excursion if proof-shell-exec-loop if if] 2 [proof-locked-region-full-p not progn cond proof-toolbar-use-enable-p redisplay_internal\ \(C\ function\) nil nil nil nil nil nil nil nil nil nil] 9 [proof-set-locked-end let proof-done-advancing funcall condition-case proof-shell-invoke-callback mapc let* save-excursion if proof-shell-exec-loop if if let proof-shell-filter-manage-output progn] 5 [intern company-coq-feature-toggle-function let company-coq-feature-active-p or if company-coq--update-context let if company-coq-maybe-proof-output-reload-things run-hooks let proof-shell-handle-delayed-output setq if if] 3 [progn if let* proof-shell-wait catch progn if let* proof-shell-kill-function kill-buffer let progn if if proof-shell-exit progn] 2 [if let* company-coq-tg--find-tactics mapcar apply let cond let* if let* company-coq-tg--find-tactics mapcar apply let if let*] 4 [if eval redisplay_internal\ \(C\ function\) redisplay progn if let* proof-shell-wait if progn if proof-shell-invisible-command proof-shell-invisible-command-invisible-result mapc if progn] 2 [window--resize-reset-1 window--resize-reset-1 window--resize-reset-1 window--resize-reset-1 window--resize-reset window--resize-root-window-vertically message map-y-or-n-p save-some-buffers let coq-compile-save-some-buffers let progn if let while] 3 [proof-string-match and while let coq-count-match + let* coq-module-opening-p or let or coq-goal-command-p funcall cond let proof-done-advancing-other] 5 [list let* pg-add-element cond let proof-done-advancing-other cond let proof-done-advancing funcall condition-case proof-shell-invoke-callback mapc let* save-excursion if] 7 [funcall redisplay--update-region-highlights apply "#<compiled 0x406067>" redisplay_internal\ \(C\ function\) nil nil nil nil nil nil nil nil nil nil nil] 5 [proof-shell-live-buffer and proof-shell-available-p and progn cond proof-toolbar-undo-enable-p redisplay_internal\ \(C\ function\) nil nil nil nil nil nil nil nil] 4 [and while let coq-count-match let* coq-module-opening-p or let or coq-goal-command-p funcall cond progn if while let] 5 [scomint-check-proc and proof-shell-live-buffer and proof-toolbar-state-enable-p redisplay_internal\ \(C\ function\) nil nil nil nil nil nil nil nil nil nil] 6 [or or progn proof-shell-insert proof-shell-insert-action-item if let* save-excursion if proof-shell-exec-loop if if let proof-shell-filter-manage-output progn if] 8 [cond let proof-done-advancing funcall condition-case proof-shell-invoke-callback mapc let* save-excursion if proof-shell-exec-loop if if let proof-shell-filter-manage-output progn] 2 [let proof-string-match and let* coq-module-opening-p or let or coq-goal-command-p funcall cond progn if while let proof-done-advancing-save] 9 [span-set-property let* pg-add-element cond let proof-done-advancing-other cond let proof-done-advancing funcall condition-case proof-shell-invoke-callback mapc let* save-excursion if] 2 [mapc span-delete if while let proof-done-advancing-save cond let proof-done-advancing funcall condition-case proof-shell-invoke-callback mapc let* save-excursion if] 2 [save-current-buffer let cond pg-response-display-with-face let* proof-shell-process-urgent-message-default cond proof-shell-process-urgent-message save-excursion if while let proof-shell-process-urgent-messages and save-excursion proof-shell-filter] 3 [x-gtk-map-stock redisplay_internal\ \(C\ function\) redisplay progn if let* proof-shell-wait progn unwind-protect let if save-current-buffer let proof-protected-process-or-retract if let*] 4 [if eval redisplay_internal\ \(C\ function\) redisplay progn if let* proof-shell-wait progn unwind-protect let if save-current-buffer let proof-protected-process-or-retract if] 4 [company-coq-tg--parse-tactic-part mapcar company-coq-tg--parse-tactic-subs cons company-coq-tg--parse-tactic mapcar let if let* if company-coq-tg--parse-group cons let cond let* if] 4 [reverse nconc setq while let* let "#<lambda 0x18fbe0c3e1a52276>" funcall cond let* cond let* company-coq-tg--format-tactic-rec let* let "#<lambda 0x79d8319b15e96a5>"] 76 [cond let* company-coq-tg--format-tactic-rec let* let "#<lambda 0xdd9c0868b027757>" funcall cond let* cond let* company-coq-tg--format-tactic-rec let* let "#<lambda 0x396cfa403b175c1f>" funcall] 4 [version-to-list version< let coq--version< coq--pre-v85 coq-include-options nconc let coq-seq-get-library-dependencies setq progn unwind-protect let coq-seq-map-module-id-to-obj-file let coq-seq-check-module] 4 [and proof-toolbar-state-enable-p redisplay_internal\ \(C\ function\) nil nil nil nil nil nil nil nil nil nil nil nil nil] 4 [save-excursion let* pg-set-span-helphighlights let pg-add-proof-element let proof-make-goalsave if let proof-done-advancing-save cond let proof-done-advancing funcall condition-case proof-shell-invoke-callback] 6 [let proof-string-match and while let coq-count-match let* coq-module-opening-p or let or coq-goal-command-p funcall cond progn if] 2 [pg-set-span-helphighlights let proof-done-advancing-other cond let proof-done-advancing funcall condition-case proof-shell-invoke-callback mapc let* save-excursion if proof-shell-exec-loop if if] 5 [let scomint-send-input let save-current-buffer proof-shell-insert proof-shell-insert-action-item if let* save-excursion if proof-shell-exec-loop if if let proof-shell-filter-manage-output progn] 2 [and cond let proof-done-advancing funcall condition-case proof-shell-invoke-callback mapc let* save-excursion if proof-shell-exec-loop if if let proof-shell-filter-manage-output] 1 [not or if let proof-done-advancing funcall condition-case proof-shell-invoke-callback mapc let* save-excursion if proof-shell-exec-loop if if let] 7 [proof-toolbar-retract-enable-p redisplay_internal\ \(C\ function\) nil nil nil nil nil nil nil nil nil nil nil nil nil nil] 174 [if let* save-excursion if proof-shell-exec-loop if if let proof-shell-filter-manage-output progn if let if if let save-excursion] 1 [profiler-cpu-profile profiler-report-cpu profiler-report if if save-current-buffer pg-profile-1 apply byte-code timer-event-handler nil nil nil nil nil nil] 6 [Automatic\ GC] 593)) (22381 28814 617335 579000) nil]

[-- Attachment #2: OpenPGP digital signature --]
[-- Type: application/pgp-signature, Size: 836 bytes --]

Re: What makes set-window-buffer slow?

[Eli Zaretskii]

> Cc: acm@muc.de, schwab@suse.de, emacs-devel@gnu.org
> From: Clément Pit--Claudel <clement.pit@gmail.com>
> Date: Fri, 24 Jun 2016 10:19:12 -0400
> 
> The proof-shell functions do this: they handle communication with the subprocess. The main loop looks like this:
> 
> * Fetch one command from the buffer
> * Send it to the subprocess
> * When a response arrives, call a hook
> * Send the next command
> 
> My code adds a functioon into that hook that calls set-window-buffer; when I remove that call, everything is snappy. When I add it back in, everything gets much slower (at least that's what I understand; this isn't happening on my machine).

What is the purpose of calling set-window-buffer?

Also, how come it doesn't happen on your machine?  Are any
customizations involved?  Is your OS different from that of the other
user?

Re: What makes set-window-buffer slow?

[Clément Pit--Claudel]

[-- Attachment #1.1: Type: text/plain, Size: 1031 bytes --]

On 2016-06-24 15:13, Eli Zaretskii wrote:
> What is the purpose of calling set-window-buffer?

When started, Proof General splits the screen in two:

|             |             |
|             |             |
| User's file | Message log |
|             |             |
|             |             |

Each time a message is received, it's displayed in the Message log window.
My extension sometimes reuses that window for other things (for example, to show company-mode's documentation buffer).
The set-window-buffer call is there to ensure that the user sees new messages. Of course in most cases that call is useless: that's why predicating it on the window not already displaying the message log makes things faster.

> Also, how come it doesn't happen on your machine?  Are any
> customizations involved?  Is your OS different from that of the other
> user?

Somewhat unclear. The OS are the same (Linux mint), and the problem does happen in emacs -Q for the other user. The version of Emacs is the same.


[-- Attachment #2: OpenPGP digital signature --]
[-- Type: application/pgp-signature, Size: 836 bytes --]

Re: What makes set-window-buffer slow?

[Eli Zaretskii]

> Cc: acm@muc.de, schwab@suse.de, emacs-devel@gnu.org
> From: Clément Pit--Claudel <clement.pit@gmail.com>
> Date: Fri, 24 Jun 2016 17:33:23 -0400
> 
> When started, Proof General splits the screen in two:
> 
> |             |             |
> |             |             |
> | User's file | Message log |
> |             |             |
> |             |             |
> 
> Each time a message is received, it's displayed in the Message log window.
> My extension sometimes reuses that window for other things (for example, to show company-mode's documentation buffer).
> The set-window-buffer call is there to ensure that the user sees new messages. Of course in most cases that call is useless: that's why predicating it on the window not already displaying the message log makes things faster.

Does the WINDOW argument of set-window-buffer name the selected window
at the time of the call?  If not, set-window-buffer will cause all the
other windows to be redisplayed, so arranging for WINDOW to be the
selected window might speed up things.

Another potential speedup might be had if you invoke set-window-buffer
with its KEEP-MARGINS argument non-nil.

Alternatively, try changing your hook to use its own window for
whatever you want to show, leaving the "Message Log" window alone.

I'm puzzled how come redisplay was called so many times (2400) in this
scenario.  Is such a large number reasonable?  How many seconds did it
take to run the scenario?

> > Also, how come it doesn't happen on your machine?  Are any
> > customizations involved?  Is your OS different from that of the other
> > user?
> 
> Somewhat unclear. The OS are the same (Linux mint), and the problem does happen in emacs -Q for the other user. The version of Emacs is the same.

How about local vs remote invocation, and/or the X configuration in
general?

Also, what about toolkits and Cairo -- did both builds use the same
optional features in this department?

Finally, if the user can try a later Emacs, it might help, because
some non-trivial redisplay optimizations were done since 24.4.

Re: What makes set-window-buffer slow?

[Clément Pit--Claudel]

[-- Attachment #1.1: Type: text/plain, Size: 3270 bytes --]

On 2016-06-25 03:30, Eli Zaretskii wrote:
>> Cc: acm@muc.de, schwab@suse.de, emacs-devel@gnu.org
>> From: Clément Pit--Claudel <clement.pit@gmail.com>
>> Date: Fri, 24 Jun 2016 17:33:23 -0400
>>
>> When started, Proof General splits the screen in two:
>>
>> |             |             |
>> |             |             |
>> | User's file | Message log |
>> |             |             |
>> |             |             |
>>
>> Each time a message is received, it's displayed in the Message log window.
>> My extension sometimes reuses that window for other things (for example, to show company-mode's documentation buffer).
>> The set-window-buffer call is there to ensure that the user sees new messages. Of course in most cases that call is useless: that's why predicating it on the window not already displaying the message log makes things faster.
> 
> Does the WINDOW argument of set-window-buffer name the selected window
> at the time of the call?  If not, set-window-buffer will cause all the
> other windows to be redisplayed, so arranging for WINDOW to be the
> selected window might speed up things.

The window was indeed not selected at the time of the call. Would a simple with-selected-window around the call do it? If so, could set-window-buffer just do that? Btw, do you think there is any issue with just not calling set-window-buffer if the window already contains that buffer?

> Another potential speedup might be had if you invoke set-window-buffer
> with its KEEP-MARGINS argument non-nil.

Interesting, thanks! That wouldn't prevent the scrollbar's length from being adjusted to the length of the newly displayed buffer, right?

> Alternatively, try changing your hook to use its own window for
> whatever you want to show, leaving the "Message Log" window alone.

I don't think that's possible, unfortunately :/

> I'm puzzled how come redisplay was called so many times (2400) in this
> scenario.  Is such a large number reasonable?  How many seconds did it
> take to run the scenario?

5 to 8 minutes, I think. (Btw, maybe the profiler could record this timing information?

>>> Also, how come it doesn't happen on your machine?  Are any
>>> customizations involved?  Is your OS different from that of the other
>>> user?
>>
>> Somewhat unclear. The OS are the same (Linux mint), and the problem does happen in emacs -Q for the other user. The version of Emacs is the same.
> 
> How about local vs remote invocation, and/or the X configuration in
> general?

I think local invocation in both cases. Mate desktop vs. Cinnamon. Would it be useful for me to profile the same code on my own machine? Maybe comparing the profiles would help.

> Also, what about toolkits and Cairo -- did both builds use the same
> optional features in this department?

I think so; I use the default build setting, plus a patch to revert a commit that makes Emacs unusable for me since April 2014.

> Finally, if the user can try a later Emacs, it might help, because
> some non-trivial redisplay optimizations were done since 24.4.

Ok, I'll keep this in mind; I don't think that will happen for them until Debian updates, though. And in any case, I don't even have this problem on 24.4...

Clément.


[-- Attachment #2: OpenPGP digital signature --]
[-- Type: application/pgp-signature, Size: 836 bytes --]

Re: What makes set-window-buffer slow?

[Eli Zaretskii]

> Cc: acm@muc.de, schwab@suse.de, emacs-devel@gnu.org
> From: Clément Pit--Claudel <clement.pit@gmail.com>
> Date: Sat, 25 Jun 2016 10:07:11 -0400
> 
> > Does the WINDOW argument of set-window-buffer name the selected window
> > at the time of the call?  If not, set-window-buffer will cause all the
> > other windows to be redisplayed, so arranging for WINDOW to be the
> > selected window might speed up things.
> 
> The window was indeed not selected at the time of the call. Would a
> simple with-selected-window around the call do it?

Yes, I think so.  Although it'd be better to arrange that to happen
without the need to select the window, if possible.

> If so, could set-window-buffer just do that?

No, of course not.  We don't know at this level what is the
programmer's intent.

> Btw, do you think there is any issue with just not calling set-window-buffer if the window already contains that buffer?

Not sure I understand the question: how can there be an issue when NOT
doing something?

> Would it be useful for me to profile the same code on my own
> machine? Maybe comparing the profiles would help.

Could be.  But identifying the differences is also useful.

> > Finally, if the user can try a later Emacs, it might help, because
> > some non-trivial redisplay optimizations were done since 24.4.
> 
> Ok, I'll keep this in mind; I don't think that will happen for them until Debian updates, though. And in any case, I don't even have this problem on 24.4...

The optimizations might well affect only some system configurations.

Re: What makes set-window-buffer slow?

[Eli Zaretskii]

> Date: Sat, 25 Jun 2016 17:27:17 +0300
> From: Eli Zaretskii <eliz@gnu.org>
> Cc: acm@muc.de, emacs-devel@gnu.org, schwab@suse.de
> 
> > Cc: acm@muc.de, schwab@suse.de, emacs-devel@gnu.org
> > From: Clément Pit--Claudel <clement.pit@gmail.com>
> > Date: Sat, 25 Jun 2016 10:07:11 -0400
> > 
> > > Does the WINDOW argument of set-window-buffer name the selected window
> > > at the time of the call?  If not, set-window-buffer will cause all the
> > > other windows to be redisplayed, so arranging for WINDOW to be the
> > > selected window might speed up things.
> > 
> > The window was indeed not selected at the time of the call. Would a
> > simple with-selected-window around the call do it?
> 
> Yes, I think so.

Actually, I see that in Emacs 24.4, this factor should have made no
difference, sorry.  (I was looking at the current sources when I wrote
the above.)