New hook for early prompt/output analyzis.

[Matafou]

proof-state-change-pre-hook happens earlier than
proof-state-change-hook, i.e. before proof-done-advancing. This should
be used to register information in the currently processed span before
proof-done-advancing classifies it.

Historically PG design was to gather these information during
proof-done-advancing (or in its hook called at the end) by just
looking at the command statement. But it is often useful to look at
the output (messages and/or prompt) to gather more accurate
information. Some of this information may be needed DURING
proof-done-advancing. Hence this early hook.

[Matafou]

Trying to be a good guy proceeding with PR instead of wild (and buggy commit). Waiting for tests and comments.

When trying to correct PR #467 I detected that there was a bit of dependency loop between proof-done-advancing and its end-hook. Some of the information gathered in the span by this hook (e.g. is this command opening a goal?) was actually needed by proof-done-advancing (e.g.should we increment proof-nesting-depth?).

Notably this does actually not help to correct PR #467 since the information (are we inside a proof?) is needed even earlier. This is the subject of another commit.

[erikmd]

Hi @Matafou, thanks, the idea looks good; two questions:

• which kind of "typical tests" would you have in mind? (BTW it might be possible to automate part of these tests in the CI if you'd like)

• shouldn't these lines be edited as well?

  • PG/generic/proof-script.el

    Line 1438 in 2ada467

    (run-hooks 'proof-state-change-hook))

  • PG/generic/proof-tree.el

    Line 817 in 632a3d7

    (run-hooks 'proof-state-change-hook))

  • PG/easycrypt/easycrypt-hooks.el

    Line 71 in 733cd24

    (add-hook 'proof-state-change-hook 'easycrypt-set-state-infos)

[Matafou]

Hi @Matafou, thanks, the idea looks good; two questions:

• which kind of "typical tests" would you have in mind? (BTW it might be possible to automate part of these tests in the CI if you'd like)

Difficult to test this currently without writing some lisp testing. Maybe once the proof-nesting generic code works (although it is more accurate now, currently the proof-nesting-depth variable is incorrect when backtracking).

• shouldn't these lines be edited as well?

  • PG/generic/proof-script.el

    Line 1438 in 2ada467

    (run-hooks 'proof-state-change-hook))

No. The proof-done-advancing-hook remains. It is only that some of its content were triggered to late, hence the need for another hook.

• PG/generic/proof-tree.el

  Line 817 in 632a3d7

  (run-hooks 'proof-state-change-hook))

Well spotted. I will add it there as the information about state number is typically done by the pre-hook now. It would probably break proof-tree otherwise.

• PG/easycrypt/easycrypt-hooks.el

  Line 71 in 733cd24

  (add-hook 'proof-state-change-hook 'easycrypt-set-state-infos)

This will have no effect but it is more consistent to change this to pre-hook too.

Thanks!

[Matafou]

I just had a look at the test infrastructure. Can we easily add adhoc lisp code to a test?

[erikmd]

I just had a look at the test infrastructure. Can we easily add adhoc lisp code to a test?

Yes, it suffices to add an ERT form in coq-tests.el such as :

(ert-deftest 090_coq-test-pr-495 ()
  "Test for PR #495 about …" 
  (coq-fixture-on-file (coq-test-full-path "test_pr495.v") 
  (lambda ()
  ;elisp code, e.g.:
  (proof-process-buffer)
  (proof-shell-wait)
  ;optional assertion: (should…)
  ;otherwise: t)

assuming you need an accompanying file test_pr495.v

Then you can run the tests in two alternative ways:

1. ./ci/test.sh or:
2. C-x C-f coq-tests.el RET
   M-: (progn (load-file "coq-tests.el") (call-interactively #'ert)) RET

[Matafou]

Cool. I will try to adopt this systematically.

[erikmd]

If you don't need an ad-hoc file, you can just replace (coq-test-full-path "test_pr495.v") with nil and the coq-fixture-on-file function will take care of starting a fresh Coq instance on a temporary Coq file

[erikmd]

Then you can run the tests in two alternative ways:

1. `./ci/test.sh` or:

2. C-x C-f coq-tests.el RET
   M-: (progn (load-file "coq-tests.el") (call-interactively #'ert)) RET

or more simply, just evaluating Line 8 in a buffer:

PG/ci/coq-tests.el

Lines 6 to 8 in d20ad3d

	;;; Eval this to run the tests interactively <C-x C-e>
	;;
	;; (progn (load-file "coq-tests.el") (call-interactively #'ert))

[erikmd]

Finally in the case of a failure in ERT interactive mode, you can click on a failing test and press b to get a backtrace, see also:
https://www.gnu.org/software/emacs/manual/html_node/ert/Running-Tests-Interactively.html#Running-Tests-Interactively

[Matafou]

I merge this and will add tests later.