VsCoqTop crashes (presumably because of pretty printer)

[TheCodingWombat]

VsCoqTop 2.1.3 (and 2.0.3), vscoq-language-server 2.1.3 (and 2.0.3), Coq 8.18.0. Ubuntu 22.04.4 LTS

Following simple code. It crashes on reflexivity. But also on induction if I use it there (reflexivity would be an error I think, induction should be possible, but both crash).

` Inductive nat : Type := | O | S (n : nat).

( Define a simple function that adds two natural numbers ) Fixpoint my_add (n m : nat) : nat := match n with | O => m | S n' => S (my_add n' m) end.

Theorem plus_Sn_m : forall n m : nat, my_add n (S m) = S (my_add n m). Proof. intros n. simpl. reflexivity. Qed. `

Following error: [top , 51675, 1719928453.934245] ========================================================== [top , 51675, 1719928453.934418] Uncaught exception Failure("tag not closed"). Raised at Stdlib.failwith in file "stdlib.ml", line 29, characters 17-33 Called from Protocol__Printing.pp_of_coqpp in file "protocol/printing.ml", line 67, characters 12-26 Called from Protocol__Printing.pp_of_coqpp in file "protocol/printing.ml", line 69, characters 44-58 Called from CList.map_loop in file "clib/cList.ml", line 291, characters 21-24 Called from CList.map in file "clib/cList.ml", line 299, characters 4-18 Called from Protocol__Printing.pp_of_coqpp in file "protocol/printing.ml", line 68, characters 15-39 Called from Protocol__Printing.pp_of_coqpp in file "protocol/printing.ml", line 70, characters 46-60 Called from CList.map_loop in file "clib/cList.ml", line 291, characters 21-24 Called from CList.map in file "clib/cList.ml", line 299, characters 4-18 Called from Protocol__Printing.pp_of_coqpp in file "protocol/printing.ml", line 68, characters 15-39 Called from Protocol__Printing.pp_of_coqpp in file "protocol/printing.ml", line 69, characters 44-58 Called from CList.map_loop in file "clib/cList.ml", line 291, characters 21-24 Called from CList.map in file "clib/cList.ml", line 299, characters 4-18 Called from Protocol__Printing.pp_of_coqpp in file "protocol/printing.ml", line 68, characters 15-39 Called from Dm__DocumentManager.get_messages in file "dm/documentManager.ml", line 175, characters 53-68 Called from Dune__exe__LspManager.handle_event in file "vscoqtop/lspManager.ml", line 583, characters 21-64 Called from Dune__exe__Vscoqtop.loop.loop in file "vscoqtop/vscoqtop.ml", line 28, characters 21-50 Called from Dune__exe__Vscoqtop.loop in file "vscoqtop/vscoqtop.ml", line 33, characters 6-15

Note: I did not always get this error in the console immediately. Sometimes the visualization of the goals checked (it didn´t change anymore, but still, when moving through the code with alt down, the server had not completely crashed.

[gares]

Unfortunately I can't reproduce it with 2.1.3 on 8.18.0

[rtetley]

I'm also unable to reproduce on the dev version. I was assuming it was because I fixed something else (preparing for the next minor release).

[gares]

Anyway, something like this

diff --git a/language-server/protocol/printing.ml b/language-server/protocol/printing.ml
index a653966..24933c8 100644
--- a/language-server/protocol/printing.ml
+++ b/language-server/protocol/printing.ml
@@ -58,7 +58,10 @@ let rec regroup_tags_aux acc = function
       regroup_tags_aux acc tl

 and regroup_tags l =
- match regroup_tags_aux [[]] l with [l] -> List.rev l | _ -> failwith "tag not closed"
+ match regroup_tags_aux [[]] l with
+ | [l] -> List.rev l
+ | [] -> failwith "nothing to regroup"
+ | _ :: _ -> failwith "tag not closed"

 let rec pp_of_coqpp t = match Pp.repr t with
   | Pp.Ppcmd_empty -> Ppcmd_empty

could help better understanding the issue next time it pops up.

Even better, make the code not fail but still print something when an error occurs. This is really a general principle of printers, better to show "BUG" than crash

[rtetley]

Agreed. I will push a fix.

[rtetley]

Okay ! Actually I get it ! It's because of diff mode (git blame provided a hint). If you turn diff mode on you can reproduce !

[TheCodingWombat]

Yes! It works without diff mode, thank you. I turned it off for now.

[rtetley]

This is a duplicate of #766