Yannick Forster (Jun 07 2022 at 13:34): Yannick Forster (Jun 07 2022 at 13:34):According to the Coq refman one can use -set syntax in _CoqProject. But the given example -arg "-set 'Default Goal Selector=!'" leads to an error message in (my) Proof General:
Don't know what to do with Goal Selector=!'
See -help for the list of supported options
What works for me is -arg "-set \"Default Goal Selector=!\"", but then make breaks. Does anybody have experience with using quoted arguments in a _CoqProject files working both in Proof General and with the coqc commands of the generated Makefile?
Pierre Roux (Jun 07 2022 at 13:46):Would -arg -set -arg "Default Goal Selector=!" work?
Paolo Giarrusso (Jun 07 2022 at 13:46):at least with -w I use -arg -w -arg -notation-overridden so I wondered about the same
Yannick Forster (Jun 07 2022 at 13:47):Don't know what to do with Goal Selector=!
See -help for the list of supported options
:(
Paolo Giarrusso (Jun 07 2022 at 13:48):okay, more quoting needed then on this one...
Paolo Giarrusso (Jun 07 2022 at 13:49):(without the nested quoting, it might work better?)
Yannick Forster (Jun 07 2022 at 13:50):Ha, I think -arg "-set" -arg "'Default Proof Using = Type'" works
Paolo Giarrusso (Jun 07 2022 at 13:57):hope that "-set" = -set?
Yannick Forster (Jun 08 2022 at 12:40):Yes, indeed
Erik Martin-Dorel (Jun 14 2022 at 23:52):Hi all!
Not sure if it impacts what you said (didn't check in detail), but FYI you might be interested in having a look at this recently-merged PR in proof-general . master:
Erik Martin-Dorel (Jun 14 2022 at 23:54):BTW @Yannick Forster, did you find a solution to your use case?
Yannick Forster (Jun 15 2022 at 15:20):Yes, using -arg "-set" -arg "'Default Proof Using = Type'" worked
Gaëtan Gilbert (Jun 15 2022 at 15:52):I think that's incompatible with coqide ;)
Last updated: Oct 13 2024 at 01:02 UTC