From c14e54fb8f2f754c319e955f9d09d1d357544f1f Mon Sep 17 00:00:00 2001 From: Hendrik Tews Date: Sat, 9 Nov 2024 14:54:09 +0100 Subject: [PATCH] test that Coq background compilation is not affected by local variables See also #797 --- ci/compile-tests/011-current-buffer/Makefile | 24 ++ ci/compile-tests/011-current-buffer/a.v | 26 ++ ci/compile-tests/011-current-buffer/b.v | 15 + ci/compile-tests/011-current-buffer/c.v | 25 ++ ci/compile-tests/011-current-buffer/d.v | 25 ++ .../011-current-buffer/runtest.el | 266 ++++++++++++++++++ ci/compile-tests/README.md | 3 + ci/compile-tests/bin/coq-error | 11 + ci/compile-tests/cct-lib.el | 2 +- coq/coq-system.el | 2 + 10 files changed, 398 insertions(+), 1 deletion(-) create mode 100644 ci/compile-tests/011-current-buffer/Makefile create mode 100644 ci/compile-tests/011-current-buffer/a.v create mode 100644 ci/compile-tests/011-current-buffer/b.v create mode 100644 ci/compile-tests/011-current-buffer/c.v create mode 100644 ci/compile-tests/011-current-buffer/d.v create mode 100644 ci/compile-tests/011-current-buffer/runtest.el create mode 100755 ci/compile-tests/bin/coq-error diff --git a/ci/compile-tests/011-current-buffer/Makefile b/ci/compile-tests/011-current-buffer/Makefile new file mode 100644 index 000000000..456af742b --- /dev/null +++ b/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 +# +# 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 diff --git a/ci/compile-tests/011-current-buffer/a.v b/ci/compile-tests/011-current-buffer/a.v new file mode 100644 index 000000000..0b35539fc --- /dev/null +++ b/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 + * + * 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 *) diff --git a/ci/compile-tests/011-current-buffer/b.v b/ci/compile-tests/011-current-buffer/b.v new file mode 100644 index 000000000..820e1449d --- /dev/null +++ b/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 + * + * 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. diff --git a/ci/compile-tests/011-current-buffer/c.v b/ci/compile-tests/011-current-buffer/c.v new file mode 100644 index 000000000..c29c82754 --- /dev/null +++ b/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 + * + * 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: ***) diff --git a/ci/compile-tests/011-current-buffer/d.v b/ci/compile-tests/011-current-buffer/d.v new file mode 100644 index 000000000..2dffd4574 --- /dev/null +++ b/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 + * + * 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: ***) diff --git a/ci/compile-tests/011-current-buffer/runtest.el b/ci/compile-tests/011-current-buffer/runtest.el new file mode 100644 index 000000000..514cc40b2 --- /dev/null +++ b/ci/compile-tests/011-current-buffer/runtest.el @@ -0,0 +1,266 @@ +;; This file is part of Proof General. -*- lexical-binding: t; -*- +;; +;; © Copyright 2024 Hendrik Tews +;; +;; Authors: Hendrik Tews +;; Maintainer: Hendrik Tews +;; +;; 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 + "Switch buffer in busy waiting hooks when t. +Whether the hook functions `switch-to-other-buffer-while-waiting' +and `switch-back-after-waiting' switch to some other buffer or +not is controled by this variable. If t, switch to the buffer in +`cdv-buffer' before starting busy waiting and switch back to the +buffer in `av-buffer' after busy waiting.") + +(defvar av-buffer nil + "Buffer to switch back after busy waiting. +See `switch-buffer-while-waiting'.") + +(defvar cdv-buffer nil + "Buffer to switch to before busy waiting. +See `switch-buffer-while-waiting'.") + +(defun switch-to-other-buffer-while-waiting () + "Hook to switch current buffer before busy waiting. +Hook function for `cct-before-busy-waiting-hook'. Switches to +`cdv-buffer' if `switch-buffer-while-waiting' is t." + (when (and switch-buffer-while-waiting cdv-buffer) + (message "Switch to buffer c.v while busy waiting") + (set-buffer cdv-buffer))) + +(defun switch-back-after-waiting () + "Hook to switch current buffer back after busy waiting. +Hook function for `cct-after-busy-waiting-hook'. Switches back to +`av-buffer' if `switch-buffer-while-waiting' is t." + (when (and 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 :failed + "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") + + ;; 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))) + (setq switch-buffer-while-waiting nil))) + +(ert-deftest test-current-buffer-coqdep () + :expected-result :failed + "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." + (unwind-protect + (progn + (message "\nRun test-current-buffer-coqdep") + + ;; (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) + + (with-current-buffer cdv-buffer + (message + (concat "\nProcess a.v to end 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<< /dev/stderr + +exit 1 diff --git a/ci/compile-tests/cct-lib.el b/ci/compile-tests/cct-lib.el index 7a5a427c9..76e9b2552 100644 --- a/ci/compile-tests/cct-lib.el +++ b/ci/compile-tests/cct-lib.el @@ -116,7 +116,7 @@ backward. Replace the word there with WORD." (insert word)) (defun cct-process-to-line (line) - "Assert/retract to line LINE and wait until processing completed. + "Assert/retract to start of line LINE and wait until processing completed. Runs `cct-before-busy-waiting-hook' and `cct-after-busy-waiting-hook' before and after busy waiting for the prover. In many tests these hooks are not used." diff --git a/coq/coq-system.el b/coq/coq-system.el index ad65cc4bc..56178c2e2 100644 --- a/coq/coq-system.el +++ b/coq/coq-system.el @@ -49,6 +49,7 @@ On Windows you might need something like: (proof-locate-executable "coqdep" t '("C:/Program Files/Coq/bin"))) "Command to invoke coqdep." :type 'string + :safe 'stringp :group 'coq) (defcustom coq-compiler @@ -56,6 +57,7 @@ On Windows you might need something like: (proof-locate-executable "coqc" t '("C:/Program Files/Coq/bin"))) "Command to invoke the coq compiler." :type 'string + :safe 'stringp :group 'coq) (defcustom coq-pinned-version nil