PG

PG copied to clipboard

Coq PG doesn't recognize the new quotation mechanism of coq/coq#9733

8

For example, with the coq-elpi plugin, we can write the following Vernacular command. But PG doesn't recognize the proper end of the command when we do `C-c C-n`. https://github.com/LPCIC/coq-elpi/blob/6d21fa61fb59a555c5075ba3e3c89844a5d14bee/theories/tutorial/elpi_lang.v#L53-L58 ```...

pi8027

remove Isabelle walkthrough example

1

https://proofgeneral.github.io/doc/master/userman/Basic-Script-Management/#Walkthrough-example-in-Isabelle it seems Isabelle is in the doc. I don't suppose Isabelle is maintained anymore?

HuStmpHrrr

User-defined `coq-prog-args` gets reset to `("-emacs")` on every `proof-shell-start`

5

Hi, Problem description: As per title. Steps to reproduce: 1. Simply set `coq-prog-args` to some values. E.g. `(setq coq-prog-args '("-set" "Printing Parentheses"))`. 2. In a Coq file, run `M-x proof-shell-start`,...

zacque0

Please support parsing `-arg -set -arg "Loose\ Hint\ Behavior=Strict"` and/or `-arg -set -arg "'Loose Hint Behavior=Strict'"` from `_CoqProject`

1

Currently, neither of these works with PG; the first gets passed as `-set LooseHintBehavior=Strict`, while the second gets passed as `-set "'Loose" "Hint Behavior=Strict'"`, it seems (based on `Don't know...

JasonGross

get warning on emacs 28

2

Hi, After an upgrade from melpa I get this warning about proof general: ``` Warning (emacs): Proof General compiled for GNU Emacs 27.2 but running on GNU Emacs 28.1: "make...

YievCkim

Dune support

51

Hi folks, the Coq mode for Dune is getting more mature, and a big blocker now is integration with Proof General. I am unsure how to best approach this; basically...

ejgallego

add customizable variables to configure which part of a goal the goal buffer will focus on

6

By setting `coq-prefer-top-of-conclusion` to `t`, we get Proof General to focus on the conclusion of the first goal after displaying the list of goals of a proof. The conclusion is...

cipher1024

~~~coq Goal False. 1:{ fail. ~~~ will put the cursor before `1` and highlight ~~~ 1:{ f ~~~ `{` works fine but is not helpful when one wants some other...

SkySkimmer

Installing the MELPA package when package-quickstart is enabled causes emacs to abort loading with the following error message: `Cannot open load file: No such file or directory, /home//.emacs.d/generic/proof-site` This error...

yvie-k

enable Tramp support for Emacs 26 or later

1

tramp support is not complete with these patches, but works if used with care. There are a few assertions that quick user interactions can trigger. Automatic background compilation via tramp...

hendriktews