blob: 8e098a291e11d773ee80ad32b80167e1a6e7946b (
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
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
|
;; isar-autotest.el: tests of Isar Proof General.
;;
;; You can run these by issuing "make test.isar" in PG home dir.
;;
;; $Id$
;;
(defvar isar-long-tests nil
"Whether or not to perform lengthy tests")
(require 'pg-autotest)
(require 'proof-site)
(proof-ready-for-assistant 'isar)
(declare-function isar-tracing:auto-quickcheck-toggle "isar.el")
(declare-function isar-tracing:auto-solve-direct-toggle "isar.el")
(declare-function isar-proof:parallel-proofs-toggle "isar.el")
(unless (bound-and-true-p byte-compile-current-file)
(pg-autotest start) ; can add 'debug flag for debug-on-error
(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")
;; Test Trac#344 (nested spans bug with old-style undo)
;; TODO: should test with both undo styles
(pg-autotest eval (proof-retract-buffer))
(proof-shell-wait)
(goto-char 135) ; first line
(pg-autotest eval (proof-goto-point))
(proof-shell-wait)
(pg-autotest eval (proof-retract-buffer))
(proof-shell-wait)
(goto-char 135) ; first line
(pg-autotest eval (proof-goto-point))
(proof-shell-wait)
(pg-autotest eval (proof-process-buffer))
(pg-autotest assert-full)
;; Speed up prover
(pg-autotest eval (isar-tracing:auto-quickcheck-toggle 0))
(pg-autotest eval (isar-tracing:auto-solve-direct-toggle 0)) ; autosolve hammers this!
(pg-autotest eval (proof-full-annotation-toggle 0))
(pg-autotest eval (isar-proof:parallel-proofs-toggle 0))
(proof-shell-wait)
(pg-autotest script-wholefile "isar/Example-Tokens.thy")
(pg-autotest remark "Testing prove-as-you-go (not replay)")
(find-file ".autotest.thy")
(erase-buffer) ; just in case exists
(setq buffer-file-name nil)
(pg-autotest eval (proof-electric-terminator-toggle 1))
(pg-autotest eval (insert "theory Example imports Main begin ")) ; no \n
(proof-electric-terminator)
(pg-autotest eval (insert "theorem and_comms: \"A & B --> B & A\"\n"))
(proof-electric-terminator)
(pg-autotest eval (insert "apply auto done\n"))
(pg-autotest eval (insert "end"))
(proof-electric-terminator)
(pg-autotest assert-full)
;; Test Trac#138
(pg-autotest eval (proof-undo-last-successful-command))
(proof-shell-wait)
(pg-autotest eval (proof-goto-end-of-locked))
(pg-autotest eval (insert "(* this is a comment *)"))
(pg-autotest eval (proof-goto-point))
(proof-shell-wait)
(pg-autotest eval (skip-chars-backward " \n\t"))
(pg-autotest eval (insert " ")) ;; shouldn't give read-only error!
(set-buffer-modified-p nil)
(kill-buffer ".autotest.thy")
(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 "Testing random jumps and edits")
(pg-autotest script-randomjumps "isar/Example.thy" 8)
(when isar-long-tests
(pg-autotest remark "Larger files...")
(pg-autotest script-wholefile "etc/isar/AHundredTheorems.thy")
(pg-autotest script-wholefile "isar/ex/Tarski.thy")
(pg-autotest script-randomjumps "isar/ex/Tarski.thy" 10)) ; better test?
(pg-autotest remark "Testing restarting the prover")
(pg-autotest quit-prover)
(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 remark "Complete")
(pg-autotest timetaken 'total)
(pg-autotest exit)
)
|
