blob: a8185557270a7a4f9d467a4238d8cf74c974b586 (
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
118
119
120
|
;;; pg-autotest.el --- Simple testing framework for Proof General
;;
;; Copyright (C) 2005 LFCS Edinburgh, David Aspinall.
;; Authors: David Aspinall
;;
;; License: GPL (GNU GENERAL PUBLIC LICENSE)
;;
;; TODO:
;; -- fix failure handling for scriptfile
;; -- force re
;; -- add macros for defining test suites
;; -- add more precise functional tests to check results
;; -- add negative tests
;; -- output test results to stdout
;;
;; $Id$
(require 'proof)
;;; Commentary:
;;
;;; Code:
(defvar pg-autotest-success t) ;; success unless error caught
;;; Some utilities
(defun pg-autotest-find-file (file)
"Find FILE (relative to `proof-home-directory') and redisplay."
(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-assert-unprocessed file))
;;; Invoke a test
(defmacro pg-autotest (fn &rest args)
`(condition-case err
(apply (intern (concat "pg-autotest-" (symbol-name (quote ,fn))))
(list ,@args))
(error
(progn
(setq pg-autotest-success nil)
(princ (format "Error in test %s: %s" (symbol-name (quote ,fn))
err)))))) ;; display-error stdout?
;;; The tests proper
(defun pg-autotest-script-wholefile (file)
"Load FILE and script line-by-line, waiting a second between each line.
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-locked-end))
(goto-char last-locked-end)
(save-current-buffer
(proof-assert-next-command-interactive)
(proof-shell-wait))
(goto-char (proof-queue-or-locked-end))
(setq making-progress (> (point) last-locked-end))
(sit-for 1))))
(pg-autotest-assert-processed file))
(defun pg-autotest-retract-file (file)
(save-excursion
(pg-autotest-find-file file)
(proof-retract-buffer)
(sit-for 1)))
(defun pg-autotest-assert-processed (file)
"Check that FILE has been fully processed."
(save-excursion
(pg-autotest-find-file file)
(unless (proof-locked-region-full-p)
(error (format "Locked region in file `%f' is not full" file)))))
(defun pg-autotest-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 `%f' is not empty" file)))))
(defun pg-autotest-message (msg)
"Give message MSG on std out & on display."
(message msg)
;; FIXME: can we send to std out even if emacs is not batch mode?
(print msg)
(sit-for 1))
(defun pg-autotest-quit-prover ()
"Exit prover process."
(if (buffer-live-p proof-shell-buffer)
(kill-buffer proof-shell-buffer)
(error "No proof shell buffer to kill")))
(defun pg-autotest-finished ()
"Exit Emacs returning Unix success 0 if all tests succeeded."
(kill-emacs (if pg-autotest-success 0 1)))
(provide 'pg-autotest)
;;; pg-autotest.el ends here
|
