Vscoq language server crashing with "File "plugins/ltac2/tac2core.ml", line 1914, characters 59-65: Assertion failed."

[taeyoung-1]

Maybe a duplicate of #1009 , but
From Ltac2 Require Import Ltac2. Ltac2 foo () := (). Ltac bar := ltac2:(foo).

yields error

[Error - 6:06:15 PM] Server process exited with code 0.
[top , 41050, 1738573576.329784] ==========================================================
[top , 41050, 1738573576.329816] File "plugins/ltac2/tac2core.ml", line 1914, characters 59-65: Assertion failed.
[top , 41050, 1738573576.329818] ==========================================================
[Info - 6:06:16 PM] Connection to server got closed. Server will restart.

[SkySkimmer]

What vscoq and coq versions?

[taeyoung-1]

I'm sorry,
vscoq-language-server 2.2.3, coq 8.20.0

[SkySkimmer]

The failing assert is https://github.com/coq/coq/blob/3d5120eb27f0e7ec08ce9449762dae5441299dda/plugins/ltac2/tac2core.ml#L1914
Printing ltac2:(...) in ltac1 at "raw" level (what comes out of the parser) is not supported in that Coq version (I believe it works in 9.0).
IDK why vscoq is trying to do this printing.

[gares]

Looks like another instance of the bug @rtetley already fixed, dunno if the fix is merged

[rtetley]

Indeed this was closed by #1021, the release is imminent !