From 0ae25c5ae3f401ad9cabe16b1636ff2e11da874c Mon Sep 17 00:00:00 2001
From: Cyril Anaclet <cyril.anaclet@gmail.com>
Date: Wed, 29 Apr 2020 18:10:40 +0200
Subject: [PATCH] [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 5c1e7d83e..4a620aa5f 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 0a9ef9633..fc1fc943a 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*)