Syntax of -arg in _CoqProject

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.

@herbelin

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.

-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.

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

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 :)

Fix parsing of -arg in _CoqProject file

@cpitclaudel

@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

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.

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.

@herbelin

@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).

@Matafou

@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.

@herbelin

-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.

I tend to agree.
Any news of a better project file format?

Were there remaining problems across PG, coq_makefile, CoqIDE, ... when writing things such as:

-arg -w
-arg -notation-overriden

and, either

-arg -set
-arg "Default Goal Selector=!"

or

-arg -set
-arg "'Default Goal Selector=!'"

Conversely, how realistic would it be to change the format (if in incompatible ways)?

@cpitclaudel

I don't think there are problems if each arg is on its own line. @cpitclaudel do you agree?

I just ran into this problem: this is a valid part of a _RocqProject file according to the makefile gnerator...

-arg "-set 'Default Goal Selector=!'"
-arg "-set 'Default Proof Using=Type'"
-arg "-set 'Suggest Proof Using'"

... however, PG chokes when I have that in the project file. I have to instead write this as follows:

-arg -set -arg "'Default Goal Selector=!'"
-arg -set -arg "'Default Proof Using=Type'"
-arg -set -arg "'Suggest Proof Using'"

Would be nice to fix PG to accept what is apparently standard syntax (a) as it's very confusing when make works but PG fails with inscrutable error messages and (b) the first form is more readable and hence easier to maintain.

@anton-trunov

The current situation is unfortunate: #113 led to some patches, then @anton-trunov improved -arg parsing in 9b3d7e5, then @Columbus240 further added a layer of unquoting in 774cb5f, but we haven't converged yet. And I still don't think that coq_makefile documents which shell syntax it expects. Happy to fix this thing if someone can point at the exact semantics that we want.

It doesn't document the full syntax but it does document that -arg "-set 'Default Proof Using=Type'" should work and should pass two arguments, -set and Default Proof Using=Type:
https://github.com/rocq-prover/rocq/blob/master/doc/sphinx/practical-tools/utilities.rst#quoting-arguments-to-rocq-c

So my interpretation of the syntax is that on the string within ", we do '-aware whitespace splitting: we split at each whitespace, except text within ' is taken verbatim and not split.

What is not clear to me is whether there are any escape sequences, i.e., what do I do if I wand to pass ' or " itself as argument? Lucky enough that's not something I ever had to do.

Nice find. This text is "new" from rocq-prover/rocq#14558 . I am not sure that the changes that were made there are consistent with the changes that were made here. I will take a look.

Adjust _RocqProject parsing to `rocq makefile` changes

@RalfJung

@RalfJung can you try #880?

Adjust _RocqProject parsing to `rocq makefile` changes

Navigation Menu

Repository navigation

Syntax of `-arg` in `_CoqProject` #392

Metadata

Assignees

Labels

Type

Projects

Milestone

Relationships

Development

	(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))

Syntax of -arg in _CoqProject #392

Description

Activity

cpitclaudel commented on Sep 27, 2018

anton-trunov commented on Sep 27, 2018

cpitclaudel commented on Sep 27, 2018

anton-trunov commented on Sep 27, 2018

anton-trunov commented on Sep 27, 2018

herbelin commented on Oct 11, 2018

cpitclaudel commented on Oct 11, 2018

Matafou commented on Dec 20, 2018

herbelin commented on Dec 21, 2018

RalfJung commented on Oct 3, 2024

Matafou commented on Oct 3, 2024

herbelin commented on Oct 3, 2024

Matafou commented on Oct 6, 2024

RalfJung commented on Jul 29, 2026

cpitclaudel commented on Jul 30, 2026

RalfJung commented on Jul 30, 2026

cpitclaudel commented on Jul 30, 2026

cpitclaudel commented on Jul 31, 2026

Metadata

Metadata

Assignees

Labels

Type

Projects

Milestone

Relationships

Development

Issue actions

Syntax of `-arg` in `_CoqProject` #392