From 579e9190340500105b3c911868cfa6478dae628d Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Wed, 21 Jun 2023 21:00:58 +0200 Subject: [PATCH] [coq] Monitor Coq calls under a `token` interruption parameter. For now the interruption token is still the global `Control.interrupt` variable, but we adapt the code to the token interface. This PR was part of #509. --- CHANGES.md | 2 + compiler/cc.ml | 1 + compiler/compile.ml | 6 +- compiler/driver.ml | 7 +- controller/lsp_core.ml | 102 ++++++++++++++++++----------- controller/request.ml | 14 ++-- controller/request.mli | 10 ++- controller/rq_completion.ml | 2 +- controller/rq_definition.ml | 2 +- controller/rq_document.ml | 2 +- controller/rq_goals.ml | 29 +++++---- controller/rq_hover.ml | 49 ++++++++------ controller/rq_hover.mli | 12 +++- controller/rq_lens.ml | 2 +- controller/rq_save.ml | 21 +++++- controller/rq_selectionRange.ml | 2 +- controller/rq_symbols.ml | 2 +- coq/init.ml | 4 +- coq/init.mli | 3 +- coq/interp.ml | 5 +- coq/interp.mli | 9 ++- coq/limits.ml | 1 + coq/limits.mli | 1 + coq/parsing.ml | 2 +- coq/parsing.mli | 7 +- coq/print.ml | 4 +- coq/print.mli | 3 +- coq/protect.ml | 18 +++--- coq/protect.mli | 4 +- coq/save.ml | 20 +++++- coq/save.mli | 20 +++++- coq/state.ml | 12 ++-- coq/state.mli | 13 ++-- coq/workspace.ml | 8 +-- coq/workspace.mli | 10 ++- fleche/doc.ml | 110 +++++++++++++++++--------------- fleche/doc.mli | 21 ++++-- fleche/info.ml | 10 +-- fleche/info.mli | 9 ++- fleche/memo.ml | 21 +++--- fleche/memo.mli | 16 +++-- fleche/theory.ml | 43 +++++++------ fleche/theory.mli | 7 +- plugins/astdump/main.ml | 2 +- plugins/save_vo/main.ml | 4 +- plugins/simple/main.ml | 2 +- 46 files changed, 414 insertions(+), 240 deletions(-) diff --git a/CHANGES.md b/CHANGES.md index 72cfd9ec..148f0e06 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -54,6 +54,8 @@ - depend on `memprof-limits` on OCaml 4.x (@ejgallego, #660) - bump minimal OCaml version to 4.12 due to `memprof-limits` (@ejgallego, #660) + - monitor all Coq-level calls under an interruption token + (@ejgallego, #661) # coq-lsp 0.1.8.1: Spring fix ----------------------------- diff --git a/compiler/cc.ml b/compiler/cc.ml index 828e2bd4..c81bf773 100644 --- a/compiler/cc.ml +++ b/compiler/cc.ml @@ -4,4 +4,5 @@ type t = ; workspaces : (string * (Coq.Workspace.t, string) Result.t) list ; default : Coq.Workspace.t ; io : Fleche.Io.CallBack.t + ; token : Coq.Limits.Token.t } diff --git a/compiler/compile.ml b/compiler/compile.ml index f99ba019..50bfbc07 100644 --- a/compiler/compile.ml +++ b/compiler/compile.ml @@ -25,7 +25,7 @@ let save_diags_file ~(doc : Fleche.Doc.t) = Util.format_to_file ~file ~f:Output.pp_diags diags let compile_file ~cc file = - let { Cc.io; root_state; workspaces; default } = cc in + let { Cc.io; root_state; workspaces; default; token } = cc in let lvl = Io.Level.info in let message = Format.asprintf "compiling file %s@\n%!" file in io.message ~lvl ~message; @@ -35,8 +35,8 @@ let compile_file ~cc file = let workspace = workspace_of_uri ~io ~workspaces ~uri ~default in let env = Doc.Env.make ~init:root_state ~workspace in let raw = Util.input_all file in - let () = Theory.create ~io ~env ~uri ~raw ~version:1 in - match Theory.Check.maybe_check ~io with + let () = Theory.create ~io ~token ~env ~uri ~raw ~version:1 in + match Theory.Check.maybe_check ~io ~token with | None -> () | Some (_, doc) -> save_diags_file ~doc; diff --git a/compiler/driver.ml b/compiler/driver.ml index 5f78127d..5e4e1be9 100644 --- a/compiler/driver.ml +++ b/compiler/driver.ml @@ -37,11 +37,14 @@ let go args = let root_state = coq_init ~debug in let roots = if List.length roots < 1 then [ Sys.getcwd () ] else roots in let default = Coq.Workspace.default ~debug ~cmdline in + let token = Coq.Limits.Token.create () in let workspaces = - List.map (fun dir -> (dir, Coq.Workspace.guess ~cmdline ~debug ~dir)) roots + List.map + (fun dir -> (dir, Coq.Workspace.guess ~token ~cmdline ~debug ~dir)) + roots in List.iter (log_workspace ~io) workspaces; - let cc = Cc.{ root_state; workspaces; default; io } in + let cc = Cc.{ root_state; workspaces; default; io; token } in (* Initialize plugins *) plugin_init plugins; Compile.compile ~cc files diff --git a/controller/lsp_core.ml b/controller/lsp_core.ml index 2ab779e3..a7dff6da 100644 --- a/controller/lsp_core.ml +++ b/controller/lsp_core.ml @@ -106,10 +106,10 @@ module State = struct open Lsp.Workspace - let add_workspace state { WorkspaceFolder.uri; _ } = + let add_workspace ~token state { WorkspaceFolder.uri; _ } = let dir = Lang.LUri.File.to_string_file uri in let { cmdline; workspaces; _ } = state in - let ws = Coq.Workspace.guess ~debug:false ~cmdline ~dir in + let ws = Coq.Workspace.guess ~token ~debug:false ~cmdline ~dir in { state with workspaces = (dir, ws) :: workspaces } let del_workspace state { WorkspaceFolder.uri; _ } = @@ -141,13 +141,13 @@ module State = struct | Some (_, Ok workspace) -> (root_state, workspace) end -let do_changeWorkspaceFolders ~ofn:_ ~state params = +let do_changeWorkspaceFolders ~ofn:_ ~token ~state params = let open Lsp.Workspace in let { DidChangeWorkspaceFoldersParams.event } = DidChangeWorkspaceFoldersParams.of_yojson (`Assoc params) |> Result.get_ok in let { WorkspaceFoldersChangeEvent.added; removed } = event in - let state = List.fold_left State.add_workspace state added in + let state = List.fold_left (State.add_workspace ~token) state added in let state = List.fold_left State.del_workspace state removed in state @@ -163,11 +163,17 @@ module Rq : sig val error : int * string -> t end - val serve : ofn:(J.t -> unit) -> id:int -> Action.t -> unit + val serve : + ofn:(J.t -> unit) -> token:Coq.Limits.Token.t -> id:int -> Action.t -> unit + val cancel : ofn:(J.t -> unit) -> code:int -> message:string -> int -> unit val serve_postponed : - ofn:(J.t -> unit) -> doc:Fleche.Doc.t -> Int.Set.t -> unit + ofn:(J.t -> unit) + -> token:Coq.Limits.Token.t + -> doc:Fleche.Doc.t + -> Int.Set.t + -> unit end = struct (* Answer a request, private *) let answer ~ofn ~id result = @@ -210,14 +216,14 @@ end = struct LIO.trace "serving" (Format.asprintf "rq: %d | %a" id Request.Data.data pr) - let serve_postponed ~ofn ~doc id = + let serve_postponed ~ofn ~token ~doc id = let f pr = debug_serve id pr; - Request.Data.serve ~doc pr + Request.Data.serve ~token ~doc pr in consume_ ~ofn ~f id - let query ~ofn ~id (pr : Request.Data.t) = + let query ~ofn ~token ~id (pr : Request.Data.t) = let uri, postpone, request = Request.Data.dm_request pr in match Fleche.Theory.Request.add { id; uri; postpone; request } with | Cancel -> @@ -226,7 +232,7 @@ end = struct Error (code, message) |> answer ~ofn ~id | Now doc -> debug_serve id pr; - Request.Data.serve ~doc pr |> answer ~ofn ~id + Request.Data.serve ~token ~doc pr |> answer ~ofn ~id | Postpone -> postpone_ ~id pr module Action = struct @@ -238,18 +244,19 @@ end = struct let error (code, msg) = now (Error (code, msg)) end - let serve ~ofn ~id action = + let serve ~ofn ~token ~id action = match action with | Action.Immediate r -> answer ~ofn ~id r - | Action.Data p -> query ~ofn ~id p + | Action.Data p -> query ~ofn ~token ~id p - let serve_postponed ~ofn ~doc rl = Int.Set.iter (serve_postponed ~ofn ~doc) rl + let serve_postponed ~ofn ~token ~doc rl = + Int.Set.iter (serve_postponed ~ofn ~token ~doc) rl end (***********************************************************************) (* Start of protocol handlers: document notifications *) -let do_open ~io ~(state : State.t) params = +let do_open ~io ~token ~(state : State.t) params = let document = field "textDocument" params |> Lsp.Doc.TextDocumentItem.of_yojson |> Result.get_ok @@ -257,9 +264,9 @@ let do_open ~io ~(state : State.t) params = let Lsp.Doc.TextDocumentItem.{ uri; version; text; _ } = document in let init, workspace = State.workspace_of_uri ~uri ~state in let env = Fleche.Doc.Env.make ~init ~workspace in - Fleche.Theory.create ~io ~env ~uri ~raw:text ~version + Fleche.Theory.create ~io ~token ~env ~uri ~raw:text ~version -let do_change ~ofn ~io params = +let do_change ~ofn ~io ~token params = let uri, version = Helpers.get_uri_version params in let changes = List.map U.to_assoc @@ list_field "contentChanges" params in match changes with @@ -272,7 +279,7 @@ let do_change ~ofn ~io params = () | change :: _ -> let raw = string_field "text" change in - let invalid_rq = Fleche.Theory.change ~io ~uri ~version ~raw in + let invalid_rq = Fleche.Theory.change ~io ~token ~uri ~version ~raw in let code = -32802 in let message = "Request got old in server" in Int.Set.iter (Rq.cancel ~ofn ~code ~message) invalid_rq @@ -420,12 +427,16 @@ let lsp_init_process ~ofn ~cmdline ~debug msg : Init_effect.t = in LIO.logMessage ~lvl:3 ~message; let result, dirs = Rq_init.do_initialize ~params in - Rq.Action.now (Ok result) |> Rq.serve ~ofn ~id; + (* We don't need to interrupt this *) + let token = Coq.Limits.Token.create () in + Rq.Action.now (Ok result) |> Rq.serve ~ofn ~token ~id; LIO.logMessage ~lvl:3 ~message:"Server initialized"; (* Workspace initialization *) let debug = debug || !Fleche.Config.v.debug in let workspaces = - List.map (fun dir -> (dir, Coq.Workspace.guess ~cmdline ~debug ~dir)) dirs + List.map + (fun dir -> (dir, Coq.Workspace.guess ~token ~cmdline ~debug ~dir)) + dirs in List.iter log_workspace workspaces; Success workspaces @@ -440,15 +451,15 @@ let lsp_init_process ~ofn ~cmdline ~debug msg : Init_effect.t = Loop (** Dispatching *) -let dispatch_notification ~io ~ofn ~state ~method_ ~params : unit = +let dispatch_notification ~io ~ofn ~token ~state ~method_ ~params : unit = match method_ with (* Lifecycle *) | "exit" -> raise Lsp_exit (* setTrace *) | "$/setTrace" -> do_trace params (* Document lifetime *) - | "textDocument/didOpen" -> do_open ~io ~state params - | "textDocument/didChange" -> do_change ~io ~ofn params + | "textDocument/didOpen" -> do_open ~io ~token ~state params + | "textDocument/didChange" -> do_change ~io ~ofn ~token params | "textDocument/didClose" -> do_close ~ofn params | "textDocument/didSave" -> Cache.save_to_disk () (* Cancel Request *) @@ -458,13 +469,14 @@ let dispatch_notification ~io ~ofn ~state ~method_ ~params : unit = (* Generic handler *) | msg -> LIO.trace "no_handler" msg -let dispatch_state_notification ~io ~ofn ~state ~method_ ~params : State.t = +let dispatch_state_notification ~io ~ofn ~token ~state ~method_ ~params : + State.t = match method_ with (* Workspace *) | "workspace/didChangeWorkspaceFolders" -> - do_changeWorkspaceFolders ~ofn ~state params + do_changeWorkspaceFolders ~ofn ~token ~state params | _ -> - dispatch_notification ~io ~ofn ~state ~method_ ~params; + dispatch_notification ~io ~ofn ~token ~state ~method_ ~params; state let dispatch_request ~method_ ~params : Rq.Action.t = @@ -493,15 +505,15 @@ let dispatch_request ~method_ ~params : Rq.Action.t = LIO.trace "no_handler" msg; Rq.Action.error (-32601, "method not found") -let dispatch_request ~ofn ~id ~method_ ~params = - dispatch_request ~method_ ~params |> Rq.serve ~ofn ~id +let dispatch_request ~ofn ~token ~id ~method_ ~params = + dispatch_request ~method_ ~params |> Rq.serve ~ofn ~token ~id -let dispatch_message ~io ~ofn ~state (com : LSP.Message.t) : State.t = +let dispatch_message ~io ~ofn ~token ~state (com : LSP.Message.t) : State.t = match com with | Notification { method_; params } -> - dispatch_state_notification ~io ~ofn ~state ~method_ ~params + dispatch_state_notification ~io ~ofn ~token ~state ~method_ ~params | Request { id; method_; params } -> - dispatch_request ~ofn ~id ~method_ ~params; + dispatch_request ~ofn ~token ~id ~method_ ~params; state (* Queue handling *) @@ -513,15 +525,29 @@ let dispatch_message ~io ~ofn ~state (com : LSP.Message.t) : State.t = Note that we should add a method to detect stale requests; maybe cancel them when a new edit comes. *) +let current_token = ref None + +let token_factory () = + let token = Coq.Limits.Token.create () in + current_token := Some token; + token + +let set_current_token () = + match !current_token with + | None -> () + | Some tok -> + current_token := None; + Coq.Limits.Token.set tok + type 'a cont = | Cont of 'a | Yield of 'a -let check_or_yield ~io ~ofn ~state = - match Fleche.Theory.Check.maybe_check ~io with +let check_or_yield ~io ~ofn ~token ~state = + match Fleche.Theory.Check.maybe_check ~io ~token with | None -> Yield state | Some (ready, doc) -> - let () = Rq.serve_postponed ~ofn ~doc ready in + let () = Rq.serve_postponed ~ofn ~token ~doc ready in Cont state module LspQueue : sig @@ -558,13 +584,13 @@ let dispatch_or_resume_check ~io ~ofn ~state = | None -> (* This is where we make progress on document checking; kind of IDLE workqueue. *) - Control.interrupt := false; - check_or_yield ~io ~ofn ~state + let token = token_factory () in + check_or_yield ~io ~ofn ~token ~state | Some com -> LIO.trace "process_queue" ("Serving Request: " ^ LSP.Message.method_ com); (* We let Coq work normally now *) - Control.interrupt := false; - Cont (dispatch_message ~io ~ofn ~state com) + let token = token_factory () in + Cont (dispatch_message ~io ~ofn ~token ~state com) (* Wrapper for the top-level call *) let dispatch_or_resume_check ~io ~ofn ~state = @@ -597,4 +623,4 @@ let enqueue_message (com : LSP.Message.t) = (* TODO: this is the place to cancel pending requests that are invalid, and in general, to perform queue optimizations *) LspQueue.push_and_optimize com; - Control.interrupt := true + set_current_token () diff --git a/controller/request.ml b/controller/request.ml index 713c7b13..f2acdb11 100644 --- a/controller/request.ml +++ b/controller/request.ml @@ -40,8 +40,10 @@ module R = struct | Completed (Ok r) -> r end -type document = doc:Fleche.Doc.t -> R.t -type position = doc:Fleche.Doc.t -> point:int * int -> R.t +type document = token:Coq.Limits.Token.t -> doc:Fleche.Doc.t -> R.t + +type position = + token:Coq.Limits.Token.t -> doc:Fleche.Doc.t -> point:int * int -> R.t (** Requests that require data access *) module Data = struct @@ -76,11 +78,11 @@ module Data = struct | PosRequest { uri; point; version; postpone; handler = _ } -> (uri, postpone, Fleche.Theory.Request.(PosInDoc { point; version })) - let serve ~doc pr = + let serve ~token ~doc pr = match pr with - | DocRequest { uri = _; postpone = _; handler } -> handler ~doc + | DocRequest { uri = _; postpone = _; handler } -> handler ~token ~doc | PosRequest { uri = _; point; version = _; postpone = _; handler } -> - handler ~point ~doc + handler ~token ~point ~doc end -let empty ~doc:_ ~point:_ = Ok (`List []) +let empty ~token:_ ~doc:_ ~point:_ = Ok (`List []) diff --git a/controller/request.mli b/controller/request.mli index 6d0328e1..da4f5b41 100644 --- a/controller/request.mli +++ b/controller/request.mli @@ -25,8 +25,12 @@ module R : sig name:string -> f:('a -> (t, Loc.t) Coq.Protect.E.t) -> 'a -> t end -type document = doc:Fleche.Doc.t -> R.t -type position = doc:Fleche.Doc.t -> point:int * int -> R.t +(* We could classify the requests that don't need to call-back Coq (and thus + don't need the interruption token; but it is not worth it. *) +type document = token:Coq.Limits.Token.t -> doc:Fleche.Doc.t -> R.t + +type position = + token:Coq.Limits.Token.t -> doc:Fleche.Doc.t -> point:int * int -> R.t (** Requests that require data access *) module Data : sig @@ -47,7 +51,7 @@ module Data : sig (* Debug printing *) val data : Format.formatter -> t -> unit val dm_request : t -> Lang.LUri.File.t * bool * Fleche.Theory.Request.request - val serve : doc:Fleche.Doc.t -> t -> R.t + val serve : token:Coq.Limits.Token.t -> doc:Fleche.Doc.t -> t -> R.t end (** Returns an empty list of results for any position / document *) diff --git a/controller/rq_completion.ml b/controller/rq_completion.ml index f546809b..dd7e1243 100644 --- a/controller/rq_completion.ml +++ b/controller/rq_completion.ml @@ -91,7 +91,7 @@ let get_char_at_point ~(doc : Fleche.Doc.t) ~point = None (* point is a utf char! *) -let completion ~doc ~point = +let completion ~token:_ ~doc ~point = (* Instead of get_char_at_point we should have a CompletionContext.t, to be addressed in further completion PRs *) (match get_char_at_point ~doc ~point with diff --git a/controller/rq_definition.ml b/controller/rq_definition.ml index 44dffcf0..8b29e668 100644 --- a/controller/rq_definition.ml +++ b/controller/rq_definition.ml @@ -5,7 +5,7 @@ (* Written by: Emilio J. Gallego Arias *) (************************************************************************) -let request ~(doc : Fleche.Doc.t) ~point = +let request ~token:_ ~(doc : Fleche.Doc.t) ~point = let { Fleche.Doc.contents; _ } = doc in Option.cata (fun id_at_point -> diff --git a/controller/rq_document.ml b/controller/rq_document.ml index d202f275..7e94b817 100644 --- a/controller/rq_document.ml +++ b/controller/rq_document.ml @@ -15,7 +15,7 @@ let to_completed = function | Stopped range -> { status = `Stopped; range } | Failed range | FailedPermanent range -> { status = `Failed; range } -let request ~doc = +let request ~token:_ ~doc = let { Fleche.Doc.nodes; completed; _ } = doc in let spans = List.map to_span nodes in let completed = to_completed completed in diff --git a/controller/rq_goals.ml b/controller/rq_goals.ml index 98e203c0..9c6430c8 100644 --- a/controller/rq_goals.ml +++ b/controller/rq_goals.ml @@ -32,26 +32,27 @@ let pp ~pp_format pp = | Pp -> Lsp.JCoq.Pp.to_yojson pp | Str -> `String (Pp.string_of_ppcmds pp) -let parse ~loc tac st = +let parse ~token ~loc tac st = let str = Gramlib.Stream.of_string tac in let str = Coq.Parsing.Parsable.make ?loc str in - Coq.Parsing.parse ~st str + Coq.Parsing.parse ~token ~st str -let parse_and_execute_in ~loc tac st = +let parse_and_execute_in ~token ~loc tac st = let open Coq.Protect.E.O in - let* ast = parse ~loc tac st in + let* ast = parse ~token ~loc tac st in match ast with - | Some ast -> (Fleche.Memo.Interp.eval (st, ast)).res + | Some ast -> (Fleche.Memo.Interp.eval ~token (st, ast)).res (* On EOF we return the previous state, the command was the empty string or a comment *) | None -> Coq.Protect.E.ok st -let run_pretac ~loc ~st pretac = +let run_pretac ~token ~loc ~st pretac = match pretac with | None -> Coq.Protect.E.ok st - | Some tac -> Coq.State.in_stateM ~st ~f:(parse_and_execute_in ~loc tac) st + | Some tac -> + Coq.State.in_stateM ~token ~st ~f:(parse_and_execute_in ~token ~loc tac) st -let get_goal_info ~doc ~point ~mode ~pretac () = +let get_goal_info ~token ~doc ~point ~mode ~pretac () = let open Fleche in let node = Info.LC.node ~doc ~point mode in match node with @@ -61,12 +62,12 @@ let get_goal_info ~doc ~point ~mode ~pretac () = let st = Doc.Node.state node in (* XXX: Get the location from node *) let loc = None in - let* st = run_pretac ~loc ~st pretac in - let+ goals = Info.Goals.goals ~st in + let* st = run_pretac ~token ~loc ~st pretac in + let+ goals = Info.Goals.goals ~token ~st in let program = Info.Goals.program ~st in (goals, Some program) -let goals ~pp_format ~mode ~pretac () ~doc ~point = +let goals ~pp_format ~mode ~pretac () ~token ~doc ~point = let open Fleche in let uri, version = (doc.Doc.uri, doc.version) in let textDocument = Lsp.Doc.VersionedTextDocumentIdentifier.{ uri; version } in @@ -74,7 +75,7 @@ let goals ~pp_format ~mode ~pretac () ~doc ~point = Lang.Point.{ line = fst point; character = snd point; offset = -1 } in let open Coq.Protect.E.O in - let+ goals, program = get_goal_info ~doc ~point ~mode ~pretac () in + let+ goals, program = get_goal_info ~token ~doc ~point ~mode ~pretac () in let node = Info.LC.node ~doc ~point Exact in let messages = mk_messages node in let error = Option.bind node mk_error in @@ -83,6 +84,6 @@ let goals ~pp_format ~mode ~pretac () ~doc ~point = to_yojson pp { textDocument; position; goals; program; messages; error }) |> Result.ok -let goals ~pp_format ~mode ~pretac () ~doc ~point = - let f () = goals ~pp_format ~mode ~pretac () ~doc ~point in +let goals ~pp_format ~mode ~pretac () ~token ~doc ~point = + let f () = goals ~pp_format ~mode ~pretac () ~token ~doc ~point in Request.R.of_execution ~name:"goals" ~f () diff --git a/controller/rq_hover.ml b/controller/rq_hover.ml index 701460d4..4470db62 100644 --- a/controller/rq_hover.ml +++ b/controller/rq_hover.ml @@ -106,9 +106,9 @@ let info_of_id ~st id = in info_of_id env sigma id -let info_of_id_at_point ~node id = +let info_of_id_at_point ~token ~node id = let st = node.Fleche.Doc.Node.state in - Coq.State.in_state ~st ~f:(info_of_id ~st) id + Coq.State.in_state ~token ~st ~f:(info_of_id ~st) id let pp_typ id = function | Def typ -> @@ -120,9 +120,9 @@ let pp_typ id = function let to_list x = Option.cata (fun x -> [ x ]) [] x -let info_type ~contents ~point ~node : string option = +let info_type ~token ~contents ~point ~node : string option = Option.bind (Rq_common.get_id_at_point ~contents ~point) (fun id -> - match info_of_id_at_point ~node id with + match info_of_id_at_point ~token ~node id with | Coq.Protect.{ E.r = R.Completed (Ok (Some info)); feedback = _ } -> Some (pp_typ id info) | _ -> None) @@ -155,7 +155,7 @@ let info_notation ~point (ast : Fleche.Doc.Node.Ast.t) = Some (ntn_key_info key) | _ -> None -let info_notation ~contents:_ ~point ~node : string option = +let info_notation ~token:_ ~contents:_ ~point ~node : string option = Option.bind node.Fleche.Doc.Node.ast (info_notation ~point) open Fleche @@ -164,10 +164,18 @@ open Fleche module Handler = struct (** Returns [Some markdown] if there is some hover to match *) type 'node h_node = - contents:Contents.t -> point:int * int -> node:'node -> string option + token:Coq.Limits.Token.t + -> contents:Contents.t + -> point:int * int + -> node:'node + -> string option type h_doc = - doc:Doc.t -> point:int * int -> node:Doc.Node.t option -> string option + token:Coq.Limits.Token.t + -> doc:Doc.t + -> point:int * int + -> node:Doc.Node.t option + -> string option type t = | MaybeNode : Doc.Node.t option h_node -> t @@ -180,22 +188,23 @@ module type HoverProvider = sig end module Loc_info : HoverProvider = struct - let h ~contents:_ ~point:_ ~node = + let h ~token:_ ~contents:_ ~point:_ ~node = match node with | None -> "no node here" | Some node -> let range = Doc.Node.range node in Format.asprintf "%a" Lang.Range.pp range - let h ~contents ~point ~node = - if !Config.v.show_loc_info_on_hover then Some (h ~contents ~point ~node) + let h ~token ~contents ~point ~node = + if !Config.v.show_loc_info_on_hover then + Some (h ~token ~contents ~point ~node) else None let h = Handler.MaybeNode h end module Stats : HoverProvider = struct - let h ~contents:_ ~point:_ ~node = + let h ~token:_ ~contents:_ ~point:_ ~node = if !Config.v.show_stats_on_hover then Some Doc.Node.(Info.print (info node)) else None @@ -214,25 +223,25 @@ module Register = struct let handlers : Handler.t list ref = ref [] let add fn = handlers := fn :: !handlers - let handle ~(doc : Doc.t) ~point ~node = + let handle ~token ~(doc : Doc.t) ~point ~node = let contents = doc.contents in function - | Handler.MaybeNode h -> h ~contents ~point ~node + | Handler.MaybeNode h -> h ~token ~contents ~point ~node | Handler.WithNode h -> - Option.bind node (fun node -> h ~contents ~point ~node) - | Handler.WithDoc h -> h ~doc ~point ~node + Option.bind node (fun node -> h ~token ~contents ~point ~node) + | Handler.WithDoc h -> h ~token ~doc ~point ~node - let fire ~doc ~point ~node = - List.filter_map (handle ~doc ~point ~node) !handlers + let fire ~token ~doc ~point ~node = + List.filter_map (handle ~token ~doc ~point ~node) !handlers end (* Register in-file hover plugins *) let () = List.iter Register.add [ Loc_info.h; Stats.h; Type.h; Notation.h ] -let hover ~doc ~point = +let hover ~token ~doc ~point = let node = Info.LC.node ~doc ~point Exact in let range = Option.map Doc.Node.range node in - let hovers = Register.fire ~doc ~point ~node in + let hovers = Register.fire ~token ~doc ~point ~node in match hovers with | [] -> `Null | hovers -> @@ -240,4 +249,4 @@ let hover ~doc ~point = let contents = { HoverContents.kind = "markdown"; value } in HoverInfo.(to_yojson { contents; range }) -let hover ~doc ~point = hover ~doc ~point |> Result.ok +let hover ~token ~doc ~point = hover ~token ~doc ~point |> Result.ok diff --git a/controller/rq_hover.mli b/controller/rq_hover.mli index 4dab92af..d9786731 100644 --- a/controller/rq_hover.mli +++ b/controller/rq_hover.mli @@ -12,10 +12,18 @@ open Fleche module Handler : sig (** Returns [Some markdown] if there is some hover to match *) type 'node h_node = - contents:Contents.t -> point:int * int -> node:'node -> string option + token:Coq.Limits.Token.t + -> contents:Contents.t + -> point:int * int + -> node:'node + -> string option type h_doc = - doc:Doc.t -> point:int * int -> node:Doc.Node.t option -> string option + token:Coq.Limits.Token.t + -> doc:Doc.t + -> point:int * int + -> node:Doc.Node.t option + -> string option (** Many use cases could be grouped into a hook that would pass an [Identifier_context.] object, containing the object, its location, diff --git a/controller/rq_lens.ml b/controller/rq_lens.ml index 78c81da4..b7c871f1 100644 --- a/controller/rq_lens.ml +++ b/controller/rq_lens.ml @@ -18,4 +18,4 @@ let mk_goals_lens (node : Fleche.Doc.Node.t) = (* Example lens to show goals, seems that args are not working *) let _goals_lens ~(doc : Fleche.Doc.t) = `List (List.map mk_goals_lens doc.nodes) -let request ~doc:_ = `Null |> Result.ok +let request ~token:_ ~doc:_ = `Null |> Result.ok diff --git a/controller/rq_save.ml b/controller/rq_save.ml index abb66b57..d0971035 100644 --- a/controller/rq_save.ml +++ b/controller/rq_save.ml @@ -1,10 +1,27 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* Ok `Null diff --git a/controller/rq_symbols.ml b/controller/rq_symbols.ml index 813c8faa..7852e0a4 100644 --- a/controller/rq_symbols.ml +++ b/controller/rq_symbols.ml @@ -26,7 +26,7 @@ let rec mk_syminfo info = let mk_syminfo info = mk_syminfo info |> Lsp.Core.DocumentSymbol.to_yojson let definition_info { Fleche.Doc.Node.Ast.ast_info; _ } = ast_info -let symbols ~(doc : Fleche.Doc.t) = +let symbols ~token:_ ~(doc : Fleche.Doc.t) = let definfo = Fleche.Doc.asts doc |> List.filter_map definition_info |> List.concat in diff --git a/coq/init.ml b/coq/init.ml index a6ea25ad..b58a1f4f 100644 --- a/coq/init.ml +++ b/coq/init.ml @@ -97,5 +97,5 @@ let doc_init ~root_state ~workspace ~uri () = (* We return the state at this point! *) Vernacstate.freeze_full_state () |> State.of_coq -let doc_init ~root_state ~workspace ~uri = - Protect.eval ~f:(doc_init ~root_state ~workspace ~uri) () +let doc_init ~token ~root_state ~workspace ~uri = + Protect.eval ~token ~f:(doc_init ~root_state ~workspace ~uri) () diff --git a/coq/init.mli b/coq/init.mli index 12dded5b..e547e3c6 100644 --- a/coq/init.mli +++ b/coq/init.mli @@ -28,7 +28,8 @@ type coq_opts = val coq_init : coq_opts -> State.t val doc_init : - root_state:State.t + token:Limits.Token.t + -> root_state:State.t -> workspace:Workspace.t -> uri:Lang.LUri.File.t -> (State.t, Loc.t) Protect.E.t diff --git a/coq/interp.ml b/coq/interp.ml index 8670bf14..b259559f 100644 --- a/coq/interp.ml +++ b/coq/interp.ml @@ -20,7 +20,7 @@ let coq_interp ~st cmd = let cmd = Ast.to_coq cmd in Vernacinterp.interp ~st cmd |> State.of_coq -let interp ~st cmd = Protect.eval cmd ~f:(coq_interp ~st) +let interp ~token ~st cmd = Protect.eval ~token cmd ~f:(coq_interp ~st) module Require = struct (* We could improve this Coq upstream by making the API a bit more @@ -40,5 +40,6 @@ module Require = struct let () = Utils.with_control ~fn ~control ~st in Vernacstate.freeze_full_state () |> State.of_coq - let interp ~st files cmd = Protect.eval ~f:(interp ~st files) cmd + let interp ~token ~st files cmd = + Protect.eval ~token ~f:(interp ~st files) cmd end diff --git a/coq/interp.mli b/coq/interp.mli index 901a7332..9b7e5118 100644 --- a/coq/interp.mli +++ b/coq/interp.mli @@ -18,7 +18,8 @@ (** Intepretation of "pure" Coq commands, that is to say, commands that are assumed not to interact with the file-system, etc... Note these commands will be memoized. *) -val interp : st:State.t -> Ast.t -> (State.t, Loc.t) Protect.E.t +val interp : + token:Limits.Token.t -> st:State.t -> Ast.t -> (State.t, Loc.t) Protect.E.t (** Interpretation of "require". We wrap this function for two reasons: @@ -26,5 +27,9 @@ val interp : st:State.t -> Ast.t -> (State.t, Loc.t) Protect.E.t - to workaround the lack of a pure interface in Coq *) module Require : sig val interp : - st:State.t -> Files.t -> Ast.Require.t -> (State.t, Loc.t) Protect.E.t + token:Limits.Token.t + -> st:State.t + -> Files.t + -> Ast.Require.t + -> (State.t, Loc.t) Protect.E.t end diff --git a/coq/limits.ml b/coq/limits.ml index 7bfbf0be..d4ce4613 100644 --- a/coq/limits.ml +++ b/coq/limits.ml @@ -46,3 +46,4 @@ module Coq : Intf = struct end module Mp = Limits_mp_impl +include Coq diff --git a/coq/limits.mli b/coq/limits.mli index 1fea90e1..c342ccd7 100644 --- a/coq/limits.mli +++ b/coq/limits.mli @@ -16,3 +16,4 @@ end module Coq : Intf module Mp : Intf +include Intf diff --git a/coq/parsing.ml b/coq/parsing.ml index 933b2384..58581066 100644 --- a/coq/parsing.ml +++ b/coq/parsing.ml @@ -9,7 +9,7 @@ let parse ~st ps = Vernacstate.Parser.parse st Pvernac.(main_entry mode) ps |> Option.map Ast.of_coq -let parse ~st ps = Protect.eval ~f:(parse ~st) ps +let parse ~token ~st ps = Protect.eval ~token ~f:(parse ~st) ps (* Read the input stream until a dot or a "end of proof" token is encountered *) let parse_to_terminator : unit Pcoq.Entry.t = diff --git a/coq/parsing.mli b/coq/parsing.mli index 5dca7af7..2973646d 100644 --- a/coq/parsing.mli +++ b/coq/parsing.mli @@ -5,5 +5,10 @@ module Parsable : sig val loc : t -> Loc.t end -val parse : st:State.t -> Parsable.t -> (Ast.t option, Loc.t) Protect.E.t +val parse : + token:Limits.Token.t + -> st:State.t + -> Parsable.t + -> (Ast.t option, Loc.t) Protect.E.t + val discard_to_dot : Parsable.t -> unit diff --git a/coq/print.ml b/coq/print.ml index ac4bf3a9..01f09273 100644 --- a/coq/print.ml +++ b/coq/print.ml @@ -1,6 +1,6 @@ let pr_letype_env ~goal_concl_style env sigma x = Printer.pr_letype_env ~goal_concl_style env sigma x -let pr_letype_env ~goal_concl_style env sigma x = +let pr_letype_env ~token ~goal_concl_style env sigma x = let f = pr_letype_env ~goal_concl_style env sigma in - Protect.eval ~f x + Protect.eval ~token ~f x diff --git a/coq/print.mli b/coq/print.mli index 31497094..e6a4dda4 100644 --- a/coq/print.mli +++ b/coq/print.mli @@ -1,5 +1,6 @@ val pr_letype_env : - goal_concl_style:bool + token:Limits.Token.t + -> goal_concl_style:bool -> Environ.env -> Evd.evar_map -> EConstr.t diff --git a/coq/protect.ml b/coq/protect.ml index deb043dd..3ef77ea6 100644 --- a/coq/protect.ml +++ b/coq/protect.ml @@ -33,15 +33,13 @@ module R = struct end (* Eval and reify exceptions *) -let eval_exn ~f x = - try - let res = f x in - R.Completed (Ok res) - with - | Sys.Break -> +let eval_exn ~token ~f x = + match Limits.limit ~token ~f x with + | Ok res -> R.Completed (Ok res) + | Error _ -> Vernacstate.Interp.invalidate_cache (); R.Interrupted - | exn -> + | exception exn -> let e, info = Exninfo.capture exn in let loc = Loc.(get_loc info) in let msg = CErrors.iprint (e, info) in @@ -63,8 +61,8 @@ module E = struct ; feedback : 'l Message.t list } - let eval ~f x = - let r = eval_exn ~f x in + let eval ~token ~f x = + let r = eval_exn ~token ~f x in let feedback = List.rev !fb_queue in let () = fb_queue := [] in { r; feedback } @@ -92,4 +90,4 @@ module E = struct end (* Eval with reified exceptions and feedback *) -let eval ~f x = E.eval ~f x +let eval ~token ~f x = E.eval ~token ~f x diff --git a/coq/protect.mli b/coq/protect.mli index 1db67f01..ee262dfe 100644 --- a/coq/protect.mli +++ b/coq/protect.mli @@ -51,5 +51,5 @@ val fb_queue : Loc.t Message.t list ref (** Eval a function and reify the exceptions. Note [f] _must_ be pure, as in case of anomaly [f] may be re-executed with debug options. Beware, not - thread-safe! *) -val eval : f:('i -> 'o) -> 'i -> ('o, Loc.t) E.t + thread-safe! [token] Does allow to interrupt the evaluation. *) +val eval : token:Limits.Token.t -> f:('i -> 'o) -> 'i -> ('o, Loc.t) E.t diff --git a/coq/save.ml b/coq/save.ml index 4e4e7ecc..90a329fc 100644 --- a/coq/save.ml +++ b/coq/save.ml @@ -1,3 +1,20 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* st:State.t -> ldir:Names.DirPath.t -> in_file:string -> (unit, Loc.t) Protect.E.t diff --git a/coq/state.ml b/coq/state.ml index 4f5bc71f..507d7537 100644 --- a/coq/state.ml +++ b/coq/state.ml @@ -94,16 +94,16 @@ let drop_proofs ~st = in { st with interp } -let in_state ~st ~f a = +let in_state ~token ~st ~f a = let f a = Vernacstate.unfreeze_full_state st; f a in - Protect.eval ~f a + Protect.eval ~token ~f a -let in_stateM ~st ~f a = +let in_stateM ~token ~st ~f a = let open Protect.E.O in - let* () = Protect.eval ~f:Vernacstate.unfreeze_full_state st in + let* () = Protect.eval ~token ~f:Vernacstate.unfreeze_full_state st in f a let admit ~st () = @@ -118,7 +118,7 @@ let admit ~st () = let st = Vernacstate.freeze_full_state () in { st with interp = { st.interp with lemmas; program } } -let admit ~st = Protect.eval ~f:(admit ~st) () +let admit ~token ~st = Protect.eval ~token ~f:(admit ~st) () let admit_goal ~st () = let () = Vernacstate.unfreeze_full_state st in @@ -129,4 +129,4 @@ let admit_goal ~st () = let lemmas = Some (Vernacstate.LemmaStack.map_top ~f lemmas) in { st with interp = { st.interp with lemmas } } -let admit_goal ~st = Protect.eval ~f:(admit_goal ~st) () +let admit_goal ~token ~st = Protect.eval ~token ~f:(admit_goal ~st) () diff --git a/coq/state.mli b/coq/state.mli index 00c3da52..0a32c941 100644 --- a/coq/state.mli +++ b/coq/state.mli @@ -18,20 +18,25 @@ val program : st:t -> Declare.OblState.View.t Names.Id.Map.t (** 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, Loc.t) Protect.E.t +val in_state : + token:Limits.Token.t -> st:t -> f:('a -> 'b) -> 'a -> ('b, Loc.t) Protect.E.t (** Execute a monadic command in state [st]. *) val in_stateM : - st:t -> f:('a -> ('b, Loc.t) Protect.E.t) -> 'a -> ('b, Loc.t) Protect.E.t + token:Limits.Token.t + -> st:t + -> f:('a -> ('b, Loc.t) Protect.E.t) + -> 'a + -> ('b, Loc.t) Protect.E.t (** Drop the proofs from the state *) val drop_proofs : st:t -> t (** Fully admit an ongoing proof *) -val admit : st:t -> (t, Loc.t) Protect.E.t +val admit : token:Limits.Token.t -> st:t -> (t, Loc.t) Protect.E.t (** Admit the current sub-goal *) -val admit_goal : st:t -> (t, Loc.t) Protect.E.t +val admit_goal : token:Limits.Token.t -> st:t -> (t, Loc.t) Protect.E.t (** Extra / interanl *) val marshal_in : in_channel -> t diff --git a/coq/workspace.ml b/coq/workspace.ml index 947ea349..6ab65b22 100644 --- a/coq/workspace.ml +++ b/coq/workspace.ml @@ -10,8 +10,8 @@ (************************************************************************) (* Coq Language Server Protocol *) -(* Copyright 2019 MINES ParisTech -- Dual License LGPL 2.1 / GPL3+ *) -(* Copyright 2019-2022 Inria -- Dual License LGPL 2.1 / GPL3+ *) +(* Copyright 2016-2019 MINES ParisTech -- Dual License LGPL 2.1 / GPL3+ *) +(* Copyright 2019-2024 Inria -- Dual License LGPL 2.1 / GPL3+ *) (* Written by: Emilio J. Gallego Arias *) (************************************************************************) @@ -351,9 +351,9 @@ let guess ~debug ~cmdline ~dir () = workspace_from_coqproject ~cmdline ~debug cp_file else workspace_from_cmdline ~debug ~cmdline -let guess ~debug ~cmdline ~dir = +let guess ~token ~debug ~cmdline ~dir = let { Protect.E.r; feedback } = - Protect.eval ~f:(guess ~debug ~cmdline ~dir) () + Protect.eval ~token ~f:(guess ~debug ~cmdline ~dir) () in ignore feedback; match r with diff --git a/coq/workspace.mli b/coq/workspace.mli index b5a4f2cd..b8720fbc 100644 --- a/coq/workspace.mli +++ b/coq/workspace.mli @@ -10,8 +10,8 @@ (************************************************************************) (* Coq Language Server Protocol *) -(* Copyright 2019 MINES ParisTech -- Dual License LGPL 2.1 / GPL3+ *) -(* Copyright 2019-2022 Inria -- Dual License LGPL 2.1 / GPL3+ *) +(* Copyright 2016-2019 MINES ParisTech -- Dual License LGPL 2.1 / GPL3+ *) +(* Copyright 2019-2024 Inria -- Dual License LGPL 2.1 / GPL3+ *) (* Written by: Emilio J. Gallego Arias *) (************************************************************************) @@ -70,7 +70,11 @@ module CmdLine : sig end val guess : - debug:bool -> cmdline:CmdLine.t -> dir:string -> (t, string) Result.t + token:Limits.Token.t + -> debug:bool + -> cmdline:CmdLine.t + -> dir:string + -> (t, string) Result.t (* Fallback workspace *) val default : debug:bool -> cmdline:CmdLine.t -> t diff --git a/fleche/doc.ml b/fleche/doc.ml index 4385d6ac..2cd798d2 100644 --- a/fleche/doc.ml +++ b/fleche/doc.ml @@ -306,7 +306,8 @@ let process_init_feedback ~lines ~stats state feedback = else [] (* Memoized call to [Coq.Init.doc_init] *) -let mk_doc ~env ~uri = Memo.Init.eval (env.Env.init, env.workspace, uri) +let mk_doc ~token ~env ~uri = + Memo.Init.eval ~token (env.Env.init, env.workspace, uri) (* Create empty doc, in state [~completed] *) let empty_doc ~uri ~contents ~version ~env ~root ~nodes ~completed = @@ -334,9 +335,9 @@ let conv_error_doc ~raw ~uri ~version ~env ~root ~completed err = let nodes = process_init_feedback ~lines ~stats root [ err ] in empty_doc ~uri ~version ~env ~root ~nodes ~completed ~contents -let create ~env ~uri ~version ~contents = +let create ~token ~env ~uri ~version ~contents = let () = Stats.reset () in - let root = mk_doc ~env ~uri in + let root = mk_doc ~token ~env ~uri in Coq.Protect.E.map root ~f:(fun root -> let nodes = [] in let completed range = Completion.Stopped range in @@ -360,9 +361,11 @@ let handle_failed_permanent ~env ~uri ~version ~contents = (** Try to create a doc, if Coq execution fails, create a failed doc with the corresponding errors; for now we refine the contents step as to better setup the initial document. *) -let handle_doc_creation_exec ~env ~uri ~version ~contents = +let handle_doc_creation_exec ~token ~env ~uri ~version ~contents = let completed range = Completion.Failed range in - let { Coq.Protect.E.r; feedback } = create ~env ~uri ~version ~contents in + let { Coq.Protect.E.r; feedback } = + create ~token ~env ~uri ~version ~contents + in let doc, extra_feedback = match r with | Interrupted -> @@ -394,15 +397,15 @@ let handle_contents_creation ~env ~uri ~version ~raw ~completed f = conv_error_doc ~raw ~uri ~version ~env ~root ~completed err | Contents.R.Ok contents -> f ~env ~uri ~version ~contents -let create ~env ~uri ~version ~raw = +let create ~token ~env ~uri ~version ~raw = let completed range = Completion.Failed range in handle_contents_creation ~env ~uri ~version ~raw ~completed - handle_doc_creation_exec + (handle_doc_creation_exec ~token) (* Used in bump, we should consolidate with create *) -let recreate ~doc ~version ~contents = +let recreate ~token ~doc ~version ~contents = let env, uri = (doc.env, doc.uri) in - handle_doc_creation_exec ~env ~uri ~version ~contents + handle_doc_creation_exec ~token ~env ~uri ~version ~contents let create_failed_permanent ~env ~uri ~version ~raw = let completed range = Completion.FailedPermanent range in @@ -459,7 +462,7 @@ let bump_version ~init_range ~version ~contents doc = ; env } -let bump_version ~version ~(contents : Contents.t) doc = +let bump_version ~token ~version ~(contents : Contents.t) doc = let init_loc = init_loc ~uri:doc.uri in let init_range = Coq.Utils.to_range ~lines:contents.lines init_loc in match doc.completed with @@ -468,16 +471,16 @@ let bump_version ~version ~(contents : Contents.t) doc = | FailedPermanent _ -> doc | Failed _ -> (* re-create the document on failed, as the env may have changed *) - recreate ~doc ~version ~contents + recreate ~token ~doc ~version ~contents | Stopped _ | Yes _ -> bump_version ~init_range ~version ~contents doc -let bump_version ~version ~raw doc = +let bump_version ~token ~version ~raw doc = let uri = doc.uri in match Contents.make ~uri ~raw with | Contents.R.Error e -> let completed range = Completion.Failed range in conv_error_doc ~raw ~uri ~version ~env:doc.env ~root:doc.root ~completed e - | Contents.R.Ok contents -> bump_version ~version ~contents doc + | Contents.R.Ok contents -> bump_version ~token ~version ~contents doc let add_node ~node doc = let diags_dirty = if node.Node.diags <> [] then true else doc.diags_dirty in @@ -515,8 +518,8 @@ let report_progress ~io ~doc (last_tok : Lang.Range.t) = (* XXX: Save on close? *) (* let close_doc _modname = () *) -let parse_stm ~st ps = - let f ps = Coq.Parsing.parse ~st ps in +let parse_stm ~token ~st ps = + let f ps = Coq.Parsing.parse ~token ~st ps in Stats.record ~kind:Stats.Kind.Parsing ~f ps module Recovery_context = struct @@ -538,7 +541,11 @@ end (* This is not in its own module because we don't want to move the definition of [Node.t] out (yet) *) module Recovery : sig - val handle : context:Recovery_context.t -> st:Coq.State.t -> Coq.State.t + val handle : + token:Coq.Limits.Token.t + -> context:Recovery_context.t + -> st:Coq.State.t + -> Coq.State.t end = struct (* Returns node before / after, will be replaced by the right structure, we can also do dynamic by looking at proof state *) @@ -553,12 +560,12 @@ end = struct Some (n, Util.hd_opt ns) | _ -> find_proof_start ns) - let recovery_for_failed_qed ~default nodes = + let recovery_for_failed_qed ~token ~default nodes = match find_proof_start nodes with | None -> Coq.Protect.E.ok (default, None) | Some ({ range; state; _ }, prev) -> ( if !Config.v.admit_on_bad_qed then - Memo.Admit.eval state + Memo.Admit.eval ~token state |> Coq.Protect.E.map ~f:(fun state -> (state, Some range)) else match prev with @@ -585,40 +592,41 @@ end = struct Some (String.init size (fun idx -> line.[idx + coff])) else None - let lex_recovery_heuristic last_tok contents nodes st = + let lex_recovery_heuristic ~token last_tok contents nodes st = let et = extract_token last_tok contents in match (et 3, et 7, et 8) with | Some ("Qed" as txt), _, _ | _, Some ("Defined" as txt), _ | _, _, Some ("Admitted" as txt) -> Io.Log.trace "lex recovery" (txt ^ " detected"); - recovery_for_failed_qed ~default:st nodes |> Coq.Protect.E.map ~f:fst + recovery_for_failed_qed ~token ~default:st nodes + |> Coq.Protect.E.map ~f:fst | _, _, _ -> Coq.Protect.E.ok st (* AST-based heuristics: Qed, bullets, ... *) - let ast_recovery_heuristic last_tok contents nodes st v = + let ast_recovery_heuristic ~token last_tok contents nodes st v = match (Coq.Ast.to_coq v).CAst.v.Vernacexpr.expr with (* Drop the top proof state if we reach a faulty Qed. *) | Vernacexpr.VernacSynPure (VernacEndProof _) -> Io.Log.trace "recovery" "qed"; - recovery_for_failed_qed ~default:st nodes |> log_qed_recovery v + recovery_for_failed_qed ~token ~default:st nodes |> log_qed_recovery v (* If a new focus (or unfocusing) fails, admit the proof and try again *) | Vernacexpr.VernacSynPure (VernacBullet _ | Vernacexpr.VernacEndSubproof) -> Io.Log.trace "recovery" "bullet"; - Coq.State.admit_goal ~st - |> Coq.Protect.E.bind ~f:(fun st -> Coq.Interp.interp ~st v) + Coq.State.admit_goal ~token ~st + |> Coq.Protect.E.bind ~f:(fun st -> Coq.Interp.interp ~token ~st v) | _ -> (* Fallback to qed special lex case *) - lex_recovery_heuristic last_tok contents nodes st + lex_recovery_heuristic ~token last_tok contents nodes st (* XXX: This should be refined. *) - let handle ~context ~st = + let handle ~token ~context ~st = let { Recovery_context.contents; last_tok; nodes; ast } = context in let { Coq.Protect.E.r; feedback = _ } = match ast with - | None -> lex_recovery_heuristic last_tok contents nodes st - | Some ast -> ast_recovery_heuristic last_tok contents nodes st ast + | None -> lex_recovery_heuristic ~token last_tok contents nodes st + | Some ast -> ast_recovery_heuristic ~token last_tok contents nodes st ast in match r with | Interrupted -> st @@ -626,11 +634,11 @@ end = struct | Completed (Error _) -> st end -let interp_and_info ~parsing_time ~st ast = +let interp_and_info ~token ~parsing_time ~st ast = let { Gc.major_words = mw_prev; _ } = Gc.quick_stat () in (* memo memory stats are disabled: slow and misleading *) let { Memo.Stats.res; cache_hit; memory = _; time } = - Memo.Interp.eval (st, ast) + Memo.Interp.eval ~token (st, ast) in let { Gc.major_words = mw_after; _ } = Gc.quick_stat () in let stats = Stats.dump () in @@ -647,9 +655,9 @@ type parse_action = | Process of Coq.Ast.t (* success! *) (* Returns parse_action, diags, parsing_time *) -let parse_action ~lines ~st last_tok doc_handle = +let parse_action ~token ~lines ~st last_tok doc_handle = let start_loc = Coq.Parsing.Parsable.loc doc_handle |> CLexer.after in - let parse_res, time = parse_stm ~st doc_handle in + let parse_res, time = parse_stm ~token ~st doc_handle in let f = Coq.Utils.to_range ~lines in let { Coq.Protect.E.r; feedback } = Coq.Protect.E.map_loc ~f parse_res in match r with @@ -722,8 +730,8 @@ let strategy_of_coq_err ~node ~state ~last_tok = function | Coq.Protect.Error.Anomaly _ -> Stop (Failed last_tok, node) | User _ -> Continue { state; last_tok; node } -let node_of_coq_result ~doc ~range ~ast ~st ~parsing_diags ~parsing_feedback - ~feedback ~info last_tok res = +let node_of_coq_result ~token ~doc ~range ~ast ~st ~parsing_diags + ~parsing_feedback ~feedback ~info last_tok res = match res with | Ok state -> let node = @@ -739,7 +747,7 @@ let node_of_coq_result ~doc ~range ~ast ~st ~parsing_diags ~parsing_feedback let context = Recovery_context.make ~contents ~last_tok ~nodes ~ast:ast.v () in - let recovery_st = Recovery.handle ~context ~st in + let recovery_st = Recovery.handle ~token ~context ~st in let node = parsed_node ~range ~ast ~state:recovery_st ~parsing_diags ~parsing_feedback ~diags:err_diags ~feedback ~info @@ -747,8 +755,8 @@ let node_of_coq_result ~doc ~range ~ast ~st ~parsing_diags ~parsing_feedback strategy_of_coq_err ~node ~state:recovery_st ~last_tok coq_err (* Build a document node, possibly executing *) -let document_action ~st ~parsing_diags ~parsing_feedback ~parsing_time ~doc - last_tok doc_handle action = +let document_action ~token ~st ~parsing_diags ~parsing_feedback ~parsing_time + ~doc last_tok doc_handle action = match action with (* End of file *) | EOF completed -> @@ -763,7 +771,7 @@ let document_action ~st ~parsing_diags ~parsing_feedback ~parsing_time ~doc let context = Recovery_context.make ~contents:doc.contents ~last_tok ~nodes:doc.nodes () in - let st = Recovery.handle ~context ~st in + let st = Recovery.handle ~token ~context ~st in let node = unparseable_node ~range:span_range ~parsing_diags ~parsing_feedback ~state:st ~parsing_time @@ -772,7 +780,7 @@ let document_action ~st ~parsing_diags ~parsing_feedback ~parsing_time ~doc (* We can interpret the command now *) | Process ast -> ( let lines = doc.contents.lines in - let process_res, info = interp_and_info ~parsing_time ~st ast in + let process_res, info = interp_and_info ~token ~parsing_time ~st ast in let f = Coq.Utils.to_range ~lines in let { Coq.Protect.E.r; feedback } = Coq.Protect.E.map_loc ~f process_res in match r with @@ -789,7 +797,7 @@ let document_action ~st ~parsing_diags ~parsing_feedback ~parsing_time ~doc this point then, hence the new last valid token last_tok_new *) let last_tok_new = Coq.Parsing.Parsable.loc doc_handle in let last_tok_new = Coq.Utils.to_range ~lines last_tok_new in - node_of_coq_result ~doc ~range:ast_range ~ast ~st ~parsing_diags + node_of_coq_result ~token ~doc ~range:ast_range ~ast ~st ~parsing_diags ~parsing_feedback ~feedback ~info last_tok_new res) module Target = struct @@ -824,7 +832,7 @@ let max_errors_node ~state ~range = ~parsing_time:0.0 (* main interpretation loop *) -let process_and_parse ~io ~target ~uri ~version doc last_tok doc_handle = +let process_and_parse ~io ~token ~target ~uri ~version doc last_tok doc_handle = let rec stm doc st (last_tok : Lang.Range.t) acc_errors = (* Reporting of progress and diagnostics (if dirty) *) let doc = send_eager_diagnostics ~io ~uri ~version ~doc in @@ -848,12 +856,12 @@ let process_and_parse ~io ~target ~uri ~version doc last_tok doc_handle = (* Parsing *) let lines = doc.contents.lines in let action, parsing_diags, parsing_feedback, parsing_time = - parse_action ~lines ~st last_tok doc_handle + parse_action ~token ~lines ~st last_tok doc_handle in (* Execution *) let action = - document_action ~st ~parsing_diags ~parsing_feedback ~parsing_time ~doc - last_tok doc_handle action + document_action ~token ~st ~parsing_diags ~parsing_feedback + ~parsing_time ~doc last_tok doc_handle action in match action with | Interrupted last_tok -> set_completion ~completed:(Stopped last_tok) doc @@ -932,7 +940,7 @@ let loc_after ~lines ~uri (r : Lang.Range.t) = } (** Setup parser and call the main routine *) -let resume_check ~io ~(last_tok : Lang.Range.t) ~doc ~target = +let resume_check ~io ~token ~(last_tok : Lang.Range.t) ~doc ~target = let uri, version, contents = (doc.uri, doc.version, doc.contents) in (* Compute resume point, basically [CLexer.after] + stream setup *) let lines = doc.contents.lines in @@ -949,10 +957,10 @@ let resume_check ~io ~(last_tok : Lang.Range.t) ~doc ~target = Coq.Parsing.Parsable.make ~loc:resume_loc Gramlib.Stream.(of_string ~offset processed_content) in - process_and_parse ~io ~target ~uri ~version doc last_tok handle + process_and_parse ~io ~token ~target ~uri ~version doc last_tok handle (** Check a document, if it was not completed already *) -let check ~io ~target ~doc () = +let check ~io ~token ~target ~doc () = match doc.completed with | Yes _ -> Io.Log.trace "check" "resuming, completed=yes, nothing to do"; @@ -962,20 +970,20 @@ let check ~io ~target ~doc () = doc | Stopped last_tok -> DDebug.resume last_tok doc.version; - let doc = resume_check ~io ~last_tok ~doc ~target in + let doc = resume_check ~io ~token ~last_tok ~doc ~target in log_doc_completion doc.completed; Util.print_stats (); doc -let save ~doc = +let save ~token ~doc = match doc.completed with | Yes _ -> let st = Util.last doc.nodes |> Option.cata Node.state doc.root in let uri = doc.uri in let ldir = Coq.Workspace.dirpath_of_uri ~uri in let in_file = Lang.LUri.File.to_string_file uri in - Coq.State.in_stateM ~st - ~f:(fun () -> Coq.Save.save_vo ~st ~ldir ~in_file) + Coq.State.in_stateM ~token ~st + ~f:(fun () -> Coq.Save.save_vo ~token ~st ~ldir ~in_file) () | _ -> let error = Pp.(str "Can't save document that failed to check") in diff --git a/fleche/doc.mli b/fleche/doc.mli index ec1b2e2e..d98cf735 100644 --- a/fleche/doc.mli +++ b/fleche/doc.mli @@ -98,12 +98,19 @@ val diags : t -> Lang.Diagnostic.t list (** Create a new Coq document, this is cached! Note that this operation always suceeds, but the document could be created in a `Failed` state if problems arise. *) -val create : env:Env.t -> uri:Lang.LUri.File.t -> version:int -> raw:string -> t +val create : + token:Coq.Limits.Token.t + -> env:Env.t + -> uri:Lang.LUri.File.t + -> version:int + -> raw:string + -> t (** Update the contents of a document, updating the right structures for incremental checking. If the operation fails, the document will be left in `Failed` state. *) -val bump_version : version:int -> raw:string -> t -> t +val bump_version : + token:Coq.Limits.Token.t -> version:int -> raw:string -> t -> t (** Checking targets, this specifies what we expect check to reach *) module Target : sig @@ -119,11 +126,17 @@ end (** [check ~io ~target ~doc ()], check document [doc], [target] will have Flèche stop after the point specified there has been reached. Output functions are in the [io] record, used to send partial updates. *) -val check : io:Io.CallBack.t -> target:Target.t -> doc:t -> unit -> t +val check : + io:Io.CallBack.t + -> token:Coq.Limits.Token.t + -> target:Target.t + -> doc:t + -> unit + -> t (** [save ~doc] will save [doc] .vo file. It will fail if proofs are open, or if the document completion status is not [Yes] *) -val save : doc:t -> (unit, Loc.t) Coq.Protect.E.t +val save : token:Coq.Limits.Token.t -> doc:t -> (unit, Loc.t) Coq.Protect.E.t (** This is internal, to workaround the Coq multiple-docs problem *) val create_failed_permanent : diff --git a/fleche/info.ml b/fleche/info.ml index 59c3cf04..1cdd1253 100644 --- a/fleche/info.ml +++ b/fleche/info.ml @@ -149,10 +149,10 @@ module O = Make (Offset) (* Related to goal request *) module Goals = struct - let pr_goal st = + let pr_goal ~token st = let ppx env sigma x = let { Coq.Protect.E.r; feedback } = - Coq.Print.pr_letype_env ~goal_concl_style:true env sigma x + Coq.Print.pr_letype_env ~token ~goal_concl_style:true env sigma x in (* XXX: We ideally want to thread this in the monad too, but it'd be better if the printer was more functional *) @@ -167,7 +167,7 @@ module Goals = struct (* We need to use [in_state] here due to printing not being pure, but we want a better design here eventually *) - let goals ~st = Coq.State.in_state ~st ~f:pr_goal st + let goals ~token ~st = Coq.State.in_state ~token ~st ~f:(pr_goal ~token) st let program ~st = Coq.State.program ~st end @@ -182,9 +182,9 @@ module Completion = struct needed *) let to_qualid p = try Some (Libnames.qualid_of_string p) with _ -> None - let candidates ~st prefix = + let candidates ~token ~st prefix = let ( let* ) = Option.bind in - Coq.State.in_state ~st prefix ~f:(fun prefix -> + Coq.State.in_state ~token ~st prefix ~f:(fun prefix -> let* p = to_qualid prefix in Nametab.completion_canditates p |> List.map (fun x -> Pp.string_of_ppcmds (pr_extref x)) diff --git a/fleche/info.mli b/fleche/info.mli index 061400e1..53c55feb 100644 --- a/fleche/info.mli +++ b/fleche/info.mli @@ -53,12 +53,17 @@ module O : S with module P := Offset (** We move towards a more modular design here, for preprocessing *) module Goals : sig val goals : - st:Coq.State.t -> (Pp.t Coq.Goals.reified_pp option, Loc.t) Coq.Protect.E.t + token:Coq.Limits.Token.t + -> st:Coq.State.t + -> (Pp.t Coq.Goals.reified_pp option, Loc.t) Coq.Protect.E.t val program : st:Coq.State.t -> Declare.OblState.View.t Names.Id.Map.t end module Completion : sig val candidates : - st:Coq.State.t -> string -> (string list option, Loc.t) Coq.Protect.E.t + token:Coq.Limits.Token.t + -> st:Coq.State.t + -> string + -> (string list option, Loc.t) Coq.Protect.E.t end diff --git a/fleche/memo.ml b/fleche/memo.ml index 22c6fb47..b28f9f8c 100644 --- a/fleche/memo.ml +++ b/fleche/memo.ml @@ -115,7 +115,7 @@ module type EvalType = sig type output - val eval : t -> (output, Loc.t) Coq.Protect.E.t + val eval : token:Coq.Limits.Token.t -> t -> (output, Loc.t) Coq.Protect.E.t end module SEval (E : EvalType) = struct @@ -126,10 +126,10 @@ module SEval (E : EvalType) = struct let cache = HC.create 1000 let size () = Obj.reachable_words (Obj.magic cache) - let eval v = + let eval ~token v = match HC.find_opt cache v with | None -> - let admitted_st = E.eval v in + let admitted_st = E.eval ~token v in HC.add_execution cache v admitted_st; admitted_st | Some admitted_st -> admitted_st @@ -164,7 +164,7 @@ module CEval (E : LocEvalType) = struct let kind = CS.Kind.Hashing in CS.record ~kind ~f:(HC.find_opt !cache) i - let eval i : _ Stats.t = + let eval ~token i : _ Stats.t = let stm_loc = E.loc_of_input i in match in_cache i with | Some (cached_loc, res), time -> @@ -176,7 +176,7 @@ module CEval (E : LocEvalType) = struct if Debug.cache then Io.Log.trace "memo" "cache miss"; CacheStats.miss (); let kind = CS.Kind.Exec in - let res, time_interp = CS.record ~kind ~f:E.eval i in + let res, time_interp = CS.record ~kind ~f:(E.eval ~token) i in let () = HC.add_execution_loc !cache i (stm_loc, res) in let time = time_hash +. time_interp in Stats.make ~time res @@ -199,7 +199,7 @@ module VernacEval = struct type output = Coq.State.t - let eval (st, stm) = Coq.Interp.interp ~st stm + let eval ~token (st, stm) = Coq.Interp.interp ~token ~st stm end module Interp = CEval (VernacEval) @@ -227,7 +227,8 @@ module RequireEval = struct type output = Coq.State.t - let eval (st, files, stm) = Coq.Interp.Require.interp ~st files stm + let eval ~token (st, files, stm) = + Coq.Interp.Require.interp ~token ~st files stm end module Require = CEval (RequireEval) @@ -237,7 +238,7 @@ module Admit = SEval (struct type output = Coq.State.t - let eval st = Coq.State.admit ~st + let eval ~token st = Coq.State.admit ~token ~st end) module InitEval = struct @@ -256,8 +257,8 @@ module InitEval = struct type output = Coq.State.t - let eval (root_state, workspace, uri) = - Coq.Init.doc_init ~root_state ~workspace ~uri + let eval ~token (root_state, workspace, uri) = + Coq.Init.doc_init ~token ~root_state ~workspace ~uri end module Init = SEval (InitEval) diff --git a/fleche/memo.mli b/fleche/memo.mli index 0a3a34f5..06d93d25 100644 --- a/fleche/memo.mli +++ b/fleche/memo.mli @@ -13,14 +13,18 @@ module Init : sig (** [size ()] Return the size in words, expensive *) val size : unit -> int - val eval : t -> (Coq.State.t, Loc.t) Coq.Protect.E.t + val eval : + token:Coq.Limits.Token.t -> t -> (Coq.State.t, Loc.t) Coq.Protect.E.t end module Interp : sig type t = Coq.State.t * Coq.Ast.t (** Interpret a command, possibly memoizing it *) - val eval : t -> (Coq.State.t, Loc.t) Coq.Protect.E.t Stats.t + val eval : + token:Coq.Limits.Token.t + -> t + -> (Coq.State.t, Loc.t) Coq.Protect.E.t Stats.t (** [size ()] Return the size in words, expensive *) val size : unit -> int @@ -33,7 +37,10 @@ module Require : sig type t = Coq.State.t * Coq.Files.t * Coq.Ast.Require.t (** Interpret a require, possibly memoizing it *) - val eval : t -> (Coq.State.t, Loc.t) Coq.Protect.E.t Stats.t + val eval : + token:Coq.Limits.Token.t + -> t + -> (Coq.State.t, Loc.t) Coq.Protect.E.t Stats.t (** [size ()] Return the size in words, expensive *) val size : unit -> int @@ -48,7 +55,8 @@ module Admit : sig (** [size ()] Return the size in words, expensive *) val size : unit -> int - val eval : t -> (Coq.State.t, Loc.t) Coq.Protect.E.t + val eval : + token:Coq.Limits.Token.t -> t -> (Coq.State.t, Loc.t) Coq.Protect.E.t end module CacheStats : sig diff --git a/fleche/theory.ml b/fleche/theory.ml index 2b4c5d1b..6d95ece5 100644 --- a/fleche/theory.ml +++ b/fleche/theory.ml @@ -139,28 +139,28 @@ let diags_of_doc doc = List.concat_map Doc.Node.diags doc.Doc.nodes general structure *) module Register : sig module Completed : sig - type t = io:Io.CallBack.t -> doc:Doc.t -> unit + type t = io:Io.CallBack.t -> token:Coq.Limits.Token.t -> doc:Doc.t -> unit end val add : Completed.t -> unit - val fire : io:Io.CallBack.t -> doc:Doc.t -> unit + val fire : io:Io.CallBack.t -> token:Coq.Limits.Token.t -> doc:Doc.t -> unit end = struct module Completed = struct - type t = io:Io.CallBack.t -> doc:Doc.t -> unit + type t = io:Io.CallBack.t -> token:Coq.Limits.Token.t -> doc:Doc.t -> unit end let callback : Completed.t list ref = ref [] let add fn = callback := fn :: !callback - let fire ~io ~doc = List.iter (fun f -> f ~io ~doc) !callback + let fire ~io ~token ~doc = List.iter (fun f -> f ~io ~token ~doc) !callback end -let send_diags ~io ~doc = +let send_diags ~io ~token:_ ~doc = let diags = diags_of_doc doc in if List.length diags > 0 || !Config.v.send_diags then let uri, version = (doc.uri, doc.version) in Io.Report.diagnostics ~io ~uri ~version diags -let send_perf_data ~io ~(doc : Doc.t) = +let send_perf_data ~io ~token:_ ~(doc : Doc.t) = (* The if below needs to be moved to registrationt time, but for now we keep it for now until the plugin workflow is clearer *) if !Config.v.send_perf_data then @@ -173,7 +173,9 @@ let () = Register.add send_diags module Check : sig val schedule : uri:Lang.LUri.File.t -> unit val deschedule : uri:Lang.LUri.File.t -> unit - val maybe_check : io:Io.CallBack.t -> (Int.Set.t * Doc.t) option + + val maybe_check : + io:Io.CallBack.t -> token:Coq.Limits.Token.t -> (Int.Set.t * Doc.t) option end = struct let pending = ref [] @@ -199,7 +201,7 @@ end = struct Option.map target_of_pt_handle (List.nth_opt pt_requests 0) (* Notification handling; reply is optional / asynchronous *) - let check ~io ~uri = + let check ~io ~token ~uri = Io.Log.trace "process_queue" "resuming document checking"; match Handle.find_opt ~uri with | Some handle -> ( @@ -214,9 +216,10 @@ end = struct None | (None | Some _) as tgt -> let target = Option.default Doc.Target.End tgt in - let doc = Doc.check ~io ~target ~doc:handle.doc () in + let doc = Doc.check ~io ~token ~target ~doc:handle.doc () in let requests = Handle.update_doc_info ~handle ~doc in - if Doc.Completion.is_completed doc.completed then Register.fire ~io ~doc; + if Doc.Completion.is_completed doc.completed then + Register.fire ~io ~token ~doc; (* Remove from the queue *) if Doc.Completion.is_completed doc.completed then pending := pend_pop !pending; @@ -227,15 +230,17 @@ end = struct ("file " ^ Lang.LUri.File.to_string_uri uri ^ " not available"); None - let maybe_check ~io = pend_try (fun uri -> check ~io ~uri) !pending + let maybe_check ~io ~token = + pend_try (fun uri -> check ~io ~token ~uri) !pending + let schedule ~uri = pending := pend_push uri !pending let deschedule ~uri = pending := CList.remove Lang.LUri.File.equal uri !pending end -let create ~env ~uri ~raw ~version = - let doc = Doc.create ~env ~uri ~raw ~version in +let create ~token ~env ~uri ~raw ~version = + let doc = Doc.create ~token ~env ~uri ~raw ~version in Handle.create ~uri ~doc; Check.schedule ~uri @@ -254,7 +259,7 @@ let sane_coq_version = (* Can't wait for the day this goes away *) let tainted = ref false -let create ~io ~env ~uri ~raw ~version = +let create ~io ~token ~env ~uri ~raw ~version = if !tainted && not sane_coq_version then ( (* Error due to Coq bug *) let message = @@ -271,16 +276,16 @@ let create ~io ~env ~uri ~raw ~version = Check.schedule ~uri) else ( tainted := true; - create ~env ~uri ~raw ~version) + create ~token ~env ~uri ~raw ~version) -let change ~io:_ ~(doc : Doc.t) ~version ~raw = +let change ~io:_ ~token ~(doc : Doc.t) ~version ~raw = let uri = doc.uri in Io.Log.trace "bump file" (Lang.LUri.File.to_string_uri uri ^ " / version: " ^ string_of_int version); let tb = Unix.gettimeofday () in (* The discrepancy here will be solved once we remove the [Protect.*.t] types from `doc.mli` *) - let doc = Doc.bump_version ~version ~raw doc in + let doc = Doc.bump_version ~token ~version ~raw doc in let diff = Unix.gettimeofday () -. tb in Io.Log.trace "bump file took" (Format.asprintf "%f" diff); (* Just in case for the future, we update the document before requesting it to @@ -289,14 +294,14 @@ let change ~io:_ ~(doc : Doc.t) ~version ~raw = Check.schedule ~uri; invalid -let change ~io ~uri ~version ~raw = +let change ~io ~token ~uri ~version ~raw = match Handle.find_opt ~uri with | None -> Io.Log.trace "DocHandle.find" ("file " ^ Lang.LUri.File.to_string_uri uri ^ " not available"); Int.Set.empty | Some { doc; _ } -> - if version > doc.version then change ~io ~doc ~version ~raw + if version > doc.version then change ~io ~token ~doc ~version ~raw else (* That's a weird case, get got changes without a version bump? Do nothing for now *) diff --git a/fleche/theory.mli b/fleche/theory.mli index 12a2e40f..58d4b632 100644 --- a/fleche/theory.mli +++ b/fleche/theory.mli @@ -19,12 +19,14 @@ module Check : sig (** Check pending documents, return [None] if there is none pending, or [Some rqs] the list of requests ready to execute after the check. Sends progress and diagnostics notifications using output function [ofn]. *) - val maybe_check : io:Io.CallBack.t -> (Int.Set.t * Doc.t) option + val maybe_check : + io:Io.CallBack.t -> token:Coq.Limits.Token.t -> (Int.Set.t * Doc.t) option end (** Create a document inside a theory *) val create : io:Io.CallBack.t + -> token:Coq.Limits.Token.t -> env:Doc.Env.t -> uri:Lang.LUri.File.t -> raw:string @@ -34,6 +36,7 @@ val create : (** Update a document inside a theory, returns the list of not valid requests *) val change : io:Io.CallBack.t + -> token:Coq.Limits.Token.t -> uri:Lang.LUri.File.t -> version:int -> raw:string @@ -74,7 +77,7 @@ end (* Experimental plugin API, not stable yet *) module Register : sig module Completed : sig - type t = io:Io.CallBack.t -> doc:Doc.t -> unit + type t = io:Io.CallBack.t -> token:Coq.Limits.Token.t -> doc:Doc.t -> unit end val add : Completed.t -> unit diff --git a/plugins/astdump/main.ml b/plugins/astdump/main.ml index eb04b4f6..bcacba4f 100644 --- a/plugins/astdump/main.ml +++ b/plugins/astdump/main.ml @@ -19,7 +19,7 @@ let dump_asts ~out_file pp asts = Format.pp_print_flush fmt (); Stdlib.close_out out -let dump_ast ~io ~(doc : Doc.t) = +let dump_ast ~io ~token:_ ~(doc : Doc.t) = let uri = doc.uri in let uri_str = Lang.LUri.File.to_string_uri uri in let out_file_j = Lang.LUri.File.to_string_file uri ^ ".json.astdump" in diff --git a/plugins/save_vo/main.ml b/plugins/save_vo/main.ml index 6fbdbd60..ede16be8 100644 --- a/plugins/save_vo/main.ml +++ b/plugins/save_vo/main.ml @@ -1,8 +1,8 @@ open Fleche (* Improve errors *) -let save_vo_file ~io:_ ~doc = - match Doc.save ~doc with +let save_vo_file ~io:_ ~token ~doc = + match Doc.save ~token ~doc with | { r = Completed (Ok ()); feedback = _ } -> () | { r = Completed (Error _); feedback = _ } -> () | { r = Interrupted; feedback = _ } -> () diff --git a/plugins/simple/main.ml b/plugins/simple/main.ml index d3dd5b34..f31cdcdb 100644 --- a/plugins/simple/main.ml +++ b/plugins/simple/main.ml @@ -1,6 +1,6 @@ open Fleche -let simple_action ~io ~doc = +let simple_action ~io ~token:_ ~doc = let uri = Lang.LUri.File.to_string_uri doc.Doc.uri in let lvl = Io.Level.info in let message =