Proof General UI and kernel out of sync from aborting tactics?

[AndreasLoow]

Hi, there seems to be some problems with aborting some of the tactics provided by CoqHammer.

To exemplify, consider this proof script (just some function and a theorem from the Coq standard library to have a non-empty script):

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.

I am using Proof General in Emacs and if I invoke and abort (using C-c C-c) the best tactics a few times (it seems to happen nondeterministically), the UI and the kernel seem to end up out of sync with each other. 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), Coq now complains:

Error: nth_ok already exists.

So somehow although according to the Proof General UI (specifically, the blue marked part of the script file) nth_ok is not defined the kernel seems to say it is.

I have seen this happen with various CoqHammer tactics, such as sauto and other auto variants.

It might be some race condition thing happening in the communication between the UI and the kernel since it seems to be somewhat nondeterministic?

[lukaszcz]

This seems to be a Proof General issue, which is a separate project. Neither CoqHammer nor Coq communicate with Proof General directly.

[AndreasLoow]

Thanks, I opened an issue in the Proof General issue tracker! (Also, thanks for the quick response and thanks for your work on CoqHammer -- it's an amazing tool.)