Improve loading; these tests are not functioning yet

3 files changed, 29 insertions, 25 deletions

diff --git a/coq/coq-autotest.el b/coq/coq-autotest.el
index 6d268b3d..0e12d48c 100644
--- a/coq/coq-autotest.el
+++ b/coq/coq-autotest.el
@@ -1,6 +1,6 @@
-;; coq-autotest.el: tests of Isar Proof General.
+;; coq-autotest.el: tests of Coq Proof General (in progress).
 ;;
-;; You can run these by issuing "make devel.test.isar" in PG home dir.
+;; You can run these by issuing "make test.coq" in PG home dir.
 ;;
 ;; $Id$
 ;;
@@ -8,12 +8,13 @@
 (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")
+(eval-when (load)
+  (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)
+  (pg-autotest-quit-prover)
+  (pg-autotest-finished))
 
 
diff --git a/generic/pg-autotest.el b/generic/pg-autotest.el
index 70d7a334..a48027f5 100644
--- a/generic/pg-autotest.el
+++ b/generic/pg-autotest.el
@@ -16,6 +16,7 @@
 ;; $Id$
 
 (require 'proof-site)
+(require 'proof-compat)
 
 (defvar pg-autotest-success t)		;; success unless error caught
 
diff --git a/isar/isar-autotest.el b/isar/isar-autotest.el
index b20dc1ae..2d5beef5 100644
--- a/isar/isar-autotest.el
+++ b/isar/isar-autotest.el
@@ -7,10 +7,12 @@
 
 (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")
+(eval-when (load)
+
+  ;; 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")
@@ -18,18 +20,18 @@
 
 ;; 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)
+  (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))