[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
[nongnu] elpa/proof-general ff596f0620 1/3: CI compile tests: add coqdep
|
From: |
ELPA Syncer |
|
Subject: |
[nongnu] elpa/proof-general ff596f0620 1/3: CI compile tests: add coqdep error detection tests |
|
Date: |
Sun, 7 Jan 2024 19:00:15 -0500 (EST) |
branch: elpa/proof-general
commit ff596f0620d943b778001a09009735012df2ee1d
Author: Hendrik Tews <hendrik@askra.de>
Commit: hendriktews <hendrik@askra.de>
CI compile tests: add coqdep error detection tests
Add 3 tests to check that coqdep errors are reliably detected, see
also issue #722. Two of them are expected to fail for 8.19, because
coqdep output changed in that version.
---
ci/compile-tests/010-coqdep-errors/Makefile | 19 ++++
ci/compile-tests/010-coqdep-errors/a.v | 21 +++++
ci/compile-tests/010-coqdep-errors/b.v | 21 +++++
ci/compile-tests/010-coqdep-errors/c.v | 16 ++++
ci/compile-tests/010-coqdep-errors/d.v | 21 +++++
ci/compile-tests/010-coqdep-errors/e.v | 15 +++
ci/compile-tests/010-coqdep-errors/runtest.el | 126 ++++++++++++++++++++++++++
ci/compile-tests/README.md | 2 +
coq/coq-compile-common.el | 5 +-
coq/coq-par-compile.el | 2 +-
coq/coq-system.el | 12 +++
11 files changed, 258 insertions(+), 2 deletions(-)
diff --git a/ci/compile-tests/010-coqdep-errors/Makefile
b/ci/compile-tests/010-coqdep-errors/Makefile
new file mode 100644
index 0000000000..76cc1939b2
--- /dev/null
+++ b/ci/compile-tests/010-coqdep-errors/Makefile
@@ -0,0 +1,19 @@
+# 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
+
+
+.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
+
+.PHONY: clean
+clean:
+ rm -f *.vo *.glob *.vio *.vos *.vok .*.aux
diff --git a/ci/compile-tests/010-coqdep-errors/a.v
b/ci/compile-tests/010-coqdep-errors/a.v
new file mode 100644
index 0000000000..95c93d537d
--- /dev/null
+++ b/ci/compile-tests/010-coqdep-errors/a.v
@@ -0,0 +1,21 @@
+(* 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.
+ *)
+
+(* This is line 19 *)
+Require X25XX.
+(* This is line 21 *)
diff --git a/ci/compile-tests/010-coqdep-errors/b.v
b/ci/compile-tests/010-coqdep-errors/b.v
new file mode 100644
index 0000000000..756e312350
--- /dev/null
+++ b/ci/compile-tests/010-coqdep-errors/b.v
@@ -0,0 +1,21 @@
+(* 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.
+ *)
+
+(* This is line 19 *)
+Require c.
+(* This is line 21 *)
diff --git a/ci/compile-tests/010-coqdep-errors/c.v
b/ci/compile-tests/010-coqdep-errors/c.v
new file mode 100644
index 0000000000..8595f626d6
--- /dev/null
+++ b/ci/compile-tests/010-coqdep-errors/c.v
@@ -0,0 +1,16 @@
+(* 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 next line intentionally contains a syntax error. *)
+Definition c : nat :=
diff --git a/ci/compile-tests/010-coqdep-errors/d.v
b/ci/compile-tests/010-coqdep-errors/d.v
new file mode 100644
index 0000000000..2d46631742
--- /dev/null
+++ b/ci/compile-tests/010-coqdep-errors/d.v
@@ -0,0 +1,21 @@
+(* 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.
+ *)
+
+(* This is line 19 *)
+Require e.
+(* This is line 21 *)
diff --git a/ci/compile-tests/010-coqdep-errors/e.v
b/ci/compile-tests/010-coqdep-errors/e.v
new file mode 100644
index 0000000000..ec5523ebf8
--- /dev/null
+++ b/ci/compile-tests/010-coqdep-errors/e.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 runtest.el in this directory.
+ *)
+
+Require X25XX.
diff --git a/ci/compile-tests/010-coqdep-errors/runtest.el
b/ci/compile-tests/010-coqdep-errors/runtest.el
new file mode 100644
index 0000000000..646ff2a5b7
--- /dev/null
+++ b/ci/compile-tests/010-coqdep-errors/runtest.el
@@ -0,0 +1,126 @@
+;; 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 reliably detects coqdep
+;; errors. There are three tests that check the following coqdep errors:
+;; - coqdep on a require fails because of a missing library (using a.v)
+;; - coqdep on a dependency fails because of a syntax error (using b.v)
+;; - coqdep on a dependency fails because of a missing library (using d.v)
+;;
+;; The following graph shows the file dependencies in these test:
+;;
+;; a b d
+;; | |
+;; c e
+
+
+;; 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)
+
+;;; Define the tests
+
+(ert-deftest cct-coqdep-fail-on-require ()
+ :expected-result (if (coq--post-v818) :failed :passed)
+ "coqdep error on missing library in a require command is detected."
+ ;; (setq cct--debug-tests t)
+ ;; (setq coq--debug-auto-compilation t)
+ (let (coqdep-errror-in-response
+ missing-module-in-response
+ missing-module-in-coq)
+ (find-file "a.v")
+ (message "coqdep error detection test: non-existing module in require")
+ (cct-process-to-line 21)
+ (cct-check-locked 20 'unlocked)
+ (with-current-buffer coq--compile-response-buffer
+ ;; (message "|%s|" (buffer-string))
+ (goto-char (1+ (length coq--compile-response-initial-content)))
+ (setq coqdep-errror-in-response (looking-at "^coqdep "))
+ (setq missing-module-in-response (search-forward "X25XX" nil t)))
+ (with-current-buffer proof-shell-buffer
+ (goto-char (point-min))
+ (setq missing-module-in-coq (search-forward "X25XX" nil t)))
+ (message
+ (concat "CHECK RESULT: *coq-compile-response* %s report a coqdep
problem\n"
+ "\tand the missing module X25XX %s in *coq-compile-response*\n"
+ "\tand it %s in *coq*")
+ (if coqdep-errror-in-response "DOES" "DOES NOT")
+ (if missing-module-in-response "IS" "IS NOT")
+ (if missing-module-in-coq "IS" "IS NOT"))
+ (should (and coqdep-errror-in-response
+ missing-module-in-response
+ (not missing-module-in-coq)))))
+
+
+(ert-deftest cct-coqdep-syntax-error-dependency ()
+ "coqdep syntax error on a dependency is detected."
+ ;; (setq cct--debug-tests t)
+ ;; (setq coq--debug-auto-compilation t)
+ (let (coqdep-errror-in-response
+ syntax-error-in-response
+ dependency-in-coq)
+ (find-file "b.v")
+ (message "coqdep error detection test: non-existing module in dependency")
+ (cct-process-to-line 21)
+ (cct-check-locked 20 'unlocked)
+ (with-current-buffer coq--compile-response-buffer
+ ;; (message "|%s|" (buffer-string))
+ (goto-char (1+ (length coq--compile-response-initial-content)))
+ (setq coqdep-errror-in-response (looking-at "^coqdep "))
+ (setq syntax-error-in-response (search-forward "Syntax error" nil t)))
+ (with-current-buffer proof-shell-buffer
+ (goto-char (point-min))
+ (setq dependency-in-coq (search-forward "Require c." nil t)))
+ (message
+ (concat "CHECK RESULT: *coq-compile-response* %s report a coqdep
problem\n"
+ "\tand *coq-compile-response* %s contain a syntax error\n"
+ "\tand 'Require c' %s in *coq*")
+ (if coqdep-errror-in-response "DOES" "DOES NOT")
+ (if syntax-error-in-response "DOES" "DOES NOT")
+ (if dependency-in-coq "IS" "IS NOT"))
+ (should (and coqdep-errror-in-response
+ syntax-error-in-response
+ (not dependency-in-coq)))))
+
+
+(ert-deftest cct-coqdep-fail-on-require-in-dependency ()
+ :expected-result (if (coq--post-v818) :failed :passed)
+ "coqdep error because of a missing library in a dependency is detected."
+ (let (coqdep-errror-in-response
+ missing-module-in-response
+ dependency-in-coq)
+ (find-file "d.v")
+ (message "coqdep error detection test: non-existing module in dependency")
+ (cct-process-to-line 21)
+ (cct-check-locked 20 'unlocked)
+ (with-current-buffer coq--compile-response-buffer
+ ;; (message "|%s|" (buffer-string))
+ (goto-char (1+ (length coq--compile-response-initial-content)))
+ (setq coqdep-errror-in-response (looking-at "^coqdep "))
+ (setq missing-module-in-response (search-forward "X25XX" nil t)))
+ (with-current-buffer proof-shell-buffer
+ (goto-char (point-min))
+ (setq dependency-in-coq (search-forward "Require d." nil t)))
+ (message
+ (concat "CHECK RESULT: *coq-compile-response* %s report a coqdep
problem\n"
+ "\tand missing module X25XX %s in *coq-compile-response*\n"
+ "\tand require %s in *coq*")
+ (if coqdep-errror-in-response "DOES" "DOES NOT")
+ (if missing-module-in-response "IS" "IS NOT")
+ (if dependency-in-coq "IS" "IS NOT"))
+ (should (and coqdep-errror-in-response
+ missing-module-in-response
+ (not dependency-in-coq)))))
diff --git a/ci/compile-tests/README.md b/ci/compile-tests/README.md
index 3bf3b62ddd..2e578c97d4 100644
--- a/ci/compile-tests/README.md
+++ b/ci/compile-tests/README.md
@@ -37,6 +37,8 @@ All tests are for parallel background compilation.
coq-compile-keep-going; test also the case, where the last
(failed) require job must be delayed, because some queue
dependee is still processing
+010-coqdep-errors
+: check that coqdep errors are reliably detected
# Tests currently missing
diff --git a/coq/coq-compile-common.el b/coq/coq-compile-common.el
index 8074d7faf1..f5a9da8bf8 100644
--- a/coq/coq-compile-common.el
+++ b/coq/coq-compile-common.el
@@ -666,6 +666,9 @@ Changes the suffix from .vo to .vok. VO-OBJ-FILE must have
a .vo suffix."
;;; manage coq--compile-response-buffer
+(defconst coq--compile-response-initial-content "-*- mode: compilation;
-*-\n\n"
+ "Content of `coq--compile-response-buffer' after initialization")
+
;; XXX apparently nobody calls this with display equal to nil
(defun coq-compile-display-error (command error-message display)
"Display COMMAND and ERROR-MESSAGE in `coq--compile-response-buffer'.
@@ -708,7 +711,7 @@ the command whose output will appear in the buffer."
;; the first line are not found for some reason ...
(let ((inhibit-read-only t))
(with-current-buffer buffer-object
- (insert "-*- mode: compilation; -*-\n\n")
+ (insert coq--compile-response-initial-content)
(when command
(insert command "\n"))))))
diff --git a/coq/coq-par-compile.el b/coq/coq-par-compile.el
index ecf7545862..4f3155d532 100644
--- a/coq/coq-par-compile.el
+++ b/coq/coq-par-compile.el
@@ -768,7 +768,7 @@ load-path options to coqdep."
(defun coq-par-analyse-coq-dep-exit (status output command)
"Analyse output OUTPUT of coqdep command COMMAND with exit status STATUS.
Returns the list of .vo dependencies if there is no error. Otherwise,
-writes an error message into `coq-compile-response-buffer', makes
+writes an error message into `coq--compile-response-buffer', makes
this buffer visible and returns a string.
This function does always return .vo dependencies, regardless of the
diff --git a/coq/coq-system.el b/coq/coq-system.el
index 5031404e28..28c9dce4f3 100644
--- a/coq/coq-system.el
+++ b/coq/coq-system.el
@@ -231,6 +231,18 @@ Return nil if the version cannot be detected."
(signal 'coq-unclassifiable-version coq-version-to-use))
(t (signal (car err) (cdr err))))))))
+(defun coq--post-v818 ()
+ "Return t if the auto-detected version of Coq is >= 8.19alpha.
+Return nil if the version cannot be detected."
+ (let ((coq-version-to-use (or (coq-version t) "8.18")))
+ (condition-case err
+ (not (coq--version< coq-version-to-use "8.19alpha"))
+ (error
+ (cond
+ ((equal (substring (cadr err) 0 15) "Invalid version")
+ (signal 'coq-unclassifiable-version coq-version-to-use))
+ (t (signal (car err) (cdr err))))))))
+
(defun coq--supports-topfile ()
"Return t if \"-topfile\" appears in coqtop options"
(string-match "-topfile" coq-autodetected-help)