Proof <term>. broken

[ghost]

Hi,

Here's how to reproduce this issue:

Goal True.
Proof I. (* <- set the cursor between the full stop and this comment and press C-C C-Enter *)
(* Error:  (in proof Unnamed_thm): Attempt to save an incomplete proof *)

I am using the curent master version of PG with Coq v8.11.1

[erikmd]

Hi @mwuttke97, thanks for the detailed report!

I tried this with Coq 8.11, 8.10, 8.9, and was able to reproduce this issue (but not systematically, namely depending on how I backtrack/progress in the script example); I looked at the *coq* buffer, and basically this bug seems to be reproducible with coqtop in the first place (due to the Unset Silent. command that is often inserted in the background by PG):

$ rlwrap coqtop
Goal True.
Unset Silent.
Proof I.
(* Error: Attempt to save an incomplete proof (in proof Unnamed_thm) *)

@Matafou do you think we should report this upstream? I mean, given #188 which implies IIUC that (ultimately) we won't need to trigger Unset Silent. anymore.

Anyway for the time being, a workaround would be to do something like this (although it is more verbose):

Goal True.
Proof.
exact I.
Qed.

[cpitclaudel]

I thought Proof I. was basically deprecated?

[erikmd]

@cpitclaudel in the 8.11 refman at least, it doesn't seem to be tagged as deprecated:

https://coq.github.io/doc/v8.11/refman/proof-engine/proof-handling.html?highlight=proof#coq:cmd.proof-term

[cpitclaudel]

Ok, my bad then :) I thought it had been replaced by the new Lemma xyz := … syntax.

[erikmd]

the new Lemma xyz := … syntax.

IINM you are thinking about this CEP: coq/ceps#42

But I agree that when the Lemma xyz := term. syntax will be available to directly provide an (opaque) proof term, one could propose to deprecate the Proof term. syntax…

[Matafou]

I think this is a bug that should be reported to coq.

[erikmd]

Hi, as pointed out by @Zimmi48 in coq/coq#12444 (comment), this issue had been reported several times already: this is a know bug for that Proof term. command that will eventually be deprecated in favor of the CEP 42 indeed.

So I'm going to close that PG issue as wont-fix. The proper fix being to do exact term. in proof mode for the time being.