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:

- calls to admit (this is tricky due to error recovery needing rework
  to fully account for execution)
- calls to `Printer`
  • Loading branch information
ejgallego committed Jan 9, 2023
1 parent f69b6f5 commit b0001cc
Show file tree
Hide file tree
Showing 15 changed files with 151 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, # # fixes #)

# 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
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
14 changes: 10 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,6 @@ 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 *)
(* let admit ~st = Protect.eval ~f:(admit ~st) () *)
10 changes: 8 additions & 2 deletions coq/state.mli
Original file line number Diff line number Diff line change
Expand Up @@ -10,10 +10,16 @@ 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

(** Admit an ongoing proof *)
(* TODO *)
(* val admit : st:t -> t Protect.R.t *)

(** Admit an ongoing proof, can produce errors *)
val admit : st:t -> t
89 changes: 65 additions & 24 deletions fleche/doc.ml
Original file line number Diff line number Diff line change
Expand Up @@ -27,6 +27,10 @@ module Completion = struct
type t =
| Yes of Loc.t (** Location of the last token in the document *)
| Stopped of Loc.t (** Location of the last valid token *)
| Failed of Loc.t (** Critical failure, like an anomaly *)

let loc = function
| Yes loc | Stopped loc | Failed loc -> loc
end

(* Private. A doc is a list of nodes for now. The first element in the list is
Expand All @@ -46,8 +50,7 @@ type t =
let mk_doc root_state workspace =
(* XXX This shouldn't be foo *)
let libname = Names.(DirPath.make [ Id.of_string "foo" ]) in
let f () = Coq.Init.doc_init ~root_state ~workspace ~libname in
Coq.Protect.eval ~f ()
Coq.Init.doc_init ~root_state ~workspace ~libname

let init_loc ~uri = Loc.initial (InFile { dirpath = None; file = uri })

Expand Down Expand Up @@ -101,10 +104,9 @@ let compute_common_prefix ~contents doc =
let completed = Completion.Stopped loc in
(nodes, completed)

let bump_version ~version ~contents doc =
let bump_version ~version ~contents ~end_loc doc =
(* When a new document, we resume checking from a common prefix *)
let nodes, completed = compute_common_prefix ~contents doc in
let end_loc = get_last_text contents in
{ doc with
version
; nodes
Expand All @@ -114,6 +116,22 @@ let bump_version ~version ~contents doc =
; completed
}

let bump_version ~version ~contents doc =
let end_loc = get_last_text contents in
match doc.completed with
(* We can do better, but we need to handle the case where the anomaly is when
restoring / executing the first sentence *)
| Failed _ ->
{ doc with
version
; nodes = []
; contents
; end_loc
; diags_dirty = true
; completed = Stopped (init_loc ~uri:doc.uri)
}
| Stopped _ | Yes _ -> bump_version ~version ~contents ~end_loc doc

let add_node ~node doc =
let diags_dirty = if node.diags <> [] then true else doc.diags_dirty in
{ doc with nodes = node :: doc.nodes; diags_dirty }
Expand Down Expand Up @@ -164,16 +182,8 @@ let report_progress ~doc last_tok =
(* let close_doc _modname = () *)

let parse_stm ~st ps =
let mode = Coq.State.mode ~st in
let st = Coq.State.parsing ~st in
let parse ps =
(* 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 Coq.Ast.of_coq
in
Stats.record ~kind:Stats.Kind.Parsing ~f:(Coq.Protect.eval ~f:parse) ps
let f ps = Coq.Parsing.parse ~st ps in
Stats.record ~kind:Stats.Kind.Parsing ~f ps

(* Read the input stream until a dot or a "end of proof" token is encountered *)
let parse_to_terminator : unit Pcoq.Entry.t =
Expand Down Expand Up @@ -318,8 +328,13 @@ let process_and_parse ~uri ~version ~fb_queue doc last_tok doc_handle =
| Ok (Some ast) ->
let () = if Debug.parsing then debug_parsed_sentence ~ast in
(Process ast, [], time)
| Error (loc, msg) ->
let err_loc = Option.get loc in
| Error (Anomaly (_, msg)) | Error (User (None, msg)) ->
(* We don't have a better altenative :(, usually missing error loc
here means an anomaly, so we stop *)
let err_loc = last_tok in
let diags = [ mk_diag err_loc 1 msg ] in
(EOF (Failed last_tok), diags, time)
| Error (User (Some err_loc, msg)) ->
let diags = [ mk_diag err_loc 1 msg ] in
discard_to_dot doc_handle;
let last_tok = Pcoq.Parsable.loc doc_handle in
Expand All @@ -329,7 +344,18 @@ let process_and_parse ~uri ~version ~fb_queue doc last_tok doc_handle =
(* Execution *)
match action with
(* End of file *)
| EOF completed -> set_completion ~completed doc
| EOF completed ->
let node =
{ loc = Completion.loc completed
; ast = None
; diags = parsing_diags
; messages = []
; state = st
; memo_info = ""
}
in
let doc = add_node ~node doc in
set_completion ~completed doc
| Skip (span_loc, last_tok) ->
(* We add the parsing diags *)
let node =
Expand Down Expand Up @@ -370,7 +396,8 @@ let process_and_parse ~uri ~version ~fb_queue doc last_tok doc_handle =
in
let doc = add_node ~node doc in
stm doc state last_tok_new
| Error (err_loc, msg) ->
| Error (Anomaly (err_loc, msg) as coq_err)
| Error (User (err_loc, msg) as coq_err) -> (
let err_loc = Option.default ast_loc err_loc in
let diags = [ mk_error_diagnostic ~loc:err_loc ~msg ~ast ] in
(* FB should be handled by Coq.Protect.eval XXX *)
Expand All @@ -390,7 +417,9 @@ let process_and_parse ~uri ~version ~fb_queue doc last_tok doc_handle =
}
in
let doc = add_node ~node doc in
stm doc st last_tok_new))
match coq_err with
| Anomaly _ -> set_completion ~completed:(Failed last_tok_new) doc
| User _ -> stm doc st last_tok_new)))
in
(* Note that nodes and diags in reversed order here *)
(match doc.nodes with
Expand Down Expand Up @@ -439,11 +468,21 @@ let log_resume last_tok =
asprintf "resuming, from: %d l: %d" last_tok.Loc.ep
last_tok.Loc.line_nb_last)

let safe_sub s pos len =
if pos < 0 || len < 0 || pos > String.length s - len then (
Io.Log.trace "string_sub"
(Format.asprintf "error for pos: %d len: %d str: %s" pos len s);
s)
else String.sub s pos len

let check ~ofmt:_ ~doc ~fb_queue =
match doc.completed with
| Yes _ ->
Io.Log.trace "check" "resuming, completed=yes, nothing to do";
doc
| Failed _ ->
Io.Log.trace "check" "can't resume, failed=yes, nothing to do";
doc
| Stopped last_tok ->
log_resume last_tok;
let uri, version, contents = (doc.uri, doc.version, doc.contents) in
Expand All @@ -453,7 +492,8 @@ let check ~ofmt:_ ~doc ~fb_queue =
let resume_loc = CLexer.after last_tok in
let offset = resume_loc.bp in
let processed_content =
String.(sub processed_content offset (length processed_content - offset))
safe_sub processed_content offset
(String.length processed_content - offset)
in
let handle =
Pcoq.Parsable.make ~loc:resume_loc
Expand All @@ -469,12 +509,13 @@ let check ~ofmt:_ ~doc ~fb_queue =
let doc = { doc with nodes = List.rev doc.nodes; contents } in
let end_msg =
let timestamp = Unix.gettimeofday () in
let loc =
let loc, status =
match doc.completed with
| Yes loc -> loc
| Stopped loc -> loc
| Yes loc -> (loc, "fully checked")
| Stopped loc -> (loc, "stopped")
| Failed loc -> (loc, "failed")
in
Format.asprintf "done [%.2f]: document fully checked %s" timestamp
Format.asprintf "done [%.2f]: document %s with pos %s" timestamp status
(Coq.Ast.pr_loc loc)
in
Io.Log.trace "check" end_msg;
Expand Down
Loading

0 comments on commit b0001cc

Please sign in to comment.