Skip to content

Commit

Permalink
coq-par-compile: add user options for extra coqc/coqdep arguments
Browse files Browse the repository at this point in the history
User options coq-compile-extra-coqc-arguments and
coq-compile-extra-coqdep-arguments are added as list of arguments to
invocation of, respetively, coqc and coqdep in addition to the
arguments computed, e.g., from _CoqProject.

This can be used to work around #724.
  • Loading branch information
hendriktews committed Feb 18, 2024
1 parent 4e6e5d9 commit 9b38f84
Show file tree
Hide file tree
Showing 2 changed files with 22 additions and 2 deletions.
16 changes: 16 additions & 0 deletions coq/coq-compile-common.el
Original file line number Diff line number Diff line change
Expand Up @@ -404,6 +404,22 @@ the ``-vok'' second stage was implemented."
:type 'number
:safe 'numberp)

(defcustom coq-compile-extra-coqdep-arguments nil
"Additional coqdep arguments for auto compilation as list of strings.
These arguments are added to all coqdep invocations during
automatic compilation in addition to the arguments computed
automatically, for instance by parsing a _CoqProject file."
:type '(repeat string)
:safe (lambda (v) (cl-every #'stringp v)))

(defcustom coq-compile-extra-coqc-arguments nil
"Additional coqc arguments for auto compilation as list of strings.
These arguments are added to all coqc invocations during
automatic compilation in addition to the arguments computed
automatically, for instance by parsing a _CoqProject file."
:type '(repeat string)
:safe (lambda (v) (cl-every #'stringp v)))

(defcustom coq-compile-command ""
"External compilation command. If empty ProofGeneral compiles itself.
If unset (the empty string) ProofGeneral computes the dependencies of
Expand Down
8 changes: 6 additions & 2 deletions coq/coq-par-compile.el
Original file line number Diff line number Diff line change
Expand Up @@ -761,7 +761,8 @@ earlier than 8.19."
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-par-coqdep-warning-arguments)
(nconc (copy-sequence coq-compile-extra-coqdep-arguments) ; copy for nconc
(coq-par-coqdep-warning-arguments)
(coq-coqdep-prog-args clpath
(file-name-directory lib-src-file)
(coq--pre-v85))
Expand All @@ -772,7 +773,10 @@ load-path options to coqdep."
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-coqc-prog-args clpath (file-name-directory lib-src-file) (coq--pre-v85))
(nconc (copy-sequence coq-compile-extra-coqc-arguments) ; copy for nconc
(coq-coqc-prog-args clpath
(file-name-directory lib-src-file)
(coq--pre-v85))
(list lib-src-file)))

(defun coq-par-analyse-coq-dep-exit (status output command)
Expand Down

0 comments on commit 9b38f84

Please sign in to comment.