search

coq-community / vscoq

A Visual Studio Code extension for Coq [maintainers=@rtetley,@huynhtrankhanh,@thery,@Blaisorblade]
MIT License
333 stars 68 forks source link

Crash During Fast Edits With Proof Delegation Enabled #703

Open vfukala opened 9 months ago

vfukala commented 9 months ago

If I have the Proof:Delegation setting set to Delegate proofs and I quickly edit the H_edit_me name (e.g. by holding down a key) in the following file...

Require Import Lia.

Derive f SuchThat True As H_edit_me.

Lemma lemm : True.
Proof.
  trivial.
Qed.

Fixpoint pow (a b : nat) : nat :=
  match b with
  | 0 => 1
  | S b' => a * pow a b'
  end.

Lemma computation : (pow 3 21) < 900.
Proof.
  simpl. lia.
Qed.

Lemma computation2 : (pow 2 27) < 900.
Proof.
  simpl. lia.
Qed.

Lemma computation3 : (pow 4 16) < 900.
Proof.
  simpl. lia.
Qed.

, I get an output from the Coq Language Server like

[Info  - 5:16:08 PM] Connection to server got closed. Server will restart.
[Info  - 5:16:09 PM] Connection to server got closed. Server will restart.
[Info  - 5:16:11 PM] Connection to server got closed. Server will restart.
[Info  - 5:16:11 PM] Connection to server got closed. Server will restart.
[Error - 5:16:12 PM] Connection to server got closed. Server will not be restarted.

and VSCode tells me image

Then I have to restart VSCode to get the language server running again.

This doesn't happen with Proof:Delegation set to No delegation.

edit: After setting

"vscoq.args": [
        "-bt",
        "-vscoq-d", 
        "all",
    ],

, I managed to fish out

[top                 , 1787622, 1703456804.192810] Main loop event ready: ExecuteToLoc 23 (1 tasks left, started 0.082 ago) , 9 events waiting
[top                 , 1787622, 1703456804.192853] ==========================================================
[top                 , 1787622, 1703456804.192994] Constant test.pow does not appear in the environment.
Raised at Exninfo.iraise in file "clib/exninfo.ml", line 79, characters 4-11
Called from Environ.lookup_constant in file "kernel/environ.ml" (inlined), line 215, characters 6-34
Called from Environ.lookup_constant_variables in file "kernel/environ.ml" (inlined), line 641, characters 13-34
Called from Environ.vars_of_global in file "kernel/environ.ml", line 671, characters 19-51
Called from Termops.global_vars_set.filtrec in file "engine/termops.ml", line 1301, characters 28-51
Called from Constr.fold in file "kernel/constr.ml", line 495, characters 35-44
Called from Stdlib__Array.fold_left in file "array.ml", line 163, characters 9-30
Called from Proof_using.set_of_type.(fun) in file "vernac/proof_using.ml", line 41, characters 19-57
Called from Stdlib__List.fold_left in file "list.ml", line 121, characters 24-34
Called from Proof_using.process_expr in file "vernac/proof_using.ml", line 91, characters 13-37
Called from Proof_using.definition_using in file "vernac/proof_using.ml" (inlined), line 98, characters 10-42
Called from Dm__ExecutionManager.interp_qed_delayed.f in file "dm/executionManager.ml", line 192, characters 18-82
Called from Dm__ExecutionManager.interp_qed_delayed in file "dm/executionManager.ml", line 206, characters 22-63
Called from Dm__ExecutionManager.execute in file "dm/executionManager.ml", line 422, characters 38-100
Called from Dm__DocumentManager.handle_event in file "dm/documentManager.ml", line 308, characters 6-85
Called from Dune__exe__LspManager.handle_event in file "vscoqtop/lspManager.ml", line 562, characters 26-62
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

[top                 , 1787622, 1703456804.193002] ==========================================================
[Error - 5:26:44 PM] Connection to server got closed. Server will not be restarted.

out of the language server output. The name of the file I'm editing is test.v.

vfukala commented 9 months ago

Similarly, when I just open this file:

Require Import LiveVerif.LiveVerifLib. *)
"
Qed.
Derive f SuchThat (fun_correct! f) As f_ok.
{
}
Qed.

, I immediately get this crash:

[top                 , 1789779, 1703457267.091113] Main loop event ready: ExecuteToLoc 7 (1 tasks left, started 0.136 ago) , 3 events waiting
[top                 , 1789779, 1703457267.091123] ==========================================================
[top                 , 1789779, 1703457267.091146] Unknown variable: f.
Raised at Exninfo.iraise in file "clib/exninfo.ml", line 79, characters 4-11
Called from Stdlib__Set.Make.iter in file "set.ml", line 378, characters 35-38
Called from Dm__ExecutionManager.interp_qed_delayed.f in file "dm/executionManager.ml", line 194, characters 6-256
Called from Dm__ExecutionManager.interp_qed_delayed in file "dm/executionManager.ml", line 206, characters 22-63
Called from Dm__ExecutionManager.execute in file "dm/executionManager.ml", line 422, characters 38-100
Called from Dm__DocumentManager.handle_event in file "dm/documentManager.ml", line 308, characters 6-85
Called from Dune__exe__LspManager.handle_event in file "vscoqtop/lspManager.ml", line 562, characters 26-62
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

[top                 , 1789779, 1703457267.091149] ==========================================================
[Error - 5:34:27 PM] Connection to server got closed. Server will not be restarted.

Same settings as before.
I also get similar errors for some larger files which are actually useful and can be successfully checked with proof delegation disabled. What I posted are just (close to) minimal examples.