You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
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...
RequireImport 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
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.
The text was updated successfully, but these errors were encountered:
RequireImport 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.
If I have the
Proof:Delegation
setting set toDelegate proofs
and I quickly edit theH_edit_me
name (e.g. by holding down a key) in the following file..., I get an output from the Coq Language Server like
and VSCode tells me
Then I have to restart VSCode to get the language server running again.
This doesn't happen with
Proof:Delegation
set toNo delegation
.edit: After setting
, I managed to fish out
out of the language server output. The name of the file I'm editing is
test.v
.The text was updated successfully, but these errors were encountered: