blob: 8d6aae9544a9f3d233ad19789f698d98c139afe8 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
|
;; isar-autotest.el: tests of Isar Proof General.
;;
;; You can run these by issuing "make test.isar" in PG home dir.
;;
;; $Id$
;;
(require 'pg-autotest)
(unless noninteractive
;; 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))
|
