From 8e12eee54e36ca16d4b4530e1509479f22929e4f Mon Sep 17 00:00:00 2001 From: Cyril Anaclet Date: Mon, 11 May 2020 15:00:47 +0200 Subject: [PATCH 01/13] First try for feature #487 --- coq/coq-abbrev.el | 9 +++++++-- coq/coq-compile-common.el | 10 ++++++++++ coq/coq-showdiff.el | 12 ++++++++++++ coq/coq.el | 9 ++++++++- 4 files changed, 37 insertions(+), 3 deletions(-) create mode 100644 coq/coq-showdiff.el diff --git a/coq/coq-abbrev.el b/coq/coq-abbrev.el index bd898a9c2..4d2c82875 100644 --- a/coq/coq-abbrev.el +++ b/coq/coq-abbrev.el @@ -78,7 +78,7 @@ ;; Common part (script, response and goals buffers) (defconst coq-menu-common-entries `( - ["Toggle 3 Windows Mode" proof-three-window-toggle + ["Toggle 3 Windows Mode" proof-three-window-toggle :style toggle :selected proof-three-window-enable :help "Toggles the use of separate windows or frames for Coq responses and goals." @@ -243,7 +243,7 @@ :active (and coq-compile-before-require coq-compile-parallel-in-background) :help "Abort background compilation and kill all compilation processes."]) - ("Diffs" + ("Diffs" ["off" (customize-set-variable 'coq-diffs 'off) :style radio @@ -259,6 +259,11 @@ :style radio :selected (eq coq-diffs 'removed) :help "Show diffs: added and removed"]) + ["Show proof diffs" + coq-show-proof-toggle + :style toggle + :selected coq-show-proof + :help "Show the proof diffs in the response buffer"] ("\"Proof using\" mode..." ["ask" (customize-set-variable 'coq-accept-proof-using-suggestion 'ask) diff --git a/coq/coq-compile-common.el b/coq/coq-compile-common.el index f9a3571e0..2a5c3f445 100644 --- a/coq/coq-compile-common.el +++ b/coq/coq-compile-common.el @@ -458,6 +458,16 @@ This option can be set via menu ;; define coq-lock-ancestors-toggle (proof-deftoggle coq-lock-ancestors) +;; Maybe not the good place +(defcustom coq-show-proof nil + "TODO: doc" + + :type 'boolean + :safe 'booleanp + :group 'coq-auto-compile) + +(proof-deftoggle coq-show-proof) + (defcustom coq-confirm-external-compilation t "If set let user change and confirm the compilation command. Otherwise start the external compilation without confirmation. diff --git a/coq/coq-showdiff.el b/coq/coq-showdiff.el new file mode 100644 index 000000000..f42431af2 --- /dev/null +++ b/coq/coq-showdiff.el @@ -0,0 +1,12 @@ +;; Temporary file, just for test +(defun coq-show-proof-fun () + (interactive) + ;; TODO: Check if we are in a proof + (when coq-show-proof + (when (eq coq-diffs 'off) + (proof-shell-invisible-command "Show Proof." )) + (when (eq coq-diffs 'on) + (proof-shell-invisible-command "Show Proof Diffs.")) + (when (eq coq-diffs 'removed) + (proof-shell-invisible-command "Show Proof Diffs removed."))) + ) \ No newline at end of file diff --git a/coq/coq.el b/coq/coq.el index 71112fc1b..8ebf3054c 100644 --- a/coq/coq.el +++ b/coq/coq.el @@ -1222,7 +1222,14 @@ be called and no command will be sent to Coq." (string-match-p "BackTo\\s-" cmd)) (if (coq--post-v810) (list "Unset Silent." (coq-diffs)) - (list "Unset Silent."))))) + (list "Unset Silent."))) + ((or + ;; 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) + (when coq-show-proof + (list "Show Proof." "Show."))))))) + (defpacustom auto-adapt-printing-width t "If non-nil, adapt automatically printing width of goals window. From ecb47478c9f9959ea25ce509076f6e3959d2c620 Mon Sep 17 00:00:00 2001 From: Cyril Anaclet Date: Thu, 14 May 2020 15:29:58 +0200 Subject: [PATCH 02/13] All case for Show and regex variable --- coq/coq-syntax.el | 3 +++ coq/coq.el | 21 ++++++++++++++++++--- generic/proof-config.el | 5 +++++ generic/proof-shell.el | 7 +++++-- 4 files changed, 31 insertions(+), 5 deletions(-) diff --git a/coq/coq-syntax.el b/coq/coq-syntax.el index 470331a69..e486997d3 100644 --- a/coq/coq-syntax.el +++ b/coq/coq-syntax.el @@ -1304,6 +1304,9 @@ It is used: "*Font-lock table for Coq terms.") +(defconst coq-show-diffs-regexp + "Show Proof\\(\\.\\| Diffs\\.\\| Diffs removed\\.\\)") + (defconst coq-save-command-regexp ;; FIXME: The surrounding grouping parens are probably not needed. (concat "\\`\\(\\(?:Time\\s-+\\|Timeout\\s-+[[:digit:]]+\\s-+\\)*\\_<" diff --git a/coq/coq.el b/coq/coq.el index 8ebf3054c..65ff488f3 100644 --- a/coq/coq.el +++ b/coq/coq.el @@ -1208,14 +1208,27 @@ be called and no command will be sent to Coq." ;; If user issued a printing option then t printing. (and (string-match-p "\\(S\\|Uns\\)et\\s-+Printing" cmd) (> (length coq-last-but-one-proofstack) 0))) - (list "Show.")) + (if coq-show-proof + (or + (when (eq coq-diffs 'off) (list "Show." "Show Proof." )) + (when (eq coq-diffs 'on) (list "Show." "Show Proof Diffs.")) + (when (eq coq-diffs 'removed) (list "Show." "Show Proof Diffs removed."))) + (list "Show."))) ((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 (and (string-match-p "BackTo\\s-" cmd) (> (length coq-last-but-one-proofstack) coq--retract-naborts))) ;; "Set Diffs" always re-prints the proof context with (if enabled) diffs - (list "Unset Silent." (if (coq--post-v810) (coq-diffs) "Show."))) + (list "Unset Silent." (if (coq--post-v810) (coq-diffs) + (if coq-show-proof + ((when (eq coq-diffs 'off) + "Show." "Show Proof." ) + (when (eq coq-diffs 'on) + "Show." "Show Proof Diffs.") + (when (eq coq-diffs 'removed) + "Show." "Show Proof Diffs removed.")) + "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). Still, we need to "Set Diffs" again @@ -1228,7 +1241,7 @@ be called and no command will be sent to Coq." (and (not (string-match-p coq-save-command-regexp-strict cmd)) (> (length coq-last-but-one-proofstack) 0) (when coq-show-proof - (list "Show Proof." "Show."))))))) + (list "Show." "Show Proof."))))))) (defpacustom auto-adapt-printing-width t @@ -1897,6 +1910,8 @@ at `proof-assistant-settings-cmds' evaluation time.") proof-save-command "Save %s. " proof-find-theorems-command "Search %s. ") + (setq proof-show-diffs-regexp coq-show-diffs-regexp) + (setq proof-shell-empty-action-list-command 'coq-empty-action-list-command) ;; FIXME da: Does Coq have a help or about command? diff --git a/generic/proof-config.el b/generic/proof-config.el index 8d5391910..16cdae93f 100644 --- a/generic/proof-config.el +++ b/generic/proof-config.el @@ -399,6 +399,11 @@ NB: This setting is not used for matching output from the prover." :type 'regexp :group 'proof-script) +(defcustom proof-show-diffs-regexp nil + "Matches all Show Proof form" + :type 'regexp + :group 'proof-script) + (defcustom proof-save-with-hole-regexp nil "Regexp which matches a command to save a named theorem. The name of the theorem is built from the variable diff --git a/generic/proof-shell.el b/generic/proof-shell.el index a0e80fa70..b6bf9225c 100644 --- a/generic/proof-shell.el +++ b/generic/proof-shell.el @@ -1615,9 +1615,12 @@ by the filter is to send the next command from the queue." (setq proof-shell-delayed-output-end end) (setq proof-shell-delayed-output-flags flags) (if (proof-shell-exec-loop) - (setq proof-shell-last-output-kind + ;; (if (and (string-match proof-show-diffs-regexp (car cmd)) + ;; (memq 'empty-action-list flags)) + ;; (setq proof-shell-last-output-kind 'response) ;; only display result for last output - (proof-shell-handle-delayed-output))) + (setq proof-shell-last-output-kind (proof-shell-handle-delayed-output))) + ;; ;; send output to the proof tree visualizer (if proof-tree-external-display (proof-tree-handle-delayed-output old-proof-marker cmd flags span))))) From aba3f2bfe2bffde6d2df21b098740100459a84be Mon Sep 17 00:00:00 2001 From: Erik Martin-Dorel Date: Fri, 15 May 2020 15:50:48 +0200 Subject: [PATCH 03/13] Fix name clash & rephrase some strings --- coq/coq-abbrev.el | 8 ++++---- coq/coq-compile-common.el | 4 ++-- coq/coq-showdiff.el | 4 ++-- coq/coq-syntax.el | 3 ++- coq/coq.el | 8 ++++---- generic/proof-config.el | 2 +- 6 files changed, 15 insertions(+), 14 deletions(-) diff --git a/coq/coq-abbrev.el b/coq/coq-abbrev.el index 4d2c82875..74ddb0769 100644 --- a/coq/coq-abbrev.el +++ b/coq/coq-abbrev.el @@ -259,11 +259,11 @@ :style radio :selected (eq coq-diffs 'removed) :help "Show diffs: added and removed"]) - ["Show proof diffs" - coq-show-proof-toggle + ["Show Proof (Diffs)" + coq-show-proof-stepwise-toggle :style toggle - :selected coq-show-proof - :help "Show the proof diffs in the response buffer"] + :selected coq-show-proof-stepwise + :help "Display the proof terms stepwise in the *response* buffer."] ("\"Proof using\" mode..." ["ask" (customize-set-variable 'coq-accept-proof-using-suggestion 'ask) diff --git a/coq/coq-compile-common.el b/coq/coq-compile-common.el index 2a5c3f445..fdb3d4b80 100644 --- a/coq/coq-compile-common.el +++ b/coq/coq-compile-common.el @@ -459,14 +459,14 @@ This option can be set via menu (proof-deftoggle coq-lock-ancestors) ;; Maybe not the good place -(defcustom coq-show-proof nil +(defcustom coq-show-proof-stepwise nil "TODO: doc" :type 'boolean :safe 'booleanp :group 'coq-auto-compile) -(proof-deftoggle coq-show-proof) +(proof-deftoggle coq-show-proof-stepwise) (defcustom coq-confirm-external-compilation t "If set let user change and confirm the compilation command. diff --git a/coq/coq-showdiff.el b/coq/coq-showdiff.el index f42431af2..0daf98f8d 100644 --- a/coq/coq-showdiff.el +++ b/coq/coq-showdiff.el @@ -2,11 +2,11 @@ (defun coq-show-proof-fun () (interactive) ;; TODO: Check if we are in a proof - (when coq-show-proof + (when coq-show-proof-stepwise (when (eq coq-diffs 'off) (proof-shell-invisible-command "Show Proof." )) (when (eq coq-diffs 'on) (proof-shell-invisible-command "Show Proof Diffs.")) (when (eq coq-diffs 'removed) (proof-shell-invisible-command "Show Proof Diffs removed."))) - ) \ No newline at end of file + ) diff --git a/coq/coq-syntax.el b/coq/coq-syntax.el index e486997d3..a27274c5d 100644 --- a/coq/coq-syntax.el +++ b/coq/coq-syntax.el @@ -1304,7 +1304,8 @@ It is used: "*Font-lock table for Coq terms.") -(defconst coq-show-diffs-regexp +(defconst coq-show-proof-diffs-regexp + ;; FIXME/TODO: enhance this regexp "Show Proof\\(\\.\\| Diffs\\.\\| Diffs removed\\.\\)") (defconst coq-save-command-regexp diff --git a/coq/coq.el b/coq/coq.el index 65ff488f3..b833765fa 100644 --- a/coq/coq.el +++ b/coq/coq.el @@ -1208,7 +1208,7 @@ be called and no command will be sent to Coq." ;; If user issued a printing option then t printing. (and (string-match-p "\\(S\\|Uns\\)et\\s-+Printing" cmd) (> (length coq-last-but-one-proofstack) 0))) - (if coq-show-proof + (if coq-show-proof-stepwise (or (when (eq coq-diffs 'off) (list "Show." "Show Proof." )) (when (eq coq-diffs 'on) (list "Show." "Show Proof Diffs.")) @@ -1221,7 +1221,7 @@ be called and no command will be sent to Coq." (> (length coq-last-but-one-proofstack) coq--retract-naborts))) ;; "Set Diffs" always re-prints the proof context with (if enabled) diffs (list "Unset Silent." (if (coq--post-v810) (coq-diffs) - (if coq-show-proof + (if coq-show-proof-stepwise ((when (eq coq-diffs 'off) "Show." "Show Proof." ) (when (eq coq-diffs 'on) @@ -1240,7 +1240,7 @@ be called and no command will be sent to Coq." ;; 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) - (when coq-show-proof + (when coq-show-proof-stepwise (list "Show." "Show Proof."))))))) @@ -1910,7 +1910,7 @@ at `proof-assistant-settings-cmds' evaluation time.") proof-save-command "Save %s. " proof-find-theorems-command "Search %s. ") - (setq proof-show-diffs-regexp coq-show-diffs-regexp) + (setq proof-show-proof-diffs-regexp coq-show-proof-diffs-regexp) (setq proof-shell-empty-action-list-command 'coq-empty-action-list-command) diff --git a/generic/proof-config.el b/generic/proof-config.el index 16cdae93f..ce72c76c6 100644 --- a/generic/proof-config.el +++ b/generic/proof-config.el @@ -399,7 +399,7 @@ NB: This setting is not used for matching output from the prover." :type 'regexp :group 'proof-script) -(defcustom proof-show-diffs-regexp nil +(defcustom proof-show-proof-diffs-regexp nil "Matches all Show Proof form" :type 'regexp :group 'proof-script) From 04aff704f3d13452bc5c52ff860c5ab564539632 Mon Sep 17 00:00:00 2001 From: Cyril Anaclet Date: Mon, 18 May 2020 13:33:57 +0200 Subject: [PATCH 04/13] WIP for #487 --- coq/coq-syntax.el | 3 +-- generic/proof-shell.el | 7 ++++--- 2 files changed, 5 insertions(+), 5 deletions(-) diff --git a/coq/coq-syntax.el b/coq/coq-syntax.el index a27274c5d..3ae7fbca0 100644 --- a/coq/coq-syntax.el +++ b/coq/coq-syntax.el @@ -1305,8 +1305,7 @@ It is used: (defconst coq-show-proof-diffs-regexp - ;; FIXME/TODO: enhance this regexp - "Show Proof\\(\\.\\| Diffs\\.\\| Diffs removed\\.\\)") + "^[ ]*Show Proof\\( Diffs\\| Diffs removed\\)?\\.$") (defconst coq-save-command-regexp ;; FIXME: The surrounding grouping parens are probably not needed. diff --git a/generic/proof-shell.el b/generic/proof-shell.el index b6bf9225c..8f23608af 100644 --- a/generic/proof-shell.el +++ b/generic/proof-shell.el @@ -1126,7 +1126,7 @@ contains only invisible elements for Prooftree synchronization." ;; but we delay this until sending the next command, attempting ;; to parallelize prover and Emacs somewhat. (PG 4.0 change) - (setq proof-action-list (cdr proof-action-list)) + (setq proof-action-list (cdr proof-action-list)) (setq cbitems (cons item (proof-shell-slurp-comments))) @@ -1193,7 +1193,8 @@ contains only invisible elements for Prooftree synchronization." (or (null proof-action-list) (cl-every (lambda (item) (memq 'proof-tree-show-subgoal (nth 3 item))) - proof-action-list))))))) + proof-action-list) + (string= (car (nth 1 item)) "Show."))))))) (defun proof-shell-insert-loopback-cmd (cmd) @@ -1715,7 +1716,7 @@ i.e., 'goals or 'response." (buffer-substring-no-properties rstart gmark))) ;; display goals output second so it persists in 2-pane mode (unless (memq 'no-goals-display flags) - (pg-goals-display proof-shell-last-goals-output both)) + (pg-goals-display proof-shell-last-goals-output t)) ;; indicate a goals output has been given 'goals)) From 22681a3caf2c8f45700585ea74dffbf48bb2ac19 Mon Sep 17 00:00:00 2001 From: Cyril Anaclet Date: Wed, 20 May 2020 14:19:14 +0200 Subject: [PATCH 05/13] Apply reviews of @erikmd --- coq/coq-compile-common.el | 8 ------- coq/coq-showdiff.el | 12 ----------- coq/coq-syntax.el | 2 +- coq/coq.el | 44 +++++++++++++++++++++++++-------------- generic/proof-config.el | 2 +- generic/proof-shell.el | 14 ++++++------- 6 files changed, 36 insertions(+), 46 deletions(-) delete mode 100644 coq/coq-showdiff.el diff --git a/coq/coq-compile-common.el b/coq/coq-compile-common.el index fdb3d4b80..938f706e6 100644 --- a/coq/coq-compile-common.el +++ b/coq/coq-compile-common.el @@ -458,14 +458,6 @@ This option can be set via menu ;; define coq-lock-ancestors-toggle (proof-deftoggle coq-lock-ancestors) -;; Maybe not the good place -(defcustom coq-show-proof-stepwise nil - "TODO: doc" - - :type 'boolean - :safe 'booleanp - :group 'coq-auto-compile) - (proof-deftoggle coq-show-proof-stepwise) (defcustom coq-confirm-external-compilation t diff --git a/coq/coq-showdiff.el b/coq/coq-showdiff.el deleted file mode 100644 index 0daf98f8d..000000000 --- a/coq/coq-showdiff.el +++ /dev/null @@ -1,12 +0,0 @@ -;; Temporary file, just for test -(defun coq-show-proof-fun () - (interactive) - ;; TODO: Check if we are in a proof - (when coq-show-proof-stepwise - (when (eq coq-diffs 'off) - (proof-shell-invisible-command "Show Proof." )) - (when (eq coq-diffs 'on) - (proof-shell-invisible-command "Show Proof Diffs.")) - (when (eq coq-diffs 'removed) - (proof-shell-invisible-command "Show Proof Diffs removed."))) - ) diff --git a/coq/coq-syntax.el b/coq/coq-syntax.el index 3ae7fbca0..47869aed5 100644 --- a/coq/coq-syntax.el +++ b/coq/coq-syntax.el @@ -1305,7 +1305,7 @@ It is used: (defconst coq-show-proof-diffs-regexp - "^[ ]*Show Proof\\( Diffs\\| Diffs removed\\)?\\.$") + "\\bShow Proof\\(?: Diffs\\| Diffs removed\\)?\\.\\b") (defconst coq-save-command-regexp ;; FIXME: The surrounding grouping parens are probably not needed. diff --git a/coq/coq.el b/coq/coq.el index b833765fa..942e85fe7 100644 --- a/coq/coq.el +++ b/coq/coq.el @@ -160,6 +160,16 @@ See also option `coq-hide-additional-subgoals'." :type '(choice regexp (const nil)) :group 'coq) +(defcustom coq-show-proof-stepwise nil + "Display the proof terms stepwise in the *response* buffer. + This option can be combined with option `coq-diffs'. + It is mostly useful in three window mode, see also + `proof-three-window-mode-policy' for details." + + :type 'boolean + :safe 'booleanp + :group 'coq-auto-compile) + ;; ;; prooftree customization ;; @@ -1208,40 +1218,42 @@ be called and no command will be sent to Coq." ;; If user issued a printing option then t printing. (and (string-match-p "\\(S\\|Uns\\)et\\s-+Printing" cmd) (> (length coq-last-but-one-proofstack) 0))) - (if coq-show-proof-stepwise + (list "Show." + (when coq-show-proof-stepwise (or - (when (eq coq-diffs 'off) (list "Show." "Show Proof." )) - (when (eq coq-diffs 'on) (list "Show." "Show Proof Diffs.")) - (when (eq coq-diffs 'removed) (list "Show." "Show Proof Diffs removed."))) - (list "Show."))) + (when (eq coq-diffs 'off) "Show Proof.") + (when (eq coq-diffs 'on) "Show Proof Diffs.") + (when (eq coq-diffs 'removed) "Show Proof Diffs removed."))))) + ((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 (and (string-match-p "BackTo\\s-" cmd) (> (length coq-last-but-one-proofstack) coq--retract-naborts))) ;; "Set Diffs" always re-prints the proof context with (if enabled) diffs - (list "Unset Silent." (if (coq--post-v810) (coq-diffs) - (if coq-show-proof-stepwise - ((when (eq coq-diffs 'off) - "Show." "Show Proof." ) - (when (eq coq-diffs 'on) - "Show." "Show Proof Diffs.") - (when (eq coq-diffs 'removed) - "Show." "Show Proof Diffs removed.")) - "Show.")))) + (list "Unset Silent." (if (coq--post-v810) (coq-diffs) "Show.") + (when coq-show-proof-stepwise + (or + (when (eq coq-diffs 'off) "Show Proof.") + (when (eq coq-diffs 'on) "Show Proof Diffs.") + (when (eq coq-diffs 'removed) "Show Proof Diffs removed."))))) + ((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 (string-match-p "BackTo\\s-" cmd)) (if (coq--post-v810) - (list "Unset Silent." (coq-diffs)) + (list "Unset Silent." (coq-diffs) ) (list "Unset Silent."))) ((or ;; 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) (when coq-show-proof-stepwise - (list "Show." "Show Proof."))))))) + (or + (when (eq coq-diffs 'off) (list "Show Proof." )) + (when (eq coq-diffs 'on) (list "Show Proof Diffs.")) + (when (eq coq-diffs 'removed) (list "Show Proof Diffs removed."))))))))) (defpacustom auto-adapt-printing-width t diff --git a/generic/proof-config.el b/generic/proof-config.el index ce72c76c6..9d3525489 100644 --- a/generic/proof-config.el +++ b/generic/proof-config.el @@ -400,7 +400,7 @@ NB: This setting is not used for matching output from the prover." :group 'proof-script) (defcustom proof-show-proof-diffs-regexp nil - "Matches all Show Proof form" + "Matches all \"Show Proof\" forms (specific to the Coq prover)." :type 'regexp :group 'proof-script) diff --git a/generic/proof-shell.el b/generic/proof-shell.el index 8f23608af..1258c7f69 100644 --- a/generic/proof-shell.el +++ b/generic/proof-shell.el @@ -1126,7 +1126,7 @@ contains only invisible elements for Prooftree synchronization." ;; but we delay this until sending the next command, attempting ;; to parallelize prover and Emacs somewhat. (PG 4.0 change) - (setq proof-action-list (cdr proof-action-list)) + (setq proof-action-list (cdr proof-action-list)) (setq cbitems (cons item (proof-shell-slurp-comments))) @@ -1194,7 +1194,8 @@ contains only invisible elements for Prooftree synchronization." (cl-every (lambda (item) (memq 'proof-tree-show-subgoal (nth 3 item))) proof-action-list) - (string= (car (nth 1 item)) "Show."))))))) + ;; If the last command in proof-action-list is a "Show Proof" form then return t + (string-match-p proof-show-proof-diffs-regexp (car (nth 1 (car (last proof-action-list))))))))))) (defun proof-shell-insert-loopback-cmd (cmd) @@ -1616,12 +1617,9 @@ by the filter is to send the next command from the queue." (setq proof-shell-delayed-output-end end) (setq proof-shell-delayed-output-flags flags) (if (proof-shell-exec-loop) - ;; (if (and (string-match proof-show-diffs-regexp (car cmd)) - ;; (memq 'empty-action-list flags)) - ;; (setq proof-shell-last-output-kind 'response) + (setq proof-shell-last-output-kind ;; only display result for last output - (setq proof-shell-last-output-kind (proof-shell-handle-delayed-output))) - ;; + (proof-shell-handle-delayed-output))) ;; send output to the proof tree visualizer (if proof-tree-external-display (proof-tree-handle-delayed-output old-proof-marker cmd flags span))))) @@ -1716,7 +1714,7 @@ i.e., 'goals or 'response." (buffer-substring-no-properties rstart gmark))) ;; display goals output second so it persists in 2-pane mode (unless (memq 'no-goals-display flags) - (pg-goals-display proof-shell-last-goals-output t)) + (pg-goals-display proof-shell-last-goals-output both)) ;; indicate a goals output has been given 'goals)) From ff9b5b11b4266b9260b74d772ae2e5848221f6f8 Mon Sep 17 00:00:00 2001 From: Erik Martin-Dorel Date: Wed, 20 May 2020 21:11:27 +0200 Subject: [PATCH 06/13] test: Add regression test (currently failing) --- ci/coq-tests.el | 11 +++++++++++ 1 file changed, 11 insertions(+) diff --git a/ci/coq-tests.el b/ci/coq-tests.el index 1a2815212..cc60f8a0a 100644 --- a/ci/coq-tests.el +++ b/ci/coq-tests.el @@ -189,6 +189,17 @@ For example, COMMENT could be (*test-definition*)" (coq-should-response "trois is defined")))) +(ert-deftest 021_coq-test-regression-goto-point () + "Regression test for proof-goto-point after a comment, PR #90" + (coq-fixture-on-file + (coq-test-full-path "test_stepwise.v") + (lambda () + (coq-test-goto-after "(*test-definition*)") + (proof-goto-point) + (proof-shell-wait) + t))) + + (ert-deftest 030_coq-test-position () "Test locked region after Qed." (coq-fixture-on-file From 411ebb27fda4d39fc22baf341dcdde2341632b8d Mon Sep 17 00:00:00 2001 From: Erik Martin-Dorel Date: Wed, 20 May 2020 21:48:20 +0200 Subject: [PATCH 07/13] =?UTF-8?q?fix:=20Do=20"Show=20Proof=E2=80=A6"=20(wi?= =?UTF-8?q?th=20"=3FGoal")=20as=20soon=20as=20the=20proof=20is=20started?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- coq/coq.el | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/coq/coq.el b/coq/coq.el index 942e85fe7..10aa07bf9 100644 --- a/coq/coq.el +++ b/coq/coq.el @@ -1246,14 +1246,16 @@ be called and no command will be sent to Coq." (list "Unset Silent." (coq-diffs) ) (list "Unset Silent."))) ((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) + (> (length coq-last-but-one-proofstack) 0))) (when coq-show-proof-stepwise (or (when (eq coq-diffs 'off) (list "Show Proof." )) (when (eq coq-diffs 'on) (list "Show Proof Diffs.")) - (when (eq coq-diffs 'removed) (list "Show Proof Diffs removed."))))))))) + (when (eq coq-diffs 'removed) (list "Show Proof Diffs removed."))))))) (defpacustom auto-adapt-printing-width t From 3ab3f5efbbb724cb2e4aebc3c4d7bfdce4008896 Mon Sep 17 00:00:00 2001 From: Anaclet Date: Mon, 25 May 2020 10:55:03 +0200 Subject: [PATCH 08/13] fix: backtrack wrong type argument --- coq/coq-syntax.el | 2 +- coq/coq.el | 40 +++++++++++++++++++++------------------- generic/proof-shell.el | 30 ++++++++++++++++-------------- 3 files changed, 38 insertions(+), 34 deletions(-) diff --git a/coq/coq-syntax.el b/coq/coq-syntax.el index 47869aed5..5b8d8c48c 100644 --- a/coq/coq-syntax.el +++ b/coq/coq-syntax.el @@ -1305,7 +1305,7 @@ It is used: (defconst coq-show-proof-diffs-regexp - "\\bShow Proof\\(?: Diffs\\| Diffs removed\\)?\\.\\b") + "\\`Show Proof\\(?: Diffs\\| Diffs removed\\)?\\.\\'") (defconst coq-save-command-regexp ;; FIXME: The surrounding grouping parens are probably not needed. diff --git a/coq/coq.el b/coq/coq.el index 10aa07bf9..9fc6e2005 100644 --- a/coq/coq.el +++ b/coq/coq.el @@ -162,9 +162,9 @@ See also option `coq-hide-additional-subgoals'." (defcustom coq-show-proof-stepwise nil "Display the proof terms stepwise in the *response* buffer. - This option can be combined with option `coq-diffs'. - It is mostly useful in three window mode, see also - `proof-three-window-mode-policy' for details." +This option can be combined with option `coq-diffs'. +It is mostly useful in three window mode, see also +`proof-three-window-mode-policy' for details." :type 'boolean :safe 'booleanp @@ -1209,7 +1209,9 @@ Printing All set." "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." +be called and no command will be sent to Coq. +Note: the last command added if `coq-show-proof-stepwise' is set +should match the `coq-show-proof-diffs-regexp'." (cond ((or ;; If closing a nested proof, Show the enclosing goal. @@ -1219,11 +1221,11 @@ be called and no command will be sent to Coq." (and (string-match-p "\\(S\\|Uns\\)et\\s-+Printing" cmd) (> (length coq-last-but-one-proofstack) 0))) (list "Show." - (when coq-show-proof-stepwise - (or - (when (eq coq-diffs 'off) "Show Proof.") - (when (eq coq-diffs 'on) "Show Proof Diffs.") - (when (eq coq-diffs 'removed) "Show Proof Diffs removed."))))) + (when coq-show-proof-stepwise + (or + (when (eq coq-diffs 'off) "Show Proof.") + (when (eq coq-diffs 'on) "Show Proof Diffs.") + (when (eq coq-diffs 'removed) "Show Proof Diffs removed."))))) ((or ;; If we go back in the buffer and the number of abort is less than @@ -1232,11 +1234,11 @@ be called and no command will be sent to Coq." (> (length coq-last-but-one-proofstack) coq--retract-naborts))) ;; "Set Diffs" always re-prints the proof context with (if enabled) diffs (list "Unset Silent." (if (coq--post-v810) (coq-diffs) "Show.") - (when coq-show-proof-stepwise - (or - (when (eq coq-diffs 'off) "Show Proof.") - (when (eq coq-diffs 'on) "Show Proof Diffs.") - (when (eq coq-diffs 'removed) "Show Proof Diffs removed."))))) + (when coq-show-proof-stepwise + (or + (when (eq coq-diffs 'off) "Show Proof.") + (when (eq coq-diffs 'on) "Show Proof Diffs.") + (when (eq coq-diffs 'removed) "Show Proof Diffs removed."))))) ((or ;; If we go back in the buffer and not in the above case, then only Unset @@ -1251,11 +1253,11 @@ be called and no command will be sent to Coq." ;; 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))) - (when coq-show-proof-stepwise - (or - (when (eq coq-diffs 'off) (list "Show Proof." )) - (when (eq coq-diffs 'on) (list "Show Proof Diffs.")) - (when (eq coq-diffs 'removed) (list "Show Proof Diffs removed."))))))) + (when coq-show-proof-stepwise + (or + (when (eq coq-diffs 'off) (list "Show Proof." )) + (when (eq coq-diffs 'on) (list "Show Proof Diffs.")) + (when (eq coq-diffs 'removed) (list "Show Proof Diffs removed."))))))) (defpacustom auto-adapt-printing-width t diff --git a/generic/proof-shell.el b/generic/proof-shell.el index 1258c7f69..9e51d4fb3 100644 --- a/generic/proof-shell.el +++ b/generic/proof-shell.el @@ -1181,21 +1181,23 @@ contains only invisible elements for Prooftree synchronization." ;; process the delayed callbacks now (mapc 'proof-shell-invoke-callback cbitems) - (unless (or proof-action-list proof-second-action-list-active) + (unless (or proof-action-list proof-second-action-list-active) ; release lock, cleanup - (proof-release-lock) - (proof-detach-queue) - (unless flags ; hint after a batch of scripting - (pg-processing-complete-hint)) - (pg-finish-tracing-display)) - - (and (not proof-second-action-list-active) - (or (null proof-action-list) - (cl-every - (lambda (item) (memq 'proof-tree-show-subgoal (nth 3 item))) - proof-action-list) - ;; If the last command in proof-action-list is a "Show Proof" form then return t - (string-match-p proof-show-proof-diffs-regexp (car (nth 1 (car (last proof-action-list))))))))))) + (proof-release-lock) + (proof-detach-queue) + (unless flags ; hint after a batch of scripting + (pg-processing-complete-hint)) + (pg-finish-tracing-display)) + + + (and (not proof-second-action-list-active) + (let ((last-command (car (nth 1 (car (last proof-action-list)))))) + (or (null proof-action-list) + (cl-every + (lambda (item) (memq 'proof-tree-show-subgoal (nth 3 item))) + proof-action-list) + ;; If the last command in proof-action-list is a "Show Proof" form then return t + (when last-command (string-match-p proof-show-proof-diffs-regexp last-command))))))))) (defun proof-shell-insert-loopback-cmd (cmd) From 8627fba2a20e42432de441391db2f35e3c48a952 Mon Sep 17 00:00:00 2001 From: Anaclet Date: Thu, 28 May 2020 09:21:53 +0200 Subject: [PATCH 09/13] fix: backtrack for "Show Proof" disabled --- coq/coq.el | 44 +++++++++++++++++++++++++++++------------- generic/proof-shell.el | 43 ++++++++++++++++++++--------------------- 2 files changed, 52 insertions(+), 35 deletions(-) diff --git a/coq/coq.el b/coq/coq.el index 9fc6e2005..df7c5a668 100644 --- a/coq/coq.el +++ b/coq/coq.el @@ -1220,12 +1220,17 @@ should match the `coq-show-proof-diffs-regexp'." ;; If user issued a printing option then t printing. (and (string-match-p "\\(S\\|Uns\\)et\\s-+Printing" cmd) (> (length coq-last-but-one-proofstack) 0))) - (list "Show." - (when coq-show-proof-stepwise - (or - (when (eq coq-diffs 'off) "Show Proof.") - (when (eq coq-diffs 'on) "Show Proof Diffs.") - (when (eq coq-diffs 'removed) "Show Proof Diffs removed."))))) + (let ((showlist (list "Show."))) + (when coq-show-proof-stepwise + (add-to-list 'showlist + (if (coq--post-v811) + (or + (when (eq coq-diffs 'off) "Show Proof.") + (when (eq coq-diffs 'on) "Show Proof Diffs.") + (when (eq coq-diffs 'removed) "Show Proof Diffs removed.")) + "Show Proof.") + t)) + showlist)) ((or ;; If we go back in the buffer and the number of abort is less than @@ -1233,12 +1238,23 @@ should match the `coq-show-proof-diffs-regexp'." (and (string-match-p "BackTo\\s-" cmd) (> (length coq-last-but-one-proofstack) coq--retract-naborts))) ;; "Set Diffs" always re-prints the proof context with (if enabled) diffs - (list "Unset Silent." (if (coq--post-v810) (coq-diffs) "Show.") - (when coq-show-proof-stepwise - (or - (when (eq coq-diffs 'off) "Show Proof.") - (when (eq coq-diffs 'on) "Show Proof Diffs.") - (when (eq coq-diffs 'removed) "Show Proof Diffs removed."))))) + ;; (list "Unset Silent." (if (coq--post-v810) (coq-diffs) "Show.") + ;; (when coq-show-proof-stepwise + ;; (or + ;; (when (eq coq-diffs 'off) "Show Proof.") + ;; (when (eq coq-diffs 'on) "Show Proof Diffs.") + ;; (when (eq coq-diffs 'removed) "Show Proof Diffs removed."))))) + (let ((showlist (list "Unset Silent." (if (coq--post-v810) (coq-diffs) "Show.")))) + (when coq-show-proof-stepwise + (add-to-list 'showlist + (if (coq--post-v811) + (or + (when (eq coq-diffs 'off) "Show Proof.") + (when (eq coq-diffs 'on) "Show Proof Diffs." ) + (when (eq coq-diffs 'removed) "Show Proof Diffs removed.")) + "Show Proof.") + t)) + showlist)) ((or ;; If we go back in the buffer and not in the above case, then only Unset @@ -1254,10 +1270,12 @@ should match the `coq-show-proof-diffs-regexp'." (and (not (string-match-p coq-save-command-regexp-strict cmd)) (> (length coq-last-but-one-proofstack) 0))) (when coq-show-proof-stepwise + (if (coq--post-v811) (or (when (eq coq-diffs 'off) (list "Show Proof." )) (when (eq coq-diffs 'on) (list "Show Proof Diffs.")) - (when (eq coq-diffs 'removed) (list "Show Proof Diffs removed."))))))) + (when (eq coq-diffs 'removed) (list "Show Proof Diffs removed."))) + (list "Show Proof.")))))) (defpacustom auto-adapt-printing-width t diff --git a/generic/proof-shell.el b/generic/proof-shell.el index 9e51d4fb3..b9ac2b3cf 100644 --- a/generic/proof-shell.el +++ b/generic/proof-shell.el @@ -1139,12 +1139,12 @@ contains only invisible elements for Prooftree synchronization." (not (memq 'empty-action-list flags)) proof-shell-empty-action-list-command) (let* ((cmd (mapconcat 'identity (nth 1 item) " ")) - (extra-cmds (apply proof-shell-empty-action-list-command (list cmd))) - ;; tag all new items with 'empty-action-list - (extra-items (mapcar (lambda (s) (proof-shell-action-list-item - s 'proof-done-invisible - (list 'invisible 'empty-action-list))) - extra-cmds))) + (extra-cmds (apply proof-shell-empty-action-list-command (list cmd))) + ;; tag all new items with 'empty-action-list + (extra-items (mapcar (lambda (s) (proof-shell-action-list-item + s 'proof-done-invisible + (list 'invisible 'empty-action-list))) + extra-cmds))) ;; action-list should be empty at this point (setq proof-action-list (append extra-items proof-action-list)))) @@ -1181,23 +1181,22 @@ contains only invisible elements for Prooftree synchronization." ;; process the delayed callbacks now (mapc 'proof-shell-invoke-callback cbitems) - (unless (or proof-action-list proof-second-action-list-active) + (unless (or proof-action-list proof-second-action-list-active) ; release lock, cleanup - (proof-release-lock) - (proof-detach-queue) - (unless flags ; hint after a batch of scripting - (pg-processing-complete-hint)) - (pg-finish-tracing-display)) - - - (and (not proof-second-action-list-active) - (let ((last-command (car (nth 1 (car (last proof-action-list)))))) - (or (null proof-action-list) - (cl-every - (lambda (item) (memq 'proof-tree-show-subgoal (nth 3 item))) - proof-action-list) - ;; If the last command in proof-action-list is a "Show Proof" form then return t - (when last-command (string-match-p proof-show-proof-diffs-regexp last-command))))))))) + (proof-release-lock) + (proof-detach-queue) + (unless flags ; hint after a batch of scripting + (pg-processing-complete-hint)) + (pg-finish-tracing-display)) + + (and (not proof-second-action-list-active) + (let ((last-command (car (nth 1 (car (last proof-action-list)))))) + (or (null proof-action-list) + (cl-every + (lambda (item) (memq 'proof-tree-show-subgoal (nth 3 item))) + proof-action-list) + ;; If the last command in proof-action-list is a "Show Proof" form then return t + (when last-command (string-match-p proof-show-proof-diffs-regexp last-command))))))))) (defun proof-shell-insert-loopback-cmd (cmd) From 5b1b8ac75056773b4452ce7a41518258010b2bbe Mon Sep 17 00:00:00 2001 From: Anaclet Date: Thu, 28 May 2020 10:34:16 +0200 Subject: [PATCH 10/13] Add tests and flags system --- ci/coq-tests.el | 69 ++++++++++++++++++++++++++++++++++++++----------- 1 file changed, 54 insertions(+), 15 deletions(-) diff --git a/ci/coq-tests.el b/ci/coq-tests.el index cc60f8a0a..da0da3d8b 100644 --- a/ci/coq-tests.el +++ b/ci/coq-tests.el @@ -66,7 +66,7 @@ (defun coq-test-exit () "Exit the Coq process." - (proof-shell-exit t)) + (proof-shell-exit t)) ; (coq-test-on-file nil (message (buffer-file-name)) (message "OK") 42) @@ -110,8 +110,13 @@ #'proof-done-invisible 'no-error-display 'no-response-display 'no-goals-display)) +(defun coq-set-flags (val flags) + (when (member 'show-proof-stepwise flags) (setq coq-show-proof-stepwise val)) + (when (member 'diffs-on flags) (if val (setq coq-diffs 'on) (setq coq-diffs 'off))) + ) -(defun coq-fixture-on-file (file body) + +(defun coq-fixture-on-file (file body &rest flags) "Fixture to setup the test env: open FILE if non-nil, or a temp file then evaluate the BODY function and finally tear-down (exit Coq)." ;; AVOID THE FOLLOWING ERROR: @@ -142,8 +147,10 @@ then evaluate the BODY function and finally tear-down (exit Coq)." (with-current-buffer buffer (setq proof-splash-enable nil) (normal-mode) ;; or (coq-mode) + (coq-set-flags t flags) (coq-mock body)))) (coq-test-exit) + (coq-set-flags nil flags) (not-modified nil) ; Clear modification (kill-buffer buffer) (when rmfile (message "Removing file %s ..." rmfile)) @@ -166,12 +173,18 @@ For example, COMMENT could be (*test-definition*)" (with-current-buffer "*response*" (buffer-substring-no-properties (point-min) (point-max))))))) +(defun coq-should-buffer (message) + (should (string-match-p message + (string-trim + (with-current-buffer "*coq*" + (buffer-substring-no-properties (point-min) (point-max))))))) + ;; TODO: Use https://github.com/rejeep/ert-async.el ;; and/or ERT https://www.gnu.org/software/emacs/manual/html_node/ert/index.html (ert-deftest 010_coq-test-running () "Test that the coqtop process is started properly." - (coq-fixture-on-file nil + (coq-fixture-on-file nil (lambda () (coq-test-cmd "Print 0.") ;; (should (process-list)) ; wouldn't be a strong enough assert. @@ -180,8 +193,8 @@ For example, COMMENT could be (*test-definition*)" (ert-deftest 020_coq-test-definition () "Test *response* output after asserting a Definition." - (coq-fixture-on-file - (coq-test-full-path "test_stepwise.v") + (coq-fixture-on-file + (coq-test-full-path "test_stepwise.v") (lambda () (coq-test-goto-before "(*test-definition*)") (proof-goto-point) @@ -191,8 +204,8 @@ For example, COMMENT could be (*test-definition*)" (ert-deftest 021_coq-test-regression-goto-point () "Regression test for proof-goto-point after a comment, PR #90" - (coq-fixture-on-file - (coq-test-full-path "test_stepwise.v") + (coq-fixture-on-file + (coq-test-full-path "test_stepwise.v") (lambda () (coq-test-goto-after "(*test-definition*)") (proof-goto-point) @@ -202,8 +215,8 @@ For example, COMMENT could be (*test-definition*)" (ert-deftest 030_coq-test-position () "Test locked region after Qed." - (coq-fixture-on-file - (coq-test-full-path "test_stepwise.v") + (coq-fixture-on-file + (coq-test-full-path "test_stepwise.v") (lambda () (coq-test-goto-before " (*test-lemma*)") (let ((proof-point (point))) @@ -214,8 +227,8 @@ For example, COMMENT could be (*test-definition*)" (ert-deftest 040_coq-test-insert () "Test retract on insert from Qed." - (coq-fixture-on-file - (coq-test-full-path "test_stepwise.v") + (coq-fixture-on-file + (coq-test-full-path "test_stepwise.v") (lambda () (coq-test-goto-before " (*test-lemma*)") (proof-goto-point) @@ -230,8 +243,8 @@ For example, COMMENT could be (*test-definition*)" (ert-deftest 050_coq-test-lemma-false () "Test retract on proof error." - (coq-fixture-on-file - (coq-test-full-path "test_stepwise.v") + (coq-fixture-on-file + (coq-test-full-path "test_stepwise.v") (lambda () (coq-test-goto-before " (*test-lemma2*)") (let ((proof-point (save-excursion (coq-test-goto-after "(*error*)")))) @@ -256,8 +269,8 @@ For example, COMMENT could be (*test-definition*)" (ert-deftest 070_coq-test-regression-wholefile-no-proof () "Regression test for no proof bug" - (coq-fixture-on-file - (coq-test-full-path "test_wholefile.v") + (coq-fixture-on-file + (coq-test-full-path "test_wholefile.v") (lambda () (proof-process-buffer) (proof-shell-wait) @@ -265,4 +278,30 @@ For example, COMMENT could be (*test-definition*)" (insert "(*.*)") (should (equal (proof-queue-or-locked-end) 1))))) +(ert-deftest 080_coq-test-regression-show-proof-stepwise() + "Regression test for the \"Show Proof\" option" + (coq-fixture-on-file + (coq-test-full-path "test_stepwise.v") + (lambda () + (coq-test-goto-before " (*test-insert*)") + (proof-goto-point) + (proof-shell-wait) + (coq-should-response "(fun (A : Prop) (proof_of_A : A) => ?Goal)")) + 'show-proof-stepwise)) + + +(ert-deftest 081_coq-test-regression-show-proof-diffs() + "Test for Show Proof Diffs" + (coq-fixture-on-file + (coq-test-full-path "test_stepwise.v") + (lambda () + (coq-test-goto-before " (*test-insert*)") + (proof-goto-point) + (proof-shell-wait) + (coq-should-buffer "(fun (A : Prop) (proof_of_A : A) => \\?Goal)")) + 'show-proof-stepwise 'diffs-on)) + + +(provide 'coq-tests) + ;;; coq-tests.el ends here From cc4b4f6cd626cc6a2f02d3e4efe95dc84d577e3b Mon Sep 17 00:00:00 2001 From: Anaclet Date: Thu, 28 May 2020 11:31:03 +0200 Subject: [PATCH 11/13] Fix the test 081 --- ci/coq-tests.el | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/ci/coq-tests.el b/ci/coq-tests.el index da0da3d8b..8040b1229 100644 --- a/ci/coq-tests.el +++ b/ci/coq-tests.el @@ -298,7 +298,10 @@ For example, COMMENT could be (*test-definition*)" (coq-test-goto-before " (*test-insert*)") (proof-goto-point) (proof-shell-wait) - (coq-should-buffer "(fun (A : Prop) (proof_of_A : A) => \\?Goal)")) + ;; If coq--post-v811, it should be "Show Proof Diffs." otherwise "Show Proof." + (if (coq--post-v811) + (coq-should-buffer "(fun (A : Prop) (proof_of_A : A) => \\?Goal)") + (coq-should-buffer "(fun (A : Prop) (proof_of_A : A) => \\?Goal)"))) 'show-proof-stepwise 'diffs-on)) From 77fd293d631bc17afc18ab36ea5d0e0a28fa5f52 Mon Sep 17 00:00:00 2001 From: Anaclet Date: Fri, 29 May 2020 10:42:15 +0200 Subject: [PATCH 12/13] Minor changes --- ci/coq-tests.el | 60 +++++++++++++++++++++++++------------------------ coq/coq.el | 7 ------ 2 files changed, 31 insertions(+), 36 deletions(-) diff --git a/ci/coq-tests.el b/ci/coq-tests.el index 8040b1229..f06e13243 100644 --- a/ci/coq-tests.el +++ b/ci/coq-tests.el @@ -112,11 +112,9 @@ (defun coq-set-flags (val flags) (when (member 'show-proof-stepwise flags) (setq coq-show-proof-stepwise val)) - (when (member 'diffs-on flags) (if val (setq coq-diffs 'on) (setq coq-diffs 'off))) - ) + (when (member 'diffs-on flags) (if val (setq coq-diffs 'on) (setq coq-diffs 'off)))) - -(defun coq-fixture-on-file (file body &rest flags) +(defun coq-fixture-on-file (file body &rest flags) "Fixture to setup the test env: open FILE if non-nil, or a temp file then evaluate the BODY function and finally tear-down (exit Coq)." ;; AVOID THE FOLLOWING ERROR: @@ -167,24 +165,28 @@ For example, COMMENT could be (*test-definition*)" (goto-char (point-min)) (search-forward comment)) -(defun coq-should-response (message) - (should (equal message +(defun coq-should-response (str) + (should (equal str (string-trim (with-current-buffer "*response*" (buffer-substring-no-properties (point-min) (point-max))))))) -(defun coq-should-buffer (message) - (should (string-match-p message +(defun coq-should-buffer-regexp (regexp) + (should (string-match-p regexp (string-trim (with-current-buffer "*coq*" (buffer-substring-no-properties (point-min) (point-max))))))) +(defun coq-should-buffer-string (str) + "Particular case of `coq-should-buffer-regexp'." + (coq-should-buffer-regexp (regexp-quote str))) + ;; TODO: Use https://github.com/rejeep/ert-async.el ;; and/or ERT https://www.gnu.org/software/emacs/manual/html_node/ert/index.html (ert-deftest 010_coq-test-running () "Test that the coqtop process is started properly." - (coq-fixture-on-file nil + (coq-fixture-on-file nil (lambda () (coq-test-cmd "Print 0.") ;; (should (process-list)) ; wouldn't be a strong enough assert. @@ -193,8 +195,8 @@ For example, COMMENT could be (*test-definition*)" (ert-deftest 020_coq-test-definition () "Test *response* output after asserting a Definition." - (coq-fixture-on-file - (coq-test-full-path "test_stepwise.v") + (coq-fixture-on-file + (coq-test-full-path "test_stepwise.v") (lambda () (coq-test-goto-before "(*test-definition*)") (proof-goto-point) @@ -203,9 +205,9 @@ For example, COMMENT could be (*test-definition*)" (ert-deftest 021_coq-test-regression-goto-point () - "Regression test for proof-goto-point after a comment, PR #90" - (coq-fixture-on-file - (coq-test-full-path "test_stepwise.v") + "Regression test for proof-goto-point after a comment, PR #490" + (coq-fixture-on-file + (coq-test-full-path "test_stepwise.v") (lambda () (coq-test-goto-after "(*test-definition*)") (proof-goto-point) @@ -215,8 +217,8 @@ For example, COMMENT could be (*test-definition*)" (ert-deftest 030_coq-test-position () "Test locked region after Qed." - (coq-fixture-on-file - (coq-test-full-path "test_stepwise.v") + (coq-fixture-on-file + (coq-test-full-path "test_stepwise.v") (lambda () (coq-test-goto-before " (*test-lemma*)") (let ((proof-point (point))) @@ -227,8 +229,8 @@ For example, COMMENT could be (*test-definition*)" (ert-deftest 040_coq-test-insert () "Test retract on insert from Qed." - (coq-fixture-on-file - (coq-test-full-path "test_stepwise.v") + (coq-fixture-on-file + (coq-test-full-path "test_stepwise.v") (lambda () (coq-test-goto-before " (*test-lemma*)") (proof-goto-point) @@ -243,8 +245,8 @@ For example, COMMENT could be (*test-definition*)" (ert-deftest 050_coq-test-lemma-false () "Test retract on proof error." - (coq-fixture-on-file - (coq-test-full-path "test_stepwise.v") + (coq-fixture-on-file + (coq-test-full-path "test_stepwise.v") (lambda () (coq-test-goto-before " (*test-lemma2*)") (let ((proof-point (save-excursion (coq-test-goto-after "(*error*)")))) @@ -269,8 +271,8 @@ For example, COMMENT could be (*test-definition*)" (ert-deftest 070_coq-test-regression-wholefile-no-proof () "Regression test for no proof bug" - (coq-fixture-on-file - (coq-test-full-path "test_wholefile.v") + (coq-fixture-on-file + (coq-test-full-path "test_wholefile.v") (lambda () (proof-process-buffer) (proof-shell-wait) @@ -280,28 +282,28 @@ For example, COMMENT could be (*test-definition*)" (ert-deftest 080_coq-test-regression-show-proof-stepwise() "Regression test for the \"Show Proof\" option" - (coq-fixture-on-file - (coq-test-full-path "test_stepwise.v") + (coq-fixture-on-file + (coq-test-full-path "test_stepwise.v") (lambda () (coq-test-goto-before " (*test-insert*)") (proof-goto-point) (proof-shell-wait) - (coq-should-response "(fun (A : Prop) (proof_of_A : A) => ?Goal)")) + (coq-should-buffer-string "(fun (A : Prop) (proof_of_A : A) => ?Goal)")) 'show-proof-stepwise)) (ert-deftest 081_coq-test-regression-show-proof-diffs() "Test for Show Proof Diffs" - (coq-fixture-on-file - (coq-test-full-path "test_stepwise.v") + (coq-fixture-on-file + (coq-test-full-path "test_stepwise.v") (lambda () (coq-test-goto-before " (*test-insert*)") (proof-goto-point) (proof-shell-wait) ;; If coq--post-v811, it should be "Show Proof Diffs." otherwise "Show Proof." (if (coq--post-v811) - (coq-should-buffer "(fun (A : Prop) (proof_of_A : A) => \\?Goal)") - (coq-should-buffer "(fun (A : Prop) (proof_of_A : A) => \\?Goal)"))) + (coq-should-buffer-string "(fun (A : Prop) (proof_of_A : A) => ?Goal)") + (coq-should-buffer-string "(fun (A : Prop) (proof_of_A : A) => ?Goal)"))) 'show-proof-stepwise 'diffs-on)) diff --git a/coq/coq.el b/coq/coq.el index df7c5a668..efa603499 100644 --- a/coq/coq.el +++ b/coq/coq.el @@ -1237,13 +1237,6 @@ should match the `coq-show-proof-diffs-regexp'." ;; the number of nested goals, then Unset Silent and Show the goal (and (string-match-p "BackTo\\s-" cmd) (> (length coq-last-but-one-proofstack) coq--retract-naborts))) - ;; "Set Diffs" always re-prints the proof context with (if enabled) diffs - ;; (list "Unset Silent." (if (coq--post-v810) (coq-diffs) "Show.") - ;; (when coq-show-proof-stepwise - ;; (or - ;; (when (eq coq-diffs 'off) "Show Proof.") - ;; (when (eq coq-diffs 'on) "Show Proof Diffs.") - ;; (when (eq coq-diffs 'removed) "Show Proof Diffs removed."))))) (let ((showlist (list "Unset Silent." (if (coq--post-v810) (coq-diffs) "Show.")))) (when coq-show-proof-stepwise (add-to-list 'showlist From 9c82b71d396b425337592f96f2e9b6a1d97be0c0 Mon Sep 17 00:00:00 2001 From: Erik Martin-Dorel Date: Fri, 29 May 2020 11:38:15 +0200 Subject: [PATCH 13/13] refactor: Remove unneeded coq-should-response --- ci/coq-tests.el | 34 +++++++++++++++------------------- 1 file changed, 15 insertions(+), 19 deletions(-) diff --git a/ci/coq-tests.el b/ci/coq-tests.el index f06e13243..ff762d9c8 100644 --- a/ci/coq-tests.el +++ b/ci/coq-tests.el @@ -165,21 +165,17 @@ For example, COMMENT could be (*test-definition*)" (goto-char (point-min)) (search-forward comment)) -(defun coq-should-response (str) - (should (equal str - (string-trim - (with-current-buffer "*response*" - (buffer-substring-no-properties (point-min) (point-max))))))) - -(defun coq-should-buffer-regexp (regexp) - (should (string-match-p regexp - (string-trim - (with-current-buffer "*coq*" - (buffer-substring-no-properties (point-min) (point-max))))))) - -(defun coq-should-buffer-string (str) +(defun coq-should-buffer-regexp (regexp &optional buffer-name) + "Check REGEXP matches in BUFFER-NAME (*response* if nil)." + (should (string-match-p + regexp + (string-trim + (with-current-buffer (or buffer-name "*response*") + (buffer-substring-no-properties (point-min) (point-max))))))) + +(defun coq-should-buffer-string (str &optional buffer-name) "Particular case of `coq-should-buffer-regexp'." - (coq-should-buffer-regexp (regexp-quote str))) + (coq-should-buffer-regexp (regexp-quote str) buffer-name)) ;; TODO: Use https://github.com/rejeep/ert-async.el ;; and/or ERT https://www.gnu.org/software/emacs/manual/html_node/ert/index.html @@ -201,7 +197,7 @@ For example, COMMENT could be (*test-definition*)" (coq-test-goto-before "(*test-definition*)") (proof-goto-point) (proof-shell-wait) - (coq-should-response "trois is defined")))) + (coq-should-buffer-string "trois is defined")))) (ert-deftest 021_coq-test-regression-goto-point () @@ -252,7 +248,7 @@ For example, COMMENT could be (*test-definition*)" (let ((proof-point (save-excursion (coq-test-goto-after "(*error*)")))) (proof-goto-point) (proof-shell-wait) - (coq-should-response "Error: Unable to unify \"false\" with \"true\".") + (coq-should-buffer-string "Error: Unable to unify \"false\" with \"true\".") (should (equal (proof-queue-or-locked-end) proof-point)))))) @@ -282,7 +278,7 @@ For example, COMMENT could be (*test-definition*)" (ert-deftest 080_coq-test-regression-show-proof-stepwise() "Regression test for the \"Show Proof\" option" - (coq-fixture-on-file + (coq-fixture-on-file (coq-test-full-path "test_stepwise.v") (lambda () (coq-test-goto-before " (*test-insert*)") @@ -294,7 +290,7 @@ For example, COMMENT could be (*test-definition*)" (ert-deftest 081_coq-test-regression-show-proof-diffs() "Test for Show Proof Diffs" - (coq-fixture-on-file + (coq-fixture-on-file (coq-test-full-path "test_stepwise.v") (lambda () (coq-test-goto-before " (*test-insert*)") @@ -302,7 +298,7 @@ For example, COMMENT could be (*test-definition*)" (proof-shell-wait) ;; If coq--post-v811, it should be "Show Proof Diffs." otherwise "Show Proof." (if (coq--post-v811) - (coq-should-buffer-string "(fun (A : Prop) (proof_of_A : A) => ?Goal)") + (coq-should-buffer-string "(fun (A : Prop) (proof_of_A : A) => ?Goal)" "*coq*") (coq-should-buffer-string "(fun (A : Prop) (proof_of_A : A) => ?Goal)"))) 'show-proof-stepwise 'diffs-on))