search

ProofGeneral / PG

This repo is the new home of Proof General
https://proofgeneral.github.io
GNU General Public License v3.0
491 stars 88 forks source link

REGRESSION: ProofGeneral cannot step over Fail correctly #779

Closed hendriktews closed 4 months ago

hendriktews commented 4 months ago

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 commented 4 months ago

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 commented 4 months ago

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 commented 4 months ago

Why is Tactic failure special? ie

Set Ltac Backtrace.
Goal False.
  Fail exact 0. (* fine *)
  Fail now auto. (* bad *)
Matafou commented 4 months ago

The fix proposition by @hendriktews looks good to me.

Matafou commented 4 months ago

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

Matafou commented 4 months ago

I just pushed a PR.

Matafou commented 4 months ago

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

hendriktews commented 4 months ago

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

yes, see the errors in #778

Matafou commented 4 months ago

Very nice to have this detected so early.

hendriktews commented 4 months ago

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