test that Coq background compilation is not affected by local variables

See also #797

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

@@ -0,0 +1,24 @@
+# This file is part of Proof General.
+# 
+# © Copyright 2024  Hendrik Tews
+# 
+# Authors: Hendrik Tews
+# Maintainer: Hendrik Tews <hendrik@askra.de>
+# 
+# SPDX-License-Identifier: GPL-3.0-or-later
+
+# This test uses ../bin/compile-test-start-delayed to start certain
+# commands with specified delays to check carfully constructed
+# internal states. compile-test-start-delayed outputs diagnostics on
+# file descriptor 9, which bypasses emacs and is joined with stderr of
+# the current make. Open file descriptor 9 here.
+.PHONY: test
+test:
+	$(MAKE) clean
+	emacs -batch -l ../../../generic/proof-site.el -l ../cct-lib.el \
+		-l runtest.el -f ert-run-tests-batch-and-exit \
+		9>&1
+
+.PHONY: clean
+clean:
+	rm -f *.vo *.glob *.vio *.vos *.vok .*.aux

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

@@ -0,0 +1,26 @@
+(* This file is part of Proof General.
+ *
+ * © Copyright 2024  Hendrik Tews
+ *
+ * Authors: Hendrik Tews
+ * Maintainer: Hendrik Tews <hendrik@askra.de>
+ *
+ * SPDX-License-Identifier: GPL-3.0-or-later
+ *
+ *
+ * This file is part of an automatic test case for parallel background
+ * compilation in coq-par-compile.el. See runtest.el in this directory.
+ *)
+
+(* The test script relies on absolute line numbers. 
+ * DO NOT INSERT ANY LINE UNLESS YOU KNOW WHAT YOU ARE DOING.
+ *)
+
+(* The delay for coqdep is specified in comments with key coqdep-delay,
+ * see compile-test-start-delayed.
+ *)
+
+
+(* This is line 24 *)
+Require Export (* coqdep-delay 1 *) b.
+(* This is line 26 *)

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

@@ -0,0 +1,15 @@
+(* This file is part of Proof General.
+ *
+ * © Copyright 2024  Hendrik Tews
+ *
+ * Authors: Hendrik Tews
+ * Maintainer: Hendrik Tews <hendrik@askra.de>
+ *
+ * SPDX-License-Identifier: GPL-3.0-or-later
+ *
+ *
+ * This file is part of an automatic test case for parallel background
+ * compilation in coq-par-compile.el. See test.el in this directory.
+ *)
+
+Definition b : nat := 2.

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

@@ -0,0 +1,25 @@
+(* This file is part of Proof General.
+ *
+ * © Copyright 2024  Hendrik Tews
+ *
+ * Authors: Hendrik Tews
+ * Maintainer: Hendrik Tews <hendrik@askra.de>
+ *
+ * SPDX-License-Identifier: GPL-3.0-or-later
+ *
+ *
+ * This file is part of an automatic test case for parallel background
+ * compilation in coq-par-compile.el. See test.el in this directory.
+ *)
+
+Definition c : nat := 2.
+
+(* Set `coq-compiler` and `coq-dependency-analyzer` as local variable
+   to something that definitely fails when the test (or the user)
+   visits this file in an ongoing background compilation and
+   background compilation picks up local variables from this file.
+ *)
+
+(*** Local Variables: ***)
+(*** coq-compiler: "coq-error" ***)
+(*** End: ***)

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

@@ -0,0 +1,25 @@
+(* This file is part of Proof General.
+ *
+ * © Copyright 2024  Hendrik Tews
+ *
+ * Authors: Hendrik Tews
+ * Maintainer: Hendrik Tews <hendrik@askra.de>
+ *
+ * SPDX-License-Identifier: GPL-3.0-or-later
+ *
+ *
+ * This file is part of an automatic test case for parallel background
+ * compilation in coq-par-compile.el. See test.el in this directory.
+ *)
+
+Definition c : nat := 2.
+
+(* Set `coq-compiler` and `coq-dependency-analyzer` as local variable
+   to something that definitely fails when the test (or the user)
+   visits this file in an ongoing background compilation and
+   background compilation picks up local variables from this file.
+ *)
+
+(*** Local Variables: ***)
+(*** coq-dependency-analyzer: "coq-error" ***)
+(*** End: ***)

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

@@ -0,0 +1,273 @@
+;; This file is part of Proof General.  -*- lexical-binding: t; -*-
+;; 
+;; © Copyright 2024  Hendrik Tews
+;; 
+;; Authors: Hendrik Tews
+;; Maintainer: Hendrik Tews <hendrik@askra.de>
+;; 
+;; SPDX-License-Identifier: GPL-3.0-or-later
+
+;;; Commentary:
+;;
+;; Coq Compile Tests (cct) --
+;; ert tests for parallel background compilation for Coq
+;;
+;; Test that parallel background compilation is not confused by local
+;; variables in unrelated buffers.
+;;
+;; The dependencies in this test are:
+;; 
+;;           a     c    d
+;;           |
+;;           b
+;;
+;; Files c and d are completely independent of file a and file b and
+;; not processed by Coq. The idea is that files c or d come from a
+;; different project that uses a different `coq-compiler' or
+;; `coq-dependency-analyzer', see also PG issue #797. These different
+;; local settings should not confuse the ongoing background
+;; compilation of file b for processing file a in a script buffer.
+;; File c sets `coq-compiler' as local variable and file d sets
+;; `coq-dependency-analyzer' as local variable.
+
+
+;; require cct-lib for the elisp compilation, otherwise this is present already
+(require 'cct-lib "ci/compile-tests/cct-lib")
+
+;;; set configuration
+(cct-configure-proof-general)
+(configure-delayed-coq)    
+
+(defvar switch-buffer-while-waiting nil
+  "XXX")
+
+(defvar av-buffer nil
+  "XXX")
+
+(defvar cdv-buffer nil
+  "XXX")
+
+(defun switch-to-other-buffer-while-waiting ()
+  "XXX"
+  (when (and nil switch-buffer-while-waiting cdv-buffer)
+    (message "Switch to buffer c.v while busy waiting")
+    (set-buffer cdv-buffer)))
+
+(defun switch-back-after-waiting ()
+  "XXX"
+  (when (and nil switch-buffer-while-waiting av-buffer)
+    (message "Switch back to buffer a.v after busy waiting")
+    (set-buffer av-buffer)))
+
+(add-hook 'cct-before-busy-waiting-hook #'switch-to-other-buffer-while-waiting)
+(add-hook 'cct-after-busy-waiting-hook #'switch-back-after-waiting)
+
+
+;;; The tests itself
+
+(ert-deftest test-current-buffer-vok ()
+  :expected-result :passed
+  "Check that second stage compilation uses the right local variables.
+Second stage compilation (vok and vio2vo) should use the local
+variables from the original scripting buffer, see also PG issue
+#797."
+  (unwind-protect
+      (progn
+        (message "\nRun test-current-buffer-vok")
+
+        ;; XXXX
+        (setq switch-buffer-while-waiting nil)
+
+        ;; configure 2nd stage
+        (if (coq--post-v811)
+            (setq coq-compile-vos 'vos-and-vok)
+          (setq coq-compile-quick 'quick-and-vio2vo))
+
+        ;; (setq cct--debug-tests t)
+        ;; (setq coq--debug-auto-compilation t)
+        (find-file "a.v")
+        (setq av-buffer (current-buffer))
+
+        (find-file "c.v")
+        (setq cdv-buffer (current-buffer))
+        (set-buffer av-buffer)
+
+        (message (concat "coqdep: %s\ncoqc: %s\nPATH %s\n"
+                         "exec-path: %s\ndetected coq version: %s")
+         coq-dependency-analyzer
+         coq-compiler
+         (getenv "PATH")
+         exec-path
+         coq-autodetected-version)
+
+        ;; Work around existing .vos and .vok files from other tests in
+        ;; this file.
+        (message "\ntouch dependency b.v to force complete (re-)compilation")
+        (should (set-file-times "b.v"))
+
+        (message "\nProcess a.v to end, including compilation of dependency b.v")
+        (cct-process-to-line 27)
+        (cct-check-locked 26 'locked)
+
+        (with-current-buffer cdv-buffer
+          (message
+           (concat "\nWait for 2nd stage (vok/vio2vo) compilation "
+                   "in buffer b.v with"
+                   "\ncoqdep: %s\ncoqc: %s")
+           coq-dependency-analyzer
+           coq-compiler))
+
+        (setq switch-buffer-while-waiting t)
+
+        ;; This will temporarily switch to buffer c.v, which sets
+        ;; coq-compiler as local variable, see the hooks above
+        (cct-wait-for-second-stage)
+
+        (message "search for coq-error error message in compile-response buffer")
+        (with-current-buffer coq--compile-response-buffer
+          (goto-char (point-min))
+          (should
+           (not
+            (re-search-forward "Error: coq-error has been executed" nil t)))))
+
+    ;; clean up
+    (dolist (buf (list av-buffer cdv-buffer))
+      (when buf
+        (with-current-buffer buf
+          (set-buffer-modified-p nil))
+        (kill-buffer buf)))))
+
+(ert-deftest test-current-buffer-coqdep ()
+  :expected-result :passed
+  "Check that dependency analysis uses the right local variables.
+Dependency analysis during parallel background compilation (i.e.,
+runing `coqdep` on dependencies) should use the local variables
+from the original scripting buffer, see also PG issue #797.
+
+To ensure we only see errors from dependency analysis, we first
+process file a completely without trying to confuse parallel
+background compilation."
+  (unwind-protect
+      (progn
+        (message "\nRun test-current-buffer-coqdep")
+
+        ;; XXXX
+        (setq switch-buffer-while-waiting nil)
+
+        ;; (setq cct--debug-tests t)
+        ;; (setq coq--debug-auto-compilation t)
+        (find-file "a.v")
+        (setq av-buffer (current-buffer))
+
+        (find-file "d.v")
+        (setq cdv-buffer (current-buffer))
+        (set-buffer av-buffer)
+
+        (message (concat "coqdep: %s\ncoqc: %s\nPATH %s\n"
+                         "exec-path: %s\ndetected coq version: %s")
+         coq-dependency-analyzer
+         coq-compiler
+         (getenv "PATH")
+         exec-path
+         coq-autodetected-version)
+
+        (message "\nProcess a.v to end, including compilation of dependency b.v")
+        (cct-process-to-line 27)
+        (cct-check-locked 26 'locked)
+
+        (message "\nRetract a.v before the require command")
+        (cct-process-to-line 20)
+        (cct-check-locked 25 'unlocked)
+
+        (with-current-buffer cdv-buffer
+          (message
+           (concat "\nProcess the require command again while visiting d.v with"
+                   "\ncoqdep: %s\ncoqc: %s")
+           coq-dependency-analyzer
+           coq-compiler))
+
+        (setq switch-buffer-while-waiting t)
+
+        ;; This will temporarily switch to buffer c.v, which sets
+        ;; coq-compiler as local variable, see the hooks above.
+        (cct-process-to-line 27)
+
+        ;; (with-current-buffer coq--compile-response-buffer
+        ;;   (message "coq-compile-response:\n%s\n<<<End"
+        ;;            (buffer-substring-no-properties (point-min) (point-max))))
+
+        (cct-check-locked 26 'locked))
+
+    ;; clean up
+    (dolist (buf (list av-buffer cdv-buffer))
+      (when buf
+        (with-current-buffer buf
+          (set-buffer-modified-p nil))
+        (kill-buffer buf)))))
+
+(ert-deftest test-current-buffer-coqc ()
+  :expected-result :passed
+  "Check that compilation of dependencies uses the right local variables.
+Compilation of dependencies during parallel background
+compilation (i.e., runing `coqc` on dependencies) should use the
+local variables from the original scripting buffer, see also PG
+issue #797.
+
+To ensure we only see errors from running `coqc`, we temporarily
+switch to buffer c.v, which sets `coq-compiler' but leaves
+`coq-dependency-analyzer' alone."
+  (unwind-protect
+      (progn
+        (message "\nRun test-current-buffer-coqc")
+
+        ;; XXXX
+        (setq switch-buffer-while-waiting nil)
+
+        ;; (setq cct--debug-tests t)
+        ;; (setq coq--debug-auto-compilation t)
+        (find-file "a.v")
+        (setq av-buffer (current-buffer))
+
+        (find-file "c.v")
+        (setq cdv-buffer (current-buffer))
+        (set-buffer av-buffer)
+
+        (message (concat "coqdep: %s\ncoqc: %s\nPATH %s\n"
+                         "exec-path: %s\ndetected coq version: %s")
+         coq-dependency-analyzer
+         coq-compiler
+         (getenv "PATH")
+         exec-path
+         coq-autodetected-version)
+
+        (with-current-buffer cdv-buffer
+          (message (concat "\nProcess a.v to end, "
+                           "including compilation of dependency b.v\n"
+                           "while temporarily visiting c.v with\n"
+                           "coqdep: %s\ncoqc: %s")
+           coq-dependency-analyzer
+           coq-compiler))
+
+        ;; Work around existing .vos and .vok files from other tests in
+        ;; this file.
+        (message "\ntouch dependency b.v to force complete (re-)compilation")
+        (should (set-file-times "b.v"))
+
+        (setq switch-buffer-while-waiting t)
+
+        ;; This will temporarily switch to buffer c.v, which sets
+        ;; coq-compiler as local variable, see the hooks above.
+        (cct-process-to-line 27)
+
+        ;; (with-current-buffer coq--compile-response-buffer
+        ;;   (message "coq-compile-response:\n%s\n<<<End"
+        ;;            (buffer-substring-no-properties (point-min) (point-max))))
+
+        (cct-check-locked 26 'locked))
+
+    ;; clean up
+    (dolist (buf (list av-buffer cdv-buffer))
+      (when buf
+        (with-current-buffer buf
+          (set-buffer-modified-p nil))
+        (kill-buffer buf)))))