PG
PG copied to clipboard
ProofGeneral
PG is unusable when `-w` is passed to Coq via _CoqProject
If my _CoqProject file contains
-arg "-w '-deprecated-appcontext -notation-overridden'"
then PG is unable to start coqtop. It seems that it tries to pass "-w" "'-deprecated-appcontext" "-notation-overridden'" to coqtop, which is wrong.
Right. This is broken. It's due to the way we process -arg, and I don't know of a straightforward way to solve this issue, unfortunately :/
The issue basically is that we don't have a command line parser in Emacs Lisp. I don't think that the semantics of _CoqProject are documented anywhere (though I'd be happy to be wrong about this). For example, I'm not sure exactly what king of quoting it allows. Whichever quoting the local shell supports?
I'm still unclear as to exactly what status CoqProject has in Coq land, in fact. Are there plans on the Coq side to allow passing a _CoqProject to coqtop and coqc, for example?
In the meantime, I just pushed what I thought would be an easy workaround: using -arg "-w \"-deprecated-appcontext -notation-overridden\"" now works in PG.
But of course it wasn't going to be that easy: though coq_makefile -arg "-w \"-deprecated-appcontext -notation-overridden\"" works fine, but coq_makefile -f _CoqProject with a _CoqProject containing the same text doesn't.
Can you raise a a bug report with the Coq people, possibly pointing them here? The docs of coq_makefile claim:
[-f file]: take the contents of file as arguments
I am not sure whether or not this is a bug in coq_makefile. I believe the current lexer is that a token is anything that matches [^ "]+ or "[^"]+" (which is then stripped of "), and tokens are passed along directly to coq_makefile as if they were arguments, with no interpretation by the shell. Note how things like $(echo 1) get stuck unevaluated into OTHERFLAGS. OTHERFLAGS gets put into COQFLAGS, which is passed to the invocation of COQC. So it's eventaully subject to whatever quoting rules there are for the execution of commands in make; StackOverflow claims that make just feeds them to the shell, so this is subject to the quoting rules of the local shell.
Do you have a suggested alternate algorithm for lexing (or parsing) _CoqProject in coq_makefile?
I'm still unclear as to exactly what status CoqProject has in Coq land, in fact.
My understanding is that it is The Official Recommendation for distributing Coq projects and setting up Coq makefiles.
I am not sure whether or not this is a bug in coq_makefile. I believe the current lexer is that a token is anything that matches [^ "]+ or "[^"]+" (which is then stripped of "), and tokens are passed along directly to coq_makefile as if they were arguments
coq_makefile claims that it can take "extra arguments" in a file, but actually moving arguments from the command line to a file breaks it; isn't that a bug?
My understanding is that it is The Official Recommendation for distributing Coq projects and setting up Coq makefiles.
Then it needs to be fixed ;) It's just absurd to have a project system that depends on multiple levels of unsafe shell argument interpolations
Hm? There's exactly one level of unsafe shell argument interpolation: the one that's happens because we're using make.
coq_makefileclaims that it can take "extra arguments" in a file, but actually moving arguments from the command line to a file breaks it; isn't that a bug?
That depends. If you have -arg "$(rm -rf /)" in your _CoqProject, should you be sad at the time you run coq_makefile, or sad at the time you run make? Alternatively, if you have coq_makefile $(echo '-arg "-w '"'"'-deprecated-appcontext -notation-overridden'"'"'"'), that works perfectly fine. Do you want coq_makefile -f _CoqProject to call out to the system shell to evaluate things if you stick $(echo '-arg "-w '"'"'-deprecated-appcontext -notation-overridden'"'"'"') in your _CoqProject?
That depends. If you have -arg "$(rm -rf /)" in your _CoqProject, should you be sad at the time you run coq_makefile, or sad at the time you run make?
I should never be sad. A configuration file shouldn't mix code and data like this.
Do you want coq_makefile -f _CoqProject to call out to the system shell to evaluate things if you stick $(echo '-arg "-w '"'"'-deprecated-appcontext -notation-overridden'"'"'"')
No. But Coq makefile will diligently put things in the Makefile, to be executed by make later, and so things will be broken for our users, which is all that matters to me :)
Let's try to find a concrete way to fix this. The -w warnings stuff is new in 8.6, right? Can we change it slightly so you can write
-w -deprecated-appcontext -w -notation-overridden
Or is this even possible now? This would get rid of the problem, right? And then we can start thinking of a nicer way to describe Coq projects for 8.7.
No. But Coq makefile will diligently put things in the Makefile, to be executed by make later, and so things will be broken for our users, which is all that matters to me :)
I don't understand. If you pass $(echo '-arg "-w '"'"'-deprecated-appcontext -notation-overridden'"'"'"') on the command line to coq_makefile, it will generate a working Makefile. There is no way it can fail to do this, because you're calling it from the shell. But if you stick it in _CoqProject, it will generate a failing Makefile, because coq_makefile doesn't invoke the shell. This seems like a natural extension of your desire for coq_makefile -f _CoqProject to use shell string unescaping to parse its contents?
The -w warnings stuff is new in 8.6, right?
Yes.
Can we change it slightly...
Reported as bug #5109.
Or is this even possible now?
No. This was the first thing I tried. Subsequent -w flags override earlier ones. I have no idea why.
This would get rid of the problem, right?
Yes.
But if you stick it in _CoqProject, it will generate a failing Makefile, because coq_makefile doesn't invoke the shell.
That's right, I misread your example.
This seems like a natural extension of your desire for coq_makefile -f _CoqProject to use shell string unescaping to parse its contents?
I don't want coq_makefile to use anything related to a shell :) But fundamentally I don't care too much about what coq_makefile does, as long as there's a sane way for us to do the same thing in PG.
Can we change it slightly...
Reported as bug #5109.
Great, thanks much!
as there's a sane way for us to do the same thing in PG.
How hard is it to implement coq_makefile's lexer? You split off tokens as space-separated not-containing quotes, or everything between double quotes (no escape characters). You can probably ignore the existence initial double quotes not immediately preceded by whitespace/start of file, and trailing quotes not immediately followed by whitespace/EOF. Strip off a single set of leading/trailing quotation marks from each token surrounded by them. Apply shell escaping to each token, and pass them along to coqtop.
How hard is it to implement coq_makefile's lexer?
It's already done: I did it a few months ago.
Apply shell escaping to each token, and pass them along to coqtop.
You mean shell _un_escaping (splitting), right? This is the hard part.
IOW, the problem is that I need to split "-w '-deprecated-appcontext -notation-overridden'" into "-w", "-deprecated-appcontext -notation-overridden". This part is the splitting that the shell usually does (which in the coq_makefile case happens when the Makefile is invoked).
Oh, I see, yes. Shell unescaping. But aren't you doing that already with split-string-and-unquote? Or does that not handle single-quoted strings?
Actually, easy kludge: can you just replace ' with \" in the contents of _CoqProject before processing it? The only way this will break things, I think, is if the directory you're binding via -Q or -R or -I has a single quote in it (which I think we can just not support), or if you use -extra or -extra-phony with a fancy command (I think PG can just drop those arguments anyway), or with the VARIABLE = value bit, which we probably don't need to support single quotes in.
Or does that not handle single-quoted strings?
Exactly :) It only handles ELisp style string quoting and escaping. And the implementation is ghastly, so I'd rather avoid rolling my own equivalent for single quotes.
Actually, easy kludge: can you just replace ' with " in the contents of _CoqProject before processing it?
I've been thinking about this, but it's not very clean :/
(also: we don't currently support -extra*, nor assignments)
but it's not very clean
Presumably you only read _CoqProject from disk in one place. Is it unclean to stick the replacement there?
Presumably you only read _CoqProject from disk in one place. Is it unclean to stick the replacement there?
Definitely. For example, everything will break if someone tries to escape a single quote with \', won't it?
everything will break if someone tries to escape a single quote
Yes, hence my argument that this should not happen, unless you have a ' in your directory name, which I think I'm comfortable calling out as officially unsupported. (Is ' even a valid filename character on Windows at all?) But it seems reasonable to emit a warning or error message if the string \' appears anywhere in _CoqProject.
Hmm. It still feels very wrong. Let's hear from the Coq side that there's no way to fix this there, and then worry again.
I was just thinking: without allowing to have multiple -ws, could we just ask for a comma-separated list, instead of a space-separated one?
-arg "-w -deprecated-appcontext,-notation-overridden"
This would fix everything for free, and it seems like a very small change
I was just thinking: without allowing to have multiple
-ws, could we just ask for a comma-separated list, instead of a space-separated one?
Sure, we could do that. Want to update the bug report?
Hi there,
Maybe we can patch coq_makefile with an option to output the command line options it has computed?
That would make the whole thing more robust to changes in coq_makefile.
Compile before require already uses coqdep, so we can use coq_makefile.
Le jeudi 29 septembre 2016, Jason Gross [email protected] a écrit :
I was just thinking: without allowing to have multiple -ws, could we just ask for a comma-separated list, instead of a space-separated one?
Sure, we could do that. Want to update the bug report?
— You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub https://github.com/ProofGeneral/PG/issues/113#issuecomment-250373019, or mute the thread https://github.com/notifications/unsubscribe-auth/AEsl6oqh7Kx7pKukvNfjnBP7rMa34Bj8ks5qu0r-gaJpZM4KJZCh .
Maybe we can patch coq_makefile with an option to output the command line options it has computed?
I don't think so: coq_makefile doesn't what options to pass to coqtop either. It just dumps a string to a Makefile, and the shell interprets it.
Out of curiosity, have there been any updates on this issue since it was last discussed?
