Rocq proofs are not omitted when there are numbered selectors

[upamanyus]

Problem

The second lemma in the following does not get skipped when proof omission is enabled:

Lemma skipped : True.
Proof.
  auto.
Qed.

Lemma not_skipped : True.
Proof.
  1: auto.
Qed.

Specifically, the numbered selector 1: seems to be unsupported for proof omission. This Rocq feature is described in the "curl-braces" section here https://rocq-prover.org/doc/V9.0.0/refman/proofs/writing-proofs/proof-mode.html#curly-braces, though curly braces are not actually required.

Possible fixes

Handling 1:{ seems doable by modifying coq-braces-regexp (note that there could be whitespace in between).
The other possibility is the cmd being 1: tactic like in the example above. It seems safe to omit any command starting with natural:, since one can only run tactics under a numbered selectors, not general Coq commands (like Hint, Time, etc.). So it could be as easy as adding another regexp to accept [0-9]+[:space:]*: for omission in coq-cmd-prevents-proof-omission.

For now, I've managed to live with disabling coq-cmd-prevents-proof-omission by adding this to my local emacs config

(defun coq-cmd-prevents-proof-omission-never (_cmd) nil)
(advice-add 'coq-cmd-prevents-proof-omission :override #'coq-cmd-prevents-proof-omission-never )

[tchajed]

For reproducing, this is M-x proof-omit-proofs-option-toggle (which is, by the way, not the most discoverable name).

[hendriktews]

Thanks for the report. I never use goal selectors, I simply forgot about them.

[hendriktews]

Besides natural: there are other forms of selectors that need to be considered. In particular ! :, natural - natural :, and [ident] :.

[hendriktews]

For reproducing, this is M-x proof-omit-proofs-option-toggle (which is, by the way, not the most discoverable name).

The toggle is macro generated for the menu, not to be discovered. The documentation recommends to configure proof-omit-proofs-option or select Proof-General -> Quick Options -> Processing -> Omit Proofs.

[erikmd]

The toggle is macro generated for the menu, not to be discovered.

Note also @upamanyus that an easy way to omit proofs consist in prepending the C-c C-RET command with a prefix:

Try: C-u C-c C-RET

It looks to me it'd be worth it to also document this in

https://proofgeneral.github.io/doc/master/userman/Coq-Proof-General/#Omitting-proofs-for-speed

WDYT, @hendriktews ?

[hendriktews]

I see there "For both, proof-goto-point and proof-process-buffer, a prefix argument toggles the omit-proofs feature for one invocation." and a longer paragraph in the generic "Script processing commands" section.

[erikmd]

Ah indeed, good point @hendriktews. But maybe this is not clear enough for novice Emacs users? as in none of the two sections you mention, the exact string C-u C-c C-RET is written.