From 977429b4501a6e5b7c0949ddf258f160e90fe48d Mon Sep 17 00:00:00 2001
From: Cyril Anaclet
Date: Tue, 21 Apr 2020 17:31:41 +0200
Subject: Add a test

---
 ci/coq-tests.el | 19 +++++++++++++++++--
 1 file changed, 17 insertions(+), 2 deletions(-)

diff --git a/ci/coq-tests.el b/ci/coq-tests.el
index 057f918e..616e3cd4 100644
--- a/ci/coq-tests.el
+++ b/ci/coq-tests.el
@@ -9,7 +9,7 @@
 
 (setq debug-on-error t) ; open the debugger on error -- may be commented-out
 
-(require 'ert-async)
+; (require 'ert-async)
 ;(setq ert-async-timeout 2)
 
 ;;; Code:
@@ -57,6 +57,8 @@
   "Exit the Coq process."
   (proof-shell-exit t))
 
+
+
 ;; AVOID THE FOLLOWING ERROR:
 ;; Starting:  -emacs
 ;; Debugger entered--Lisp error: (wrong-type-argument stringp nil)
@@ -123,12 +125,25 @@
      #'proof-done-invisible
      'no-error-display 'no-response-display 'no-goals-display)))
 
+; Fixture for init and exit coq
+(defun coq-init-exit (body)
+       (unwind-protect
+           (progn  (coq-test-init)
+                  (funcall body))
+          (coq-test-exit)))
+
 (defun coq-test-001 ()
   ;; TODO: retrieve the test status, maybe by changing the function above
-  (coq-test-cmd "Print nat."))
+  (coq-test-cmd (process-list)))
 ;; 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 coq-test-running ()
+  (coq-init-exit
+   (lambda () 
+  (coq-test-cmd "Check 0.")
+  (should  (get-process "coq")))))
+
 (defun coq-test-main ()
   (coq-mock #'coq-test-001))
 
-- 
cgit v1.2.3


From 7ab2270c4837db49df6d5630b67ce346f5e51872 Mon Sep 17 00:00:00 2001
From: Cyril Anaclet
Date: Fri, 24 Apr 2020 10:10:37 +0200
Subject: Add ERT tests (WIP)

Co-authored-by: Cyril Anaclet <cyril.anaclet@gmail.com>
Co-authored-by: Erik Martin-Dorel <erik.martin-dorel@irit.fr>
---
 ci/coq-tests.el | 144 ++++++++++++++++++++++++++++++++++++--------------------
 ci/test1.v      |  12 +++++
 2 files changed, 104 insertions(+), 52 deletions(-)
 create mode 100644 ci/test1.v

diff --git a/ci/coq-tests.el b/ci/coq-tests.el
index 616e3cd4..f127b196 100644
--- a/ci/coq-tests.el
+++ b/ci/coq-tests.el
@@ -5,7 +5,7 @@
 
 ;;;  Eval this to run the tests interactively <C-x C-e>
 ;;
-;; (call-interactively #'ert-run-tests-interactively)
+;; (progn (load-file "coq-tests.el") (call-interactively #'ert))
 
 (setq debug-on-error t) ; open the debugger on error -- may be commented-out
 
@@ -45,6 +45,18 @@
 
 (defconst coq-test-file-prefix "coq_test_")
 
+(defun get-string-from-file (filePath)
+  "Return filePath's file content."
+  (with-temp-buffer
+    (insert-file-contents filePath)
+    (buffer-string)))
+
+(defun read-lines (filePath)
+  "Return a list of lines of a file at filePath."
+  (with-temp-buffer
+    (insert-file-contents filePath)
+    (split-string (buffer-string) "\n" t)))
+
 (defun coq-test-init ()
   "Ensure `coq' is loaded."
   (unless (featurep 'coq)
@@ -57,33 +69,7 @@
   "Exit the Coq process."
   (proof-shell-exit t))
 
-
-
-;; AVOID THE FOLLOWING ERROR:
-;; Starting:  -emacs
-;; Debugger entered--Lisp error: (wrong-type-argument stringp nil)
-;;   file-name-directory(nil)
-;;   scomint-exec-1("coq" #<buffer *coq*> nil ("-emacs"))
-;;   scomint-exec(#<buffer *coq*> "coq" nil nil ("-emacs"))
-;;   scomint-make-in-buffer("coq" nil nil nil "-emacs")
-;;   apply(scomint-make-in-buffer "coq" nil nil nil "-emacs")
-;;   scomint-make("coq" nil nil "-emacs")
-;;   apply(scomint-make ("coq" nil nil "-emacs"))
-;;   proof-shell-start()
-;;   proof-shell-ready-prover()
-(defmacro coq-test-on-file (&rest body)
-  "Eval BODY like `progn' after opening a temporary Coq file."
-  ;; For more info: https://mullikine.github.io/posts/macro-tutorial/
-  `(let ((file (concat (make-temp-file coq-test-file-prefix) ".v")))
-     (message "Opening file %s ..." file)
-     (save-excursion          
-       (let ((buffer (find-file file))
-             (res (progn ,@body)))
-         (progn (kill-buffer buffer)
-                (ignore-errors (delete-file file))
-                res)))))
-; (pp (macroexpand '(coq-test-on-file (message "OK"))))
-; (coq-test-on-file (message (buffer-file-name)) (message "OK") 42)
+; (coq-test-on-file nil (message (buffer-file-name)) (message "OK") 42)
 
 ;; DEFINITION OF MOCKS, SEE `coq-mock' BELOW
 ;; Another solution would consist in using el-mock, mentioned in:
@@ -117,20 +103,48 @@
 ;; (coq-mock #'main)
 
 (defun coq-test-cmd (cmd)
-  (coq-test-on-file
-    (coq-test-init)
-    (proof-shell-invisible-command
-     cmd
-     'waitforit
-     #'proof-done-invisible
-     'no-error-display 'no-response-display 'no-goals-display)))
-
-; Fixture for init and exit coq
-(defun coq-init-exit (body)
-       (unwind-protect
-           (progn  (coq-test-init)
-                  (funcall body))
-          (coq-test-exit)))
+  ;;(coq-test-on-file)
+  ;;(coq-test-init)
+  (proof-shell-invisible-command
+   cmd
+   'waitforit
+   #'proof-done-invisible
+   'no-error-display 'no-response-display 'no-goals-display))
+
+
+(defun coq-fixture-on-file (file body)
+  "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:
+;; Starting:  -emacs
+;; Debugger entered--Lisp error: (wrong-type-argument stringp nil)
+;;   file-name-directory(nil)
+;;   scomint-exec-1("coq" #<buffer *coq*> nil ("-emacs"))
+;;   scomint-exec(#<buffer *coq*> "coq" nil nil ("-emacs"))
+;;   scomint-make-in-buffer("coq" nil nil nil "-emacs")
+;;   apply(scomint-make-in-buffer "coq" nil nil nil "-emacs")
+;;   scomint-make("coq" nil nil "-emacs")
+;;   apply(scomint-make ("coq" nil nil "-emacs"))
+;;   proof-shell-start()
+;;   proof-shell-ready-prover()
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;; For info on macros: https://mullikine.github.io/posts/macro-tutorial
+;;; (pp (macroexpand '(macro args)))
+  (save-excursion
+      (let* ((openfile (or file
+                           (concat (make-temp-file coq-test-file-prefix) ".v")))
+             ;; if FILE is nil, create a temporary Coq file, removed in the end
+             (rmfile (unless file openfile))
+             (buffer (find-file openfile)))
+        (message "Opening file %s ..." file)
+        (unwind-protect
+            (progn
+              (coq-test-init)
+              (set-buffer buffer)
+              (coq-mock body))
+          (kill-buffer buffer)
+          (when rmfile (message "Removing file %s ..." rmfile))
+          (ignore-errors (delete-file rmfile))))))
 
 (defun coq-test-001 ()
   ;; TODO: retrieve the test status, maybe by changing the function above
@@ -138,17 +152,43 @@
 ;; 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 coq-test-running ()
-  (coq-init-exit
-   (lambda () 
-  (coq-test-cmd "Check 0.")
-  (should  (get-process "coq")))))
-
-(defun coq-test-main ()
-  (coq-mock #'coq-test-001))
 
-;(ignore-errors (coq-test-exit))
-(coq-test-main)
+(ert-deftest coq-test-running ()
+  (coq-fixture-on-file nil
+   (lambda ()
+     (coq-test-cmd "Print 0.")
+     ;; (should (process-list)) ; wouldn't be a strong enough assert.
+     (should (get-process "coq")))))
+
+
+(ert-deftest coq-test-print ()
+  (coq-fixture-on-file "./test1.v"
+   (lambda ()
+     (coq-test-cmd (car (read-lines "./test1.v")))
+     ;; TODO/Cyril: call (proof-goto-point (point-max))
+     (should (equal "trois is defined"
+		    (string-trim
+                     (setq temp
+                     (with-current-buffer "*response*"
+                       (buffer-substring-no-properties (point-min) (point-max))))))))))
+
+;; TODO
+;; (ert-deftest coq-test-lemma ()
+;;   (coq-init-exit
+;;    (lambda ()
+;;      (coq-test-cmd (car (read-lines "./test1.v")))
+;;      (should (equal "trois is defined"
+;; 		    (with-current-buffer "*response*"
+;; 		      (goto-char (point-min))
+;; 		      (buffer-substring-no-properties (line-beginning-position) (line-end-position) )
+;; 		      )
+;; 		    )))))
+
+;; (defun coq-test-main ()
+;;   (coq-mock #'coq-test-001))
+
+;; ;(ignore-errors (coq-test-exit))
+;; (coq-test-main)
 
 (provide 'coq-tests)
 ;;; learn-ocaml-tests.el ends here
diff --git a/ci/test1.v b/ci/test1.v
new file mode 100644
index 00000000..0c4b77fe
--- /dev/null
+++ b/ci/test1.v
@@ -0,0 +1,12 @@
+Definition trois := 3. 
+Print trois.
+Eval compute in 10 * trois * trois.
+
+
+
+Lemma  easy_proof : (forall A : Prop, A -> A). 
+Proof using .
+  intros A.
+  intros proof_of_A.
+  exact proof_of_A.
+Qed.
-- 
cgit v1.2.3


From b3fb85c3da48e61bea57aacdd2d0a9468cea9d72 Mon Sep 17 00:00:00 2001
From: Erik Martin-Dorel
Date: Wed, 29 Apr 2020 00:31:45 +0200
Subject: fix(test.sh): $_dir naming

---
 ci/test.sh | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/ci/test.sh b/ci/test.sh
index b29d5af7..3d9b4a72 100755
--- a/ci/test.sh
+++ b/ci/test.sh
@@ -29,8 +29,8 @@ assert () {
 
 assert emacs --version
 
-srcdir=$( cd "$( dirname "${BASH_SOURCE[0]}" )" >/dev/null && cd .. && pwd )
-rootdir=$( cd "$( dirname "${BASH_SOURCE[0]}" )" >/dev/null && pwd )
+rootdir=$( cd "$( dirname "${BASH_SOURCE[0]}" )" >/dev/null && cd .. && pwd )
+srcdir=$( cd "$( dirname "${BASH_SOURCE[0]}" )" >/dev/null && pwd )
 
 # form="(message \"OK\")"
 form="(progn (add-to-list 'load-path \"$rootdir\") (add-to-list 'load-path \"$srcdir\"))"
-- 
cgit v1.2.3


From 94c6da5c8c9db07f406cd28ca9d6532d09b9df15 Mon Sep 17 00:00:00 2001
From: Erik Martin-Dorel
Date: Wed, 29 Apr 2020 01:19:52 +0200
Subject: fix: coq-tests.el and related files

* The "./test1.v" relative filename triggered an issue
  => use (coq-test-full-path "test1.v")

* The (coq-test-cmd "...") was not optimal for coq-test-print
  => use (progn
     (coq-test-goto-before "(*some-unique-identifier*)")
     (proof-goto-point)
     (proof-shell-wait))

* The (string-trim "...") function was not defined in batch mode
  => use (require 'subr-x)

& Remove forgotten "(setq temp" snippet.
---
 ci/coq-tests.el | 50 ++++++++++++++++++++++++++++++++++----------------
 ci/test.sh      |  5 +++--
 ci/test1.v      |  4 ++--
 3 files changed, 39 insertions(+), 20 deletions(-)

diff --git a/ci/coq-tests.el b/ci/coq-tests.el
index f127b196..fe3510e0 100644
--- a/ci/coq-tests.el
+++ b/ci/coq-tests.el
@@ -7,10 +7,16 @@
 ;;
 ;; (progn (load-file "coq-tests.el") (call-interactively #'ert))
 
+(unless (and (boundp 'coq-test-dir) coq-test-dir) ; if set by ./test.sh
+  (if buffer-file-name
+      (setq coq-test-dir (file-name-directory buffer-file-name))
+    (error "You should set 'coq-test-dir, or run coq-test.el from a file buffer.")))
+
 (setq debug-on-error t) ; open the debugger on error -- may be commented-out
 
-; (require 'ert-async)
-;(setq ert-async-timeout 2)
+(require 'subr-x) ;; for (string-trim)
+;;(require 'ert-async)
+;;(setq ert-async-timeout 2)
 
 ;;; Code:
 
@@ -43,6 +49,10 @@
 ; 
 ; (test-process-invisible-tactics-then-reset-and-insert)
 
+(defun coq-test-full-path (basename)
+  "Return the absolute path of BASENAME (a filename such as ./foo.v)."
+  (concat coq-test-dir basename))
+
 (defconst coq-test-file-prefix "coq_test_")
 
 (defun get-string-from-file (filePath)
@@ -136,23 +146,30 @@ then evaluate the BODY function and finally tear-down (exit Coq)."
              ;; if FILE is nil, create a temporary Coq file, removed in the end
              (rmfile (unless file openfile))
              (buffer (find-file openfile)))
-        (message "Opening file %s ..." file)
+        (message "Opening file %s ..." openfile)
         (unwind-protect
             (progn
               (coq-test-init)
-              (set-buffer buffer)
-              (coq-mock body))
+              (with-current-buffer buffer
+                (coq-mock body)))
           (kill-buffer buffer)
           (when rmfile (message "Removing file %s ..." rmfile))
           (ignore-errors (delete-file rmfile))))))
 
-(defun coq-test-001 ()
-  ;; TODO: retrieve the test status, maybe by changing the function above
-  (coq-test-cmd (process-list)))
+(defun coq-test-goto-before (comment)
+  "Go just before COMMENT (a unique string in the .v file).
+For example, COMMENT could be (*test-definition*)"
+  (goto-char (point-max))
+  (search-backward comment))
+
+(defun coq-test-goto-after (comment)
+  "Go just before COMMENT (a unique string in the .v file)."
+  (goto-char (point-min))
+  (search-forward comment))
+
 ;; 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 coq-test-running ()
   (coq-fixture-on-file nil
    (lambda ()
@@ -160,17 +177,17 @@ then evaluate the BODY function and finally tear-down (exit Coq)."
      ;; (should (process-list)) ; wouldn't be a strong enough assert.
      (should (get-process "coq")))))
 
-
 (ert-deftest coq-test-print ()
-  (coq-fixture-on-file "./test1.v"
+  (coq-fixture-on-file
+   (coq-test-full-path "test1.v")
    (lambda ()
-     (coq-test-cmd (car (read-lines "./test1.v")))
-     ;; TODO/Cyril: call (proof-goto-point (point-max))
+     (coq-test-goto-before "(*test-definition*)")
+     (proof-goto-point)
+     (proof-shell-wait)
      (should (equal "trois is defined"
 		    (string-trim
-                     (setq temp
                      (with-current-buffer "*response*"
-                       (buffer-substring-no-properties (point-min) (point-max))))))))))
+                       (buffer-substring-no-properties (point-min) (point-max)))))))))
 
 ;; TODO
 ;; (ert-deftest coq-test-lemma ()
@@ -191,4 +208,5 @@ then evaluate the BODY function and finally tear-down (exit Coq)."
 ;; (coq-test-main)
 
 (provide 'coq-tests)
-;;; learn-ocaml-tests.el ends here
+
+;;; coq-tests.el ends here
diff --git a/ci/test.sh b/ci/test.sh
index 3d9b4a72..50d07579 100755
--- a/ci/test.sh
+++ b/ci/test.sh
@@ -32,7 +32,8 @@ assert emacs --version
 rootdir=$( cd "$( dirname "${BASH_SOURCE[0]}" )" >/dev/null && cd .. && pwd )
 srcdir=$( cd "$( dirname "${BASH_SOURCE[0]}" )" >/dev/null && pwd )
 
-# form="(message \"OK\")"
-form="(progn (add-to-list 'load-path \"$rootdir\") (add-to-list 'load-path \"$srcdir\"))"
+form="(progn (add-to-list 'load-path \"$rootdir\")
+(add-to-list 'load-path \"$srcdir\")
+(setq coq-test-dir \"$srcdir/\"))"  # we need a trailing slash here
 
 assert emacs --batch -l ert --eval "$form" -l init-tests.el -l proof-general.el -l coq-tests.el -f ert-run-tests-batch-and-exit
diff --git a/ci/test1.v b/ci/test1.v
index 0c4b77fe..0a9ef963 100644
--- a/ci/test1.v
+++ b/ci/test1.v
@@ -1,10 +1,10 @@
-Definition trois := 3. 
+Definition trois := 3. (*test-definition*)
 Print trois.
 Eval compute in 10 * trois * trois.
 
 
 
-Lemma  easy_proof : (forall A : Prop, A -> A). 
+Lemma easy_proof : forall A : Prop, A -> A.
 Proof using .
   intros A.
   intros proof_of_A.
-- 
cgit v1.2.3


From 74982be8ec4c15661dc9e74abcde85102ea3b343 Mon Sep 17 00:00:00 2001
From: Erik Martin-Dorel
Date: Wed, 29 Apr 2020 01:30:14 +0200
Subject: ci: Build all branches for now

TODO: revert this commit before creating a Pull Request
---
 .github/workflows/test.yml | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/.github/workflows/test.yml b/.github/workflows/test.yml
index 984f0cc5..61f8e30d 100644
--- a/.github/workflows/test.yml
+++ b/.github/workflows/test.yml
@@ -3,8 +3,9 @@ name: CI
 on:
   push:
     branches:
-      - master
-      - hybrid
+      #- master
+      #- hybrid
+      - "**"
   pull_request:
     branches:
       - '**'
-- 
cgit v1.2.3


From a2ef60931a194ee441ed0edd5bac68eed3179c50 Mon Sep 17 00:00:00 2001
From: Erik Martin-Dorel
Date: Wed, 29 Apr 2020 11:29:26 +0200
Subject: fix: ERT tests OK in batch & interactive mode at once

---
 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 fe3510e0..5c1e7d83 100644
--- a/ci/coq-tests.el
+++ b/ci/coq-tests.el
@@ -71,7 +71,7 @@
   "Ensure `coq' is loaded."
   (unless (featurep 'coq)
     (add-to-list 'load-path
-		 (locate-dominating-file buffer-file-name "proof-general.el"))
+		 (locate-dominating-file coq-test-dir "proof-general.el"))
     (load "proof-general")
     (proofgeneral "coq")))
 
@@ -151,7 +151,10 @@ then evaluate the BODY function and finally tear-down (exit Coq)."
             (progn
               (coq-test-init)
               (with-current-buffer buffer
+                (setq proof-splash-enable nil)
+                (normal-mode) ;; or (coq-mode)
                 (coq-mock body)))
+          (coq-test-exit)
           (kill-buffer buffer)
           (when rmfile (message "Removing file %s ..." rmfile))
           (ignore-errors (delete-file rmfile))))))
-- 
cgit v1.2.3


From 0ae25c5ae3f401ad9cabe16b1636ff2e11da874c Mon Sep 17 00:00:00 2001
From: Cyril Anaclet
Date: Wed, 29 Apr 2020 18:10:40 +0200
Subject: [WIP] add 2 tests

---
 ci/coq-tests.el | 83 ++++++++++++++++++++++++++++++++++-----------------------
 ci/test1.v      |  4 +--
 2 files changed, 51 insertions(+), 36 deletions(-)

diff --git a/ci/coq-tests.el b/ci/coq-tests.el
index 5c1e7d83..4a620aa5 100644
--- a/ci/coq-tests.el
+++ b/ci/coq-tests.el
@@ -141,23 +141,24 @@ then evaluate the BODY function and finally tear-down (exit Coq)."
 ;;; For info on macros: https://mullikine.github.io/posts/macro-tutorial
 ;;; (pp (macroexpand '(macro args)))
   (save-excursion
-      (let* ((openfile (or file
-                           (concat (make-temp-file coq-test-file-prefix) ".v")))
-             ;; if FILE is nil, create a temporary Coq file, removed in the end
-             (rmfile (unless file openfile))
-             (buffer (find-file openfile)))
-        (message "Opening file %s ..." openfile)
-        (unwind-protect
-            (progn
-              (coq-test-init)
-              (with-current-buffer buffer
-                (setq proof-splash-enable nil)
-                (normal-mode) ;; or (coq-mode)
-                (coq-mock body)))
-          (coq-test-exit)
-          (kill-buffer buffer)
-          (when rmfile (message "Removing file %s ..." rmfile))
-          (ignore-errors (delete-file rmfile))))))
+    (let* ((openfile (or file
+                         (concat (make-temp-file coq-test-file-prefix) ".v")))
+           ;; if FILE is nil, create a temporary Coq file, removed in the end
+           (rmfile (unless file openfile))
+           (buffer (find-file openfile)))    
+      (message "Opening file %s ..." openfile)
+      (unwind-protect
+          (progn
+            (coq-test-init)
+            (with-current-buffer buffer
+              (setq proof-splash-enable nil)
+              (normal-mode) ;; or (coq-mode)
+              (coq-mock body))))
+      (coq-test-exit)
+      (not-modified nil) ; Clear modification  
+      (kill-buffer buffer) 
+      (when rmfile (message "Removing file %s ..." rmfile))
+      (ignore-errors (delete-file rmfile)))))
 
 (defun coq-test-goto-before (comment)
   "Go just before COMMENT (a unique string in the .v file).
@@ -192,23 +193,37 @@ For example, COMMENT could be (*test-definition*)"
                      (with-current-buffer "*response*"
                        (buffer-substring-no-properties (point-min) (point-max)))))))))
 
-;; TODO
-;; (ert-deftest coq-test-lemma ()
-;;   (coq-init-exit
-;;    (lambda ()
-;;      (coq-test-cmd (car (read-lines "./test1.v")))
-;;      (should (equal "trois is defined"
-;; 		    (with-current-buffer "*response*"
-;; 		      (goto-char (point-min))
-;; 		      (buffer-substring-no-properties (line-beginning-position) (line-end-position) )
-;; 		      )
-;; 		    )))))
-
-;; (defun coq-test-main ()
-;;   (coq-mock #'coq-test-001))
-
-;; ;(ignore-errors (coq-test-exit))
-;; (coq-test-main)
+
+(ert-deftest coq-test-position ()
+  (coq-fixture-on-file
+   (coq-test-full-path "test1.v")
+   (lambda ()
+     (coq-test-goto-before " (*test-lemma*)")
+     (proof-goto-point)
+     (proof-shell-wait)
+     (should (equal (proof-queue-or-locked-end) (point))))))
+
+
+(ert-deftest coq-test-insert ()
+  (coq-fixture-on-file
+   (coq-test-full-path "test1.v")
+   (lambda ()
+     (coq-test-goto-before " (*test-lemma*)")
+     (proof-goto-point)
+     (proof-shell-wait)
+     (let ((proof-point (point)))
+       (coq-test-goto-before "(*test-insert*)")
+       (move-beginning-of-line nil)
+       (insert "\n")
+       (previous-line)
+       (insert "  (0)")
+       (coq-test-goto-after "(0)")
+       ;; The locked end point should go up compared to before 
+       (should (< (proof-queue-or-locked-end) proof-point)))))) 
+
+
+;;TODO
+;other tests
 
 (provide 'coq-tests)
 
diff --git a/ci/test1.v b/ci/test1.v
index 0a9ef963..fc1fc943 100644
--- a/ci/test1.v
+++ b/ci/test1.v
@@ -7,6 +7,6 @@ Eval compute in 10 * trois * trois.
 Lemma easy_proof : forall A : Prop, A -> A.
 Proof using .
   intros A.
-  intros proof_of_A.
+  intros proof_of_A. (*test-insert*)
   exact proof_of_A.
-Qed.
+Qed. (*test-lemma*) 
-- 
cgit v1.2.3


From 42c5e4cc7dd34232d5e73192d989ea1cdb24b33f Mon Sep 17 00:00:00 2001
From: Erik Martin-Dorel
Date: Fri, 1 May 2020 02:25:40 +0200
Subject: test: Slightly increase 'ert-batch-backtrace-right-margin

---
 ci/coq-tests.el | 1 +
 1 file changed, 1 insertion(+)

diff --git a/ci/coq-tests.el b/ci/coq-tests.el
index 4a620aa5..6d9a87ec 100644
--- a/ci/coq-tests.el
+++ b/ci/coq-tests.el
@@ -13,6 +13,7 @@
     (error "You should set 'coq-test-dir, or run coq-test.el from a file buffer.")))
 
 (setq debug-on-error t) ; open the debugger on error -- may be commented-out
+(setq ert-batch-backtrace-right-margin 79)
 
 (require 'subr-x) ;; for (string-trim)
 ;;(require 'ert-async)
-- 
cgit v1.2.3


From 5d3ca2c07392c36f9caea67bbbc4c14661c8fa08 Mon Sep 17 00:00:00 2001
From: Erik Martin-Dorel
Date: Fri, 1 May 2020 02:27:31 +0200
Subject: test: Add ert-problem-matcher for CI workflow

---
 .github/ert.json           | 20 ++++++++++++++++++++
 .github/workflows/test.yml |  5 +++++
 2 files changed, 25 insertions(+)
 create mode 100644 .github/ert.json

diff --git a/.github/ert.json b/.github/ert.json
new file mode 100644
index 00000000..df68cf26
--- /dev/null
+++ b/.github/ert.json
@@ -0,0 +1,20 @@
+{
+    "problemMatcher": [
+        {
+            "owner": "ert-problem-matcher",
+            "severity": "error",
+            "pattern": [
+                {
+                    "regexp": "^Test\\s+(.*?)\\s+condition:$"
+                },
+                {
+                    "regexp": "^\\s+(.*)$"
+                },
+                {
+                    "regexp": "^\\s+((?:FAILED|failed|SKIPPED|skipped|ABORTED|aborted|QUIT|quit)\\s+[0-9]+/[0-9]+\\s+.*)$",
+                    "message": 1
+                }
+            ]
+        }
+    ]
+}
diff --git a/.github/workflows/test.yml b/.github/workflows/test.yml
index 61f8e30d..e2a3ea4d 100644
--- a/.github/workflows/test.yml
+++ b/.github/workflows/test.yml
@@ -67,6 +67,9 @@ jobs:
     steps:
     - uses: actions/checkout@v2
 
+    - name: Add ert problem matcher
+      run: echo "::add-matcher::.github/ert.json"
+      
     - uses: coq-community/docker-coq-action@v1
       id: docker-coq-action
       with:
@@ -84,3 +87,5 @@ jobs:
           startGroup Run tests
             ./ci/test.sh
           endGroup
+
+  # - run: echo "::remove-matcher owner=ert-problem-matcher::"
-- 
cgit v1.2.3


From 31108dc120285765142b2bb4f44f34febbe79188 Mon Sep 17 00:00:00 2001
From: Erik Martin-Dorel
Date: Fri, 1 May 2020 03:36:27 +0200
Subject: fix: add some "sudo chown coq:coq" command

* This should solve the "(buffer-read-only #<buffer test1.v>)" error,
  probably due to permission issues.
---
 .github/workflows/test.yml | 1 +
 1 file changed, 1 insertion(+)

diff --git a/.github/workflows/test.yml b/.github/workflows/test.yml
index e2a3ea4d..db4bb766 100644
--- a/.github/workflows/test.yml
+++ b/.github/workflows/test.yml
@@ -85,6 +85,7 @@ jobs:
             sudo DEBIAN_FRONTEND=noninteractive apt-get install -y -q --no-install-recommends emacs
           endGroup
           startGroup Run tests
+            sudo chown -R coq:coq ./ci
             ./ci/test.sh
           endGroup
 
-- 
cgit v1.2.3


From 866a9da96a53c387050e7d8f7df9a0a3e35b435f Mon Sep 17 00:00:00 2001
From: Cyril Anaclet
Date: Mon, 4 May 2020 11:24:20 +0200
Subject: test: Add tests and some fix

---
 ci/coq-tests.el     |  45 +++++++++++-----
 ci/test1.v          |  14 ++++-
 ci/test_wholefile.v | 145 ++++++++++++++++++++++++++++++++++++++++++++++++++++
 3 files changed, 190 insertions(+), 14 deletions(-)
 create mode 100644 ci/test_wholefile.v

diff --git a/ci/coq-tests.el b/ci/coq-tests.el
index 6d9a87ec..323448ae 100644
--- a/ci/coq-tests.el
+++ b/ci/coq-tests.el
@@ -78,7 +78,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)
 
@@ -172,6 +172,12 @@ For example, COMMENT could be (*test-definition*)"
   (goto-char (point-min))
   (search-forward comment))
 
+(defun should-response (message)
+  (should (equal message
+		 (string-trim
+                  (with-current-buffer "*response*"
+                    (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
 
@@ -182,6 +188,7 @@ For example, COMMENT could be (*test-definition*)"
      ;; (should (process-list)) ; wouldn't be a strong enough assert.
      (should (get-process "coq")))))
 
+
 (ert-deftest coq-test-print ()
   (coq-fixture-on-file
    (coq-test-full-path "test1.v")
@@ -189,10 +196,7 @@ For example, COMMENT could be (*test-definition*)"
      (coq-test-goto-before "(*test-definition*)")
      (proof-goto-point)
      (proof-shell-wait)
-     (should (equal "trois is defined"
-		    (string-trim
-                     (with-current-buffer "*response*"
-                       (buffer-substring-no-properties (point-min) (point-max)))))))))
+     (should-response "trois is defined"))))
 
 
 (ert-deftest coq-test-position ()
@@ -200,9 +204,10 @@ For example, COMMENT could be (*test-definition*)"
    (coq-test-full-path "test1.v")
    (lambda ()
      (coq-test-goto-before " (*test-lemma*)")
+     (let ((proof-point (point)))
      (proof-goto-point)
      (proof-shell-wait)
-     (should (equal (proof-queue-or-locked-end) (point))))))
+     (should (equal (proof-queue-or-locked-end) proof-point))))))
 
 
 (ert-deftest coq-test-insert ()
@@ -216,15 +221,31 @@ For example, COMMENT could be (*test-definition*)"
        (coq-test-goto-before "(*test-insert*)")
        (move-beginning-of-line nil)
        (insert "\n")
-       (previous-line)
-       (insert "  (0)")
-       (coq-test-goto-after "(0)")
        ;; The locked end point should go up compared to before 
-       (should (< (proof-queue-or-locked-end) proof-point)))))) 
+       (should (< (proof-queue-or-locked-end) proof-point))))))
+
+
+(ert-deftest coq-test-lemma-false ()
+  (coq-fixture-on-file
+   (coq-test-full-path "test1.v")
+   (lambda ()
+     (coq-test-goto-before " (*test-lemma2*)")
+     (let ((proof-point (save-excursion (coq-test-goto-after "(*error*)")))) 
+     (proof-goto-point)
+     (proof-shell-wait)
+     (should-response "Error: Unable to unify \"false\" with \"true\".")
+     (should (equal (proof-queue-or-locked-end) proof-point))))))
+
 
+(ert-deftest coq-test-wholefile ()
+  (coq-fixture-on-file
+   (coq-test-full-path "test_wholefile.v")
+   (lambda ()
+     (let ((proof-point (save-excursion (coq-test-goto-after "(*end here*)"))))
+     (proof-process-buffer)
+     (proof-shell-wait)
+     (should (equal (proof-queue-or-locked-end)  proof-point))))))
 
-;;TODO
-;other tests
 
 (provide 'coq-tests)
 
diff --git a/ci/test1.v b/ci/test1.v
index fc1fc943..3812adbd 100644
--- a/ci/test1.v
+++ b/ci/test1.v
@@ -1,7 +1,7 @@
 Definition trois := 3. (*test-definition*)
 Print trois.
 Eval compute in 10 * trois * trois.
-
+ 
 
 
 Lemma easy_proof : forall A : Prop, A -> A.
@@ -9,4 +9,14 @@ Proof using .
   intros A.
   intros proof_of_A. (*test-insert*)
   exact proof_of_A.
-Qed. (*test-lemma*) 
+Qed. (*test-lemma*)
+
+Lemma false_proof : forall A B : bool, A = B. 
+Proof.
+  intros A B.
+  destruct A.
+  destruct B.
+  reflexivity. (*error*)
+  reflexivity.
+Qed. (*test-lemma2*)
+  
diff --git a/ci/test_wholefile.v b/ci/test_wholefile.v
new file mode 100644
index 00000000..0a87d9a6
--- /dev/null
+++ b/ci/test_wholefile.v
@@ -0,0 +1,145 @@
+(*taking from coq.inria.fr *)
+
+Require Export ArithRing.
+Require Export Compare_dec.
+Require Export Wf_nat.
+Require Export Arith.
+Require Export Omega.
+
+Theorem minus_minus : forall a b c : nat, a - b - c = a - (b + c).
+intros a; elim a; auto.
+intros n' Hrec b; case b; auto.
+Qed.
+
+Remark expand_mult2 : forall x : nat, 2 * x = x + x.
+intros x; ring.
+Qed.
+
+Theorem lt_neq : forall x y : nat, x < y -> x <> y.
+unfold not in |- *; intros x y H H1; elim (lt_irrefl x);
+ pattern x at 2 in |- *; rewrite H1; auto.
+Qed.
+Hint Resolve lt_neq.
+
+Theorem monotonic_inverse :
+ forall f : nat -> nat,
+ (forall x y : nat, x < y -> f x < f y) ->
+ forall x y : nat, f x < f y -> x < y.
+intros f Hmon x y Hlt; case (le_gt_dec y x); auto.
+intros Hle; elim (le_lt_or_eq _ _ Hle).
+intros Hlt'; elim (lt_asym _ _ Hlt); apply Hmon; auto.
+intros Heq; elim (lt_neq _ _ Hlt); rewrite Heq; auto.
+Qed.
+
+Theorem mult_lt : forall a b c : nat, c <> 0 -> a < b -> a * c < b * c.
+intros a b c; elim c.
+intros H; elim H; auto.
+intros c'; case c'.
+intros; omega.
+intros c'' Hrec Hneq Hlt;
+ repeat rewrite <- (fun x : nat => mult_n_Sm x (S c'')).
+auto with *.
+Qed.
+
+Remark add_sub_square_identity :
+ forall a b : nat,
+ (b + a - b) * (b + a - b) = (b + a) * (b + a) + b * b - 2 * ((b + a) * b).
+intros a b; rewrite minus_plus.
+repeat rewrite mult_plus_distr_r || rewrite <- (mult_comm (b + a)).
+replace (b * b + a * b + (b * a + a * a) + b * b) with
+ (b * b + a * b + (b * b + a * b + a * a)); try (ring; fail).
+rewrite expand_mult2; repeat rewrite minus_plus; auto with *.
+Qed.
+
+Theorem sub_square_identity :
+ forall a b : nat, b <= a -> (a - b) * (a - b) = a * a + b * b - 2 * (a * b).
+intros a b H; rewrite (le_plus_minus b a H); apply add_sub_square_identity.
+Qed.
+
+Theorem square_monotonic : forall x y : nat, x < y -> x * x < y * y.
+intros x; case x.
+intros y; case y; simpl in |- *; auto with *.
+intros x' y Hlt; apply lt_trans with (S x' * y).
+rewrite (mult_comm (S x') y); apply mult_lt; auto.
+apply mult_lt; omega.
+Qed.
+
+Theorem root_monotonic : forall x y : nat, x * x < y * y -> x < y.
+exact (monotonic_inverse (fun x : nat => x * x) square_monotonic).
+Qed.
+
+Remark square_recompose : forall x y : nat, x * y * (x * y) = x * x * (y * y).
+intros; ring.
+Qed.
+
+Remark mult2_recompose : forall x y : nat, x * (2 * y) = x * 2 * y.
+intros; ring.
+Qed.
+Section sqrt2_decrease.
+Variables (p q : nat) (pos_q : 0 < q) (hyp_sqrt : p * p = 2 * (q * q)).
+
+Theorem sqrt_q_non_zero : 0 <> q * q.
+generalize pos_q; case q.
+intros H; elim (lt_n_O 0); auto.
+intros n H.
+simpl in |- *; discriminate.
+Qed.
+Hint Resolve sqrt_q_non_zero.
+
+Ltac solve_comparison :=
+  apply root_monotonic; repeat rewrite square_recompose; rewrite hyp_sqrt;
+   rewrite mult2_recompose; apply mult_lt; auto with arith.
+
+Theorem comparison1 : q < p.
+replace q with (1 * q); try ring.
+replace p with (1 * p); try ring.
+solve_comparison.
+Qed.
+
+Theorem comparison2 : 2 * p < 3 * q.
+solve_comparison.
+Qed.
+
+Theorem comparison3 : 4 * q < 3 * p.
+solve_comparison.
+Qed.
+Hint Resolve comparison1 comparison2 comparison3: arith.
+
+Theorem comparison4 : 3 * q - 2 * p < q.
+apply plus_lt_reg_l with (2 * p).
+rewrite <- le_plus_minus; try (simple apply lt_le_weak; auto with arith).
+replace (3 * q) with (2 * q + q); try ring.
+apply plus_lt_le_compat; auto.
+repeat rewrite (mult_comm 2); apply mult_lt; auto with arith.
+Qed.
+
+Remark mult_minus_distr_l : forall a b c : nat, a * (b - c) = a * b - a * c.
+intros a b c; repeat rewrite (mult_comm a); apply mult_minus_distr_r.
+Qed.
+
+Remark minus_eq_decompose :
+ forall a b c d : nat, a = b -> c = d -> a - c = b - d.
+intros a b c d H H0; rewrite H; rewrite H0; auto.
+Qed.
+
+Theorem new_equality :
+ (3 * p - 4 * q) * (3 * p - 4 * q) = 2 * ((3 * q - 2 * p) * (3 * q - 2 * p)).
+repeat rewrite sub_square_identity; auto with arith.
+repeat rewrite square_recompose; rewrite mult_minus_distr_l.
+apply minus_eq_decompose; try rewrite hyp_sqrt; ring.
+Qed.
+End sqrt2_decrease.
+Hint Resolve lt_le_weak comparison2: sqrt.
+
+Theorem sqrt2_not_rational :
+ forall p q : nat, q <> 0 -> p * p = 2 * (q * q) -> False.
+intros p q; generalize p; clear p; elim q using (well_founded_ind lt_wf).
+clear q; intros q Hrec p Hneq; generalize (neq_O_lt _ (sym_not_equal Hneq));
+ intros Hlt_O_q Heq.
+apply (Hrec (3 * q - 2 * p) (comparison4 _ _ Hlt_O_q Heq) (3 * p - 4 * q)).
+apply sym_not_equal; apply lt_neq; apply plus_lt_reg_l with (2 * p);
+ rewrite <- plus_n_O; rewrite <- le_plus_minus; auto with *.
+apply new_equality; auto.
+Qed.
+
+(*end here*)
-- 
cgit v1.2.3


From 3bc39fbd726676e5d1a650b683f0b5d72dbd1c3b Mon Sep 17 00:00:00 2001
From: Erik Martin-Dorel
Date: Mon, 4 May 2020 14:23:58 +0200
Subject: fix: Tweak comments and workaround ProofGeneral/PG#485

---
 ci/test_wholefile.v | 5 ++---
 1 file changed, 2 insertions(+), 3 deletions(-)

diff --git a/ci/test_wholefile.v b/ci/test_wholefile.v
index 0a87d9a6..d8b57d20 100644
--- a/ci/test_wholefile.v
+++ b/ci/test_wholefile.v
@@ -1,4 +1,4 @@
-(*taking from coq.inria.fr *)
+(* taken from https://coq.inria.fr/distrib/8.2/contribs/QArithSternBrocot.sqrt2.html *)
 
 Require Export ArithRing.
 Require Export Compare_dec.
@@ -133,6 +133,7 @@ Hint Resolve lt_le_weak comparison2: sqrt.
 
 Theorem sqrt2_not_rational :
  forall p q : nat, q <> 0 -> p * p = 2 * (q * q) -> False.
+Proof.
 intros p q; generalize p; clear p; elim q using (well_founded_ind lt_wf).
 clear q; intros q Hrec p Hneq; generalize (neq_O_lt _ (sym_not_equal Hneq));
  intros Hlt_O_q Heq.
@@ -141,5 +142,3 @@ apply sym_not_equal; apply lt_neq; apply plus_lt_reg_l with (2 * p);
  rewrite <- plus_n_O; rewrite <- le_plus_minus; auto with *.
 apply new_equality; auto.
 Qed.
-
-(*end here*)
-- 
cgit v1.2.3


From f3e0245173bae40c132f049b8352a41d4c08ab48 Mon Sep 17 00:00:00 2001
From: Erik Martin-Dorel
Date: Mon, 4 May 2020 14:26:04 +0200
Subject: fix: ert.json

* The zone between "Test ... condition:" & "FAILED ..." can have more
  than 1 line!
---
 .github/ert.json | 6 ------
 1 file changed, 6 deletions(-)

diff --git a/.github/ert.json b/.github/ert.json
index df68cf26..02dc5548 100644
--- a/.github/ert.json
+++ b/.github/ert.json
@@ -4,12 +4,6 @@
             "owner": "ert-problem-matcher",
             "severity": "error",
             "pattern": [
-                {
-                    "regexp": "^Test\\s+(.*?)\\s+condition:$"
-                },
-                {
-                    "regexp": "^\\s+(.*)$"
-                },
                 {
                     "regexp": "^\\s+((?:FAILED|failed|SKIPPED|skipped|ABORTED|aborted|QUIT|quit)\\s+[0-9]+/[0-9]+\\s+.*)$",
                     "message": 1
-- 
cgit v1.2.3


From 141fa6c9dfa50a4df94eb98ade46c4c1a08b4b9c Mon Sep 17 00:00:00 2001
From: Erik Martin-Dorel
Date: Mon, 4 May 2020 14:40:47 +0200
Subject: refactor: Remove unneeded auxiliary functions & Use "coq-" prefix

---
 ci/coq-tests.el | 29 +++++++++--------------------
 1 file changed, 9 insertions(+), 20 deletions(-)

diff --git a/ci/coq-tests.el b/ci/coq-tests.el
index 323448ae..41bbf0aa 100644
--- a/ci/coq-tests.el
+++ b/ci/coq-tests.el
@@ -56,18 +56,6 @@
 
 (defconst coq-test-file-prefix "coq_test_")
 
-(defun get-string-from-file (filePath)
-  "Return filePath's file content."
-  (with-temp-buffer
-    (insert-file-contents filePath)
-    (buffer-string)))
-
-(defun read-lines (filePath)
-  "Return a list of lines of a file at filePath."
-  (with-temp-buffer
-    (insert-file-contents filePath)
-    (split-string (buffer-string) "\n" t)))
-
 (defun coq-test-init ()
   "Ensure `coq' is loaded."
   (unless (featurep 'coq)
@@ -85,7 +73,7 @@
 ;; DEFINITION OF MOCKS, SEE `coq-mock' BELOW
 ;; Another solution would consist in using el-mock, mentioned in:
 ;; https://www.gnu.org/software/emacs/manual/html_mono/ert.html#Mocks-and-Stubs
-(defun mock-proof-display-three-b (&rest rest)
+(defun coq-mock-proof-display-three-b (&rest rest)
   (message (concat "Skipping proof-display-three-b on input: "
                    (pp-to-string rest)))
   ; Result:
@@ -108,7 +96,7 @@
 (defun coq-mock (f)
   (require 'pg-response) ; load the feature defining proof-display-three-b first
    (cl-letf (;((symbol-function 'foo) #'mock-foo)
-             ((symbol-function 'proof-display-three-b) #'mock-proof-display-three-b))
+             ((symbol-function 'proof-display-three-b) #'coq-mock-proof-display-three-b))
      (funcall f)))
 ;; Run <C-x C-e> on:
 ;; (coq-mock #'main)
@@ -172,7 +160,7 @@ For example, COMMENT could be (*test-definition*)"
   (goto-char (point-min))
   (search-forward comment))
 
-(defun should-response (message)
+(defun coq-should-response (message)
   (should (equal message
 		 (string-trim
                   (with-current-buffer "*response*"
@@ -196,7 +184,7 @@ For example, COMMENT could be (*test-definition*)"
      (coq-test-goto-before "(*test-definition*)")
      (proof-goto-point)
      (proof-shell-wait)
-     (should-response "trois is defined"))))
+     (coq-should-response "trois is defined"))))
 
 
 (ert-deftest coq-test-position ()
@@ -233,7 +221,7 @@ For example, COMMENT could be (*test-definition*)"
      (let ((proof-point (save-excursion (coq-test-goto-after "(*error*)")))) 
      (proof-goto-point)
      (proof-shell-wait)
-     (should-response "Error: Unable to unify \"false\" with \"true\".")
+     (coq-should-response "Error: Unable to unify \"false\" with \"true\".")
      (should (equal (proof-queue-or-locked-end) proof-point))))))
 
 
@@ -241,11 +229,12 @@ For example, COMMENT could be (*test-definition*)"
   (coq-fixture-on-file
    (coq-test-full-path "test_wholefile.v")
    (lambda ()
-     (let ((proof-point (save-excursion (coq-test-goto-after "(*end here*)"))))
+     (let ((proof-point (save-excursion
+			  (coq-test-goto-before "Theorem")
+			  (search-forward "Qed."))))
      (proof-process-buffer)
      (proof-shell-wait)
-     (should (equal (proof-queue-or-locked-end)  proof-point))))))
-
+     (should (equal (proof-queue-or-locked-end) proof-point))))))
 
 (provide 'coq-tests)
 
-- 
cgit v1.2.3


From 395f6f076ed4061417b4a5747797dab413ad2453 Mon Sep 17 00:00:00 2001
From: Erik Martin-Dorel
Date: Mon, 4 May 2020 14:50:11 +0200
Subject: docs: Add docstrings in tests

---
 ci/coq-tests.el | 18 ++++++++++++------
 1 file changed, 12 insertions(+), 6 deletions(-)

diff --git a/ci/coq-tests.el b/ci/coq-tests.el
index 41bbf0aa..e88736e9 100644
--- a/ci/coq-tests.el
+++ b/ci/coq-tests.el
@@ -169,7 +169,8 @@ For example, COMMENT could be (*test-definition*)"
 ;; 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 coq-test-running ()
+(ert-deftest 010_coq-test-running ()
+  "Test that the coqtop process is started properly."
   (coq-fixture-on-file nil
    (lambda ()
      (coq-test-cmd "Print 0.")
@@ -177,7 +178,8 @@ For example, COMMENT could be (*test-definition*)"
      (should (get-process "coq")))))
 
 
-(ert-deftest coq-test-print ()
+(ert-deftest 020_coq-test-definition ()
+  "Test *response* output after asserting a Definition."
   (coq-fixture-on-file
    (coq-test-full-path "test1.v")
    (lambda ()
@@ -187,7 +189,8 @@ For example, COMMENT could be (*test-definition*)"
      (coq-should-response "trois is defined"))))
 
 
-(ert-deftest coq-test-position ()
+(ert-deftest 030_coq-test-position ()
+  "Test locked region after Qed."
   (coq-fixture-on-file
    (coq-test-full-path "test1.v")
    (lambda ()
@@ -198,7 +201,8 @@ For example, COMMENT could be (*test-definition*)"
      (should (equal (proof-queue-or-locked-end) proof-point))))))
 
 
-(ert-deftest coq-test-insert ()
+(ert-deftest 040_coq-test-insert ()
+  "Test retract on insert from Qed."
   (coq-fixture-on-file
    (coq-test-full-path "test1.v")
    (lambda ()
@@ -213,7 +217,8 @@ For example, COMMENT could be (*test-definition*)"
        (should (< (proof-queue-or-locked-end) proof-point))))))
 
 
-(ert-deftest coq-test-lemma-false ()
+(ert-deftest 050_coq-test-lemma-false ()
+  "Test retract on proof error."
   (coq-fixture-on-file
    (coq-test-full-path "test1.v")
    (lambda ()
@@ -225,7 +230,8 @@ For example, COMMENT could be (*test-definition*)"
      (should (equal (proof-queue-or-locked-end) proof-point))))))
 
 
-(ert-deftest coq-test-wholefile ()
+(ert-deftest 060_coq-test-wholefile ()
+  "Test `proof-process-buffer'."
   (coq-fixture-on-file
    (coq-test-full-path "test_wholefile.v")
    (lambda ()
-- 
cgit v1.2.3


From 6f2f532af7d065779bca1e7c994d065f50338d9c Mon Sep 17 00:00:00 2001
From: Erik Martin-Dorel
Date: Mon, 4 May 2020 14:54:43 +0200
Subject: test: Remove "Proof." workaround

---
 ci/test_wholefile.v | 1 -
 1 file changed, 1 deletion(-)

diff --git a/ci/test_wholefile.v b/ci/test_wholefile.v
index d8b57d20..f947d1c5 100644
--- a/ci/test_wholefile.v
+++ b/ci/test_wholefile.v
@@ -133,7 +133,6 @@ Hint Resolve lt_le_weak comparison2: sqrt.
 
 Theorem sqrt2_not_rational :
  forall p q : nat, q <> 0 -> p * p = 2 * (q * q) -> False.
-Proof.
 intros p q; generalize p; clear p; elim q using (well_founded_ind lt_wf).
 clear q; intros q Hrec p Hneq; generalize (neq_O_lt _ (sym_not_equal Hneq));
  intros Hlt_O_q Heq.
-- 
cgit v1.2.3


From dd6c458085d4050411fa4bd1ad4aca26e4145950 Mon Sep 17 00:00:00 2001
From: Erik Martin-Dorel
Date: Mon, 4 May 2020 14:59:50 +0200
Subject: refactor: Rename test file

---
 ci/coq-tests.el    |  8 ++++----
 ci/test1.v         | 22 ----------------------
 ci/test_stepwise.v | 22 ++++++++++++++++++++++
 3 files changed, 26 insertions(+), 26 deletions(-)
 delete mode 100644 ci/test1.v
 create mode 100644 ci/test_stepwise.v

diff --git a/ci/coq-tests.el b/ci/coq-tests.el
index e88736e9..ac97a110 100644
--- a/ci/coq-tests.el
+++ b/ci/coq-tests.el
@@ -181,7 +181,7 @@ 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 "test1.v")
+   (coq-test-full-path "test_stepwise.v")
    (lambda ()
      (coq-test-goto-before "(*test-definition*)")
      (proof-goto-point)
@@ -192,7 +192,7 @@ 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 "test1.v")
+   (coq-test-full-path "test_stepwise.v")
    (lambda ()
      (coq-test-goto-before " (*test-lemma*)")
      (let ((proof-point (point)))
@@ -204,7 +204,7 @@ 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 "test1.v")
+   (coq-test-full-path "test_stepwise.v")
    (lambda ()
      (coq-test-goto-before " (*test-lemma*)")
      (proof-goto-point)
@@ -220,7 +220,7 @@ 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 "test1.v")
+   (coq-test-full-path "test_stepwise.v")
    (lambda ()
      (coq-test-goto-before " (*test-lemma2*)")
      (let ((proof-point (save-excursion (coq-test-goto-after "(*error*)")))) 
diff --git a/ci/test1.v b/ci/test1.v
deleted file mode 100644
index 3812adbd..00000000
--- a/ci/test1.v
+++ /dev/null
@@ -1,22 +0,0 @@
-Definition trois := 3. (*test-definition*)
-Print trois.
-Eval compute in 10 * trois * trois.
- 
-
-
-Lemma easy_proof : forall A : Prop, A -> A.
-Proof using .
-  intros A.
-  intros proof_of_A. (*test-insert*)
-  exact proof_of_A.
-Qed. (*test-lemma*)
-
-Lemma false_proof : forall A B : bool, A = B. 
-Proof.
-  intros A B.
-  destruct A.
-  destruct B.
-  reflexivity. (*error*)
-  reflexivity.
-Qed. (*test-lemma2*)
-  
diff --git a/ci/test_stepwise.v b/ci/test_stepwise.v
new file mode 100644
index 00000000..3812adbd
--- /dev/null
+++ b/ci/test_stepwise.v
@@ -0,0 +1,22 @@
+Definition trois := 3. (*test-definition*)
+Print trois.
+Eval compute in 10 * trois * trois.
+ 
+
+
+Lemma easy_proof : forall A : Prop, A -> A.
+Proof using .
+  intros A.
+  intros proof_of_A. (*test-insert*)
+  exact proof_of_A.
+Qed. (*test-lemma*)
+
+Lemma false_proof : forall A B : bool, A = B. 
+Proof.
+  intros A B.
+  destruct A.
+  destruct B.
+  reflexivity. (*error*)
+  reflexivity.
+Qed. (*test-lemma2*)
+  
-- 
cgit v1.2.3


From 5900b15ec4dc6fd344c641c2d676157be70bd551 Mon Sep 17 00:00:00 2001
From: Pierre Courtieu
Date: Mon, 4 May 2020 14:40:59 +0200
Subject: Fixing #485, bug on proof without "Proof".

Due to a re-search that should fail silently.
---
 coq/coq.el | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/coq/coq.el b/coq/coq.el
index cb43f3a9..ca1e36a1 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -2661,7 +2661,7 @@ built from the list of strings in SUGGESTED."
   (with-current-buffer proof-script-buffer
     (save-excursion
       (goto-char (span-start span))
-      (let* ((endpos (re-search-forward coq-proof-using-regexp)))
+      (let* ((endpos (re-search-forward coq-proof-using-regexp (span-end span) t)))
         (when endpos
           (let* ((suggested (span-property span 'dependencies))
                  (proof-pos (match-beginning 0))
-- 
cgit v1.2.3


From 4f25bf77571205bcc32d6d2cbf00d516c670243c Mon Sep 17 00:00:00 2001
From: Cyril Anaclet
Date: Mon, 4 May 2020 17:12:14 +0200
Subject: add test

---
 ci/coq-tests.el | 12 ++++++++++++
 1 file changed, 12 insertions(+)

diff --git a/ci/coq-tests.el b/ci/coq-tests.el
index ac97a110..015b831e 100644
--- a/ci/coq-tests.el
+++ b/ci/coq-tests.el
@@ -242,6 +242,18 @@ For example, COMMENT could be (*test-definition*)"
      (proof-shell-wait)
      (should (equal (proof-queue-or-locked-end) proof-point))))))
 
+
+(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")
+   (lambda ()
+     (proof-process-buffer)
+     (proof-shell-wait)
+     (goto-char (point-min))
+     (insert "(*.*)")
+     (should (equal (proof-queue-or-locked-end) 1)))))
+
 (provide 'coq-tests)
 
 ;;; coq-tests.el ends here
-- 
cgit v1.2.3


From 63dc6a6bc23f2eff3e3c3bbee9e79d4097d8f139 Mon Sep 17 00:00:00 2001
From: Erik Martin-Dorel
Date: Mon, 4 May 2020 21:54:31 +0200
Subject: docs: Add a comment in ci/test_wholefile.v

* see also https://github.com/ProofGeneral/PG/issues/485
---
 ci/test_wholefile.v | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/ci/test_wholefile.v b/ci/test_wholefile.v
index f947d1c5..9deee01d 100644
--- a/ci/test_wholefile.v
+++ b/ci/test_wholefile.v
@@ -1,4 +1,6 @@
 (* taken from https://coq.inria.fr/distrib/8.2/contribs/QArithSternBrocot.sqrt2.html *)
+(* Note: this file contains no "Proof" command (invariant to preserve)
+   in order to exercise 070_coq-test-regression-wholefile-no-proof. *)
 
 Require Export ArithRing.
 Require Export Compare_dec.
-- 
cgit v1.2.3