ProofGeneral does not handle "Proof term." directives

[RalfJung]

Consider the following proof script:

Definition sth (n : nat) := True.
Lemma sth_all n : sth n. Proof. exact I. Qed.
Lemma sth_0 : sth 0. Proof sth_all 0.
Lemma sth_1 : sth 1. Proof sth_all 1.

ProofGeneral seems to be confused by these (very rarely used) Proof term. statements: when I step after that Proof sth_all 0. (directly giving the proof term instead of using tactics), it still shows an open goal. When I step to the end of the file it complains about nested proofs, but there are no nested proofs here. It then also shows an error, "Attempt to save an incomplete proof".

The same script works fine when being fed directly to coqc.

[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