From e8acb1bd8a219b941e01aa6ecb123dbab115d6ef Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Mon, 9 Jan 2023 00:00:59 +0100 Subject: [PATCH] [coq] Protect all base API calls Indeed I didn't realize that goal printing could raise an anomaly, due to setting state; thus #91 is not fully fixed. So we go full principled and make `Protect` mandatory on the exported APIs. TODO: - calls to admit (this is tricky due to error recovery needing rework to fully account for execution) - calls to `Printer` --- coq/init.ml | 5 ++++- coq/init.mli | 2 +- coq/parsing.ml | 10 ++++++++++ coq/parsing.mli | 1 + coq/state.ml | 14 ++++++++++---- coq/state.mli | 10 ++++++++-- fleche/doc.ml | 28 ++++++++++++++-------------- fleche/info.ml | 11 ++++++++--- fleche/memo.mli | 3 +++ 9 files changed, 59 insertions(+), 25 deletions(-) create mode 100644 coq/parsing.ml create mode 100644 coq/parsing.mli diff --git a/coq/init.ml b/coq/init.ml index c33a9685f..91de9ffbd 100644 --- a/coq/init.ml +++ b/coq/init.ml @@ -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); @@ -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) () diff --git a/coq/init.mli b/coq/init.mli index 2358bf1a1..42351de8d 100644 --- a/coq/init.mli +++ b/coq/init.mli @@ -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 diff --git a/coq/parsing.ml b/coq/parsing.ml new file mode 100644 index 000000000..9f396c887 --- /dev/null +++ b/coq/parsing.ml @@ -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 diff --git a/coq/parsing.mli b/coq/parsing.mli new file mode 100644 index 000000000..aba4a267b --- /dev/null +++ b/coq/parsing.mli @@ -0,0 +1 @@ +val parse : st:State.t -> Pcoq.Parsable.t -> Ast.t option Protect.R.t diff --git a/coq/state.ml b/coq/state.ml index 368ccdd4c..c73b73f67 100644 --- a/coq/state.ml +++ b/coq/state.ml @@ -77,10 +77,6 @@ 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 @@ -88,6 +84,13 @@ let drop_proofs ~st = 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 @@ -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) () *) diff --git a/coq/state.mli b/coq/state.mli index d1fbea864..cf62f928c 100644 --- a/coq/state.mli +++ b/coq/state.mli @@ -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 diff --git a/fleche/doc.ml b/fleche/doc.ml index baa1810e8..be2cd8823 100644 --- a/fleche/doc.ml +++ b/fleche/doc.ml @@ -46,8 +46,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 }) @@ -164,16 +163,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 = @@ -319,7 +310,9 @@ let process_and_parse ~uri ~version ~fb_queue doc last_tok doc_handle = let () = if Debug.parsing then debug_parsed_sentence ~ast in (Process ast, [], time) | Error (loc, msg) -> - let err_loc = Option.get loc in + (* We don't have a better altenative :(, usually missing + error loc here means an anomaly *) + let err_loc = Option.default last_tok loc in let diags = [ mk_diag err_loc 1 msg ] in discard_to_dot doc_handle; let last_tok = Pcoq.Parsable.loc doc_handle in @@ -439,6 +432,13 @@ 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 > 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 _ -> @@ -453,7 +453,7 @@ 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 diff --git a/fleche/info.ml b/fleche/info.ml index 7b88aa561..2e57de6b1 100644 --- a/fleche/info.ml +++ b/fleche/info.ml @@ -181,10 +181,15 @@ module Make (P : Point) : S with module P := P = struct let node = find ~doc ~point approx in Option.bind node (fun node -> node.Doc.ast) + let in_state ~st ~f node = + match Coq.State.in_state ~st ~f node with + | Coq.Protect.R.Completed (Result.Ok res) -> res + | Coq.Protect.R.Completed (Result.Error _) | Coq.Protect.R.Interrupted -> + None + let goals ~doc ~point approx = find ~doc ~point approx - |> obind (fun node -> - Coq.State.in_state ~st:node.Doc.state ~f:pr_goal node.Doc.state) + |> obind (fun node -> in_state ~st:node.Doc.state ~f:pr_goal node.Doc.state) let messages ~doc ~point approx = find ~doc ~point approx |> Option.map (fun node -> node.Doc.messages) @@ -205,7 +210,7 @@ module Make (P : Point) : S with module P := P = struct let completion ~doc ~point prefix = find ~doc ~point Exact |> obind (fun node -> - Coq.State.in_state ~st:node.Doc.state prefix ~f:(fun prefix -> + in_state ~st:node.Doc.state prefix ~f:(fun prefix -> to_qualid prefix |> obind (fun p -> Nametab.completion_canditates p diff --git a/fleche/memo.mli b/fleche/memo.mli index c28bc1b6a..534386df5 100644 --- a/fleche/memo.mli +++ b/fleche/memo.mli @@ -17,6 +17,9 @@ val interp_command : -> Coq.State.t Coq.Interp.interp_result Stats.t val interp_admitted : st:Coq.State.t -> Coq.State.t +(* TODO *) +(* val interp_admitted : st:Coq.State.t -> Coq.State.t Coq.Protect.R.t *) + val mem_stats : unit -> int val load_from_disk : file:string -> unit val save_to_disk : file:string -> unit