Stream: Proof General users

Topic: Quoting arguments in `_CoqProject`


view this post on Zulip 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?

view this post on Zulip Pierre Roux (Jun 07 2022 at 13:46):

Would -arg -set -arg "Default Goal Selector=!" work?

view this post on Zulip 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

view this post on Zulip 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

:(

view this post on Zulip Paolo Giarrusso (Jun 07 2022 at 13:48):

okay, more quoting needed then on this one...

view this post on Zulip Paolo Giarrusso (Jun 07 2022 at 13:49):

(without the nested quoting, it might work better?)

view this post on Zulip Yannick Forster (Jun 07 2022 at 13:50):

Ha, I think -arg "-set" -arg "'Default Proof Using = Type'" works

view this post on Zulip Paolo Giarrusso (Jun 07 2022 at 13:57):

hope that "-set" = -set?

view this post on Zulip Yannick Forster (Jun 08 2022 at 12:40):

Yes, indeed

view this post on Zulip 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:

view this post on Zulip Erik Martin-Dorel (Jun 14 2022 at 23:54):

BTW @Yannick Forster, did you find a solution to your use case?

view this post on Zulip Yannick Forster (Jun 15 2022 at 15:20):

Yes, using -arg "-set" -arg "'Default Proof Using = Type'" worked

view this post on Zulip Gaëtan Gilbert (Jun 15 2022 at 15:52):

I think that's incompatible with coqide ;)


Last updated: Mar 29 2024 at 11:01 UTC