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
224
225
226
227
228
|
;; This file is part of Proof General.
;;
;; © Copyright 2020 Hendrik Tews
;;
;; Authors: Hendrik Tews
;; Maintainer: Hendrik Tews <hendrik@askra.de>
;;
;; License: GPL (GNU GENERAL PUBLIC LICENSE)
;;; Commentary:
;;
;; Coq Compile Tests (cct) --
;; ert tests for parallel background compilation for Coq
;;
;; This file contains common definitions for the automated tests of
;; parallel background compilation.
;; Require some libraries for the elisp compilation. When compiling,
;; nothing is loaded, but all Proof General directories are in the
;; load path. When this file is loaded as part of a test, proof-site
;; has been loaded but only the generic subdir is in the load path.
;; This file references variables from coq-compile-common and
;; functions from proof-shell, therefore coq-compile-common must be
;; required for compilation. When running a test, these files would be
;; loaded anyway when the test visits the first Coq file. For
;; executing tests, the coq subdir will only be added to the load path
;; when the first Coq file is visited. Therefore we have to add it
;; here via proof-ready-for-assistant. For compilation, we have to
;; require proof-site, otherwise proof-ready-for-assistant won't be
;; defined.
(require 'proof-site)
(proof-ready-for-assistant 'coq)
(require 'coq-compile-common)
(require 'ert)
(defmacro cct-implies (p q)
"Short-circuit logical implication.
Evaluate Q only if P is non-nil."
`(or (not ,p) ,q))
(defun cct-list-subset (l1 l2)
"Return t if all elements of L1 are in L2 (compared by `equal')"
(let ((res t))
(while (and l1 res)
(unless (member (pop l1) l2)
(setq res nil)))
res))
;; Reimplementation of seq-set-equal-p for lists, because
;; seq-set-equal-p is not present before emacs 26.
;; XXX consider seq-set-equal-p when emacs 25 support is dropped.
(defun cct-list-set-equal (l1 l2)
"Return t if L1 and L2 contain the elements (compared by `equal')"
(and (cct-list-subset l1 l2)
(cct-list-subset l2 l1)))
(defun cct-goto-line (line)
"Put point on start of line LINE.
Very similar to `goto-line', but the documentation of `goto-line'
says, programs should use this piece of code."
(goto-char (point-min))
(forward-line (1- line)))
(defun cct-library-vo-of-v-file (v-src-file)
"Return .vo file name for V-SRC-FILE.
Changes the suffix from .v to .vo. V-SRC-FILE must have a .v suffix."
(concat v-src-file "o"))
(defun cct-record-change-time (file)
"Return cons of FILE and its modification time.
The modification time is an emacs time value, it's nil if file
cannot be accessed."
(cons file (nth 5 (file-attributes file))))
(defun cct-record-change-times (files)
"Return an assoc list of FILES with their modification times.
The modification time is an emacs time value, it's nil if file
cannot be accessed."
(mapcar 'cct-record-change-time files))
(defun cct-split-change-times (file-change-times files)
"Split assoc list FILE-CHANGE-TIMES.
FILE-CHANGE-TIMES must be an assoc list and FILES must be a
subset (i.e., each key occurring at most once) of the keys of
FILE-CHANGE-TIMES as list. This function returns two associations
lists (as cons cell). The car contains those associations in
FILE-CHANGE-TIMES with keys not in FILES, the cdr contains those
with keys in FILES."
(let (out in)
(dolist (file-time file-change-times (cons out in))
(if (member (car file-time) files)
(push file-time in)
(push file-time out)))))
(defun cct-process-to-line (line)
"Assert/retract to line LINE and wait until processing completed."
(cct-goto-line line)
(proof-goto-point)
(while (or proof-second-action-list-active (consp proof-action-list))
;; (message "wait for coq/compilation with %d items queued\n"
;; (length proof-action-list))
;;
;; accept-process-output without timeout returns rather quickly,
;; apparently most times without process output or any other event
;; to process.
(accept-process-output nil 0.1)))
(defun cct-get-vanilla-span (line)
"Get THE vanilla span for line LINE, report an error if there is none.
PG uses a number of overlapping and non-overlapping spans (read
overlays) in the asserted and queue region of the proof buffer,
see the comments in generic/proof-script.el. Spans of type
vanilla (stored at 'type in the span property list) are created
for real commands (not for comments). They hold various
information that is used, among others, for backtracking.
This function returns the vanilla span that covers line LINE and
reports a test failure if there is none or more than one vanilla spans."
(let (spans)
(cct-goto-line line)
(setq spans (spans-filter (overlays-at (point)) 'type 'vanilla))
(should (eq (length spans) 1))
(car spans)))
(defun cct-last-message-line ()
"Extract the last line from the *Messages* buffer.
Useful if the message is not present in the echo area any more
and `current-message' does not return anything."
(with-current-buffer "*Messages*"
(goto-char (point-max))
(forward-line -1)
(buffer-substring (point) (- (point-max) 1))))
(defun cct-check-locked (line locked-state)
"Check that line LINE has locked state LOCKED-STATE
LOCKED-STATE must be 'locked or 'unlocked. This function checks
whether line LINE is inside or outside the asserted (locked)
region of the buffer and signals a test failure if not."
(let ((locked (eq locked-state 'locked)))
;; (message "tcl line %d check %s: %s %s\n"
;; line (if locked "locked" "unlocked")
;; proof-locked-span
;; (if (overlayp proof-locked-span)
;; (span-end proof-locked-span)
;; "no-span"))
(cl-assert (or locked (eq locked-state 'unlocked))
nil "test-check-locked 2nd argument wrong")
(cct-goto-line line)
(should (cct-implies locked (span-end proof-locked-span)))
(should
(or
(and (not locked)
(or (not proof-locked-span) (not (span-end proof-locked-span))))
(and (span-end proof-locked-span)
(funcall (if locked '< '>)
(point) (span-end proof-locked-span)))))))
(defun cct-locked-ancestors (line ancestors)
"Check that the vanilla span at line LINE has ANCESTORS recorded.
The comparison treats ANCESTORS as set but the file names must
be `equal' as strings.
Ancestors are recoreded in the 'coq-locked-ancestors property of
the vanilla spans of require commands, see the in-file
documentation of coq/coq-par-compile.el."
(let ((locked-ancestors
(span-property (cct-get-vanilla-span line) 'coq-locked-ancestors)))
(should
(cct-list-set-equal locked-ancestors ancestors))))
(defun cct-file-unchanged (file time)
"Check that modification time of FILE equals TIME.
Used to check that FILE has not been changed since TIME was
recorded before."
(let ((file-time (nth 5 (file-attributes file))))
;; (message "TFU on %s: rec: %s now: %s\n"
;; file
;; (format-time-string "%H:%M:%S.%3N" time)
;; (format-time-string "%H:%M:%S.%3N" file-time))
(should
(and file-time (equal time file-time)))))
(defun cct-unmodified-change-times (file-time-assoc)
"Check that files in FILE-TIME-ASSOC have not been changed.
FILE-TIME-ASSOC must be an association list of files and emacs
times as returned by `cct-record-change-times' or
`cct-split-change-times'. This function checks that the
modification time of files in FILE-TIME-ASSOC equals the time
recorded in FILE-TIME-ASSOC, i.e., that the file has not been
changed since FILE-TIME-ASSOC has been recorded."
(mapc
(lambda (file-time-cons)
(cct-file-unchanged (car file-time-cons) (cdr file-time-cons)))
file-time-assoc))
(defun cct-file-newer (file time)
"Check that FILE exists and its modification time is more recent than TIME."
(let ((file-time (nth 5 (file-attributes file))))
(should (and file-time (time-less-p time file-time)))))
(defun cct-older-change-times (file-time-assoc)
"Check that files exist and have been changed.
FILE-TIME-ASSOC must be an association list of files and emacs
times as returned by `cct-record-change-times' or
`cct-split-change-times'. This function checks that the files in
FILE-TIME-ASSOC do exist and that their modification time is more
recent than in the association list, i.e., they have been updated
or changed since recording the time in the association."
(mapc
(lambda (file-time-cons)
(cct-file-newer (car file-time-cons) (cdr file-time-cons)))
file-time-assoc))
(defun cct-configure-proof-general ()
"Configure Proof General for test execution."
(setq delete-old-versions t
coq-compile-before-require t
coq-compile-keep-going t
proof-auto-action-when-deactivating-scripting 'retract
proof-three-window-enable nil
coq-compile-auto-save 'save-coq
coq--debug-auto-compilation nil))
(provide 'cct-lib)
|
