Skip to content

Commit

Permalink
coq: run silently and explicitly Show when necessary
Browse files Browse the repository at this point in the history
This is a step towards fixing ProofGeneral#568. It fixes the cases after Proof,
comments, auto, errors, Search and Check, leaving now 2 instead of 8
failing tests in ci/simple-tests/test-goals-present.el. Admitted is
not handled correctly any more, which is a regression.

Using proof-shell-handle-delayed-output-hook and
proof-shell-handle-error-or-interrupt-hook we issue a Show command as
a priority action item when the last (normal) action item has been
processed.

The new action item flag 'keep-response tells the generic machinery to
not clear the response buffer and to keep it present in two-pane mode
in case an error was detected or the last command was a Search or
Check that produced a response.

The new action item flag 'coq-show-when-silent is used to distinguish
the additional Show commands and to avoid an endless loop of Show
commands.

Set proof-shell-last-output-kind now in
proof-shell-handle-delayed-output such that it correctly reflects the
cases of goals and response (which has not been the case since commit
037dc9b from 2009.

This commit breaks coq-show-proof-stepwise to some extend. Expect
080_coq-test-regression-show-proof-stepwise to fail.

Additionally:
- update manuals
- expect errors in tests 020_coq-test-definition,
  090_coq-test-regression-Fail and 091_coq-test-regression-Fail
  because messages are not printed in silent mode
  • Loading branch information
hendriktews committed Apr 18, 2024
1 parent d30569d commit e2c661d
Show file tree
Hide file tree
Showing 6 changed files with 161 additions and 41 deletions.
16 changes: 16 additions & 0 deletions ci/coq-tests.el
Original file line number Diff line number Diff line change
Expand Up @@ -196,6 +196,8 @@ For example, COMMENT could be (*test-definition*)"


(ert-deftest 020_coq-test-definition ()
;; There are no infomsgr when running silent.
:expected-result :failed
"Test *response* output after asserting a Definition."
(coq-fixture-on-file
(coq-test-full-path "test_stepwise.v")
Expand Down Expand Up @@ -291,6 +293,9 @@ For example, COMMENT could be (*test-definition*)"

(ert-deftest 080_coq-test-regression-show-proof-stepwise()
"Regression test for the \"Show Proof\" option"
;; When running silent, the Show Proof command is issued, but its
;; output is not (yet) kept in the response buffer.
:expected-result :failed
(coq-fixture-on-file
(coq-test-full-path "test_stepwise.v")
(lambda ()
Expand All @@ -317,6 +322,10 @@ For example, COMMENT could be (*test-definition*)"


(ert-deftest 090_coq-test-regression-Fail()
;; When running silent, the message about indeed failing is not
;; shown. One might fix this test by checking that there is no
;; error, which would be shown without Fail.
:expected-result :failed
"Test for Fail"
(coq-fixture-on-file
(coq-test-full-path "test_stepwise.v")
Expand All @@ -338,6 +347,13 @@ Tactic failure: Cannot solve this goal." "*coq*")))))
;; (coq-should-buffer-regexp (regexp-quote "The command has indeed failed with message: Tactic failure: Cannot solve this goal.") "*response*")

(ert-deftest 091_coq-test-regression-Fail()
;; XXX What is the difference between this test and
;; 090_coq-test-regression-Fail?

;; When running silent, the message about indeed failing is not
;; shown. One might fix this test by checking that there is no
;; error, which would be shown without Fail.
:expected-result :failed
"Test for Fail"
(coq-fixture-on-file
(coq-test-full-path "test_stepwise.v")
Expand Down
8 changes: 1 addition & 7 deletions ci/simple-tests/coq-test-goals-present.el
Original file line number Diff line number Diff line change
Expand Up @@ -260,17 +260,14 @@ which action the goals buffer should have been reset."

(ert-deftest goals-after-proof ()
"Test goals are present after ``Proof''."
:expected-result (if coq--post-v87 :failed :passed)
(goals-after-test coq-src-proof "Proof" nil))

(ert-deftest goals-after-comment ()
"Test goals are present after a comment."
:expected-result :failed
(goals-after-test coq-src-comment "comment" nil))

(ert-deftest goals-after-auto ()
"Test goals are present after ``auto''."
:expected-result (if coq--post-v87 :failed :passed)
(goals-after-test coq-src-auto "auto" nil))

(ert-deftest goals-after-simpl ()
Expand All @@ -279,11 +276,11 @@ which action the goals buffer should have been reset."

(ert-deftest goals-after-error ()
"Test goals are present after an error."
:expected-result :failed
(goals-after-test coq-src-error "error" t))

(ert-deftest goals-reset-after-admitted ()
"The goals buffer is reset after an Admitted."
:expected-result :failed
(goals-buffer-should-get-reset coq-src-admitted "intros P" "Admitted"))

(ert-deftest goals-reset-no-more-goals ()
Expand Down Expand Up @@ -359,7 +356,6 @@ two-pane mode."

(ert-deftest goals-up-to-date-at-error ()
"Check that goals are updated before showing the error."
:expected-result :failed
(update-goals-when-response coq-src-update-goal-after-error
"Lemma foo"
"H : eq_one 1 -> False"
Expand All @@ -382,7 +378,6 @@ This test checks several commands inside a proof with a final
Search command. After processing these commands, the goals buffer
should have been updated and the response buffer should contain
something and be visible in two-pane mode."
:expected-result :failed
(update-goals-when-response coq-src-update-goal-after-search
"Lemma g"
"2 = 2"
Expand All @@ -405,7 +400,6 @@ This test checks several commands inside a proof with a final
Check command. After processing these commands, the goals buffer
should have been updated and the response buffer should contain
something and be visible in two-pane mode."
:expected-result :failed
(update-goals-when-response coq-src-update-goal-after-check
"Lemma h"
"3 = 3"
Expand Down
128 changes: 106 additions & 22 deletions coq/coq.el
Original file line number Diff line number Diff line change
Expand Up @@ -122,8 +122,21 @@ Namely, goals that do not fit in the goals window."
;; should re-intialize to coq-search-blacklist-string instead of
;; keeping the current value (that may come from another file).
,(format "Add Search Blacklist %s. " coq-search-blacklist-current-string))
'("Set Suggest Proof Using. ") coq-user-init-cmd)
"Command to initialize the Coq Proof Assistant.")
'("Set Suggest Proof Using. "
"Set Silent. ")
coq-user-init-cmd)
"Commands for initial Coq configuration, Coq variant of `proof-shell-init-cmd'.
List of commands sent to the Coq background process just after it
has been started. This happens inside `proof-shell-config-done',
when the major mode `coq-shell-mode' is configured in the `*coq*'
buffer.
Sets silent mode.
In normal interaction, Coq is started because the user asserts
some commands. Therefore the commands here are followed by those
inserted inside `proof-assert-command-hook', respectively,
`coq-adapt-printing-width'.")

;; FIXME: Even if we don't use coq-indent for indentation, we still need it for
;; coq-script-parse-cmdend-forward/backward and coq-find-real-start.
Expand Down Expand Up @@ -1207,12 +1220,15 @@ Printing All set."
;; command and *not* have the goal redisplayed, the command must be tagged with
;; 'empty-action-list.
(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.
"Return the list of commands to send to Coq if CMD is last in the action list.
Return the list of commands to be sent to Coq when
`proof-action-list' is empty, CMD was the last command just sent
to Coq and CMD was not tagged with `'empty-action-list'.
Note: the last command added if `coq-show-proof-stepwise' is set
should match the `coq-show-proof-diffs-regexp'."
should match the `coq-show-proof-diffs-regexp'.
This function is called from `proof-shell-exec-loop' via
`proof-shell-empty-action-list-command'."
(cond
((or
;; If closing a nested proof, Show the enclosing goal.
Expand All @@ -1225,28 +1241,29 @@ should match the `coq-show-proof-diffs-regexp'."
. ,(coq--show-proof-stepwise-cmds)))

((or
;; If we go back in the buffer and the number of abort is less than
;; the number of nested goals, then Unset Silent and Show the goal
;; If we go back in the buffer and the number of abort is less than the
;; number of nested goals, that is, if we are inside a proof, then Show
;; the goal.
(and (string-match-p "BackTo\\s-" cmd)
(> (length coq-last-but-one-proofstack) coq--retract-naborts)))
`("Unset Silent."
,(if (coq--post-v810) (coq-diffs) "Show.")
. ,(coq--show-proof-stepwise-cmds)))
(append
(if (coq--post-v810) (list (coq-diffs)) ())
;; '("Show.")
(coq--show-proof-stepwise-cmds)))

((or
;; If we go back in the buffer and not in the above case, then only Unset
;; silent (there is no goal to show). Still, we need to "Set Diffs" again
;; If we go back in the buffer and not in the above case, i.e., outside a
;; proof, then only set the Diffs option.
(string-match-p "BackTo\\s-" cmd))
(if (coq--post-v810)
(list "Unset Silent." (coq-diffs) )
(list "Unset Silent.")))
(if (coq--post-v810) (list (coq-diffs)) ()))

((or
;; If starting a proof, Show Proof if need be
(coq-goal-command-str-p cmd)
;; If doing (not closing) a proof, Show Proof if need be
(and (not (string-match-p coq-save-command-regexp-strict cmd))
(> (length coq-last-but-one-proofstack) 0)))
(coq--show-proof-stepwise-cmds))))
(coq--show-proof-stepwise-cmds))))

;; This does not Set Printing Width, it rather tells pg to do that before each
;; command (if necessary)
Expand Down Expand Up @@ -1326,7 +1343,9 @@ redisplayed."
(let ((wdth (or width (coq-guess-goal-buffer-at-next-command))))
;; if no available width, or unchanged, do nothing
(when (and wdth (not (equal wdth coq-shell-current-line-width)))
(proof-shell-invisible-command (format "Set Printing Width %S." (- wdth 1)) t)
(proof-shell-invisible-command
(format "Set Printing Width %S." (- wdth 1))
t)
(setq coq-shell-current-line-width wdth)
;; Show iff show non nil and some proof is under way
(when (and show (not (null (cl-caddr (coq-last-prompt-info-safe)))))
Expand Down Expand Up @@ -1846,7 +1865,7 @@ at `proof-assistant-settings-cmds' evaluation time.")
(let ((pt2 (point)))
(re-search-backward "Goal:\\|^TcDebug\\|^</prompt>" nil t)
(when (looking-at "Goal")
(pg-goals-display (buffer-substring (point) pt2) nil))))))))
(pg-goals-display (buffer-substring (point) pt2) nil nil))))))))

;; overwrite the generic one, interactive prompt is Debug mode;; try to display
;; the debug goal in the goals buffer.
Expand Down Expand Up @@ -1943,8 +1962,11 @@ at `proof-assistant-settings-cmds' evaluation time.")
;; span menu
(setq proof-script-span-context-menu-extensions #'coq-create-span-menu)

(setq proof-shell-start-silent-cmd "Set Silent. "
proof-shell-stop-silent-cmd "Unset Silent. ")
;; When proof-shell-start-silent-cmd and proof-shell-stop-silent-cmd stay at
;; their default value nil, the generic code won't switch Coq to silent and
;; noisy at, respectively, the beginning and end of longer asserted regions.
;; (setq proof-shell-start-silent-cmd "Set Silent. "
;; proof-shell-stop-silent-cmd "Unset Silent. ")

;; prooftree config
(setq
Expand All @@ -1969,6 +1991,21 @@ at `proof-assistant-settings-cmds' evaluation time.")
)

(defun coq-shell-mode-config ()
"Initialization of `coq-shell-mode' that runs in the `*coq*' buffer.
The interaction buffer with Coq, `*coq*', uses a major mode that
is derived via `proof-shell-mode' from `scomint-mode'. This
function runs as the body of `coq-shell-mode' when the `*coq*'
buffer is initialized, which happens when the Coq background
process is started. This function intitalizes the Coq
personalization of Proof General in the interaction buffer with
Coq. At the end, this function calls `proof-shell-config-done',
which initializes the Coq session, e.g., by sending
`proof-shell-init-cmd', respectively, `coq-shell-init-cmd' to Coq.
In normal interaction, the proof assistant is started because the
user assert some commands. Therefore this function runs only
shortly before `proof-assert-command-hook', respectively,
`coq-adapt-printing-width'."
(setq
proof-shell-cd-cmd coq-shell-cd
proof-shell-filename-escapes '(("\\\\" . "\\\\") ("\"" . "\\\""))
Expand Down Expand Up @@ -3017,6 +3054,53 @@ buffer."
(add-hook 'proof-shell-handle-error-or-interrupt-hook #'coq-highlight-error-hook t)


(defun coq-show-goals-inside-proof (keep-response)
"Update goals buffer when action item list has been processed.
Add a Show command as priority action, such that it will still be
processed if the generic machinery inside `proof-shell-filter'
believes it has processed the last item from the action list.
When Coq runs in silent mode, we need to update the goals
precisely when everything else from the action list has been
processed.
The Show command is only added inside proofs and only if the last
processed command was not a show command from this function. The
action item flag `'coq-show-when-silent' is used for the latter.
KEEP-RESPONSE should be set if the last command produced some
error or response that should be kept and shown to the user. If
set, the flag `'keep-response' is added to the action item."
(when (and coq-last-but-one-proofstack
(not (member 'coq-show-when-silent
proof-shell-delayed-output-flags)))
(let* ((flags-1 (list 'coq-show-when-silent 'invisible 'empty-action-list))
(flags (if keep-response (cons 'keep-response flags-1) flags-1)))
(proof-add-to-priority-queue
(proof-shell-action-list-item "Show. " 'proof-done-invisible flags)))))

(defun coq-show-goals-on-error ()
"Update goals after error.
This function is intended for
`proof-shell-handle-error-or-interrupt-hook' to update the goals
buffer after an error has been detected. See also
`coq-show-goals-inside-proof'."
(coq-show-goals-inside-proof t))

(defun coq-show-goals-standard-case ()
"Update goals after last command when no error was detected.
This function is intended for
`proof-shell-handle-delayed-output-hook' to update the goals
buffer after the last command has been processed and no error has
been detected. Take care to keep the response buffer visible if
the last command was a Search, a Check or something similar. See
also `coq-show-goals-inside-proof'."
(coq-show-goals-inside-proof (eq proof-shell-last-output-kind 'response)))

(add-hook 'proof-shell-handle-error-or-interrupt-hook
#'coq-show-goals-on-error)
(add-hook 'proof-shell-handle-delayed-output-hook
#'coq-show-goals-standard-case)

;;
;; Scroll response buffer to maximize display of first goal
;;
Expand Down
5 changes: 5 additions & 0 deletions doc/PG-adapting.texi
Original file line number Diff line number Diff line change
Expand Up @@ -3888,8 +3888,13 @@ bother the user. They may include
@code{'no-response-display} do not display messages in @strong{response} buffer
@code{'no-error-display} do not display errors/take error action
@code{'no-goals-display} do not goals in @strong{goals} buffer
@code{'keep-response} do not erase the response buffer when goals are shown
@code{'proof-tree-show-subgoal} item inserted by the proof-tree package
@code{'priority-action} item added via @code{proof-add-to-priority-queue}
@code{'empty-action-list} @code{proof-shell-empty-action-list-command} should not be
called if this is the last item in the action list
@code{'coq-show-when-silent} Coq specific flag used for the final Show when
running completely silent.
@end lisp
Note that @code{'invisible} does not imply any of the others. If flags
are non-empty, interactive cues will be surpressed. (E.g.,
Expand Down
17 changes: 13 additions & 4 deletions generic/pg-goals.el
Original file line number Diff line number Diff line change
Expand Up @@ -79,7 +79,7 @@ May enable proof-by-pointing or similar features.
;;
;; Goals buffer processing
;;
(defun pg-goals-display (string keepresponse)
(defun pg-goals-display (string keepresponse nodisplay)
"Display STRING in the `proof-goals-buffer', properly marked up.
Converts term substructure markup into mouse-highlighted extents.
Expand All @@ -90,7 +90,13 @@ function tries to do that by calling `pg-response-maybe-erase'.
If KEEPRESPONSE is non-nil, we assume that a response message
corresponding to this goals message has already been displayed
before this goals message (see `proof-shell-handle-delayed-output'),
so the response buffer should not be cleared."
so the response buffer should not be cleared.
IF NODISPLAY is non-nil, do not display the goals buffer in some
window (but the goals buffer is updated as described above and
any window currently showing it will keep it). In two-pane mode,
NODISPLAY has the effect that the goals are updated but the
response buffer is displayed."
;; Response buffer may be out of date. It may contain (error)
;; messages relating to earlier proof states

Expand All @@ -114,8 +120,11 @@ so the response buffer should not be cleared."
(set-buffer-modified-p nil)

;; Keep point at the start of the buffer.
(proof-display-and-keep-buffer
proof-goals-buffer (point-min))))
;; (For Coq, somebody sets point to the conclusion in the goal, so the
;; position argument in proof-display-and-keep-buffer has no effect.)
(unless nodisplay
(proof-display-and-keep-buffer
proof-goals-buffer (point-min)))))

;;
;; Actions in the goals buffer
Expand Down
Loading

0 comments on commit e2c661d

Please sign in to comment.