Syntax of `-arg` in `_CoqProject`

[herbelin]

Hi, I'm writing in relation with a CoqIDE issue rocq-prover/rocq#5773.

The _CoqProject file supports a syntax -arg which is not documented in the Coq reference manual but which we fortunately found documented in ProofGeneral. We realized that there are however some ambiguities with this syntax, in particular regarding options which span over several "tokens" of the command line, as e.g. for -arg "-w -notation-overriden", vs -arg -w -notation-overriden, vs one line -arg -w and the next line -arg notation-overriden, etc.

That would be good to be able to document more precisely this syntax and that PG, CoqIDE and coq_makefile parse it consistently. For instance, is -arg intended to take a space-free argument, or, if non space-free, a double-quote surrounded argument? Are single-quote surrounded argument allowed? How to pass an argument which contains quotes, as, if, e.g., I would like to pass -arg '-Q "" Foo'? Etc. In the case of coq_makefile the parsing rules are here. What are the parsing rules for PG?

PS: "Remark" is written using the French spelling here.

[cpitclaudel]

Hi @herbelin!

The parsing code in PG is here:

PG/coq/coq-system.el

Lines 471 to 537 in 733cd24

	(defconst coq--project-file-separator "[\r\n[:space:]]+")
	(defconst coq--makefile-switch-arities
	'(("-R" . 2)
	("-Q" . 2)
	("-I" . 1)
	("-arg" . 1)
	("-opt" . 0)
	("-byte" . 0)))
	(defun coq--read-one-option-from-project-file (switch arity raw-args)
	"Cons SWITCH with ARITY arguments from RAW-ARGS.
	If ARITY is nil, return SWITCH."
	(if arity
	(let ((arguments
	(condition-case-unless-debug nil
	(cl-subseq raw-args 0 arity)
	(warn "Invalid _CoqProject: not enough arguments for %S" switch))))
	(cons switch arguments))
	switch))
	(defun coq--read-options-from-project-file (contents)
	"Read options from CONTENTS of _CoqProject.
	Returns a mixed list of option-value pairs and strings."
	(let ((raw-args (split-string-and-unquote contents coq--project-file-separator))
	(options nil))
	(while raw-args
	(let* ((switch (pop raw-args))
	(arity (cdr (assoc switch coq--makefile-switch-arities))))
	(push (coq--read-one-option-from-project-file switch arity raw-args) options)
	(setq raw-args (nthcdr (or arity 0) raw-args))))
	(nreverse options))) ; Order of options is important sometimes (Cf. #7980)
	(defun coq--extract-prog-args (options)
	"Extract coqtop arguments from _CoqProject options OPTIONS.
	OPTIONS is a list or conses (switch . argument) and strings.
	Note that the semantics of the -arg flags in coq project files
	are weird: -arg \"a b\" means pass a and b, separately, to
	coqtop."
	(let ((args nil))
	(dolist (opt options)
	(pcase opt
	((or "-byte" "-op")
	(push opt args))
	(`("-arg" ,concatenated-args)
	(setq args
	(append (split-string-and-unquote (cadr opt) coq--project-file-separator)
	args)))))
	(cons "-emacs" args)))
	(defun coq--extract-load-path-1 (option base-directory)
	"Convert one _CoqProject OPTION, relative to BASE-DIRECTORY."
	(pcase option
	(`("-I" ,path)
	(list 'ocamlimport (expand-file-name path base-directory)))
	(`("-R" ,path ,alias)
	(list 'rec (expand-file-name path base-directory) alias))
	(`("-Q" ,path ,alias)
	(list 'recnoimport (expand-file-name path base-directory) alias))))
	(defun coq--extract-load-path (options base-directory)
	"Extract loadpath from _CoqProject options OPTIONS.
	OPTIONS is a list or conses (switch . arguments) and strings.
	Paths are taken relative to BASE-DIRECTORY."
	(cl-loop for opt in options
	for extracted = (coq--extract-load-path-1 opt base-directory)
	when extracted collect extracted))

Note in particular the implementation coq--extract-prog-args, which further splits the arguments passed to -arg.

You can use the following to test how it behaves:

(coq--read-options-from-project-file "…contents of _CoqProject…")

And you can use the following to see what we pass to Coq:

(coq--extract-prog-args (coq--read-options-from-project-file "..."))

For example:

M-: (coq--extract-prog-args (coq--read-options-from-project-file "-arg \"-w -notation-overriden\"")) RET
⇒ ("-emacs" "-w" "-notation-overriden")

Concretely:

• -arg "-w -notation-overriden" is supported and yields
• -arg -w -notation-overriden is not supported
• -arg -w -arg notation-overriden is supported
• Single quotes are not recognized
• Escaped quotes are supported: -arg "-Q \"\" Foo" yields ("-emacs" "-Q" "" "Foo")

The core of the difficulty, I think, is this statement in the help of coq_makefile (I think it was removed since 8.4; this is what it said in 8.4): [-f file]: take the contents of file as arguments. The problem here is that normally it's the shell that splits input strings, passing the program a list or individual arguments; with -f, coq_makefile has to take responsibility for splitting the input string. Additionally, -arg requires further splitting, since coqc needs to receive each argument separately.

[anton-trunov]

-arg -w -arg notation-overriden is supported

I think it's not supported though, because I tried that and it didn't work with PG (but it works with CoqIDE).

M-: (coq--extract-prog-args (coq--read-options-from-project-file "-arg -w -arg notation-overriden")) RET
⇒ ("-emacs" "notation-overriden" "-w" )

I might be wrong, but it seems the order is reversed and the leading hyphen got cut off from -notation-overriden.

[cpitclaudel]

it seems the order is reversed

Ah, good point, that's a bug

and the leading hyphen got cut off from -notation-overriden

Hmm, but you didn't include it in the input to coq--read-options-from-project-file, so I think that's normal

[anton-trunov]

Hmm, but you didn't include it in the input to coq--read-options-from-project-file, so I think that's normal

oops, you are right :) I re-checked and the hyphen survives :)

[anton-trunov]

@cpitclaudel #393 fixes the problem, I think; I tested it on on a real Coq project

-arg "-w -notation-overriden"
-arg -w -arg notation-overriden
-arg -w -arg -notation-overriden -arg -w -arg -redundant-canonical-projection

[herbelin]

Hi, just an extra question about the use of double quotes. Maybe it is too late and users already use the syntax but I was wondering whether -arg "-w -notation-overriden" should not be interpreted like in CoqIDE, i.e. as if -w -notation-overriden was a single argument (and thus being invalid for coqtop). Additionally, the latter would be consistent with PG feeling which itself qualifies coq_makefile convention as weird. This would also be consistent with PG manual which says "-arg must be followed by one and only one option to pass to coqtop/coqc, use several -arg to issue several options".

I mean, in the case of -arg "-w -notation-overriden", it is obvious for a human that we mean two arguments. But if I want to give a name with spaces, like, say, /Program Files/coq/foo.v, shall it be clear that I need to write "\"/Program Files/coq\"" rather than simply "/Program Files/coq/foo.v", knowing that make and thus coq_makefile are anyway unable to deal with spaces in filename (but, maybe coq_makefile will move to dune and that may become different).

PS: In PG manual, I found another typo: "intial" instead of "initial".

I'm asking to eventually decide what to exactly document in the Coq reference manual.

[cpitclaudel]

No strong opinion :) When I wrote the new arg parsing code in PG I added this comment (ignore the \ escapes; they were needed for ELisp docstrings:

PG/coq/coq-system.el

Lines 504 to 510 in 5b7b84b

	(defun coq--extract-prog-args (options)
	"Extract coqtop arguments from _CoqProject options OPTIONS.
	OPTIONS is a list or conses (switch . argument) and strings.
	Note that the semantics of the -arg flags in coq project files
	are weird: -arg \"a b\" means pass a and b, separately, to
	coqtop."
	(let ((args nil))

I'm fine with deprecating this approach. I hope we can soon get a better configuration format.

[Matafou]

@herbelin @cpitclaudel is there some news about this? I don't have strong opinion either. But it is very important that coqide, pg and coq_makefile behave all the same (and any other ide).

[herbelin]

@Matafou: I finally made rocq-prover/rocq#8714 which documents what works with both PG, CoqIDE and coq_makeflle.

Note ongoing discussions about the format of _CoqProject. See item "Format of _CoqProject file" at https://github.com/coq/coq/wiki/Next-Coq-Working-Group (the page shall move though) where @charguer is advocating for supporting any Coq option without -arg in _CoqProject.

Note also ongoing discussions on possibly replacing coq_makefile with dune.

[RalfJung]

-arg "-w -notation-overriden"

I agree with @herbelin, this should pass a single argument -w -notation-overriden (which then gets rejected by Coq). If PG/coq_makefile do space splitting of -arg flags, they also need to provide a way to escape spaces, and then complexity quickly spirals upwards.