[vscoq2] language server hangs up with some specific erroneous inputs

[zeptometer]

Hi all. First, thank you all for your active development of this fantastic extension!

I tried using the extension to solve exercises of Software Foundations, and I found the language server keeps failing and finally hangs up when I edit the source code. Here is a minified source code that reproduces this behavior.

Inductive bool : Type :=
  | true
  | false.

Definition negb (b:bool) : bool :=
  match b with
  | true => false
  | false => true
  end.

Definition andb3 (b1:bool) (b2:bool) (b3:bool) : bool :=
  if b1 then
    if b2 then
      if b3 then
        true
      else
        false
    else
      false
  else
    false.

Example test_andb33:                 (andb3 true false true) = false.
(* Comment from reporter: Admitted is missing here*)

Example test_andb34:                 (andb3 true true false) = false.
Admitted.

Module NatPlayground2.

Fixpoint plus (n : nat) (m : nat) : nat :=
  match n with
  | O => m
  | S n' => S (plus n' m)
  end.

Compute (plus 3 2).
(* Comment from reporter: Missing `End NatPlayground2.`*)

And I use the following environments:

• OS: WSL Ubuntu 22.04
• coq: 8.18.0
• vscode-langauge-server: 2.0.1 (installed via git repo)

Feel free to let me know if you need further information.

[rtetley]

Hi ! Thanks for your feedback :-) It seems that the

Module NatPlayground2. 

line is the culprit. If I comment it out it no longer crashes. This is still buggy behaviour. We will investigate !

[zeptometer]

Thank you for your quick response!

It seems that the

Module NatPlayground2. 

line is the culprit. If I comment it out it no longer crashes. This is still buggy behaviour. We will investigate !

The cause seems more complicated. It stopped to crash also when I modified other parts: for example,

• Replace the definition of andb3 with Admitted
• Remove the line Compute (plus 3 2).

So I guess this behavior is not caused by a specific line in this code. And I found that I can even minify the reproducing code. I hope this helps you investigate the root cause :)

Inductive bool : Type :=
  | true
  | false.

Definition andb3 (b1:bool) (b2:bool) (b3:bool) : bool :=
  if b1 then
    if b2 then
      if b3 then
        true
      else
        false
    else
      false
  else
    false.

Example test_andb33:                 (andb3 true false true) = false.
(* Comment from reporter: Admitted is missing here*)

Module NatPlayground2.

Fixpoint plus (n : nat) (m : nat) : nat :=
  match n with
  | O => m
  | S n' => S (plus n' m)
  end.

Compute (plus 3 2).
(* Comment from reporter: Missing `End NatPlayground2.`*)

[gares]

I guess passing -vscoq-d all to the language server can help see what goes wrong.

I've no time to try it out myself now, but I would guess that opening a module inside a proof (the one of test_andb33) is part of the problem.

[rtetley]

After investigation, this seems to come from the Module command which fails in the interp phase but succeeds in the synterp phase. When you declare a logical object after that, the nametab resolves to a full name which includes the open module (in this case, NatPlayground2.plus) whereas the logical environment does not include the module name. The discrepancy is introduced in the following line: https://github.com/coq/coq/blob/2db45f6ba3507d36acf219d97d4b5819e56bbebf/kernel/safe_typing.ml#L853C1-L854C1 We will think of a fix or workaround. Thanks for reporting ;-)

[gares]

Can you tell why the interp phase fails exactly?

I guess that there is a general problem when a command has a non-trivial synterp effect, but an error at interp time (hence, no effect by recovery I imagine). I wonder if interp error-recovery should also backtrack on the synterp effect.

It would avoid some untested Coq code paths, but also expose other code paths. Eg

Import ModuleWithArrowNotations.
Check (a ~~~> b).

would parse the expression, but interpret it in a state where the notation is not defined (if the Import fails, for some reason, at interp time).

Another alternative is to detect the discrepancy between the two phases and invalidate everything after the offending command, forcing a re-parsing as well.

[rtetley]

I believe it fails because in the example a Module is declared on top of an open proof.

[gares]

So in this case we can enforce some invariant on the document structure, e.g. the proof has no terminator, we add Admitted implicitly. But I don't know if all synterp-interp sync problems can be prevented by ensuring structural invariants.