diff options
Diffstat (limited to 'isar')
| -rw-r--r-- | isar/isar-autotest.el | 35 |
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) + + |