Skip to content

Commit

Permalink
[coq] Protect all base API calls, stop checking on anomaly
Browse files Browse the repository at this point in the history
Work on tricky issues made me realize that we don't handle anomalies
and Coq errors still in the best way, thus #91 is not really solved.

There are 2 issues this PR solves:
- goal printing can raise an anomalies and errors, due
  to setting state and printing,
- it is safer to stop checking and set the document to failed when an
  anomaly happens (tho we could make this configurable).

Thus, we go full principled in terms of API and make `Protect`
mandatory on the exported APIs from `coq` library.

We also introduce a `Failed` state that prevents further checking of
that document without having finished it.

Really fixes #91, and a step towards #153

TODO: protect calls to admit, but we leave this for a further PR as it
is quite tricky due to error recovery needing rework to fully account
for `Protect.R` results.
  • Loading branch information
ejgallego committed Jan 9, 2023
1 parent f69b6f5 commit 5435734
Show file tree
Hide file tree
Showing 16 changed files with 156 additions and 58 deletions.
6 changes: 6 additions & 0 deletions CHANGES.md
Original file line number Diff line number Diff line change
@@ -1,3 +1,9 @@
# coq-lsp 0.1.3:
------------------------

- Much improved handling of Coq fatal errors, the server is now
hardened against them (@ejgallego, #155, #157, #160, fixes #91)

# coq-lsp 0.1.2: Message
------------------------

Expand Down
11 changes: 6 additions & 5 deletions controller/coq_lsp.ml
Original file line number Diff line number Diff line change
Expand Up @@ -210,8 +210,8 @@ module Check = struct
let completed uri =
let doc = DocHandle.find_doc ~uri in
match doc.completed with
| Yes _ -> true
| _ -> false
| Yes _ | Failed _ -> true
| Stopped _ -> false

let schedule ~uri = pending := Some uri
end
Expand All @@ -231,7 +231,8 @@ let do_open ~state params =
DocHandle.create ~uri ~doc;
Check.schedule ~uri
(* Maybe send some diagnostics in this case? *)
| Coq.Protect.R.Completed (Result.Error (_, msg)) ->
| Coq.Protect.R.Completed (Result.Error (Anomaly (_, msg)))
| Coq.Protect.R.Completed (Result.Error (User (_, msg))) ->
let msg = Pp.string_of_ppcmds msg in
LIO.trace "Fleche.Doc.create" ("internal error" ^ msg)
| Coq.Protect.R.Interrupted -> ()
Expand Down Expand Up @@ -306,7 +307,7 @@ let do_symbols ofmt ~id params =
let slist = Coq.Ast.grab_definitions f ast in
let msg = LSP.mk_reply ~id ~result:(`List slist) in
LIO.send_json ofmt msg
| Stopped _ ->
| Stopped _ | Failed _ ->
(* -32802 = RequestFailed | -32803 = ServerCancelled ; *)
let code = -32802 in
let message = "Document is not ready" in
Expand All @@ -319,7 +320,7 @@ let do_position_request ofmt ~id params ~handler =
let in_range =
match doc.completed with
| Yes _ -> true
| Stopped loc ->
| Failed loc | Stopped loc ->
line < loc.line_nb_last
|| (line = loc.line_nb_last && col <= loc.ep - loc.bol_pos_last)
in
Expand Down
5 changes: 4 additions & 1 deletion coq/init.ml
Original file line number Diff line number Diff line change
Expand Up @@ -72,7 +72,7 @@ let coq_init opts =
(**************************************************************************)

(* Inits the context for a document *)
let doc_init ~root_state ~workspace ~libname =
let doc_init ~root_state ~workspace ~libname () =
(* Lsp.Io.log_error "init" "starting"; *)
Vernacstate.unfreeze_interp_state (State.to_coq root_state);

Expand All @@ -83,3 +83,6 @@ let doc_init ~root_state ~workspace ~libname =

(* We return the state at this point! *)
Vernacstate.freeze_interp_state ~marshallable:false |> State.of_coq

let doc_init ~root_state ~workspace ~libname =
Protect.eval ~f:(doc_init ~root_state ~workspace ~libname) ()
2 changes: 1 addition & 1 deletion coq/init.mli
Original file line number Diff line number Diff line change
Expand Up @@ -33,4 +33,4 @@ val doc_init :
root_state:State.t
-> workspace:Workspace.t
-> libname:Names.DirPath.t
-> State.t
-> State.t Protect.R.t
21 changes: 9 additions & 12 deletions coq/interp.ml
Original file line number Diff line number Diff line change
Expand Up @@ -50,18 +50,15 @@ let marshal_out f oc res =
| Ok res ->
Marshal.to_channel oc 0 [];
f oc res.Info.res
| Error (loc, msg) ->
| Error _err ->
Marshal.to_channel oc 1 [];
Marshal.to_channel oc loc [];
Marshal.to_channel oc msg [];
(* Marshal.to_channel oc loc []; *)
(* Marshal.to_channel oc msg []; *)
())

let marshal_in f ic =
let tag : int = Marshal.from_channel ic in
if tag = 0 then
let res = f ic in
Protect.R.Completed (Ok { Info.res; feedback = [] })
else
let loc : Loc.t option = Marshal.from_channel ic in
let msg : Pp.t = Marshal.from_channel ic in
Protect.R.Completed (Error (loc, msg))
(* Needs to be implemeted by Protect.marshal_in *)
let marshal_in _f _ic = Obj.magic 0
(* let tag : int = Marshal.from_channel ic in if tag = 0 then let res = f ic in
Protect.R.Completed (Ok { Info.res; feedback = [] }) else let loc : Loc.t
option = Marshal.from_channel ic in let msg : Pp.t = Marshal.from_channel ic
in Protect.R.Completed (Error (User (loc, msg))) *)
10 changes: 10 additions & 0 deletions coq/parsing.ml
Original file line number Diff line number Diff line change
@@ -0,0 +1,10 @@
let parse ~st ps =
let mode = State.mode ~st in
let st = State.parsing ~st in
(* Coq is missing this, so we add it here. Note that this MUST run inside
coq_protect *)
Control.check_for_interrupt ();
Vernacstate.Parser.parse st Pvernac.(main_entry mode) ps
|> Option.map Ast.of_coq

let parse ~st ps = Protect.eval ~f:(parse ~st) ps
1 change: 1 addition & 0 deletions coq/parsing.mli
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
val parse : st:State.t -> Pcoq.Parsable.t -> Ast.t option Protect.R.t
8 changes: 8 additions & 0 deletions coq/print.ml
Original file line number Diff line number Diff line change
@@ -0,0 +1,8 @@
let pr_ltype_env ~goal_concl_style env sigma x =
Printer.pr_ltype_env ~goal_concl_style env sigma x

let pr_ltype_env ~goal_concl_style env sigma x =
let f = pr_ltype_env ~goal_concl_style env sigma in
match Protect.eval ~f x with
| Protect.R.Completed (Ok pr) -> pr
| _ -> Pp.str "printer failed!"
2 changes: 2 additions & 0 deletions coq/print.mli
Original file line number Diff line number Diff line change
@@ -0,0 +1,2 @@
val pr_ltype_env :
goal_concl_style:bool -> Environ.env -> Evd.evar_map -> Constr.t -> Pp.t
15 changes: 12 additions & 3 deletions coq/protect.ml
Original file line number Diff line number Diff line change
@@ -1,5 +1,13 @@
module Error = struct
type t = Loc.t option * Pp.t
type payload = Loc.t option * Pp.t

type t =
| User of payload
| Anomaly of payload

let map ~f = function
| User e -> User (f e)
| Anomaly e -> Anomaly (f e)
end

module R = struct
Expand All @@ -13,7 +21,7 @@ module R = struct
| Interrupted -> Interrupted

let map_error ~f = function
| Completed (Error (loc, msg)) -> Completed (Error (f (loc, msg)))
| Completed (Error e) -> Completed (Error (Error.map ~f e))
| res -> res

let map_loc ~f =
Expand All @@ -31,4 +39,5 @@ let eval ~f x =
let e, info = Exninfo.capture exn in
let loc = Loc.(get_loc info) in
let msg = CErrors.iprint (e, info) in
R.Completed (Error (loc, msg))
if CErrors.is_anomaly e then R.Completed (Error (Anomaly (loc, msg)))
else R.Completed (Error (User (loc, msg)))
10 changes: 7 additions & 3 deletions coq/protect.mli
Original file line number Diff line number Diff line change
@@ -1,14 +1,18 @@
module Error : sig
type t = Loc.t option * Pp.t
type payload = Loc.t option * Pp.t

type t = private
| User of payload
| Anomaly of payload
end

module R : sig
type 'a t =
type 'a t = private
| Completed of ('a, Error.t) result
| Interrupted (* signal sent, eval didn't complete *)

val map : f:('a -> 'b) -> 'a t -> 'b t
val map_error : f:(Error.t -> Error.t) -> 'a t -> 'a t
val map_error : f:(Error.payload -> Error.payload) -> 'a t -> 'a t

(** Update the loc stored in the result, this is used by our cache-aware
location *)
Expand Down
15 changes: 11 additions & 4 deletions coq/state.ml
Original file line number Diff line number Diff line change
Expand Up @@ -77,17 +77,20 @@ let mode ~st =
let parsing ~st = st.Vernacstate.parsing
let lemmas ~st = st.Vernacstate.lemmas

let in_state ~st ~f a =
Vernacstate.unfreeze_interp_state st;
f a

let drop_proofs ~st =
let open Vernacstate in
{ st with
lemmas =
Option.cata (fun s -> snd @@ Vernacstate.LemmaStack.pop s) None st.lemmas
}

let in_state ~st ~f a =
let f a =
Vernacstate.unfreeze_interp_state st;
f a
in
Protect.eval ~f a

let admit ~st =
let () = Vernacstate.unfreeze_interp_state st in
match st.Vernacstate.lemmas with
Expand All @@ -99,3 +102,7 @@ let admit ~st =
let program = NeList.map_head (fun _ -> pm) st.Vernacstate.program in
let st = Vernacstate.freeze_interp_state ~marshallable:false in
{ st with lemmas; program }

(* TODO: implement protect once error recovery supports a failing recovery
execution *)
(* let admit ~st = Protect.eval ~f:(admit ~st) () *)
5 changes: 4 additions & 1 deletion coq/state.mli
Original file line number Diff line number Diff line change
Expand Up @@ -10,7 +10,10 @@ val hash : t -> int
val mode : st:t -> Pvernac.proof_mode option
val parsing : st:t -> Vernacstate.Parser.t
val lemmas : st:t -> Vernacstate.LemmaStack.t option
val in_state : st:t -> f:('a -> 'b) -> 'a -> 'b

(** Execute a command in state [st]. Unfortunately this can produce anomalies as
Coq state setting is imperative, so we need to wrap it in protect. *)
val in_state : st:t -> f:('a -> 'b) -> 'a -> 'b Protect.R.t

(** Drop the proofs from the state *)
val drop_proofs : st:t -> t
Expand Down
Loading

0 comments on commit 5435734

Please sign in to comment.