Merge pull request #486 from ProofGeneral/coq-tests-for-master

Coq tests for master

.github/ert.json

@@ -0,0 +1,14 @@
+{
+    "problemMatcher": [
+        {
+            "owner": "ert-problem-matcher",
+            "severity": "error",
+            "pattern": [
+                {
+                    "regexp": "^\\s+((?:FAILED|failed|SKIPPED|skipped|ABORTED|aborted|QUIT|quit)\\s+[0-9]+/[0-9]+\\s+.*)$",
+                    "message": 1
+                }
+            ]
+        }
+    ]
+}

.github/workflows/test.yml

@@ -3,8 +3,9 @@ name: CI
 on:
   push:
     branches:
-      - master
-      - hybrid
+      #- master
+      #- hybrid
+      - "**"
   pull_request:
     branches:
       - '**'
@@ -66,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:
@@ -81,5 +85,8 @@ 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
+
+  # - run: echo "::remove-matcher owner=ert-problem-matcher::"

ci/coq-tests.el

@@ -5,12 +5,19 @@
 
 ;;;  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))
+
+(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
+(setq ert-batch-backtrace-right-margin 79)
 
-(require 'ert-async)
-;(setq ert-async-timeout 2)
+(require 'subr-x) ;; for (string-trim)
+;;(require 'ert-async)
+;;(setq ert-async-timeout 2)
 
 ;;; Code:
 
@@ -43,50 +50,30 @@
 ; 
 ; (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 coq-test-init ()
   "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")))
 
 (defun coq-test-exit ()
   "Exit the Coq process."
-  (proof-shell-exit t))
+  (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:
 ;; 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:
@@ -109,31 +96,164 @@
 (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)
 
 (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)))
-
-(defun coq-test-001 ()
-  ;; TODO: retrieve the test status, maybe by changing the function above
-  (coq-test-cmd "Print nat."))
+  ;;(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 ..." 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).
+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))
+
+(defun coq-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
 
-(defun coq-test-main ()
-  (coq-mock #'coq-test-001))
+(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.")
+     ;; (should (process-list)) ; wouldn't be a strong enough assert.
+     (should (get-process "coq")))))
+
 
-;(ignore-errors (coq-test-exit))
-(coq-test-main)
+(ert-deftest 020_coq-test-definition ()
+  "Test *response* output after asserting a Definition."
+  (coq-fixture-on-file
+   (coq-test-full-path "test_stepwise.v")
+   (lambda ()
+     (coq-test-goto-before "(*test-definition*)")
+     (proof-goto-point)
+     (proof-shell-wait)
+     (coq-should-response "trois is defined"))))
+
+
+(ert-deftest 030_coq-test-position ()
+  "Test locked region after Qed."
+  (coq-fixture-on-file
+   (coq-test-full-path "test_stepwise.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) proof-point))))))
+
+
+(ert-deftest 040_coq-test-insert ()
+  "Test retract on insert from Qed."
+  (coq-fixture-on-file
+   (coq-test-full-path "test_stepwise.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")
+       ;; The locked end point should go up compared to before 
+       (should (< (proof-queue-or-locked-end) proof-point))))))
+
+
+(ert-deftest 050_coq-test-lemma-false ()
+  "Test retract on proof error."
+  (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*)")))) 
+     (proof-goto-point)
+     (proof-shell-wait)
+     (coq-should-response "Error: Unable to unify \"false\" with \"true\".")
+     (should (equal (proof-queue-or-locked-end) proof-point))))))
+
+
+(ert-deftest 060_coq-test-wholefile ()
+  "Test `proof-process-buffer'."
+  (coq-fixture-on-file
+   (coq-test-full-path "test_wholefile.v")
+   (lambda ()
+     (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))))))
+
+
+(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)
-;;; learn-ocaml-tests.el ends here
+
+;;; coq-tests.el ends here

ci/test.sh

@@ -29,10 +29,11 @@ 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\"))"
+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

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