Stream: Coq devs & plugin devs

Topic: Different proof editing example

Ali Caglayan (Feb 23 2022 at 16:24):

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

Ali Caglayan (Feb 23 2022 at 16:28):

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.

Ali Caglayan (Feb 23 2022 at 16:28):

Also seems to work for 8.15.0

Ali Caglayan (Feb 23 2022 at 16:30):

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

Ali Caglayan (Feb 23 2022 at 16:30):

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.

Ali Caglayan (Feb 23 2022 at 16:30):

The buffer is completely locked now.

Ali Caglayan (Feb 23 2022 at 16:33):

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

Ali Caglayan (Feb 23 2022 at 16:33):

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

Pierre-Marie Pédrot (Feb 23 2022 at 16:34):

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

Ali Caglayan (Feb 23 2022 at 16:38):

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

Ali Caglayan (Feb 23 2022 at 16:41):

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).

Jim Fehrle (Feb 23 2022 at 16:42):

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

Ali Caglayan (Feb 23 2022 at 16:42):

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

Jim Fehrle (Feb 23 2022 at 16:43):

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

Ali Caglayan (Feb 23 2022 at 16:44):

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

Ali Caglayan (Feb 23 2022 at 16:45):

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?

Jim Fehrle (Feb 23 2022 at 16:47):

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.

Jim Fehrle (Feb 23 2022 at 16:47):

Click to join video call

Ali Caglayan (Feb 23 2022 at 16:48):

Ok I have joined

Pierre-Marie Pédrot (Feb 23 2022 at 16:49):

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: May 31 2023 at 17:01 UTC