Please remove automatic Set/Unset commands

[andres-erbsen]

Please remove automatic Set/Unset commands.

Set and Unset during a proof trigger coq STM to synchronize a bunch of stuff, which can be very expensive. https://gist.github.com/andres-erbsen/edd3902c927bf67cba0ca1e9a7718d7c is an example flame graph of coq during Unset Silent, stepping back and forth in https://github.com/mit-plv/bedrock2/commit/48e2314623e8695df7f0bf2e390ce224baf7a161#diff-5c7e120c9281033af09d97fd489aa26aR74 is an example that is essentially unusable with the current ProofGeneral.

see also #212

[JasonGross]

Note that this will break interaction with old versions of Coq; perhaps this should be controlled by an option that can be set in ~/.emacs, something like enable-compatibility-with-coq-before-8.7-at-the-cost-of-performance or something?

[ejgallego]

Note that quite a bit of code can be cleaned up if PG chooses to work with an explícit goal display mode.

[cpitclaudel]

Note that this will break interaction with old versions of Coq; perhaps this should be controlled by an option that can be set in ~/.emacs

Rather, we could just condition this on being in Coq >= some version number

[andres-erbsen]

Adding the following to .emacs makes this performance issue go away. It also causes PG to show the goal in the messages window when backtracking. Thanks @cpitclaudel for helping me out.

(add-hook 'coq-mode-hook
          (lambda ()
            (setq proof-shell-start-silent-cmd nil
                  proof-shell-stop-silent-cmd nil
                  coq-auto-adapt-printing-width nil)
            (coq-set-auto-adapt-printing-width)
            (defun coq-empty-action-list-command (cmd)
              "Return the list of commands to send to Coq after CMD
if it is the last command of the action list.
If CMD is tagged with 'empty-action-list then this function won't
be called and no command will be sent to Coq."
              (cond
               ((or
                 ;; If closing a nested proof, Show the enclosing goal.
                 (and (string-match coq-save-command-regexp-strict cmd)
                      (> (length coq-last-but-one-proofstack) 1))
                 ;; If user issued a printing option then t printing.
                 (and (string-match "\\(S\\|Uns\\)et\\s-+Printing" cmd)
                      (> (length coq-last-but-one-proofstack) 0)))
                (list "Show."))
               ((or
                 ;; if we go back in the buffer and that the number of abort is less than
                 ;; the number of nested goals, then Unset Silent and Show the goal
                 (and (string-match "Backtrack\\s-+[[:digit:]]+\\s-+[[:digit:]]+\\(\\s-+[[:digit:]]*\\)" cmd)
                      (> (length (coq-get-span-proofstack (proof-last-locked-span)))
                         ;; the number of aborts is the third arg of Backtrack.
                         (string-to-number (match-string 1 cmd)))))
                (list  "Show."))
               ((or
                 ;; If we go back in the buffer and not in the above case, then only Unset
                 ;; silent (there is no goal to show).
                 (string-match "Backtrack" cmd))
                (list ))))))

[HuStmpHrrr]

is this a generally useful thing? should this go into PG directly so that everyone can have the benefit?

[cpitclaudel]

Yes, there is a performance bug here and it should be fixed. Unfortunately, I don't have time to work on it at the moment, so I helped @andres-erbsen find a quick-and-dirty workaround.

[Matafou]

The workaround is not very satisfying as a real solution. The reason of Set Silent/Unset Silent. is performance. If you go trough a big script showing all the intermediate goals this is potentially millions of lines that emacs will have to read (and lex lightly).

Being always in Silent mode and asking for the goal when needed is also not possible: we would miss information messages like "subgoal solved, next bullet is ++".

@ejgallego do you see an intermediate solution in the current non-structured coqtop? We could have coq's "-emacs" mode to be "no goals, everything else"?

Until we at last switch to some better protocol that is.

[ejgallego]

@ejgallego do you see an intermediate solution in the current non-structured coqtop? We could have coq's "-emacs" mode to be "no goals, everything else"?

Yes we could do that.

I think we are deprecating silent and instead we will use levels [info, debug, warning], so indeed we could fix the information messages depending on that flag.

[Matafou]

Actually I just checked and "Show" does print the info messages too. I was not aware of that (although I implemented these messages...). So maybe being completely silent and only do "Show" is OK.

[ejgallego]

Yeah I think that being completely silent is the way to go; nothing that still you have the debug/info channel.

If we find some problems should be easy to fix Coq side.

[Matafou]

OK I will first make a branch a test with several versions of coq to see if we need backward compatibility checks.

Basically this is a variant of @cpitclaudel workaround: no more Set/Unset Silent except ONE Set Silent at the very beginning + Show in more cases at the beginning of the session.

Tested. It seems to work, the only difference I see currently in my tests is that we don't get intermediate messages like "Foo is defined.". Not a big deal I would say.

[Matafou]

In fine we may still need a specific pseudo-silent mode anyway.

[ejgallego]

like "Foo is defined.". Not a big deal I would say.

I will move these missing messages to remain outside silent. Another thing we could do is to have -emacs set silent.

[Matafou]

I will move these missing messages to remain outside silent. Another thing we could do is to have -emacs set silent.

Is it reasonable to change the behaviour of Set Silent itself?

[ejgallego]

I feel that Set Silent in a sense is going away in favor of the feedback mechanism which allows for finer filtering.

I think indeed we can change the behavior, with care of course.

[cpitclaudel]

Tested. It seems to work, the only difference I see currently in my tests is that we don't get intermediate messages like "Foo is defined.". Not a big deal I would say.

Can we make sure that this doesn't break company-coq? I think it uses xxx defined as a sign that it needs to reload completion lists.

[Matafou]

Can we make sure that this doesn't break company-coq? I think it uses xxx defined as a sign that it needs to reload completion lists.

Indeed this probably breaks...

[ejgallego]

So maybe the better plan is just to make -emacs not to print goals, we let PG use the default not silent mode.

[Matafou]

So maybe the better plan is just to make -emacs not to print goals, we let PG use the default not silent mode.

OK but this must wait for coq-8.10?

[ejgallego]

Yes, I'd be supportive to get this into 8.9.1 [so PG could also check] or to add an option like Set Printing Goals

[ejgallego]

But in general user messages such as "Foo is Defined" are kinda fragile and at some point won't depend on the silent flag [for example we may move the Foo is defined to the INFO feedback level.

[monnier]

Can we make sure that this doesn't break company-coq? I think it uses xxx defined as a sign that it needs to reload completion lists. Indeed this probably breaks...

Maybe company-coq can be changed to use some other heuristic to decide when to reload the completion lists.

After all, I suspect that for most people it's much easier to upgrade their company-coq than to upgrade their Coq.

[cpitclaudel]

Maybe company-coq can be changed to use some other heuristic to decide when to reload the completion lists.

Of course, if we can find another heuristic :)

[JasonGross]

I make essential use of idtac when debugging tactics, and also like to be able to see the time taken by commands when I move forward across a couple dozen commands with Time. Would this change impact my ability to see either of those?

[Matafou]

OK this breaks a few other things anyway: commands like "Fail xxx." "Show Intros." etc do not display anything. Lots a features of both pg and company-coq depend on this.

[Matafou]

Yes it breaks these features currently.