[nongnu] elpa/proof-general 19ca6e04d3 3/3: coq-par-compile: support coqdep warnings from 8.19 onwards

[ELPA Syncer]

branch: elpa/proof-general
commit 19ca6e04d3182f84c637b44b99be2be9838394db
Author: Hendrik Tews <hendrik@askra.de>
Commit: hendriktews <hendrik@askra.de>

    coq-par-compile: support coqdep warnings from 8.19 onwards
    
    Add user option coq-compile-coqdep-warnings to configure warnings for
    Coq 8.19 or later. The default value +module-not-found ensures Proof
    General reliably detects missing modules via a coqdep error. This
    changes kinds of supersedes the earlier commit
    36b1d28a8c4468fb1bdd38e6393750ab4f1cae6e that adapts the coqdep
    warning regexp.
---
 CHANGES                   |  5 +++++
 coq/coq-compile-common.el | 12 ++++++++++++
 coq/coq-par-compile.el    | 14 ++++++++++++--
 3 files changed, 29 insertions(+), 2 deletions(-)

diff --git a/CHANGES b/CHANGES
index 3c2e54ffb3..0f2590b5d8 100644
--- a/CHANGES
+++ b/CHANGES
@@ -9,6 +9,11 @@ the Git ChangeLog, the GitHub repo 
https://github.com/ProofGeneral/PG
 
 *** 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
 
 ** Generic changes
diff --git a/coq/coq-compile-common.el b/coq/coq-compile-common.el
index b19f697fe4..e8868c901e 100644
--- a/coq/coq-compile-common.el
+++ b/coq/coq-compile-common.el
@@ -522,6 +522,18 @@ 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[ \n].* is required "
           "and has not been found")
diff --git a/coq/coq-par-compile.el b/coq/coq-par-compile.el
index 4f3155d532..aead112c72 100644
--- a/coq/coq-par-compile.el
+++ b/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)))