Syntax of `-arg` in `_CoqProject`

[herbelin]

Hi, I'm writing in relation with a CoqIDE issue coq/coq#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: https://github.com/ProofGeneral/PG/blob/733cd24a7368ee186884da488da0f59bbedb627e/coq/coq-system.el#L471-L537

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:

https://github.com/ProofGeneral/PG/blob/5b7b84bc5b44fd87905b16a67367ece4e7fa7ee3/coq/coq-system.el#L504-L510

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 coq/coq#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.

[Matafou]

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

[herbelin]

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

[Matafou]

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