diff --git a/CHANGES b/CHANGES index 3c2e54ffb..0f2590b5d 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 b19f697fe..e8868c901 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 4f3155d53..aead112c7 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)))