Feature request: sparate commands for jumping to current point with/without omitting proofs

[RalfJung]

Feature request: sparate commands for jumping to current point with/without omitting proofs

[erikmd]

@RalfJung Cc @ProofGeneral/core
just FYI, the implementation addressing this feature request is now available in MELPA,
and I tweeted an announcement: https://twitter.com/ErikMartinDorel/status/1620037817660473344

[erikmd]

if there was a command that behave almost like C-c C-Enter, but with skipping proofs, then I would leave the "omit proofs" flag off usually (so that C-c C-Enter, C-c C-b, and so on all do not omit proofs).

Thanks a lot @RalfJung for your testing and feedback!

Good news: in proof-general 4.5, there's already (almost!) the feature you are interested in:

• You can enable the "omit proof" feature by default,
  manually by the menu or doing M-: (proof-omit-proofs-option-toggle 1) RET
• and then, add a prefix argument at the time you want to disable the feature and run all opaque proofs,
  i.e. just run C-u C-c C-RET or C-u C-c C-b

However, I realize that having the prefix argument the other way around (disabling "omit proofs" by default), or conversely, namely, like a real "Boolean toggle", could be nice.

→ I just opened PR #683, hopefully this can be integrated in master soon if this looks good as well to @hendriktews (the author of the omit proofs feature)

[RalfJung]

I didn't know about C-u, that already works very nicely. :) I haven't thought deeply about which one I want to be the default (C-c C-RET), so for now I will see how "omit by default, C-u for full checking" works for me. Thanks!

[hendriktews]

I didn't know about C-u, that already works very nicely. :) I

This was documented from the very beginning, see https://proofgeneral.github.io/doc/master/userman/Coq-Proof-General/#Omitting-proofs-for-speed Ralf, if you, as one of our power users, have a suggestion on how we could communicate these kind of things to Proof General users in a better way, we would love to hear about it! Seriously. For some time already, I have the suspicion that the Proof General user manual is a write-only medium.

[RalfJung]

Yeah that's a good question. I don't re-read the manual after each git pull, obviously... I didn't even know "omit proofs" existed until Tej pointed it out to me. The PG 4.5 release notes mention it but that was way after I started using the feature.

To be fair though, looking at the PG 4.5 release notes, it mentions "omit proofs" but doesn't indicate the existence of C-u. If I don't even suspect a feature might exist, then obviously I will not go search the manual for it. I could recommend linking to that section of the documentation from the release notes, but in this particular case I am not sure if it would have helped.

[RalfJung]

In terms of the documentation itself:

With a prefix argument, both proof-goto-point and proof-process-buffer will temporarily disable the omit proofs feature and send the full proof script to Coq.

Maybe it is my lack of emacs knowledge, but this tells me nothing. I have no clue what a "prefix argument" is. Quick googling helps, but it would also be good to just say that this means one has to do C-u C-c C-RET etc.

[erikmd]

FYI @RalfJung, here is the documentation of the standard emacs keybinding C-u (displayed by C-h k C-u):

universal-argument is an interactive and byte-compiled function
defined in simple.el.gz.

Signature
(universal-argument)

Documentation
Begin a numeric argument for the following command.

Digits or minus sign following C-u make up the numeric argument.
C-u following the digits or minus sign ends the argument.
C-u without digits or minus sign provides 4 as argument.
Repeating C-u without digits or minus sign
 multiplies the argument by 4 each time.
For some commands, just C-u by itself serves as a flag
that is different in effect from any particular numeric argument.
These commands include C-SPC and M-x start-kbd-macro.

Key Bindings
global-map C-u

To sum up, it is useful to:

• repeat some characters (try C-u 64 * or what it amounts to the same, C-u C-u C-u *, as 64=4×4×4)
• pass some arguments to functions, see also https://www.gnu.org/software/emacs/manual/html_node/elisp/Prefix-Command-Arguments.html for details.