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(+)

(limited to 'ci')

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 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(-)

(limited to 'ci')

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  "<diff\\.added\\.bg>(fun <diff\\.added>(</diff\\.added>A : Prop<diff\\.added>) (proof_of_A : A)</diff\\.added> => \\?Goal)</diff\\.added\\.bg>"))
+   '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(-)

(limited to 'ci')

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  "<diff\\.added\\.bg>(fun <diff\\.added>(</diff\\.added>A : Prop<diff\\.added>) (proof_of_A : A)</diff\\.added> => \\?Goal)</diff\\.added\\.bg>"))
+     ;; If coq--post-v811, it should be "Show Proof Diffs." otherwise "Show Proof."
+     (if (coq--post-v811)
+	 (coq-should-buffer  "<diff\\.added\\.bg>(fun <diff\\.added>(</diff\\.added>A : Prop<diff\\.added>) (proof_of_A : A)</diff\\.added> => \\?Goal)</diff\\.added\\.bg>")
+       (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 +++++++++++++++++++++++++++++----------------------------
 1 file changed, 31 insertions(+), 29 deletions(-)

(limited to 'ci')

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  "<diff\\.added\\.bg>(fun <diff\\.added>(</diff\\.added>A : Prop<diff\\.added>) (proof_of_A : A)</diff\\.added> => \\?Goal)</diff\\.added\\.bg>")
-       (coq-should-buffer "(fun (A : Prop) (proof_of_A : A) => \\?Goal)")))
+	 (coq-should-buffer-string  "<diff.added.bg>(fun <diff.added>(</diff.added>A : Prop<diff.added>) (proof_of_A : A)</diff.added> => ?Goal)</diff.added.bg>")
+       (coq-should-buffer-string "(fun (A : Prop) (proof_of_A : A) => ?Goal)")))
    'show-proof-stepwise 'diffs-on))
  
 
-- 
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(-)

(limited to 'ci')

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  "<diff.added.bg>(fun <diff.added>(</diff.added>A : Prop<diff.added>) (proof_of_A : A)</diff.added> => ?Goal)</diff.added.bg>")
+	 (coq-should-buffer-string "<diff.added.bg>(fun <diff.added>(</diff.added>A : Prop<diff.added>) (proof_of_A : A)</diff.added> => ?Goal)</diff.added.bg>" "*coq*")
        (coq-should-buffer-string "(fun (A : Prop) (proof_of_A : A) => ?Goal)")))
    'show-proof-stepwise 'diffs-on))
  
-- 
cgit v1.2.3