add feature to omit complete opaque proofs

[hendriktews]

This commit adds a feature to recognize complete opaque proofs in
the asserted region and to replace them with an admitted proof.
This can drastically improve the processing time for the asserted
region at the cost of not checking the omitted proofs. Omitted
proofs are displayed in some shade of purple in the locked
region.

With this commit, the feature is supported for Coq for files in
which proofs are started with some form of Proof using and
ended with either Qed, Defined or Admitted.

To enable, configure proof-omit-proofs-option or click
Proof General -> Quick Options -> Processing -> Omit Proofs.

[hendriktews]

For files with big proofs I measure a reduction of the processing time of the asserted region to 10%. For files with small proofs and many definitions it goes down to 30-40%.
Documentation in the manual, a test and a prefix argument to selectively process all proofs will follow in separate commits.

[erikmd]

Hi @hendriktews, thanks, that looks very nice! :)

And let us know when/if you'd like we test the feature ^^

[hendriktews]

This new test omit-proofs-omit-and-not-omit fails now and then because of #563.

[hendriktews]

And let us know when/if you'd like we test the feature ^^

It's ready for testing now. All you need to know is documented in proof-omit-proofs-option.

[hendriktews]

I consider this now complete. I have used the feature for a while for some 2000 lines file and it reduced waiting time there considerably. Does anybody want to try?

[erikmd]

I consider this now complete. I have used the feature for a while for some 2000 lines file and it reduced waiting time there considerably. Does anybody want to try?

Hi @hendriktews, thanks, I'd like to try − as soon as I can (not this week but before our next meeting on 14th April of course), anyway feel free to merge if other people here, Cc @ProofGeneral/core, were already able to take a closer look :)

Thanks a lot 👍

[Matafou]

I definitely want to try.

[hendriktews]

changed according to discussion in maintainer telco: Support proof starts without using and treat Abort as end of a non-opaque proof. @erikmd Do you want to check whether it works now in your file that contains Abort?

[erikmd]

Thanks @hendriktews 👍 yes I've just fetched your last commits and tested on that example file, so I can confim it works very fine!

[erikmd]

However there's a small issue I guess: the C-u prefix for skipping the "proof-omitting feature" does not work with Company-Coq.

[erikmd]

@hendriktews to be more precise: after installing the company-coq package from MELPA and enabling it, M-x company-coq-mode RET, I get: C-h k C-c C-RET ↓

C-c <C-return> runs the command company-coq-proof-goto-point (found in
company-coq--core-map), which is an interactive compiled Lisp function
in ‘company-coq.el’.

It is bound to C-c RET, C-c <C-return>, <menu-bar> <Proof-General>
<Goto Point>.

(company-coq-proof-goto-point &rest ARGS)

Pass ARGS to ‘proof-goto-point’, hiding company dialog.

Do you think it's feasible to overcome this limitation directly from PG? or maybe we can just open a PR in company-coq's repo.

[hendriktews]

company-coq binds a different command to C-c C-return, then it is not really a surprise, that it is not working, is it?

Do you think it's feasible to overcome this limitation directly from PG? or maybe we can just open a PR in company-coq's repo.

No, company-coq-proof-goto-point needs a different interactive declaration. Try to change that into (interactive "P"). With C-c C-b (proof-process-buffer) the prefix works also in company-coq?

[erikmd]

@hendriktews

company-coq binds a different command to C-c C-return, then it is not really a surprise, that it is not working, is it?

Exactly, I just wanted to mean this :) that the issue was related to the rebinding.

No, company-coq-proof-goto-point needs a different interactive declaration. Try to change that into (interactive "P").

Yes that seems to suffice. So I opened PR cpitclaudel/company-coq#247

With C-c C-b (proof-process-buffer) the prefix works also in company-coq?

Yes!

BTW, do you agree with the suggestion I had mentioned to extend the manual w.r.t. "Proof using" ?

Anyway when C-u C-c C-RET will also work with Company-Coq, it'll be awesome! this PR is definitely a nice feature :)

[cpitclaudel]

👍 👏 great job :)

[hendriktews]

BTW, do you agree with the suggestion I had mentioned to extend the manual w.r.t. "Proof using" ?

See my comment there (which I entered already the other day, but github decided to discard it, maybe because I clicked resolve before comment.

[cpitclaudel]

Can we merge this? The fix to company-coq isn't backwards-compatible.

[erikmd]

Hi @hendriktews! sorry for late reply.

Moreover, a Proof using recommendation has not much to do with this PR.

I'm not fully convinced that this PR has not much to do with Proof using 😅

Indeed, if there is no Proof using annotation, the feature replacing Qed with Admitted will often make the script fail!

Here is a toy example:

(* Proof-General > Quick Options > Omit Proofs *)
Section Foo.
  Variables (A : Type) (other : True).
  Lemma id : A -> A.
  Proof .
    auto.
  Qed.
End Foo.
Fail Definition bar := id nat 0. (* while it would be OK with `Proof using A.` above *)

Hence my earlier suggestion to add a small note in 11.5, advising to read 11.3 as well :)

But if you strongly disagree with this addition, maybe @Matafou (which implemented the Proof using helper feature IINM and also discussed this topic at the telco) could help to come to a decision?

[Matafou]

Proof using has definitely to do with this PR. If you use this in a section that is not decorated with proof using then after section ending coqtop will compute a wrong type for each lemma of the section. It should be made clear in the doc and in the CHANGE.

[erikmd]

Thanks @Matafou for your comment!
So I'm going to readily push a commit that documents that Proof-using requirement in the manual and file CHANGES.
Apart from this detail, the PR looks very fine, so @Matafou / @hendriktews / @cpitclaudel, feel free to merge when you see fit (otherwise I'll do it on tomorrow Wednesday in the evening).

Thanks again Hendrik, for this very nice feature!

[erikmd]

OK, so let's merge this now.

[hendriktews]

Thanks for polishing and merging. The argument about sections and proof using is certainly valid and it is good to have this in the manual (although I am not sure if anybody ever reads the manual).