Skip to content

Commit 71d3d24

Browse files
hendriktewshendriktews
committed
test that Coq background compilation is not affected by local variables
See also ProofGeneral#797
1 parent b30d65d commit 71d3d24

File tree

10 files changed

+405
-1
lines changed

10 files changed

+405
-1
lines changed

‎ci/compile-tests/011-current-buffer/Makefile

+24
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,24 @@
1+
# This file is part of Proof General.
2+
#
3+
# © Copyright 2024 Hendrik Tews
4+
#
5+
# Authors: Hendrik Tews
6+
# Maintainer: Hendrik Tews <[email protected]>
7+
#
8+
# SPDX-License-Identifier: GPL-3.0-or-later
9+
10+
# This test uses ../bin/compile-test-start-delayed to start certain
11+
# commands with specified delays to check carfully constructed
12+
# internal states. compile-test-start-delayed outputs diagnostics on
13+
# file descriptor 9, which bypasses emacs and is joined with stderr of
14+
# the current make. Open file descriptor 9 here.
15+
.PHONY: test
16+
test:
17+
$(MAKE) clean
18+
emacs -batch -l ../../../generic/proof-site.el -l ../cct-lib.el \
19+
-l runtest.el -f ert-run-tests-batch-and-exit \
20+
9>&1
21+
22+
.PHONY: clean
23+
clean:
24+
rm -f *.vo *.glob *.vio *.vos *.vok .*.aux

‎ci/compile-tests/011-current-buffer/a.v

+26
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,26 @@
1+
(* This file is part of Proof General.
2+
*
3+
* © Copyright 2024 Hendrik Tews
4+
*
5+
* Authors: Hendrik Tews
6+
* Maintainer: Hendrik Tews <[email protected]>
7+
*
8+
* SPDX-License-Identifier: GPL-3.0-or-later
9+
*
10+
*
11+
* This file is part of an automatic test case for parallel background
12+
* compilation in coq-par-compile.el. See runtest.el in this directory.
13+
*)
14+
15+
(* The test script relies on absolute line numbers.
16+
* DO NOT INSERT ANY LINE UNLESS YOU KNOW WHAT YOU ARE DOING.
17+
*)
18+
19+
(* The delay for coqdep is specified in comments with key coqdep-delay,
20+
* see compile-test-start-delayed.
21+
*)
22+
23+
24+
(* This is line 24 *)
25+
Require Export (* coqdep-delay 1 *) b.
26+
(* This is line 26 *)

‎ci/compile-tests/011-current-buffer/b.v

+15
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,15 @@
1+
(* This file is part of Proof General.
2+
*
3+
* © Copyright 2024 Hendrik Tews
4+
*
5+
* Authors: Hendrik Tews
6+
* Maintainer: Hendrik Tews <[email protected]>
7+
*
8+
* SPDX-License-Identifier: GPL-3.0-or-later
9+
*
10+
*
11+
* This file is part of an automatic test case for parallel background
12+
* compilation in coq-par-compile.el. See test.el in this directory.
13+
*)
14+
15+
Definition b : nat := 2.

‎ci/compile-tests/011-current-buffer/c.v

+25
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,25 @@
1+
(* This file is part of Proof General.
2+
*
3+
* © Copyright 2024 Hendrik Tews
4+
*
5+
* Authors: Hendrik Tews
6+
* Maintainer: Hendrik Tews <[email protected]>
7+
*
8+
* SPDX-License-Identifier: GPL-3.0-or-later
9+
*
10+
*
11+
* This file is part of an automatic test case for parallel background
12+
* compilation in coq-par-compile.el. See test.el in this directory.
13+
*)
14+
15+
Definition c : nat := 2.
16+
17+
(* Set `coq-compiler` and `coq-dependency-analyzer` as local variable
18+
to something that definitely fails when the test (or the user)
19+
visits this file in an ongoing background compilation and
20+
background compilation picks up local variables from this file.
21+
*)
22+
23+
(*** Local Variables: ***)
24+
(*** coq-compiler: "coq-error" ***)
25+
(*** End: ***)

‎ci/compile-tests/011-current-buffer/d.v

+25
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,25 @@
1+
(* This file is part of Proof General.
2+
*
3+
* © Copyright 2024 Hendrik Tews
4+
*
5+
* Authors: Hendrik Tews
6+
* Maintainer: Hendrik Tews <[email protected]>
7+
*
8+
* SPDX-License-Identifier: GPL-3.0-or-later
9+
*
10+
*
11+
* This file is part of an automatic test case for parallel background
12+
* compilation in coq-par-compile.el. See test.el in this directory.
13+
*)
14+
15+
Definition c : nat := 2.
16+
17+
(* Set `coq-compiler` and `coq-dependency-analyzer` as local variable
18+
to something that definitely fails when the test (or the user)
19+
visits this file in an ongoing background compilation and
20+
background compilation picks up local variables from this file.
21+
*)
22+
23+
(*** Local Variables: ***)
24+
(*** coq-dependency-analyzer: "coq-error" ***)
25+
(*** End: ***)

‎ci/compile-tests/011-current-buffer/runtest.el

+273
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,273 @@
1+
;; This file is part of Proof General. -*- lexical-binding: t; -*-
2+
;;
3+
;; © Copyright 2024 Hendrik Tews
4+
;;
5+
;; Authors: Hendrik Tews
6+
;; Maintainer: Hendrik Tews <[email protected]>
7+
;;
8+
;; SPDX-License-Identifier: GPL-3.0-or-later
9+
10+
;;; Commentary:
11+
;;
12+
;; Coq Compile Tests (cct) --
13+
;; ert tests for parallel background compilation for Coq
14+
;;
15+
;; Test that parallel background compilation is not confused by local
16+
;; variables in unrelated buffers.
17+
;;
18+
;; The dependencies in this test are:
19+
;;
20+
;; a c d
21+
;; |
22+
;; b
23+
;;
24+
;; Files c and d are completely independent of file a and file b and
25+
;; not processed by Coq. The idea is that files c or d come from a
26+
;; different project that uses a different `coq-compiler' or
27+
;; `coq-dependency-analyzer', see also PG issue #797. These different
28+
;; local settings should not confuse the ongoing background
29+
;; compilation of file b for processing file a in a script buffer.
30+
;; File c sets `coq-compiler' as local variable and file d sets
31+
;; `coq-dependency-analyzer' as local variable.
32+
33+
34+
;; require cct-lib for the elisp compilation, otherwise this is present already
35+
(require 'cct-lib "ci/compile-tests/cct-lib")
36+
37+
;;; set configuration
38+
(cct-configure-proof-general)
39+
(configure-delayed-coq)
40+
41+
(defvar switch-buffer-while-waiting nil
42+
"XXX")
43+
44+
(defvar av-buffer nil
45+
"XXX")
46+
47+
(defvar cdv-buffer nil
48+
"XXX")
49+
50+
(defun switch-to-other-buffer-while-waiting ()
51+
"XXX"
52+
(when (and nil switch-buffer-while-waiting cdv-buffer)
53+
(message "Switch to buffer c.v while busy waiting")
54+
(set-buffer cdv-buffer)))
55+
56+
(defun switch-back-after-waiting ()
57+
"XXX"
58+
(when (and nil switch-buffer-while-waiting av-buffer)
59+
(message "Switch back to buffer a.v after busy waiting")
60+
(set-buffer av-buffer)))
61+
62+
(add-hook 'cct-before-busy-waiting-hook #'switch-to-other-buffer-while-waiting)
63+
(add-hook 'cct-after-busy-waiting-hook #'switch-back-after-waiting)
64+
65+
66+
;;; The tests itself
67+
68+
(ert-deftest test-current-buffer-vok ()
69+
:expected-result :passed
70+
"Check that second stage compilation uses the right local variables.
71+
Second stage compilation (vok and vio2vo) should use the local
72+
variables from the original scripting buffer, see also PG issue
73+
#797."
74+
(unwind-protect
75+
(progn
76+
(message "\nRun test-current-buffer-vok")
77+
78+
;; XXXX
79+
(setq switch-buffer-while-waiting nil)
80+
81+
;; configure 2nd stage
82+
(if (coq--post-v811)
83+
(setq coq-compile-vos 'vos-and-vok)
84+
(setq coq-compile-quick 'quick-and-vio2vo))
85+
86+
;; (setq cct--debug-tests t)
87+
;; (setq coq--debug-auto-compilation t)
88+
(find-file "a.v")
89+
(setq av-buffer (current-buffer))
90+
91+
(find-file "c.v")
92+
(setq cdv-buffer (current-buffer))
93+
(set-buffer av-buffer)
94+
95+
(message (concat "coqdep: %s\ncoqc: %s\nPATH %s\n"
96+
"exec-path: %s\ndetected coq version: %s")
97+
coq-dependency-analyzer
98+
coq-compiler
99+
(getenv "PATH")
100+
exec-path
101+
coq-autodetected-version)
102+
103+
;; Work around existing .vos and .vok files from other tests in
104+
;; this file.
105+
(message "\ntouch dependency b.v to force complete (re-)compilation")
106+
(should (set-file-times "b.v"))
107+
108+
(message "\nProcess a.v to end, including compilation of dependency b.v")
109+
(cct-process-to-line 27)
110+
(cct-check-locked 26 'locked)
111+
112+
(with-current-buffer cdv-buffer
113+
(message
114+
(concat "\nWait for 2nd stage (vok/vio2vo) compilation "
115+
"in buffer b.v with"
116+
"\ncoqdep: %s\ncoqc: %s")
117+
coq-dependency-analyzer
118+
coq-compiler))
119+
120+
(setq switch-buffer-while-waiting t)
121+
122+
;; This will temporarily switch to buffer c.v, which sets
123+
;; coq-compiler as local variable, see the hooks above
124+
(cct-wait-for-second-stage)
125+
126+
(message "search for coq-error error message in compile-response buffer")
127+
(with-current-buffer coq--compile-response-buffer
128+
(goto-char (point-min))
129+
(should
130+
(not
131+
(re-search-forward "Error: coq-error has been executed" nil t)))))
132+
133+
;; clean up
134+
(dolist (buf (list av-buffer cdv-buffer))
135+
(when buf
136+
(with-current-buffer buf
137+
(set-buffer-modified-p nil))
138+
(kill-buffer buf)))))
139+
140+
(ert-deftest test-current-buffer-coqdep ()
141+
:expected-result :passed
142+
"Check that dependency analysis uses the right local variables.
143+
Dependency analysis during parallel background compilation (i.e.,
144+
runing `coqdep` on dependencies) should use the local variables
145+
from the original scripting buffer, see also PG issue #797.
146+
147+
To ensure we only see errors from dependency analysis, we first
148+
process file a completely without trying to confuse parallel
149+
background compilation."
150+
(unwind-protect
151+
(progn
152+
(message "\nRun test-current-buffer-coqdep")
153+
154+
;; XXXX
155+
(setq switch-buffer-while-waiting nil)
156+
157+
;; (setq cct--debug-tests t)
158+
;; (setq coq--debug-auto-compilation t)
159+
(find-file "a.v")
160+
(setq av-buffer (current-buffer))
161+
162+
(find-file "d.v")
163+
(setq cdv-buffer (current-buffer))
164+
(set-buffer av-buffer)
165+
166+
(message (concat "coqdep: %s\ncoqc: %s\nPATH %s\n"
167+
"exec-path: %s\ndetected coq version: %s")
168+
coq-dependency-analyzer
169+
coq-compiler
170+
(getenv "PATH")
171+
exec-path
172+
coq-autodetected-version)
173+
174+
(message "\nProcess a.v to end, including compilation of dependency b.v")
175+
(cct-process-to-line 27)
176+
(cct-check-locked 26 'locked)
177+
178+
(message "\nRetract a.v before the require command")
179+
(cct-process-to-line 20)
180+
(cct-check-locked 25 'unlocked)
181+
182+
(with-current-buffer cdv-buffer
183+
(message
184+
(concat "\nProcess the require command again while visiting d.v with"
185+
"\ncoqdep: %s\ncoqc: %s")
186+
coq-dependency-analyzer
187+
coq-compiler))
188+
189+
(setq switch-buffer-while-waiting t)
190+
191+
;; This will temporarily switch to buffer c.v, which sets
192+
;; coq-compiler as local variable, see the hooks above.
193+
(cct-process-to-line 27)
194+
195+
;; (with-current-buffer coq--compile-response-buffer
196+
;; (message "coq-compile-response:\n%s\n<<<End"
197+
;; (buffer-substring-no-properties (point-min) (point-max))))
198+
199+
(cct-check-locked 26 'locked))
200+
201+
;; clean up
202+
(dolist (buf (list av-buffer cdv-buffer))
203+
(when buf
204+
(with-current-buffer buf
205+
(set-buffer-modified-p nil))
206+
(kill-buffer buf)))))
207+
208+
(ert-deftest test-current-buffer-coqc ()
209+
:expected-result :passed
210+
"Check that compilation of dependencies uses the right local variables.
211+
Compilation of dependencies during parallel background
212+
compilation (i.e., runing `coqc` on dependencies) should use the
213+
local variables from the original scripting buffer, see also PG
214+
issue #797.
215+
216+
To ensure we only see errors from running `coqc`, we temporarily
217+
switch to buffer c.v, which sets `coq-compiler' but leaves
218+
`coq-dependency-analyzer' alone."
219+
(unwind-protect
220+
(progn
221+
(message "\nRun test-current-buffer-coqc")
222+
223+
;; XXXX
224+
(setq switch-buffer-while-waiting nil)
225+
226+
;; (setq cct--debug-tests t)
227+
;; (setq coq--debug-auto-compilation t)
228+
(find-file "a.v")
229+
(setq av-buffer (current-buffer))
230+
231+
(find-file "c.v")
232+
(setq cdv-buffer (current-buffer))
233+
(set-buffer av-buffer)
234+
235+
(message (concat "coqdep: %s\ncoqc: %s\nPATH %s\n"
236+
"exec-path: %s\ndetected coq version: %s")
237+
coq-dependency-analyzer
238+
coq-compiler
239+
(getenv "PATH")
240+
exec-path
241+
coq-autodetected-version)
242+
243+
(with-current-buffer cdv-buffer
244+
(message (concat "\nProcess a.v to end, "
245+
"including compilation of dependency b.v\n"
246+
"while temporarily visiting c.v with\n"
247+
"coqdep: %s\ncoqc: %s")
248+
coq-dependency-analyzer
249+
coq-compiler))
250+
251+
;; Work around existing .vos and .vok files from other tests in
252+
;; this file.
253+
(message "\ntouch dependency b.v to force complete (re-)compilation")
254+
(should (set-file-times "b.v"))
255+
256+
(setq switch-buffer-while-waiting t)
257+
258+
;; This will temporarily switch to buffer c.v, which sets
259+
;; coq-compiler as local variable, see the hooks above.
260+
(cct-process-to-line 27)
261+
262+
;; (with-current-buffer coq--compile-response-buffer
263+
;; (message "coq-compile-response:\n%s\n<<<End"
264+
;; (buffer-substring-no-properties (point-min) (point-max))))
265+
266+
(cct-check-locked 26 'locked))
267+
268+
;; clean up
269+
(dolist (buf (list av-buffer cdv-buffer))
270+
(when buf
271+
(with-current-buffer buf
272+
(set-buffer-modified-p nil))
273+
(kill-buffer buf)))))

0 commit comments

Comments
 (0)