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
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
|
;;; pg-autotest.el --- Simple testing framework for Proof General
;;
;; Copyright (C) 2005, 2009-10 LFCS Edinburgh, David Aspinall.
;; Authors: David Aspinall
;;
;; License: GPL (GNU GENERAL PUBLIC LICENSE)
;;
;; TODO:
;; -- fix failure handling for scriptfile
;; -- add macros for defining test suites
;; -- add more precise functional tests to check results
;; -- add negative tests
;;
;; $Id$
(require 'proof)
(require 'proof-shell)
;;; Commentary:
;;
;; Support for running a series of scripted UI tests.
;;
;;; Code:
(defvar pg-autotest-success t
"Flag indicating overall successful state of tests.")
(defvar pg-autotest-log t
"Value for 'standard-output' during tests.")
(setq debug-on-error t) ;; enable in case a test goes wrong
;;; Some utilities
(defun pg-autotest-find-file (file)
"Find FILE (relative to `proof-home-directory')."
(let* ((name (concat proof-home-directory file)))
(if (file-exists-p name)
(find-file name)
(error (format "autotest: requested file %s does not exist" name)))))
(defun pg-autotest-find-file-restart (file)
"Find FILE and make ready to script there."
;; Ensure scripting off; if completely full, will register, otherwise retract
(proof-deactivate-scripting-auto)
(pg-autotest-find-file file)
(goto-char (point-min))
(unless (proof-locked-region-empty-p)
;; Should retract and unregister if was completely full
(proof-goto-point))
(pg-autotest-test-assert-unprocessed file))
;;; Invoke a test
(defmacro pg-autotest (fn &rest args)
`(unwind-protect
(progn
(setq standard-output pg-autotest-log)
(condition-case err
(let ((scaffoldfn
(intern (concat "pg-autotest-"
(symbol-name (quote ,fn))))))
(if (fboundp scaffoldfn)
(apply scaffoldfn (list ,@args))
(pg-autotest-message
"TEST: %s"
(prin1-to-string (cons (quote ,fn)
(quote ,args))))
(apply (intern (concat "pg-autotest-test-"
(symbol-name (quote ,fn))))
(list ,@args))))
(error
(progn
(setq pg-autotest-success nil)
(pg-autotest-message
"ERROR %s: %s" (quote ,fn) (prin1-to-string err))))))
(setq standard-output t)))
;;; Test output and timing
(defun pg-autotest-log (file)
(save-excursion
(find-file file)
(erase-buffer)
(setq pg-autotest-log (current-buffer))
(pg-autotest-message (concat "Tests started "
(format-time-string "%D %H:%M")))))
(defun pg-autotest-message (msg &rest args)
"Give message MSG in log file output and on display."
(let ((fmsg (if args (apply 'format msg args) msg)))
(proof-with-current-buffer-if-exists
pg-autotest-log
(insert fmsg "\n"))
(message fmsg)
(redisplay t)))
(defun pg-autotest-remark (msg)
(pg-autotest-message "\n\nREMARK: %s\n" msg))
(defun pg-autotest-timestart (&optional clockname)
"Make a note of current time, named 'local or CLOCKNAME."
(put 'pg-autotest-time (or clockname 'local)
(current-time)))
(defun pg-autotest-timetaken (&optional clockname)
"Report time since (startclock CLOCKNAME)."
(let* ((timestart (get 'pg-autotest-time (or clockname 'local)))
(timetaken
(time-subtract (current-time) timestart)))
(pg-autotest-message
"TIME: %f (%s)"
(float-time timetaken)
(if clockname (symbol-name clockname)
"this test"))))
(defun pg-autotest-exit ()
"Exit Emacs returning Unix success 0 if all tests succeeded."
(pg-autotest-message (concat "\nTests completed "
(format-time-string "%D %H:%M")))
(proof-with-current-buffer-if-exists
pg-autotest-log
(save-buffer 0))
(kill-emacs (if pg-autotest-success 0 1)))
;;; The test script functions proper
(defun pg-autotest-test-process-wholefile (file)
"Load FILE and script in one go.
An error is signalled if scripting doesn't completely the whole buffer."
(pg-autotest-find-file-restart file)
(proof-process-buffer)
(proof-shell-wait)
(pg-autotest-test-assert-processed file))
(defun pg-autotest-test-script-wholefile (file)
"Process FILE line-by-line, using `proof-shell-wait'.
An error is signalled if scripting doesn't complete."
(pg-autotest-find-file-restart file)
(save-excursion
(let ((making-progress t) last-locked-end)
(while making-progress
(setq last-locked-end (proof-unprocessed-begin))
(goto-char last-locked-end)
(save-current-buffer
(condition-case err
(proof-assert-next-command-interactive)
(error
(let ((msg (car-safe (cdr-safe err))))
(unless (string-equal msg
;; normal user error message at end of buffer
"At end of the locked region, nothing to do to!")
(pg-autotest-message
"proof-assert-next-command-interactive hit an error: %s"
msg)))))
(proof-shell-wait))
(goto-char (proof-queue-or-locked-end))
(setq making-progress (> (point) last-locked-end)))))
(pg-autotest-test-assert-processed file))
(defun pg-autotest-test-script-randomjumps (file jumps)
"Load FILE and process in it by jumping around randomly JUMPS times.
This should be robust against synchronization errors; we test this by
completely processing the buffer as the last step."
(pg-autotest-find-file-restart file)
(while (> jumps 0)
(let ((random-point (random (point-max))))
;; TODO: random use of retract/process whole buffer too
(pg-autotest-message
" random jump to point: %d" random-point)
(goto-char random-point)
(unless (if (>= (point) (proof-unprocessed-begin))
(proof-only-whitespace-to-locked-region-p))
(proof-goto-point)
(proof-shell-wait) ;; TODO: check no prover error.
(decf jumps))))
(proof-process-buffer)
(proof-shell-wait)
(pg-autotest-test-assert-processed file))
(defun pg-autotest-test-retract-file (file)
(save-excursion
(pg-autotest-find-file file)
(proof-retract-buffer)
(sit-for 1)))
(defun pg-autotest-test-assert-processed (file)
"Check that FILE has been fully processed."
(save-excursion ;; TODO: also check on included files list
(pg-autotest-find-file file)
(pg-autotest-test-assert-full)))
(defun pg-autotest-test-assert-full ()
"Check that current buffer has been fully processed."
(unless (proof-locked-region-full-p)
(error (format "Locked region in buffer `%s' is not full"
(buffer-name)))))
(defun pg-autotest-test-assert-unprocessed (file)
"Check that FILE has been fully unprocessed."
(save-excursion
(pg-autotest-find-file file)
(unless (proof-locked-region-empty-p)
(error (format "Locked region in file `%s' is not empty" file)))))
(defun pg-autotest-test-eval (body)
"Evaluate given expression for side effect."
(eval body))
(defun pg-autotest-test-quit-prover ()
"Exit prover process."
(if (buffer-live-p proof-shell-buffer)
(kill-buffer proof-shell-buffer)
(error "No proof shell buffer to kill")))
(provide 'pg-autotest)
;;; pg-autotest.el ends here
|
