Proof term for vos

[mrhaandi]

Description of the problem

The documentation of Proof term states that it is equivalent to exact term. Qed.

However, if I compile Proof term as vos, I get a large file (possibly containing the term), whereas for exact term. Qed. a vos compilation produces a small interface file.

In both cases the About command states that the proof is opaque.

Example

v1.v containing

Lemma test : True.
Proof.
exact (
let H : True := I in 
... many more "let H : True := I in" ...
H).
Qed.

Running coqc v1.v -vos produces a small interface file.

v2.v containing

Lemma test : True.
Proof (
let H : True := I in 
... many more "let H : True := I in" ...
H).

Running coqc v2.v -vos produces a large interface file.

Coq Version

The Coq Proof Assistant, version 8.13.1 (March 2021)
compiled on Mar 12 2021 9:23:15 with OCaml 4.11.1

[Zimmi48]

Is this really a documentation issue? Maybe this is a way to say that this is going to be a won't fix except maybe to insist in the documentation on Proof term being broken at many levels and strongly discouraged.

[SkySkimmer]

I guess we could drop the opaque table in vos mode so it's not strictly documentation.

[mrhaandi]

My use case for Proof term was to encapsulate machine-generated proof terms in an opaque way.
Proof. exact term. Qed. works, but feels somewhat convoluted because it switches to the tactic level, although I already have the actual term.
In the transparent case there is Definition/Fixpoint.
Because I also want a slick vos file, the somewhat incorrect documentation of Proof term misled me.
Since there is a working (slightly inconvenient for code generation) alternative Proof. exact term. Qed., a "won't fix" with better documentation is OK.

[Zimmi48]

Note that longer-term, there's a planned alternative for Proof term (see coq/ceps#42). We didn't deprecate Proof term yet precisely because this better alternative isn't implemented yet.

[ejgallego]

IMHO we should indeed deprecate Proof term which is broken today and have Theorem foo := term. instead, which is just an alias for Definition foo := term but making foo opaque. I think that should not be controversial.

[ejgallego]

Implementing the above should be very easy with the current status of the API, provided parsing does work ok, which I think it shouldn't be a big deal either.

[Zimmi48]

This wasn't controversial indeed. And this is why I started implementing it. Only to discover that there was this weird semantics to Theorem ... with .... This is what led me to writing this CEP (which is also non-controversial, it was even quite successful) to get a proper design overall. Sorry that I didn't get to finish it but I still believe that it should be completed before being implemented (not necessarily by me, although I'm willing to at least put the effort in going through the CEP process to the end).