ProofGeneral does not handle "Proof term." directives

[RalfJung]

ProofGeneral does not handle "Proof term." directives

[erikmd]

Thanks @RalfJung !

I know the Proof term. vernacular and use it sometimes, it's true that you found a workaround with the exact tactic but this is definitely something to fix!
Don't have the time to investigate, Cc-ing @ProofGeneral/core just in case… if another maintainer can take a look sooner.

Thanks again!

[Matafou]

Hi.
Proof term is more or less supported (even indentation-wise), but this is indeed yet another instance of the known bug #568 that the goals buffer sometimes do not updated (here it should become empty).

[RalfJung]

No I think this is not just a stale goal buffer issue. If I step all the way to the end of the file, I get an error: "Attempt to save an incomplete proof", even though the script completes when run via coqc. I also get warnings about nested proofs. So it does seem like PG is actually confused and got Coq into a wrong state. It seems as if only Proof. is sent to Coq, and the term is omitted.

[Matafou]

I can't reproduce. Can you check your pg version and also if the coqtop pg is using is the one you think? It seems to work with coq-8.15.

[RalfJung]

This is with PG 8416875, Coq 8.16.1.

To reproduce:

• open a file with the example script
• C-c C-b

Then it prints two warnings:

Warning (comp): pg-user.el:489:41: Warning: docstring wider than 80 characters Disable showing Disable logging
Warning (proof-script): found second proof start at line 4 - are there nested proofs? Disable showing Disable logging

(the first warning disappears when I repeat this; I had quite a few such warnings the last weeks but they all seem to show up only once)
and an error

Error:  (in proof sth_1): Attempt to save an incomplete proof

My custom settings are

 '(coq-compile-before-require t)
 '(coq-compile-parallel-in-background t)
 '(coq-compile-quick 'no-quick)
 '(coq-compile-vos 'vos)
 '(coq-one-command-per-line nil)
 '(proof-follow-mode 'followdown)
 '(proof-next-command-insert-space nil)
 '(proof-omit-proofs-configured t)
 '(proof-omit-proofs-option t)
 '(proof-splash-enable nil)
 '(proof-three-window-enable t)
 '(proof-three-window-mode-policy 'hybrid)

[Matafou]

OK. I can reproduce. This is rather strange. The following coqtop text session produces the error.

• Notice that from Lemma sth_0 I paste each command one after the other.
• Notice that I insert Set Silent/Unset Silent. at some points and that the error doe not occur if I don't.

Is this a coq bug? Why would Set Silent change the semantics?

Welcome to Coq 8.16.1

Coq < Definition sth (n : nat) := True.
sth is defined

Coq < Lemma sth_all n : sth n. Proof. exact I. Qed.
1 goal
  
  n : nat
  ============================
  sth n


No more goals.


Coq < Set Silent.

Coq < Lemma sth_0 : sth 0.

sth_0 < Proof sth_all 0.

Coq < Lemma sth_1 : sth 1. 

sth_1 < Unset Silent.

sth_1 < Proof sth_all 1.
Toplevel input, characters 0-16:
> Proof sth_all 1.
> ^^^^^^^^^^^^^^^^
Error:  (in proof sth_1): Attempt to save an incomplete proof

sth_1 < 

[Matafou]

Or is it that the Proof command must happen exactly after the Lemma?

[RalfJung]

Or is it that the Proof command must happen exactly after the Lemma?

Yeah that's what it looks like to me.

[Matafou]

Mmh that is a strange semantics. How is it even checked by Coq?
I don't see any easy fix to this. Even a Print command between the 2 commands breaks the script.

[Matafou]

Ho this is a known problem, even in Coq documentation. See #498. This coq feature is deprecated in coq's documentation.
I think we can close this bug report as duplicate of won't fix known bug.

[Matafou]

For reference to the deprecation of Proof term: https://coq.inria.fr/distrib/current/refman/proofs/writing-proofs/proof-mode.html?highlight=proof#coq:cmd.Proof-%60term%60