From 8e12eee54e36ca16d4b4530e1509479f22929e4f Mon Sep 17 00:00:00 2001
From: Cyril Anaclet
Date: Mon, 11 May 2020 15:00:47 +0200
Subject: 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 bd898a9c..4d2c8287 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 f9a3571e..2a5c3f44 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 00000000..f42431af
--- /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 71112fc1..8ebf3054 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.
--
cgit v1.2.3
From ecb47478c9f9959ea25ce509076f6e3959d2c620 Mon Sep 17 00:00:00 2001
From: Cyril Anaclet
Date: Thu, 14 May 2020 15:29:58 +0200
Subject: 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 470331a6..e486997d 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 8ebf3054..65ff488f 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 8d539191..16cdae93 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 a0e80fa7..b6bf9225 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)))))
--
cgit v1.2.3
From aba3f2bfe2bffde6d2df21b098740100459a84be Mon Sep 17 00:00:00 2001
From: Erik Martin-Dorel
Date: Fri, 15 May 2020 15:50:48 +0200
Subject: 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 4d2c8287..74ddb076 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 2a5c3f44..fdb3d4b8 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 f42431af..0daf98f8 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 e486997d..a27274c5 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 65ff488f..b833765f 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 16cdae93..ce72c76c 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)
--
cgit v1.2.3
From 04aff704f3d13452bc5c52ff860c5ab564539632 Mon Sep 17 00:00:00 2001
From: Cyril Anaclet
Date: Mon, 18 May 2020 13:33:57 +0200
Subject: 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 a27274c5..3ae7fbca 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 b6bf9225..8f23608a 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))
--
cgit v1.2.3
From 22681a3caf2c8f45700585ea74dffbf48bb2ac19 Mon Sep 17 00:00:00 2001
From: Cyril Anaclet
Date: Wed, 20 May 2020 14:19:14 +0200
Subject: 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 fdb3d4b8..938f706e 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 0daf98f8..00000000
--- 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 3ae7fbca..47869aed 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 b833765f..942e85fe 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 ce72c76c..9d352548 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 8f23608a..1258c7f6 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))
--
cgit v1.2.3
From ff9b5b11b4266b9260b74d772ae2e5848221f6f8 Mon Sep 17 00:00:00 2001
From: Erik Martin-Dorel
Date: Wed, 20 May 2020 21:11:27 +0200
Subject: 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 1a281521..cc60f8a0 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
--
cgit v1.2.3
From 411ebb27fda4d39fc22baf341dcdde2341632b8d Mon Sep 17 00:00:00 2001
From: Erik Martin-Dorel
Date: Wed, 20 May 2020 21:48:20 +0200
Subject: fix: Do "Show Proof…" (with "?Goal") as soon as the proof is started
---
coq/coq.el | 6 ++++--
1 file changed, 4 insertions(+), 2 deletions(-)
diff --git a/coq/coq.el b/coq/coq.el
index 942e85fe..10aa07bf 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
--
cgit v1.2.3
From 3ab3f5efbbb724cb2e4aebc3c4d7bfdce4008896 Mon Sep 17 00:00:00 2001
From: Anaclet
Date: Mon, 25 May 2020 10:55:03 +0200
Subject: 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 47869aed..5b8d8c48 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 10aa07bf..9fc6e200 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 1258c7f6..9e51d4fb 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)
--
cgit v1.2.3
From 8627fba2a20e42432de441391db2f35e3c48a952 Mon Sep 17 00:00:00 2001
From: Anaclet
Date: Thu, 28 May 2020 09:21:53 +0200
Subject: 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 9fc6e200..df7c5a66 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 9e51d4fb..b9ac2b3c 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)
--
cgit v1.2.3
From 5b1b8ac75056773b4452ce7a41518258010b2bbe Mon Sep 17 00:00:00 2001
From: Anaclet
Date: Thu, 28 May 2020 10:34:16 +0200
Subject: 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 cc60f8a0..da0da3d8 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
--
cgit v1.2.3
From cc4b4f6cd626cc6a2f02d3e4efe95dc84d577e3b Mon Sep 17 00:00:00 2001
From: Anaclet
Date: Thu, 28 May 2020 11:31:03 +0200
Subject: 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 da0da3d8..8040b122 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))
--
cgit v1.2.3
From 77fd293d631bc17afc18ab36ea5d0e0a28fa5f52 Mon Sep 17 00:00:00 2001
From: Anaclet
Date: Fri, 29 May 2020 10:42:15 +0200
Subject: 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 8040b122..f06e1324 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 df7c5a66..efa60349 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
--
cgit v1.2.3
From 9c82b71d396b425337592f96f2e9b6a1d97be0c0 Mon Sep 17 00:00:00 2001
From: Erik Martin-Dorel
Date: Fri, 29 May 2020 11:38:15 +0200
Subject: 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 f06e1324..ff762d9c 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))
--
cgit v1.2.3