omit-proofs: handle commands that may have global effects

[hendriktews]

Add the predicate `proof-script-cmd-prevents-proof-omission' to the omit-proofs framework, whose purpose is to check whether commands inside proofs might have global effects such that the proof must not be omitted.

Fixes #688

[erikmd]

as suggested in issue #689 (comment)

I guess the lowercase test is unneeded; why not using something like this?

Suggested change

	(if (proof-string-match coq-lowercase-command-regexp cmd)
	nil
	(not (coq-state-preserving-p cmd))))
	(or (proof-string-match coq-keywords-state-changing-commands cmd)
	; (not (proof-string-match coq-keywords-local-state-changing-commands cmd)) ; TODO
	))

For the TODO line, I'd rely on @hendriktews's suggestion to add another STATECH value and extend this:

PG/coq/coq-syntax.el

Lines 1158 to 1168 in 8416875

	(defvar coq-keywords-state-changing-commands
	(append
	coq-keywords-state-changing-misc-commands
	coq-keywords-decl ; all state changing
	coq-keywords-defn ; idem
	coq-keywords-goal)) ; idem
	;;
	(defvar coq-keywords-state-preserving-commands
	(coq-build-regexp-list-from-db coq-commands-db 'filter-state-preserving))

[erikmd]

Sorry I believe some improvement of you for the omit-proof feature (maybe this PR, I didn't re-checked) was stalled because of belated review from Pierre and I; sorry for that.

So @hendriktews, do you think you'd need further test or discussion from us for this PR?

Anyway I'd like to propose we pause our recurring PG maint telco this month (too many deadlines for me about grading or so in the upcoming two weeks), and resume in Feb…

Kind regards

[hendriktews]

There has been no progress on the preferred solutions that we discussed last year. Therefore I propose merging this PR as is (assuming all tests pass). Erik, note that your suggestion does not work as proposed, because coq-keywords-state-changing-commands is a list. As long as the proposed coq-keywords-local-state-changing-commands does not exist, it has the same problem with Focus, namely not omitting proofs that contain Focus.

[hendriktews]

Hi @erikmd , no problem! I am pretty confident about this PR and about #696 in the sense that they are not perfect, but good enough. So I don't need anything. I just want to give you the chance to comment, but if you are busy, I'll merge in a week or so. I commit to improve this fix when someone is motivated to add the coq-keywords-local-state-changing-commands that we discussed.