Added simple testing framework (in progress)

4 files changed, 187 insertions, 1 deletions

diff --git a/Makefile.devel b/Makefile.devel
index 8f2fb1ad..f232c9c9 100644
--- a/Makefile.devel
+++ b/Makefile.devel
@@ -153,6 +153,10 @@ CVSROOT=$(shell cat CVS/Root)
 # Emacs for batch compiling
 BATCHEMACS=xemacs -batch -q -no-site-file
 
+# Emacs for interactive use in testing
+EMACS=emacs
+EMACSFLAGS=-q -no-site-file
+
 # GNU version of tar, please
 TAR=tar
 # zip utility
@@ -201,7 +205,9 @@ RELEASENAMERPM = $(RELEASENAME)-1.noarch.rpm
 DISTINSTALLDIR=/export/local/share/elisp
 
 # Copied from distributed Makefile
-ELISP_DIRS=acl2 coq demoisa generic hol98 isa isar lclam lego lib mmm phox plastic twelf
+PROVERS=acl2 coq demoisa generic hol98 isa isar lclam lego phox plastic twelf
+OTHER_ELISP=lib mmm
+ELISP_DIRS=$(PROVERS) $(OTHER_ELISP)
 SUBDIRS=$(ELISP_DIRS) etc doc images
 
 PWD=$(shell pwd)
@@ -236,6 +242,16 @@ tags:	$(EL)
 	$(ETAGS) $(EL) TODO.developer doc/ProofGeneral.texi doc/PG-adapting.texi > TAGS
 
 
+############################################################
+#
+# Run tests for a particular prover and particular Emacs
+#
+test.%:	
+	if [ -f "$*/$*-autotest.el" ]; then if $(EMACS) $(EMACSFLAGS) -l generic/proof-site.el $*/$*-autotest.el -f eval-current-buffer; then echo "Autotests run successfully on `date`" > $*/.autotest.txt; else rm -f $*/autotest.txt; exit 1; fi; fi
+
+testall.%: 
+	for prover in ${PROVERS}; do $(MAKE) devel.test.$$prover EMACS=$*; done
+
 
 ############################################################
 #
diff --git a/coq/coq-autotest.el b/coq/coq-autotest.el
new file mode 100644
index 00000000..6d268b3d
--- /dev/null
+++ b/coq/coq-autotest.el
@@ -0,0 +1,19 @@
+;; coq-autotest.el: tests of Isar Proof General.
+;;
+;; You can run these by issuing "make devel.test.isar" in PG home dir.
+;;
+;; $Id$
+;;
+
+(require 'pg-autotest)
+
+;; The included test files
+(pg-autotest  message "Testing standard examples")
+(pg-autotest script-wholefile "coq/example.v")
+(pg-autotest script-wholefile "coq/example-x-symbol.v")
+(pg-autotest script-wholefile "coq/ex-module.v")
+
+(pg-autotest-quit-prover)
+(pg-autotest-finished)
+
+
diff --git a/generic/pg-autotest.el b/generic/pg-autotest.el
new file mode 100644
index 00000000..70d7a334
--- /dev/null
+++ b/generic/pg-autotest.el
@@ -0,0 +1,116 @@
+;; pg-autotest.el: Simple testing framework for Proof General
+;;
+;; Copyright (C) 2005 LFCS Edinburgh, David Aspinall.
+;; Authors:   David Aspinall
+;;
+;; License:   GPL (GNU GENERAL PUBLIC LICENSE)
+;;
+;; TODO:
+;; -- fix failure handling for scriptfile
+;; -- force re
+;; -- add macros for defining test suites 
+;; -- add more precise functional tests to check results
+;; -- add negative tests
+;; -- output test results to stdout
+;; 
+;; $Id$
+
+(require 'proof-site)
+
+(defvar pg-autotest-success t)		;; success unless error caught
+
+;;; Some utilities
+
+(defun pg-autotest-find-file (file)
+  "Find FILE (relative to `proof-home-directory') and redisplay."
+  (let* ((name   (concat proof-home-directory file)))
+    (if (file-exists-p name)
+	(find-file name)
+      (error "autotest: requested file %s does not exist" name))))
+
+(defun pg-autotest-find-file-restart (file)
+  "Find FILE and make ready to script there."
+  ;; Ensure scripting off; if completely full, will register, otherwise retract
+  (proof-deactivate-scripting-auto)
+  (pg-autotest-find-file file)
+  (goto-char (point-min))
+  (unless (proof-locked-region-empty-p)
+    ;; Should retract and unregister if was completely full
+    (proof-goto-point))
+  (pg-autotest-assert-unprocessed file))
+
+;;; Invoke a test
+
+(defmacro pg-autotest (fn &rest args)
+  `(condition-case err
+       (apply (intern (concat "pg-autotest-" (symbol-name (quote ,fn))))
+	      (list ,@args))
+     (error
+      (progn
+	(setq pg-autotest-success nil)
+	(princ (format "Error in test %s: %s" (symbol-name (quote ,fn)) 
+		       err)))))) ;; display-error stdout?
+
+
+
+;;; The tests proper
+
+(defun pg-autotest-script-wholefile (file)
+  "Load FILE and script line-by-line, waiting a second between each line.
+An error is signalled if scripting doesn't complete."
+  (pg-autotest-find-file-restart file)
+  (save-excursion
+    (let ((making-progress t) last-locked-end)
+      (while making-progress
+	(setq last-locked-end (proof-locked-end))
+	(goto-char last-locked-end)
+	(save-current-buffer
+	  (proof-assert-next-command-interactive)
+	  (proof-shell-wait))
+	(goto-char (proof-queue-or-locked-end))
+	(setq making-progress (> (point) last-locked-end))
+	(sit-for 1))))
+  (pg-autotest-assert-processed file))
+
+(defun pg-autotest-retract-file (file)
+  (save-excursion
+    (pg-autotest-find-file file)
+    (proof-retract-buffer)
+    (sit-for 1)))
+
+(defun pg-autotest-assert-processed (file)
+  "Check that FILE has been fully processed."
+  (save-excursion
+    (pg-autotest-find-file file)
+    (unless (proof-locked-region-full-p)
+      (error "Locked region in file `%s' is not full." file))))
+
+(defun pg-autotest-assert-unprocessed (file)
+  "Check that FILE has been fully unprocessed."
+  (save-excursion
+    (pg-autotest-find-file file)
+    (unless (proof-locked-region-empty-p)
+      (error "Locked region in file `%f' is not empty."))))
+
+(defun pg-autotest-message (msg)
+  "Give message MSG on std out & on display."
+  (message msg)
+  ;; FIXME: can we send to std out even if emacs is not batch mode?
+  (print msg)
+  (sit-for 1))
+
+(defun pg-autotest-quit-prover ()
+  "Exit prover process."
+  (if (buffer-live-p proof-shell-buffer)
+	(kill-buffer proof-shell-buffer)
+    (error "No proof shell buffer to kill!")))
+
+(defun pg-autotest-finished ()
+  "Exit Emacs returning Unix success 0 if all tests succeeded."
+  (kill-emacs (if pg-autotest-success 0 1)))
+    
+    
+
+(provide 'pg-autotest)
+;;; pg-autotest.el ends here
+
diff --git a/isar/isar-autotest.el b/isar/isar-autotest.el
new file mode 100644
index 00000000..5cd5b2b8
--- /dev/null
+++ b/isar/isar-autotest.el
@@ -0,0 +1,35 @@
+;; isar-autotest.el: tests of Isar Proof General.
+;;
+;; You can run these by issuing "make devel.test.isar" in PG home dir.
+;;
+;; $Id$
+;;
+
+(require 'pg-autotest)
+
+;; The included test files
+(pg-autotest  message "Testing standard Example.thy, Example-Xsym.thy")
+(pg-autotest script-wholefile "isar/Example.thy")
+(pg-autotest script-wholefile "isar/Example-Xsym.thy")
+
+; These require Complex theory
+;(pg-autotest script-wholefile "isar/Root2_Isar.thy")
+;(pg-autotest script-wholefile "isar/Root2_Tactic.thy")
+
+;; The standard simple multiple file examples
+
+(pg-autotest message	       "Simple test of multiple files...")
+(pg-autotest script-wholefile  "etc/isar/multiple/C.thy")
+(pg-autotest assert-processed   "etc/isar/multiple/C.thy")
+(pg-autotest assert-processed   "etc/isar/multiple/A.thy")
+(pg-autotest assert-processed   "etc/isar/multiple/B.thy")
+(pg-autotest retract-file      "etc/isar/multiple/B.thy")
+(pg-autotest assert-unprocessed "etc/isar/multiple/B.thy")
+(pg-autotest assert-unprocessed "etc/isar/multiple/C.thy")
+(pg-autotest assert-processed   "etc/isar/multiple/A.thy")
+
+
+(pg-autotest-quit-prover)
+(pg-autotest-finished)
+
+