UI and kernel out of sync from aborting tactics?

Hi,

it seems that aborting long-running tactics (using C-c C-c) can cause the UI and kernel to go out of sync. I have noticed this with CoqHammer's tactics specifically, e.g. best or sauto. I initially reported this problem as CoqHammer issue here: lukaszcz/coqhammer#180. However, after Łukasz pointed that it is unlikely that it is something CoqHammer is doing causing this problem I tried the CoqHammer tactics in both Coqtail and vscode and indeed the same issue seems to not appear there.

The following seems to be a somewhat reliable way to reproduce an example of the issue. Take this proof script (just some fragment from the Coq standard library with CoqHammer loaded):

From Coq Require Import List.

From Hammer Require Import Tactics.

Import ListNotations.

Fixpoint nth_ok {A : Type} (n:nat) (l:list A) (default:A) : bool :=
  match n, l with
    | O, x :: l' => true
    | O, other => false
    | S m, [] => false
    | S m, x :: t => nth_ok m t default
  end.

Lemma nth_in_or_default : forall (A:Type) (n:nat) (l:list A) (d:A),
 {In (nth n l d) l} + {nth n l d = d}.
Proof.
 best.

Now, invoking best and aborting (using C-c C-c) a few times seems to confuse the UI of Proof General. E.g. if you C-c Enter just before the Fixpoint definition and then try to move beyond it (e.g. doing C-c Enter just after it), then Coq complains that the definition exists already.

Could this be a Proof General problem? I haven't noticed this with any long-running non-CoqHammer tactics, such as e.g. firstorder.

ProofGeneral / PG

UI and kernel out of sync from aborting tactics? #764