blob: cc3d6640c6cb56b1d98be9fc38821846a0cb283d (
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
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
|
;; isar-autotest.el: tests of Isar Proof General.
;;
;; You can run these by issuing "make test.isar" in PG home dir.
;;
;; $Id$
;;
(eval-when-compile
(require 'cl))
(eval-when (compile)
(require 'proof-site)
(proof-ready-for-assistant 'isar))
(declare-function isar-tracing:auto-quickcheck-toggle "isar.el")
(declare-function isar-tracing:auto-solve-toggle "isar.el")
(require 'pg-autotest)
(unless noninteractive
(pg-autotest log ".autotest.log") ; convention
(pg-autotest timestart 'total)
(pg-autotest remark "Testing standard Example.thy, Example-Xsym.thy")
(pg-autotest script-wholefile "isar/Example.thy")
(pg-autotest script-wholefile "isar/Example-Tokens.thy")
(pg-autotest remark "Testing random jumps")
(pg-autotest eval (isar-tracing:auto-quickcheck-toggle 0))
(pg-autotest eval (isar-tracing:auto-solve-toggle 0)) ; autosolve hammers this!
(pg-autotest script-randomjumps "isar/Example.thy" 5)
(pg-autotest script-randomjumps "etc/isar/AHundredTheorems.thy" 10)
(pg-autotest remark "Testing restarting the prover")
(pg-autotest quit-prover)
(pg-autotest remark "Now in tokens mode")
(pg-autotest eval (proof-unicode-tokens-toggle))
(pg-autotest script-wholefile "isar/Example-Tokens.thy")
(pg-autotest remark "A larger file:")
(pg-autotest timestart)
(pg-autotest script-wholefile "isar/ex/Tarski.thy")
(pg-autotest timetaken)
(pg-autotest remark "Simple test of multiple file behaviour:")
(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 timetaken 'total)
(pg-autotest exit)
)
|
