Columbus240
Columbus240
Well, it's your repo, and the ebuild works for me. I copied the ebuild to my local overlay and it works just fine. Even though I know that webkit-gtk is...
I just noticed that this issue is related to #392.
> Of course this works with Emacs: > > ``` > -arg -set -arg "\"Default Goal Selector=!\"" > ``` > > … but not with _CoqProject... Jup, have noticed that...
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...
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...
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...
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...
@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...
Maybe also consider adding tests for #103 and #102 (or checking whether the current tests are already appropriate). Another example similar to #103 : `Goal True. Abort.`
I'll describe my use-case on Zulip. I don't think it fits here.