whitelist for admissible commands inside proofs

[hendriktews]

In the last PG maintainer meeting we discussed the following solution for #688 and #687: Treat the current proof as a non-opaque proof if it contains a command starting with a capital letter, except for a number of white-listed harmless commands.
Non-opaque proofs (such as those terminated by Defined) are not
omitted.
@Matafou , @erikmd : Can you suggest commands for such a whitelist?

[Matafou]

I will try to build a list when I have some time.
The things I see right now are

Print Check About Search...
Time
Show
Focus (edited)

I see a problem with Module names: you can call a tactic by its long name: like Foo.tac. So you should probably ignoring commands starting with capitals if followed by a dot...

[erikmd]

@hendriktews I didn't skim the Coq refman right now,
but I'd suggest to check the list of Coq commands recognized by PG's C-c C-v as state-preserving. Maybe there's a strong overlap here.

[Matafou]

There is an overlap, but this list is very conservative (it is for passing command to coq directly via the minibuffer (C-c C-v).

[erikmd]

Yes I know. What I meant is that: thanks to this command, PG already maintains a list of all Coq commands that are state-preserving. Certainly not exhaustive w.r.t. the whitelist mentioned in #689. But in order to comply as much as possible with the principle Dont-Repeat-Yourself, I would suggest to just double-check manually what are these state-preserving commands, and maybe just add programmatically in Lisp a few more commands that are not state-preserving but which should be included in the whitelist. Typically, Time.

FTR, this list is defined here:

PG/coq/coq-syntax.el

Lines 1245 to 1247 in 8416875

	(defvar coq-non-retractable-instruct
	(append coq-state-preserving-tactics
	coq-keywords-state-preserving-commands))

and doing C-h v coq-keywords-state-preserving-commands RET yields:

("\\_<Obligations\\_>" "\\_<About\\_>" "\\_<Check\\_>" "\\_<Compute\\_>"
"\\_<fail\\_>" "\\_<Inspect\\_>" "\\_<Locate\\s-+File\\_>"
"\\_<Locate\\s-+Library\\_>" "\\_<Locate\\s-+Notation\\_>" "\\_<Locate\\_>"
"\\_<Print\\s-+Coercions\\_>" "\\_<Print\\s-+Hint\\_>" "\\_<Print Ltac2\\_>"
"\\_<Print\\_>" "\\_<Pwd\\_>" "\\_<Search\\_>" "\\_<SearchPattern\\_>"
"\\_<SearchRewrite\\_>" "\\_<Show\\_>" "\\_<Test\\_>" "\\_<Timeout\\_>"
"\\_<Add\\s-+LoadPath\\_>" "\\_<Add\\s-+ML\\s-+Path\\_>"
"\\_<Add\\s-+Rec\\s-+LoadPath\\_>" "\\_<Add\\s-+Rec\\s-+ML\\s-+Path\\_>"
"\\_<Admit\\s-+Obligations\\_>" "\\_<Cd\\_>" "\\_<Comments\\_>"
"\\_<Declare\\_>" "\\_<Eval\\_>" "\\_<Extract\\s-+Constant\\_>"
"\\_<Extract\\s-+Inlined\\s-+Constant\\_>" "\\_<Extract\\_>"
"\\_<Extraction\\s-+Library\\_>" "\\_<Extraction\\_>" "\\_<Focus\\_>"
"\\_<From\\_>" "\\_<Ltac2 Eval\\_>" "\\_<Typeclasses\\s-+Opaque\\_>"
"\\_<Opaque\\_>" "\\_<Preterm\\_>" "\\_<Qed\\_>"
"\\_<Recursive\\s-+Extraction\\_>"
"\\_<Recursive\\s-+Extraction\\s-+Library\\_>"
"\\_<Recursive\\s-+Extraction\\s-+Module\\_>" "\\_<Remove\\s-+Hints\\_>"
"\\_<Remove\\s-+LoadPath\\_>" "\\_<Remove\\s-+LoadPath\\_>"
"\\_<Reserved\\s-+Infix\\_>" "\\_<Reserved\\s-+Notation\\_>"
"\\_<Transparent\\_>" "\\_<Unfocus\\_>")

[Matafou]

Seems ok. We need to remove a nombre of commands from this list I think. I see a few that are state changing (Opaque etc). Don't even know why they are here.

[erikmd]

Hi @Matafou

I see a few that are state changing (Opaque etc). Don't even know why they are here.

That's just a small bug!

• I opened PR coq-syntax.el: Fix state-changing booleans for commands #692 to fix it.

• As you can see, the fact the commands are state-preserving or not is directly encoded by a bool in coq-syntax.el lists.

• The documentation is as follows:

PG/coq/coq-db.el

Lines 36 to 47 in 8416875

	\(MENUNAME ABBREV INSERT STATECH KWREG INSERT-FUN HIDE)
	MENUNAME is the name of form (or form variant) as it should appear in menus or
	completion lists.
	ABBREV is the abbreviation for completion via \\[expand-abbrev].
	INSERT is the complete text of the form, which may contain holes denoted by
	\"#\" or \"@{xxx}\".
	If non-nil the optional STATECH specifies that the command is not state
	preserving for coq.

[erikmd]

and maybe just add programmatically in Lisp a few more commands that are not state-preserving but which should be included in the whitelist. Typically, Time.

For the record, after reviewing the list above, I see three other commands that should be in the whitelist:

• Time … (cancelled, cf. this comment)
• Focus … (non state-preserving, but with a side-effect local to the proof)
• Unfocus … (idem)

[hendriktews]

Thanks for the input. I guess, we do not want to permit Focus for C-c C-v but we do want to omit proofs that contain Focus (if they don't contain other state changing commands at least). Therefore we need a predicate similar to coq-state-preserving-p that accepts Focus and similar stuff. We could define a third value for STATECH, maybe 'local, and use this for Focus and friends, and derive the new predicate also from the syntax DB. What do you think?

[hendriktews]

* [ ]  `Time …`

You can do Time Hint..., so I guess Time should not be whitelisted.

[hendriktews]

The STATECH flag in the syntax db only distinguishes between state changing and not. Obviously, tactics (e.g. auto) are state changing. Therefore in #694 function coq-cmd-prevents-proof-omission must first check for upper case. What do you think about distinguishing via STATECH commands that have

• no effect (eg. Show)
• proof local effect only (all tactics and Focus)
• global effect (eg. Hint)

[erikmd]

I guess, we do not want to permit Focus for C-c C-v but we do want to omit proofs that contain Focus (if they don't contain other state changing commands at least). Therefore we need a predicate similar to coq-state-preserving-p that accepts Focus and similar stuff. We could define a third value for STATECH, maybe 'local, and use this for Focus and friends, and derive the new predicate also from the syntax DB. What do you think?

Fully agree, your idea looks very good to me.

[erikmd]

Therefore in #694 function coq-cmd-prevents-proof-omission must first check for upper case.

Was it really necessary? because AFAIK, commands and tactics are kept apart in separate lists.

[erikmd]

What do you think about distinguishing via STATECH commands that have

• no effect (eg. Show)
• proof local effect only (… e.g. Focus)
• global effect (eg. Hint)

LGTM!

[hendriktews]

Therefore in #694 function coq-cmd-prevents-proof-omission must first check for upper case.

I changed to a lowercase check, because because the previous version had problems with #[local] Show. (I know that Show does not support this attribute, but maybe there is or will be some other state-preserving command that supports some attribute.)

[hendriktews]

Was it really necessary? because AFAIK, commands and tactics are kept apart in separate lists.

I am open for suggestions, that is why #694 is a draft PR.

[Matafou]

That sounds like a good idea. That said the STATECH boolean has not been correctly maintained for a long time, and we don't rely much on it. This change would make quite important that this boolean is faithful, at least for the case where it goes against the lower/uppercase law.

[erikmd]

That said the STATECH boolean has not been correctly maintained for a long time, and we don't rely much on it.

Sure… but that does not look like a drawback to me!

Actually, I've proofread the list of all STATECH-related commands since #689 (comment) and the few commands that had an incorrect STATECH boolean are fixed here:

• PR coq-syntax.el: Fix state-changing booleans for commands #692

at least for the case where it goes against the lower/uppercase law.

Regarding this latter point, how about discussing this at our next PG telco? (on March 29 IINM)