search

ProofGeneral / PG

This repo is the new home of Proof General
https://proofgeneral.github.io
GNU General Public License v3.0
491 stars 88 forks source link

PG gets confused by comment in _CoqProject file that involves "-arg" #794

Open RalfJung opened 1 month ago

RalfJung commented 1 month ago

I have this in my _CoqProject file:

#-arg -w -arg -notation-incompatible-prefix

I have this because I want to temporarily disable this flag to see where exactly the warning gets triggered.

However, this seems to confuse PG. I now get errors when starting Coq:

Don't know what to do with -notation-incompatible-prefix
See -help for the list of supported options

It seems like PG is passing -notation-incompatible-prefix, i.e. the 2nd of the two arguments in the above comment, to Coq. However this doesn't make a lot of sense since the entire line is commented out! I would expect none of the two arguments to be passed.

When this _CoqProject is passed to coq_makefile, things work as expected.

hendriktews commented 1 month ago

Thanks for the report. IMO we should fix this, because the Coq refman says that _CoqProject may contain "Comments, started with an unquoted # and continuing to the end of the line." and also that "# outside of double quotes starts a comment that continues to the end of the line. Comments are ignored."