Extend testing

2 files changed, 90 insertions, 27 deletions

diff --git a/generic/pg-autotest.el b/generic/pg-autotest.el
index 3e9f2961..d084febd 100644
--- a/generic/pg-autotest.el
+++ b/generic/pg-autotest.el
@@ -5,6 +5,10 @@
 ;;
 ;; License:   GPL (GNU GENERAL PUBLIC LICENSE)
 ;;
+;;; Commentary:
+;;
+;; Support for running a series of scripted UI tests.
+;;
 ;; TODO:
 ;; -- fix failure handling for scriptfile
 ;; -- add macros for defining test suites
@@ -13,13 +17,13 @@
 ;;
 ;; $Id$
 
+(require 'proof-splash)
+(setq proof-splash-enable nil)		; prevent splash when testing
+
 (require 'proof)
 (require 'proof-shell)
+(require 'proof-utils)
 
-;;; Commentary:
-;;
-;; Support for running a series of scripted UI tests.
-;;
 
 ;;; Code:
 
@@ -31,6 +35,10 @@
 
 (setq debug-on-error t) 		;; enable in case a test goes wrong
 
+(defadvice proof-debug (before proof-debug-to-log (msg &rest args))
+  "Output the debug message to the test log."
+  (pg-autotest-message msg args))
+
 ;;; Some utilities
 
 (defun pg-autotest-find-file (file)
@@ -162,22 +170,52 @@ An error is signalled if scripting doesn't complete."
 
 (defun pg-autotest-test-script-randomjumps (file jumps)
   "Load FILE and process in it by jumping around randomly JUMPS times.
+Additionally some edits are made but undone.
 This should be robust against synchronization errors; we test this by
 completely processing the buffer as the last step."
   (pg-autotest-find-file-restart file)
   (while (> jumps 0)
-    (let ((random-point   (random (point-max))))
-      ;; TODO: random use of retract/process whole buffer too
-      (pg-autotest-message
-       "         random jump to point: %d" random-point)
-      (goto-char random-point)
-      (unless (if (>= (point) (proof-unprocessed-begin))
-		  (proof-only-whitespace-to-locked-region-p))
-	(proof-goto-point)
-	(proof-shell-wait) ;; TODO: check no prover error.
-	(decf jumps))))
-  (proof-process-buffer)
-  (proof-shell-wait)
+    (let* ((random-point     (random (point-max)))
+	   (random-edit      nil) ; (< 20 (random 100)))
+	   (random-other     (< 10 (random 100)))
+	   (random-thing     (and random-other (random 3))))
+      (cond
+       ((and (eq random-thing 0)
+	     (not (proof-locked-region-full-p)))
+	(pg-autotest-message
+	 " random jump: processing whole buffer")
+	(proof-process-buffer)
+	(proof-shell-wait)
+	(decf jumps))
+
+	((and (eq random-thing 1) 
+	      (not (proof-locked-region-empty-p)))
+	 (pg-autotest-message
+	  " random jump: retracting whole buffer")
+	 (proof-retract-buffer)
+	 (proof-shell-wait)
+	 (decf jumps))
+
+	(t
+	 (pg-autotest-message
+	  " random jump: going to point: %d" random-point))
+	 (goto-char random-point)
+	 (unless (if (>= (point) (proof-unprocessed-begin))
+		     (proof-only-whitespace-to-locked-region-p))
+	   (proof-goto-point)
+	   (if (eq random-thing 2)
+	       (progn ;; interrupt after 2 secs
+		 (sit-for 1)
+		 (sit-for 1)
+		 (when proof-shell-busy
+		   (pg-autotest-message
+		    " random jump: interrupting prover")
+		   (proof-interrupt-process)))
+	     (proof-shell-wait))
+	   (decf jumps)))))
+  (unless (proof-locked-region-full-p)
+    (proof-process-buffer)
+    (proof-shell-wait))
   (pg-autotest-test-assert-processed file))
 
 (defun pg-autotest-test-retract-file (file)
@@ -194,9 +232,10 @@ completely processing the buffer as the last step."
 
 (defun pg-autotest-test-assert-full ()
   "Check that current buffer has been fully processed."
-    (unless (proof-locked-region-full-p)
-      (error (format "Locked region in buffer `%s' is not full"
-		     (buffer-name)))))
+  (proof-shell-wait)
+  (unless (proof-locked-region-full-p)
+    (error (format "Locked region in buffer `%s' is not full"
+		   (buffer-name)))))
 
 (defun pg-autotest-test-assert-unprocessed (file)
   "Check that FILE has been fully unprocessed."
diff --git a/isar/isar-autotest.el b/isar/isar-autotest.el
index 19fe473a..9c63140b 100644
--- a/isar/isar-autotest.el
+++ b/isar/isar-autotest.el
@@ -5,6 +5,9 @@
 ;; $Id$
 ;;
 
+(defvar isar-long-tests nil
+  "Whether or not to perform lengthy tests")
+
 (eval-when-compile
   (require 'cl))
 
@@ -17,6 +20,9 @@
 
 (require 'pg-autotest)
 
+(setq proof-general-debug t)	 ; for development: see debug messages
+
+
 (unless noninteractive
 
   (pg-autotest log ".autotest.log")  ; convention
@@ -27,20 +33,38 @@
   (pg-autotest script-wholefile "isar/Example.thy")
   (pg-autotest script-wholefile "isar/Example-Tokens.thy")
 
-  (pg-autotest remark "Larger files...")
-  (pg-autotest eval (isar-tracing:auto-quickcheck-toggle 0))
-  (pg-autotest eval (isar-tracing:auto-solve-toggle 0)) ; autosolve hammers this!
-  (pg-autotest eval (proof-full-annotation-toggle 0))
-  (pg-autotest script-wholefile "etc/isar/AHundredTheorems.thy")
+  (pg-autotest remark "Testing prove-as-you-go (not replay)")
+  (find-file ".autotest.thy")
+  (erase-buffer) ; just in case exists
+  (setq buffer-file-name nil)
+  (pg-autotest eval (proof-electric-terminator-toggle 1))
+  (pg-autotest eval (insert "theory Example imports Main begin ")) ; no \n
+  (proof-electric-terminator)
+  (pg-autotest eval (insert "theorem and_comms: \"A & B --> B & A\"\n"))
+  (proof-electric-terminator)
+  (pg-autotest eval (insert "apply auto done\n"))
+  (pg-autotest eval (insert "end"))
+  (proof-electric-terminator)
+  (pg-autotest assert-full)
+  (set-buffer-modified-p nil)
+  (kill-buffer ".autotest.thy")
 
   (pg-autotest remark "Now in tokens mode")
   (pg-autotest eval (proof-unicode-tokens-toggle))
   (pg-autotest script-wholefile "isar/Example-Tokens.thy")
-  (pg-autotest script-wholefile "isar/ex/Tarski.thy")
 
-  (pg-autotest remark "Testing random jumps")
+  (pg-autotest remark "Testing random jumps and edits")
   (pg-autotest script-randomjumps "isar/Example.thy" 5)
-  (pg-autotest script-randomjumps "isar/ex/Tarski.thy" 10) ; better test?
+
+  (when isar-long-tests
+      (pg-autotest remark "Larger files...")
+      (pg-autotest eval (isar-tracing:auto-quickcheck-toggle 0))
+      (pg-autotest eval (isar-tracing:auto-solve-toggle 0)) ; autosolve hammers this!
+      (pg-autotest eval (proof-full-annotation-toggle 0))
+      (pg-autotest script-wholefile "etc/isar/AHundredTheorems.thy")
+      (pg-autotest script-wholefile "isar/ex/Tarski.thy")
+      (pg-autotest script-randomjumps "isar/ex/Tarski.thy" 10)) ; better test?
+
 
   (pg-autotest remark "Testing restarting the prover")
   (pg-autotest quit-prover)