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
|
;; This file is part of Proof General.
;;
;; © Copyright 2021 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
;;
;; Test two require jobs with different delays such that
;; coq-par-retire-top-level-job happens when the other require job is
;; in each possible state. For specifying the different delays there
;; are 6 mini projects, one for each test in this file. Each project
;; consists of four files, a1.v, b1.v, c1.v and d1.v for the first one
;; and a6.v, b6.v, c6.v and d6.v for the sixth one.
;;
;; The dependencies are the same in all projects:
;;
;; a
;; / \
;; b c
;; \ /
;; d
;;
;; Test 1 delays coqdep on require c, such that queue kickoff happens
;; in state 'enqueued-coqdep, the dependency link d->c is created when
;; d is ready and kickoff-queue-maybe on require c happens when
;; require b is in state 'ready.
;;
;; Test 2 delays coqdep on c, such that queue kickoff happens in state
;; 'waiting-dep.
;;
;; Test 3 delays coqdep on require b, such that kickoff-queue-maybe on
;; require c happens when require b is in state 'enqueued-coqdep and
;; queue kickoff happens in state 'waiting-queue.
;;
;; Test 4 delays coqdep on b, such that kickoff-queue-maybe on require
;; c happens when require b is in state 'waiting-dep.
;;
;; Test 5 delays coqdep on d, such that the second dependency on d is
;; created when d is in state enqueued-coqdep.
;;
;; Test 6 delays coqdep on c for 2 seconds and coqc on d for 4
;; seconds, such that the dependency link d->c is created when d is in
;; state enqueued-coqc.
;; require cct-lib for the elisp compilation, otherwise this is present already
(require 'cct-lib)
;;; set configuration
(cct-configure-proof-general)
(configure-delayed-coq)
(defconst pre-b-ancestors '("./b" "./d")
"Ancestors of b without suffixes.")
(defconst pre-c-ancestors '("./c")
"Ancestors of c without suffixes.")
(defconst pre-all-ancestors (append pre-b-ancestors pre-c-ancestors)
"All ancestors without suffixes.")
(defun b-ancestors (n)
"Ancestors of b for part N."
(mapcar (lambda (a) (concat a (format "%d.v" n))) pre-b-ancestors))
(defun c-ancestors (n)
"Ancestors of c for part N."
(mapcar (lambda (a) (concat a (format "%d.v" n))) pre-c-ancestors))
(defun all-ancestors (n)
"All ancestors for part N."
(mapcar (lambda (a) (concat a (format "%d.v" n))) pre-all-ancestors))
(defun all-compiled-ancestors (n)
"All vo ancestor files for part N."
(mapcar 'cct-library-vo-of-v-file (all-ancestors n)))
(defun check-main-buffer (n vo-times new-sum recompiled-files
other-locked-files)
"Perform various checks in buffer aN.v.
See `cct-generic-check-main-buffer'."
(cct-generic-check-main-buffer
(format "a%d.v" n) ; main-buf
25 ; main-unlocked
41 ; main-locked
31 ; main-sum-line
new-sum
vo-times
recompiled-files
`((25 . ,(b-ancestors n)) (26 . ,(c-ancestors n))) ; require-ancestors
other-locked-files
27 ; other-locked-line
))
;;; Define the test
(defun test-slow-require (n)
"Test part N of slow require job tests.
XXX Test a setting where the second require job is still in state
'enqueued-coqdep when the first one finishes."
(let*
;; .v file names are used as file and as buffer names
((av (format "a%d.v" n))
(bv (format "b%d.v" n))
(cv (format "c%d.v" n))
(dv (format "d%d.v" n))
;; .vo names compared with ancestors, they need a "./" prefix
(bvo (concat "./" (cct-library-vo-of-v-file bv)))
(cvo (concat "./" (cct-library-vo-of-v-file cv)))
(dvo (concat "./" (cct-library-vo-of-v-file dv)))
vo-times other-locked-files)
;; (setq cct--debug-tests t)
;; (setq coq--debug-auto-compilation t)
(find-file av)
(message "coqdep: %s\ncoqc: %s\nPATH %s\nexec-path: %s"
coq-dependency-analyzer
coq-compiler
(getenv "PATH")
exec-path)
;; 1. process original content - compile everything
(message "\n%d.1. process original content - compile everything\n" n)
;;(setq coq--debug-auto-compilation t)
(cct-process-to-line 42)
(cct-check-locked 41 'locked)
(cct-locked-ancestors 25 (b-ancestors n))
(cct-locked-ancestors 26 (c-ancestors n))
;; (cl-assert nil nil "exit")
(setq vo-times (cct-record-change-times (all-compiled-ancestors n)))
;; 2. retract and process again - nothing should be compiled
(message "\n%d.2. retract and process again - nothing should be compiled\n"
n)
(cct-process-to-line 24)
(check-main-buffer n vo-times "9" nil nil)
;; 3. change d and process again - b and c should be compiled
(message "\n%d.3. change d and process again - b and c should be compiled\n"
n)
(find-file dv)
(push dv other-locked-files)
(cct-check-locked 23 'locked)
(cct-replace-last-word 27 "5")
(check-main-buffer n vo-times "10" (list bvo cvo dvo)
other-locked-files)
;; 4. change b and process again - only b should be compiled
(message "\n%d.4. change b and process again - only b should be compiled\n"
n)
(setq vo-times (cct-record-change-times (all-compiled-ancestors n)))
(find-file bv)
(push bv other-locked-files)
(cct-check-locked 23 'locked)
(cct-replace-last-word 27 "4")
(check-main-buffer n vo-times "12" (list bvo) other-locked-files)
;; 5. change c and process again - only c should be compiled
(message "\n%d.5. change c and process again - only c should be compiled\n"
n)
(setq vo-times (cct-record-change-times (all-compiled-ancestors n)))
(find-file cv)
(push cv other-locked-files)
(cct-check-locked 23 'locked)
(cct-replace-last-word 27 "8")
(check-main-buffer n vo-times "17" (list cvo) other-locked-files)
;; 6. delete d and process again - b and c should be compiled
(message "\n%d.6. delete d and process again - b and c should be compiled\n"
n)
(setq vo-times (cct-record-change-times (all-compiled-ancestors n)))
(delete-file dvo)
(set-buffer av)
(cct-process-to-line 24)
(check-main-buffer n vo-times "17" (list bvo cvo dvo)
other-locked-files)
;; 7. delete b and process again - only b should be compiled
(message "\n%d.7. delete b and process again - only b should be compiled\n"
n)
(setq vo-times (cct-record-change-times (all-compiled-ancestors n)))
(delete-file bvo)
(set-buffer av)
(cct-process-to-line 24)
(check-main-buffer n vo-times "17" (list bvo) other-locked-files)
;; 8. delete c and process again - only c should be compiled
(message "\n%d.8. delete c and process again - only c should be compiled\n"
n)
(setq vo-times (cct-record-change-times (all-compiled-ancestors n)))
(delete-file cvo)
(set-buffer av)
(cct-process-to-line 24)
(check-main-buffer n vo-times "17" (list cvo) other-locked-files)
))
(ert-deftest cct-slow-require-1 () (test-slow-require 1))
(ert-deftest cct-slow-require-2 () (test-slow-require 2))
(ert-deftest cct-slow-require-3 () (test-slow-require 3))
(ert-deftest cct-slow-require-4 () (test-slow-require 4))
(ert-deftest cct-slow-require-5 () (test-slow-require 5))
(ert-deftest cct-slow-require-6 () (test-slow-require 6))
|
