Skip to content

Commit c14e54f

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

File tree

10 files changed

+398
-1
lines changed

10 files changed

+398
-1
lines changed

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

Lines changed: 24 additions & 0 deletions
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 <hendrik@askra.de>
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

Lines changed: 26 additions & 0 deletions
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 <hendrik@askra.de>
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

Lines changed: 15 additions & 0 deletions
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 <hendrik@askra.de>
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

Lines changed: 25 additions & 0 deletions
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 <hendrik@askra.de>
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

Lines changed: 25 additions & 0 deletions
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 <hendrik@askra.de>
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

Lines changed: 266 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,266 @@
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 <hendrik@askra.de>
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+
"Switch buffer in busy waiting hooks when t.
43+
Whether the hook functions `switch-to-other-buffer-while-waiting'
44+
and `switch-back-after-waiting' switch to some other buffer or
45+
not is controled by this variable. If t, switch to the buffer in
46+
`cdv-buffer' before starting busy waiting and switch back to the
47+
buffer in `av-buffer' after busy waiting.")
48+
49+
(defvar av-buffer nil
50+
"Buffer to switch back after busy waiting.
51+
See `switch-buffer-while-waiting'.")
52+
53+
(defvar cdv-buffer nil
54+
"Buffer to switch to before busy waiting.
55+
See `switch-buffer-while-waiting'.")
56+
57+
(defun switch-to-other-buffer-while-waiting ()
58+
"Hook to switch current buffer before busy waiting.
59+
Hook function for `cct-before-busy-waiting-hook'. Switches to
60+
`cdv-buffer' if `switch-buffer-while-waiting' is t."
61+
(when (and switch-buffer-while-waiting cdv-buffer)
62+
(message "Switch to buffer c.v while busy waiting")
63+
(set-buffer cdv-buffer)))
64+
65+
(defun switch-back-after-waiting ()
66+
"Hook to switch current buffer back after busy waiting.
67+
Hook function for `cct-after-busy-waiting-hook'. Switches back to
68+
`av-buffer' if `switch-buffer-while-waiting' is t."
69+
(when (and switch-buffer-while-waiting av-buffer)
70+
(message "Switch back to buffer a.v after busy waiting")
71+
(set-buffer av-buffer)))
72+
73+
(add-hook 'cct-before-busy-waiting-hook #'switch-to-other-buffer-while-waiting)
74+
(add-hook 'cct-after-busy-waiting-hook #'switch-back-after-waiting)
75+
76+
77+
;;; The tests itself
78+
79+
(ert-deftest test-current-buffer-vok ()
80+
:expected-result :failed
81+
"Check that second stage compilation uses the right local variables.
82+
Second stage compilation (vok and vio2vo) should use the local
83+
variables from the original scripting buffer, see also PG issue
84+
#797."
85+
(unwind-protect
86+
(progn
87+
(message "\nRun test-current-buffer-vok")
88+
89+
;; configure 2nd stage
90+
(if (coq--post-v811)
91+
(setq coq-compile-vos 'vos-and-vok)
92+
(setq coq-compile-quick 'quick-and-vio2vo))
93+
94+
;; (setq cct--debug-tests t)
95+
;; (setq coq--debug-auto-compilation t)
96+
(find-file "a.v")
97+
(setq av-buffer (current-buffer))
98+
99+
(find-file "c.v")
100+
(setq cdv-buffer (current-buffer))
101+
(set-buffer av-buffer)
102+
103+
(message (concat "coqdep: %s\ncoqc: %s\nPATH %s\n"
104+
"exec-path: %s\ndetected coq version: %s")
105+
coq-dependency-analyzer
106+
coq-compiler
107+
(getenv "PATH")
108+
exec-path
109+
coq-autodetected-version)
110+
111+
;; Work around existing .vos and .vok files from other tests in
112+
;; this file.
113+
(message "\ntouch dependency b.v to force complete (re-)compilation")
114+
(should (set-file-times "b.v"))
115+
116+
(message "\nProcess a.v to end, including compilation of dependency b.v")
117+
(cct-process-to-line 27)
118+
(cct-check-locked 26 'locked)
119+
120+
(with-current-buffer cdv-buffer
121+
(message
122+
(concat "\nWait for 2nd stage (vok/vio2vo) compilation "
123+
"in buffer b.v with"
124+
"\ncoqdep: %s\ncoqc: %s")
125+
coq-dependency-analyzer
126+
coq-compiler))
127+
128+
(setq switch-buffer-while-waiting t)
129+
130+
;; This will temporarily switch to buffer c.v, which sets
131+
;; coq-compiler as local variable, see the hooks above
132+
(cct-wait-for-second-stage)
133+
134+
(message "search for coq-error error message in compile-response buffer")
135+
(with-current-buffer coq--compile-response-buffer
136+
(goto-char (point-min))
137+
(should
138+
(not
139+
(re-search-forward "Error: coq-error has been executed" nil t)))))
140+
141+
;; clean up
142+
(dolist (buf (list av-buffer cdv-buffer))
143+
(when buf
144+
(with-current-buffer buf
145+
(set-buffer-modified-p nil))
146+
(kill-buffer buf)))
147+
(setq switch-buffer-while-waiting nil)))
148+
149+
(ert-deftest test-current-buffer-coqdep ()
150+
:expected-result :failed
151+
"Check that dependency analysis uses the right local variables.
152+
Dependency analysis during parallel background compilation (i.e.,
153+
runing `coqdep` on dependencies) should use the local variables
154+
from the original scripting buffer, see also PG issue #797."
155+
(unwind-protect
156+
(progn
157+
(message "\nRun test-current-buffer-coqdep")
158+
159+
;; (setq cct--debug-tests t)
160+
;; (setq coq--debug-auto-compilation t)
161+
(find-file "a.v")
162+
(setq av-buffer (current-buffer))
163+
164+
(find-file "d.v")
165+
(setq cdv-buffer (current-buffer))
166+
(set-buffer av-buffer)
167+
168+
(message (concat "coqdep: %s\ncoqc: %s\nPATH %s\n"
169+
"exec-path: %s\ndetected coq version: %s")
170+
coq-dependency-analyzer
171+
coq-compiler
172+
(getenv "PATH")
173+
exec-path
174+
coq-autodetected-version)
175+
176+
(with-current-buffer cdv-buffer
177+
(message
178+
(concat "\nProcess a.v to end while visiting d.v with"
179+
"\ncoqdep: %s\ncoqc: %s")
180+
coq-dependency-analyzer
181+
coq-compiler))
182+
183+
(setq switch-buffer-while-waiting t)
184+
185+
;; This will temporarily switch to buffer c.v, which sets
186+
;; coq-compiler as local variable, see the hooks above.
187+
(cct-process-to-line 27)
188+
189+
;; (with-current-buffer coq--compile-response-buffer
190+
;; (message "coq-compile-response:\n%s\n<<<End"
191+
;; (buffer-substring-no-properties (point-min) (point-max))))
192+
193+
(cct-check-locked 26 'locked))
194+
195+
;; clean up
196+
(dolist (buf (list av-buffer cdv-buffer))
197+
(when buf
198+
(with-current-buffer buf
199+
(set-buffer-modified-p nil))
200+
(kill-buffer buf)))
201+
(setq switch-buffer-while-waiting nil)))
202+
203+
(ert-deftest test-current-buffer-coqc ()
204+
:expected-result :failed
205+
"Check that compilation of dependencies uses the right local variables.
206+
Compilation of dependencies during parallel background
207+
compilation (i.e., runing `coqc` on dependencies) should use the
208+
local variables from the original scripting buffer, see also PG
209+
issue #797.
210+
211+
To ensure we only see errors from running `coqc`, we temporarily
212+
switch to buffer c.v, which sets `coq-compiler' but leaves
213+
`coq-dependency-analyzer' alone."
214+
(unwind-protect
215+
(progn
216+
(message "\nRun test-current-buffer-coqc")
217+
218+
;; (setq cct--debug-tests t)
219+
;; (setq coq--debug-auto-compilation t)
220+
(find-file "a.v")
221+
(setq av-buffer (current-buffer))
222+
223+
(find-file "c.v")
224+
(setq cdv-buffer (current-buffer))
225+
(set-buffer av-buffer)
226+
227+
(message (concat "coqdep: %s\ncoqc: %s\nPATH %s\n"
228+
"exec-path: %s\ndetected coq version: %s")
229+
coq-dependency-analyzer
230+
coq-compiler
231+
(getenv "PATH")
232+
exec-path
233+
coq-autodetected-version)
234+
235+
(with-current-buffer cdv-buffer
236+
(message (concat "\nProcess a.v to end, "
237+
"including compilation of dependency b.v\n"
238+
"while temporarily visiting c.v with\n"
239+
"coqdep: %s\ncoqc: %s")
240+
coq-dependency-analyzer
241+
coq-compiler))
242+
243+
;; Work around existing .vos and .vok files from other tests in
244+
;; this file.
245+
(message "\ntouch dependency b.v to force complete (re-)compilation")
246+
(should (set-file-times "b.v"))
247+
248+
(setq switch-buffer-while-waiting t)
249+
250+
;; This will temporarily switch to buffer c.v, which sets
251+
;; coq-compiler as local variable, see the hooks above.
252+
(cct-process-to-line 27)
253+
254+
;; (with-current-buffer coq--compile-response-buffer
255+
;; (message "coq-compile-response:\n%s\n<<<End"
256+
;; (buffer-substring-no-properties (point-min) (point-max))))
257+
258+
(cct-check-locked 26 'locked))
259+
260+
;; clean up
261+
(dolist (buf (list av-buffer cdv-buffer))
262+
(when buf
263+
(with-current-buffer buf
264+
(set-buffer-modified-p nil))
265+
(kill-buffer buf)))
266+
(setq switch-buffer-while-waiting nil)))

‎ci/compile-tests/README.md

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -39,6 +39,9 @@ All tests are for parallel background compilation.
3939
dependee is still processing
4040
010-coqdep-errors
4141
: check that coqdep errors are reliably detected
42+
011-current-buffer
43+
: check that background compilation is not confused by local variables
44+
in unrelated buffers
4245

4346
# Tests currently missing
4447

0 commit comments

Comments
 (0)