reliably detect coqdep errors for 8.19

CHANGES

@@ -5,7 +5,14 @@ the Git ChangeLog, the GitHub repo https://github.com/ProofGeneral/PG
 
 * Changes of Proof General 4.6 from Proof General 4.5
 
-N/A
+** Coq changes
+
+*** support Coq 8.19
+
+**** New option coq-compile-coqdep-warnings to configure the warning
+     command line argument (-w) of coqdep. The default of this option
+     is +module-not-found to let Proof General reliably detect missing
+     modules as coqdep error.
 
 * Changes of Proof General 4.5 from Proof General 4.4
 

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 <[email protected]>
+# 
+# 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 <[email protected]>
+ *
+ * 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 <[email protected]>
+ *
+ * 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 <[email protected]>
+ *
+ * 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 <[email protected]>
+ *
+ * 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 <[email protected]>
+ *
+ * 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,124 @@
+;; This file is part of Proof General.  -*- lexical-binding: t; -*-
+;; 
+;; © Copyright 2024  Hendrik Tews
+;; 
+;; Authors: Hendrik Tews
+;; Maintainer: Hendrik Tews <[email protected]>
+;; 
+;; 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 ()
+  "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 ()
+  "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

@@ -522,8 +522,20 @@ or not."
   :type '(repeat regexp)
   :safe (lambda (v) (cl-every #'stringp v)))
 
+(defcustom coq-compile-coqdep-warnings '("+module-not-found")
+  "List of warning options passed to coqdep via `-w` for Coq 8.19 or later.
+List of warning options to be passed to coqdep via command line
+switch `-w`, which is supported from Coq 8.19 onwards. This
+option is ignored for a detected Coq version earlier than 8.19. A
+minus in front of a warning disables the warning, a plus turns
+the warning into an error. This option should contain
+'+module-not-found' to let Proof General reliably detect missing
+modules via an coqdep error."
+  :type '(repeat string)
+  :safe (lambda (v) (cl-every #'stringp v)))
+
 (defcustom coq-coqdep-error-regexp
-  (concat "^\\*\\*\\* Warning: in file .*, library .* is required "
+  (concat "^\\(\\*\\*\\* \\)?Warning: in file .*, library[ \n].* is required "
           "and has not been found")
   "Regexp to match errors in the output of coqdep.
 coqdep indicates errors not always via a non-zero exit status,
@@ -666,6 +678,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 +723,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

@@ -745,14 +745,24 @@ ignored, because they can never participate in a cycle."
     (mapcar (lambda (j) (get j 'src-file)) cycle)))
 
 
-;;; map coq module names to files, using synchronously running coqdep
+;;; map coq module names to files, using coqdep
+
+(defun coq-par-coqdep-warning-arguments ()
+  "Return a fresh list with the warning command line arguments for coqdep.
+Warnings (`-w`) are supported in coqdep from 8.19 onwards.
+Therefore return the empty list for a detected Coq version
+earlier than 8.19."
+  (if (and (coq--post-v818) (consp coq-compile-coqdep-warnings))
+      (list "-w" (mapconcat #'identity coq-compile-coqdep-warnings ","))
+    ()))
 
 (defun coq-par-coqdep-arguments (lib-src-file clpath)
   "Compute the command line arguments for invoking coqdep on LIB-SRC-FILE.
 Argument CLPATH must be `coq-load-path' from the buffer
 that triggered the compilation, in order to provide correct
 load-path options to coqdep."
-  (nconc (coq-coqdep-prog-args clpath
+  (nconc (coq-par-coqdep-warning-arguments)
+         (coq-coqdep-prog-args clpath
                                (file-name-directory lib-src-file)
                                (coq--pre-v85))
          (list lib-src-file)))
@@ -768,7 +778,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)