Added simple testing framework (in progress)

1 files changed, 35 insertions, 0 deletions

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