ProofGeneral
PG mangles strings in _CoqProject
In my _CoqProject I have the line
-arg -set -arg "'Default Goal Selector=!'"
because this way I managed to convince the other Coq tools (coq_makefile, coqc, etc) that they should Set Default Goal Selector "!".
But PG produces the following value in coq-prog-args: ("-emacs" "-set" "'Default" "Goal" "Selectors=!'") while I expected ("-emacs" "-set" "Default Goal Selector=!").
The issue probably is, that the processing done by coq_makefile is weird.
This coq_makefile stuff has been a plague for years. Hopefully at some point in the future we can get a simple coq project format that's declarative (instead of a bunch of shell commands); something like JSON or TOML or CFG or …
Of course this works with Emacs:
-arg -set -arg "\"Default Goal Selector=!\""
… but not with _CoqProject...
Thanks for the PR by the way. I'd be fine merging it as-is; I don't expect it would cause much trouble, and I don't want to spend much time on this exciting source of broken-ness.
Of course this works with Emacs:
-arg -set -arg "\"Default Goal Selector=!\""… but not with _CoqProject...
Jup, have noticed that as well. Erm, don’t merge the branch for now. I put some more thought into it and understand now, why exactly the interaction of coq_makefile, make and coqc is so messed up regarding quotations. I’ll submit a PR to coq in a few hours. If that PR doesn’t get accepted, I’d propose merging my quick fix.
Another solution that works with coq_makefile but not with ProofGeneral: -arg "-set 'Default Goal Selector=!'". I think this syntax would be acceptable in the current state of affairs (if it were sufficiently well documented).
To simulate the behaviour of the interaction of coq_makefile and make, ProofGeneral would need to do the following:
- Split the input stream into tokens (i.e. a list of strings) as done here: https://github.com/coq/coq/blob/7c91b3cdfa1a7edb27a184a37c481ca61c6a2eaa/lib/coqProject_file.ml#L91-L139.
- Treat all the other options as before.
- Create an empty buffer "ExtraArgs". For every "-arg" followed by a token x, append x to ExtraArgs (with spaces inbetween).
- Split ExtraArgs at space-boundaries, but keeping stuff enclosed in single-quotes together, removing the single-quotes. To be more precise: do all the splitting and expanding, that make would do.
- Put the result into
coq-prog-args.
Another way would be, to do away with -arg. But this means coq_makefile would need to know the arity of each argument. I.e. there’d have to be a central database in the Coq repo for this, meaning a lot of maintenance.
Or the possibilities I wrote about in the linked, retracted PR coq/coq#14557.
Another option that would make our lives much easier: coq_makefile could have a mode in which it prints out a JSON expression instead of a Makefile. Then PG would just invoke that and read the result.
Is JSON an appropriate format for this? I have little experience with it and only heard that it’s a lax language in some respects. But other than that, it is probably the easiest solution in the long term.
I noticed: if we let coq_makefile output how it interprets _CoqProject (as JSON or otherwise), this isn’t enough for ProofGeneral. We would still need to replicate the behaviour of make (if coq/coq#14557 or something similar isn’t implemented), which is the same problem ProofGeneral currently has.
@cpitclaudel, How about using https://github.com/janestreet/ecaml to use coqProject_file.ml from the coq project to parse _CoqProject? This way ProofGeneral would have a new dependency, but it would (probably) always parse _CoqProject correctly, according to the Coq version used.
That plugin requires dynamic module support in Emacs, which IIRC requires recompiling Emacs (distro-built versions don't enable modules by default). At least this was the case in Emacs 25, not sure if it's changed.