Skip to content

Commit

Permalink
Fixing Set/Unset Printing broken by auto "Show".
Browse files Browse the repository at this point in the history 
Current coq trunk has a bug with Show that I reported (there is a
spurious Show executed) which makes C-u C-c C-a C-s fail for now.
Should be fixed shortly.
  • Loading branch information
@Matafou
Matafou committed May 16, 2017
1 parent b6b38b7 commit afb29a6
Showing 1 changed file with 23 additions and 9 deletions.
32 changes: 23 additions & 9 deletions coq/coq.el
View file
Original file line number Diff line number Diff line change
Expand Up @@ -951,20 +951,25 @@ Otherwise propose identifier at point if any."
(string-match "is on\\>" resp)))

(defun coq-command-with-set-unset (setcmd cmd unsetcmd &optional postformatcmd testcmd)
"Play commands SETCMD then CMD and then silently UNSETCMD."
"Play commands SETCMD then CMD and then silently UNSETCMD. The
last UNSETCMD is performed with tag 'empty-action-list so that it
does not trigger 'proof-shell-empty-action (which dos \"Shwo\" at
the time of writing this documentation)."
(let* ((postform (if (eq postformatcmd nil) 'identity postformatcmd))
(flag-is-on (and testcmd (coq-flag-is-on-p testcmd))))
(unless flag-is-on (proof-shell-invisible-command
(format " %s . " (funcall postform setcmd)) 'wait))
(proof-shell-invisible-command
(format " %s . " (funcall postform cmd)) 'wait)
(unless flag-is-on (proof-shell-invisible-command-invisible-result
(format " %s . " (funcall postform unsetcmd))))))
(unless flag-is-on (proof-shell-invisible-command
(format " %s . " (funcall postform unsetcmd))
'waitforit nil 'empty-action-list))))

(defun coq-ask-do-set-unset (ask do setcmd unsetcmd
&optional dontguess postformatcmd tescmd)
"Ask for an ident id and execute command DO in SETCMD mode.
More precisely it executes SETCMD, then DO id and finally silently UNSETCMD."
More precisely it executes SETCMD, then DO id and finally
silently UNSETCMD. See `coq-command-with-set-unset'."
(let* ((cmd) (postform (if (eq postformatcmd nil) 'identity postformatcmd tescmd)))
(proof-shell-ready-prover)
(setq cmd (coq-guess-or-ask-for-string ask dontguess))
Expand Down Expand Up @@ -1218,12 +1223,21 @@ flag Printing All set."
;; of coq) Coq does not show the goals of enclosing proof when closing a nested
;; proof. This is coq's proof-shell-empty-action-list-command function which
;; inserts a "Show" if the last command of an action list is a save command and
;; there is more than one open proof before that save.
;; there is more than one open proof before that save. If you want to issue a
;; command and *not* have the goal redisplayed, the command must be tagged with
;; 'empty-action-list.
(defun coq-empty-action-list-command (cmd)
(when (or (and (string-match coq-save-command-regexp-strict cmd)
(> (length coq-last-but-one-proofstack) 1))
(and (string-match "\\(S\\|Uns\\)et\\s-+Printing" cmd)
(> (length coq-last-but-one-proofstack) 0)))
"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. "
(when (or
;; If clsing a nested proof, return t.
(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.")))

(defpacustom auto-adapt-printing-width t
Expand Down

6 comments on commit afb29a6

@ejgallego
Copy link

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

@Matafou this will be fixed once coq/coq#640 is merged. However I keep wondering about the future of -emacs. For instance, it seems to me that having to maintain a list of commands that print the goals between Coq and PG is fragile and prone to error. Wouldn't it easier for PG to just issue Show when desired? [Another option would be to quote the goals, but I guess you are OK with the current status now]

@Matafou
Copy link
Contributor Author

@Matafou Matafou commented on afb29a6 May 18, 2017 via email

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

@ejgallego
Copy link

@ejgallego ejgallego commented on afb29a6 May 18, 2017 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Hi Pierre, I am not sure if you mean "strange auto show" for the current bug, or in general.

What I mean is that in general, "auto goal show" relies on heurisitics, so it is prone to breaking, as PG has to be in sync with emacs heuristics. So an option to avoid this kind of problems in the future would be to entirely disable goal display when -emacs is passed to the current toplevel.

@Matafou
Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Yes we can do that. However for efficiency reason we don't want to print goals too often (people do have big goals), so it would result in moving the heuristic from coq to pg (when pg should send a "Show."?) and I guess coq is better at knowing when the goal has changed. Or maybe the information that the goal has changed can be sent by coq?

And moreover my point was that some people use "coqtop" without emacs, and they WANT goal to be printed automatically instead of typing "Show" evey now and then. So you will still have a heuristic present in coq code anyway.

@ejgallego
Copy link

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Well, it is the current model that is the most inefficient as the client has no control over when the goals are printed; and a large goal will be printed many times likely unnecessarily. When PG should send a Show, well, is PG business. Not to say if you do go to point and process 1000 sentences, Coq will print the goals 1000 times in the current model.

A set of heuristics has to be always maintained, in the current model, we have to maintain two sets (Coq and PG) and keep them in sync. In my proposed model, only one.

By the wa, AFACIT, currently Coq does not detect if the goal has changed, and that optimization could be implemented in the two models so it is orthogonal.

some people use "coqtop" without emacs,

You hit the crux of the question, people != emacs, what humans need is not what emacs needs.

@Matafou
Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Well, it is the current model that is the most inefficient as the client has no control over when the goals are printed; and a large goal will be printed many times likely unnecessarily. When PG should send a Show, well, is PG business. Not to say if you do go to point and process 1000 sentences, Coq will print the goals 1000 times in the current model.

Of course the client has control! Obviously PG Set Silent before sending a group of command to coq, and unsets silent just before the last command.

I fully agree that this is not the right way and the new protocols are way better. Let us just make the old one survive one more version that is all.

By the wa, AFACIT, currently Coq does not detect if the goal has changed, and that optimization could be implemented in the two models so it is orthogonal.

Does coqide issue a "Goal" after a Print command if it already saw the goal before the print command? If efficiency becomes an issue (on big goals) that might be something to optimize indeed.

Please sign in to comment.