Skip to content

Commit

Permalink
coq-par-compile: support coqdep warnings from 8.19 onwards
Browse files Browse the repository at this point in the history
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
36b1d28 that adapts the coqdep
warning regexp.
  • Loading branch information
hendriktews committed Jan 7, 2024
1 parent 227e462 commit 19ca6e0
Show file tree
Hide file tree
Showing 3 changed files with 29 additions and 2 deletions.
5 changes: 5 additions & 0 deletions CHANGES
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
12 changes: 12 additions & 0 deletions coq/coq-compile-common.el
Original file line number Diff line number Diff line change
Expand Up @@ -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")
Expand Down
14 changes: 12 additions & 2 deletions coq/coq-par-compile.el
Original file line number Diff line number Diff line change
Expand Up @@ -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)))
Expand Down

0 comments on commit 19ca6e0

Please sign in to comment.