PG Every command to Coq also sends "Show." and gets error "This command requires an open proof."

I'm using Coq 8.10.2. I'm going through the beginning of Software Foundations and every time I submit any command to Coq, like Compute (negb true)., ProofGeneral also submits Show. afterwards. Then I get the error:

Toplevel input, characters 0-5:
> Show.
> ^^^^^^
Error: This command requires an open proof.

This also takes over the *response* window, so I had to turn off proof-tidy-response to be able to see anything, but it is also very crowded now and the buffer seems to refresh back to the first error a lot.

GH seems to think this is related to #212, but I don't see how that is relevant to the user experience. How can I solve this problem?

Feb 13 '20 19:02 jeapostrophe

I can't reproduce this behaviour. Can you give a coq file that make you have it please?

Mar 02 '20 13:03 Matafou

Can you also give the version of PG you have?

Mar 02 '20 13:03 Matafou

@jeapostrophe do you still have this issue? I can't reproduce it.

Mar 12 '20 17:03 Matafou

Yes. Any Coq file will do. It happens with the first samples on this page --- https://softwarefoundations.cis.upenn.edu/lf-current/Basics.html#lab19

The versions of Emacs and Coq and PG are just the defaults on Homebrew right now.

Mar 12 '20 17:03 jeapostrophe

Homebrew stable package? It dates back to 2016. If this is the case you should hopfor the HEAD homebrew package or the MELPA package.

Mar 13 '20 09:03 Matafou