CI compile tests: add coqdep error detection tests

Add 3 tests to check that coqdep errors are reliably detected, see
also issue ProofGeneral#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

@@ -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

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 *)

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 *)

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 :=

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 *)

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.

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)))))

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
 

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"))))))
 

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

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)