REGRESSION: ProofGeneral cannot step over Fail correctly

[hendriktews]

This problem was originally reported as #597 and fixed in 2021.
Now with Coq 8.20+rc1, the message for Fail is

The command has indeed failed with message:
Tactic failure: Cannot solve this goal.
In nested Ltac calls to "now (tactic)" and "easy", last call failed.

And PG does not step over FAIL.
To reproduce, see ci/test_stepwise.v, assert to the end of the line containing FailTrace, and assert the next line.
(Before 8.20 the message printed by coq seemed to be

The command has indeed failed with message:
In nested Ltac calls to "now (tactic)" and "easy", last call failed.
Tactic failure: Cannot solve this goal.

)

[hendriktews]

Hi Pierre, you fixed #597 last time. Can you have a look? Maybe only Tactic failure: Cannot solve this goal needs to be added to coq--error-header-re-list. If you have not yet installed 8.20rc, I can test a patch.

[hendriktews]

Adding Tactic failure: to coq--error-header-re-list does not solve the problem. Reason: coq--error-header-re-list needs to contain In nested Ltac call for older Coq versions, therefore, there is always a mach for In nested Ltac call without message:\n in front of it. Even worse, when coq--error-header-re-list contains Tactic failure, then there is also a match without message:\n in front of it for older coq versions. If there is a match, proof-shell-handle-immediate-output believes coq reported an error.
To fix it, we would need an entry in coq--error-header-re-list that matches both

Tactic failure: Cannot solve this goal.
In nested Ltac calls to "now (tactic)" and "easy", last call failed.

and

Tactic failure: Cannot solve this goal.
In nested Ltac calls to "now (tactic)" and "easy", last call failed.

from the beginning.
Instead of adding more regex magic, I would suggest to add another generic variable, eg, proof-shell-no-error-regexp and modify proof-shell-handle-immediate-output to do

(and (proof-re-search-forward-safe proof-shell-error-regexp end t)
         (not (proof-re-search-forward-safe proof-shell-no-error-regexp end t)))

instead of only searching for proof-shell-error-regexp.

[SkySkimmer]

Why is Tactic failure special? ie

Set Ltac Backtrace.
Goal False.
  Fail exact 0. (* fine *)
  Fail now auto. (* bad *)

[Matafou]

The fix proposition by @hendriktews looks good to me.

[Matafou]

@SkySkimmer because a previous ugly workaround.
@hendriktews do you propose a PR or should I?

[Matafou]

I just pushed a PR.

[Matafou]

@hendriktews did you initially detect the problem with the CI?

[hendriktews]

@hendriktews did you initially detect the problem with the CI?

yes, see the errors in #778

[Matafou]

Very nice to have this detected so early.

[hendriktews]

yes, the honor is yours, for adding the test in 2021!