ProofGeneral cannot step over Fail correctly when Set Ltac Backtrace is enabled

[Blaisorblade]

On my (Spacemacs) installation, if Set Ltac Backtrace is enabled, Fail still works correctly in Coq (8.13.2), but ProofGeneral does not seem to understand that. The same example works in VsCoq.

Goal False.
Proof.
  Fail (now auto). (* Stepping to here succeeds. *)
  auto. (* Stepping to here succeeds. *)
Abort.

#[local] Set Ltac Backtrace.
Goal False.
  Fail (now auto). (* Stepping to here fails. *)
  auto. (* Stepping to here succeeds. *)
Abort.

I was alerted to this interaction by @jhaag (but his symptoms are different, so questions remain).

[cpitclaudel]

Yep, I can see that too, by pressing C-c C-n step by step.

It's the string "In nested Ltac call" that causes PG to think that there's an error in that output. Not sure why the "has indeed failed" doesn't take precedence in detecting that there's in fact no issue.

(PG uses special strings to determine that an error occurs, which can lead to funny consequences, like this:

Axiom nested Ltac call: nat.
Axiom In: nat -> nat -> nat -> nat.
Check In nested Ltac call.

)

[Blaisorblade]

Thanks. FWIW "Set Ltac Backtrace" was even the default in Coq until recently (at least 8.8?) so this is a regression?

[cpitclaudel]

Not sure: did it ever work?

[Blaisorblade]

Good question, I was making assumptions... Insert Padme meme "but it had to work, right?" 😅.

How did people ever use Fail before, when Proof General was the only IDE?

[cpitclaudel]

Same as they do now: it works in most cases, I think?
Fail doesn't print the error header, and normally that's enough:

Fail Check 1 = nat.
  The command has indeed failed with message:
  The term "nat" has type "Set" while it is expected to have type "nat".
Check 1 = nat.
  Error: The term "nat" has type "Set" while it is expected to have type "nat".

now auto.
  Error: Tactic failure: Cannot solve this goal.
Fail now auto.
  The command has indeed failed with message:
  Tactic failure: Cannot solve this goal.

But the Ltac backtrace case is special because the error header isn't on the same line.
Also, when was did having the backtrace on become the default?

[Blaisorblade]

Also, when was did having the backtrace on become the default?

The change was in 8.10 but went the other way — before we always got backtraces, now we got a flag and they're disabled by default (coq/coq#9142).

[jhaag]

Fwiw, this is what I'm seeing locally:

  Goal not True.
  Proof.
    (* by auto. *)
    (* > In nested Ltac calls to "by (tactic)" and "tactics.done", last call failed. *)
    (* > No applicable tactic. *)

    Fail (by auto).
    (* > In nested Ltac calls to "by (tactic)" and "tactics.done", last call failed. *)
    (* > No applicable tactic. *)
  Abort.

[RalfJung]

I also just ran into this issue, where Fail <tactic>. is supposed to succeed, but PG considers it failed with the output starting with

In nested Ltac calls to "f_contractive" and
"simple apply (_ : Proper (_ ==> dist_later _ ==> _) f)", last call failed.

This is problematic since Fail <foo>. is required to be able to get reasonable output from Set Typeclasses Debug -- for commands that fail, PG does not print that debug output. try tactic is a suitable work-around for now.

[Matafou]

Indeed this feature is broken. Strange that it has not be spotted earlier.

[Matafou]

I have a fix consisting in prefixing the regexp of coq-error-message by the following ugly regexp saying 'not "Message:".

\\(?:[^:]\\|[^e]:\\|[^g]e:\\|[^a]ge:\\|[^s]age:\\|[^s]sage:\\|[^e]ssage:\\|[^m]essage:\\)\n

This is not perfect but IMHO much sufficient. I only wonder if this would slow PG significantly.

[Matafou]

(useless to say that once again we all long for an better protocol...)

[Blaisorblade]

I only wonder if this would slow PG significantly.

Guess: It shouldn't unless the regexp engine has exponential backtracking; for actually regular regexp languages, there's no good reason for that, and the match should take time linear in the string, especially once you "optimize" the regexp matcher.

[cpitclaudel]

The engine has exponential backtracking for sure (I don't know of a complete implementation of one that doesn't, though re2 comes close). Not sure if it matters here.