@Jim Fehrle Let's discuss here, give me some time I'm fetching my examples.

In CoqIDE 8.14.1:

```
Lemma bar : True.
Proof.
try idtac.
try idtac.
Fail idtac.
try idtac.
exact I.
Qed.
Lemma foo : True.
exact I.
Qed.
```

Stepping to the end gives an error in the proof, but I am able to edit it and step down to the Qed. Notice also how the Qed's are highlighted in grey. When I get to the Qed it jumps to the end.

Also seems to work for 8.15.0

You have to step to end not step line by line.

Here is an example demonstrating the behavior when coqide's main process is busy:

```
Lemma bar : True.
Proof.
try idtac.
try idtac.
Fail idtac.
try idtac.
exact I.
Qed.
Lemma foo : True.
exact I.
Qed.
Fixpoint many_things_type (n : nat) : Type :=
match n with
| 0 => Set
| S m => forall (x : nat), many_things_type m
end.
Definition just_too_many_things_to_print : Type :=
Eval cbv in many_things_type 10000.
Print just_too_many_things_to_print.
```

The buffer is completely locked now.

So the behaviour 8.14 to 8.15 to your patch seems to be the same for the first one.

For the second one, I see that your patch lets me edit the buffer (to no effect) whilst the other versions lock up

@Ali Caglayan you should also test with Qed proofs that take a while

@Pierre-Marie Pédrot Have you got an ltac busy tactic example?

More issues: In 8.15.0, Ctrl+d will comment out a line.

```
Lemma bar : True.
Proof.
try idtac.
try idtac.
Fail idtac.
try idtac.
exact I.
Qed.
Lemma foo : True.
exact I.
Qed.
```

If you Ctrl+d on the erroneous line in the first proof, the comment gets left half open. Trying to undo from here is also wrong/buggy (gets rid of the new line).

I didn't see your messages here until I got an email from Zulip.

@Jim Fehrle No worries, I only sent them 10 min ago.

But best to capture our conclusion in an issue--less ephemeral than Zulip.

We can definitely open some issues later, I just wanted to get on the same page about async proofs.

Just trying my first example in this thread, do you see what I mean with the ability to edit proofs and not recheck the whole document?

I don't have 8.14 installed. In 8.13 I don't see any gray in the script buffer. This is probably easier to discuss if we do a video call.

Ok I have joined

```
Ltac wait n :=
match n with
| 0 => idtac
| S ?n => wait n; wait n
end.
Lemma foo: True.
Proof.
wait 18.
constructor.
Qed.
```

Last updated: Oct 13 2024 at 01:02 UTC