diff --git a/.gitmodules b/.gitmodules index 3b91060f0..e69de29bb 100644 --- a/.gitmodules +++ b/.gitmodules @@ -1,8 +0,0 @@ -[submodule "coq"] - path = vendor/coq - url = https://github.com/ejgallego/coq.git - branch = proof+no_global_partial -[submodule "coq-serapi"] - path = vendor/coq-serapi - url = https://github.com/ejgallego/coq-serapi.git - branch = v8.17 diff --git a/CHANGES.md b/CHANGES.md index b92be3152..4ca9c3a24 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -1,3 +1,29 @@ +# coq-lsp 0.1.3: Event +---------------------- + + - Much improved handling of Coq fatal errors, the server is now + hardened against them (@ejgallego, #155, #157, #160, fixes #91) + - `coq-lsp` now follows the LSP specification regarding + initialization strictly (@ejgallego, #168) + - New setting for goals to be updated when the selection changes due + to a command; this makes VsCodeVim cursor tracking work; thanks to + Cactus (Anton) Golov for detailed bug reporting and testing + (@ejgallego, @jesyspa, #170, fixes #163) + - `coq-lsp` will now warn the user when two files have been opened + simultaneously and the parser may go into a broken state :/ + (@ejgallego, #169) + - Implement request postponement and cancellation. Thus + `documentSymbols` will now be postponed until the document is + ready, (@ejgallego, #141, #146, fixes #124) + - Protocol and VS Code interfaces now support shelved and given_up + goals (@ejgallego, #175) + - Allow to postpone requests to wait for data to become available on + document points; this is implemented to provide a nicer "show goals + while I type" experience. Client default has been changed to "show + goals on mouse, click, typing, and cursor movement) (@ejgallego, + #177, #179) + - Store stats per document (@ejgallego, #180, fixes #173) + # coq-lsp 0.1.2: Message ------------------------ diff --git a/Makefile b/Makefile index 7e6ae1ef1..2039fc554 100644 --- a/Makefile +++ b/Makefile @@ -1,10 +1,6 @@ COQ_BUILD_CONTEXT=../_build/default/coq -PKG_SET= \ -vendor/coq/coq-core.install \ -vendor/coq/coq-stdlib.install \ -vendor/coq-serapi/coq-serapi.install \ -coq-lsp.install +PKG_SET=coq-lsp.install # Get the ocamlformat version from the .ocamlformat file OCAMLFORMAT=ocamlformat.$$(awk -F = '$$1 == "version" {print $$2}' .ocamlformat) @@ -15,7 +11,7 @@ $(OCAMLFORMAT) \ ocaml-lsp-server .PHONY: build -build: coq_boot +build: dune build $(DUNEOPT) $(PKG_SET) .PHONY: check @@ -83,3 +79,11 @@ submodules-deinit: .PHONY: extension extension: cd editor/code && npm i && npm run compile + +# Run prettier +.PHONY: ts-fmt +ts-fmt: + cd editor/code && npx prettier -w . + +.PHONY: make-fmt +make-fmt: build fmt diff --git a/README.md b/README.md index e7ddcf5d9..ba6cb4b56 100644 --- a/README.md +++ b/README.md @@ -27,12 +27,19 @@ to stop by. https://marketplace.visualstudio.com/items?itemName=ejgallego.coq-lsp - GNU Emacs: `M-x eglot [Enter] coq-lsp [Enter]` +## FAQ + +See our [list of frequently-asked questions](./etc/FAQ.md). + ## Troubleshooting - Most problems can be resolved by restarting `coq-lsp`, in Visual Studio Code, `Ctrl+Shift+P` will give you access to the `coq-lsp.restart` command. - In VSCode, the "Output" window will have a "Coq LSP Server Events" channel which should contain some important information. +- As of today, `coq-lsp` may have trouble when more than one file is open at + the same time, this is a problem upstream. For now, you are advised to + work on a single file if this problem appears. ## Features @@ -52,7 +59,7 @@ should not, please file a bug! ### Smart, Cache-aware Error recovery -`coq-lsp` won't stop checking on errors, but support (and encourages) working +`coq-lsp` won't stop checking on errors, but supports (and encourages) working with proof documents that are only partially working. Moreover, error recovery integrates with the incremental cache, and will recognize proof structure. @@ -252,6 +259,10 @@ inspirations, and sharing of ideas from colleagues. In particular, we'd like to thank Rudi Grinberg, Andrey Mokhov, Clément Pit-Claudel, and Makarius Wenzel for their help and advice. +As noted above, the original implementation was based on the Lambdapi LSP +server, thanks to all our collaborators in that project! + + diff --git a/controller/cache.ml b/controller/cache.ml new file mode 100644 index 000000000..6bd88087f --- /dev/null +++ b/controller/cache.ml @@ -0,0 +1,47 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* + LIO.trace "memo" (Printexc.to_string exn); + Sys.remove memo_cache_file; + () + +(* We disable it for now, see todo.org for more information *) +let save_to_disk () = if false then memo_save_to_disk () + +let memo_read_from_disk () = + try + if Sys.file_exists memo_cache_file then ( + LIO.trace "memo" "trying to load cache file"; + Fleche.Memo.load_from_disk ~file:memo_cache_file; + LIO.trace "memo" "cache file loaded") + else LIO.trace "memo" "cache file not present" + with exn -> + LIO.trace "memo" ("loading cache failed: " ^ Printexc.to_string exn); + Sys.remove memo_cache_file; + () + +let read_from_disk () = if false then memo_read_from_disk () diff --git a/controller/cache.mli b/controller/cache.mli new file mode 100644 index 000000000..781541061 --- /dev/null +++ b/controller/cache.mli @@ -0,0 +1,19 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* unit +val read_from_disk : unit -> unit diff --git a/controller/coq_lsp.ml b/controller/coq_lsp.ml index a91d613cb..a84d5ec68 100644 --- a/controller/coq_lsp.ml +++ b/controller/coq_lsp.ml @@ -11,7 +11,7 @@ (************************************************************************) (* 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 2019-2023 Inria -- Dual License LGPL 2.1 / GPL3+ *) (* Written by: Emilio J. Gallego Arias *) (************************************************************************) @@ -25,11 +25,6 @@ let list_field name dict = U.to_list List.(assoc name dict) let string_field name dict = U.to_string List.(assoc name dict) (* Conditionals *) -let _option_empty x = - match x with - | None -> true - | Some _ -> false - let option_cata f d x = match x with | None -> d @@ -40,8 +35,8 @@ let option_default x d = | None -> d | Some x -> x -let oint_field name dict = option_cata U.to_int 0 List.(assoc_opt name dict) let ostring_field name dict = Option.map U.to_string (List.assoc_opt name dict) +let oint_field name dict = Option.map U.to_int (List.assoc_opt name dict) let odict_field name dict = option_default @@ -55,37 +50,62 @@ module State = struct type t = { root_state : Coq.State.t ; workspace : Coq.Workspace.t - ; fb_queue : Coq.Message.t list ref } end module LIO = Lsp.Io module LSP = Lsp.Base +module Check = Doc_manager.Check + +module PendingRequest = struct + type t = + | DocRequest of + { uri : string + ; handler : doc:Fleche.Doc.t -> J.t + } + | PosRequest of + { uri : string + ; point : int * int + ; handler : doc:Fleche.Doc.t -> point:int * int -> J.t + } +end + +module RResult = struct + type t = + | Ok of Yojson.Safe.t + | Error of int * string + | Postpone of PendingRequest.t + + let ok x = Ok x +end (* Request Handling: The client expects a reply *) module CoqLspOption = struct type t = [%import: Fleche.Config.t] [@@deriving yojson] end -let do_client_options coq_lsp_options = +let do_client_options coq_lsp_options : unit = LIO.trace "init" "custom client options:"; LIO.trace_object "init" (`Assoc coq_lsp_options); match CoqLspOption.of_yojson (`Assoc coq_lsp_options) with | Ok v -> Fleche.Config.v := v | Error msg -> LIO.trace "CoqLspOption.of_yojson error: " msg -let check_client_version version : unit = - LIO.trace "version" version; - match version with - | "any" | "0.1.2" -> () - | v -> - let message = Format.asprintf "Incorrect version: %s , expected 0.1.2" v in +let check_client_version client_version : unit = + LIO.trace "client_version" client_version; + if String.(equal client_version "any" || equal client_version Version.server) + then () (* Version OK *) + else + let message = + Format.asprintf "Incorrect client version: %s , expected %s." + client_version Version.server + in LIO.logMessage ~lvl:1 ~message -let do_initialize ofmt ~id params = +let do_initialize ~params = let trace = ostring_field "trace" params - |> option_cata LIO.TraceValue.parse LIO.TraceValue.Off + |> option_cata LIO.TraceValue.of_string LIO.TraceValue.Off in LIO.set_trace_value trace; let coq_lsp_options = odict_field "initializationOptions" params in @@ -102,104 +122,52 @@ let do_initialize ofmt ~id params = ; ("codeActionProvider", `Bool false) ] in - let msg = - LSP.mk_reply ~id - ~result: - (`Assoc - [ ("capabilities", `Assoc capabilities) - ; ( "serverInfo" - , `Assoc - [ ("name", `String "coq-lsp (C) Inria 2022") - ; ("version", `String "0.1+alpha") - ] ) - ]) - in - LIO.send_json ofmt msg - -let do_shutdown ofmt ~id = - let msg = LSP.mk_reply ~id ~result:`Null in - LIO.send_json ofmt msg - -(* Handler for document *) -module DocHandle = struct - type t = - { doc : Fleche.Doc.t - ; requests : unit (* placeholder for requests attached to a document *) - } - - let doc_table : (string, t) Hashtbl.t = Hashtbl.create 39 - - let create ~uri ~doc = - (match Hashtbl.find_opt doc_table uri with - | None -> () - | Some _ -> - LIO.trace "do_open" ("file " ^ uri ^ " not properly closed by client")); - Hashtbl.add doc_table uri { doc; requests = () } - - let close ~uri = Hashtbl.remove doc_table uri - let find ~uri = Hashtbl.find doc_table uri - let find_doc ~uri = (find ~uri).doc - - let _update ~handle ~(doc : Fleche.Doc.t) = - Hashtbl.replace doc_table doc.uri { handle with doc } - - (* Clear requests *) - let update_doc_version ~(doc : Fleche.Doc.t) = - Hashtbl.replace doc_table doc.uri { doc; requests = () } - - (* trigger pending incremental requests *) - let update_doc_info ~handle ~(doc : Fleche.Doc.t) = - Hashtbl.replace doc_table doc.uri { handle with doc } -end - -let lsp_of_diags ~uri ~version diags = - List.map - (fun { Fleche.Types.Diagnostic.range; severity; message; extra = _ } -> - (range, severity, message, None)) - diags - |> LSP.mk_diagnostics ~uri ~version - -let lsp_of_progress ~uri ~version progress = - let progress = - List.map - (fun (range, kind) -> - `Assoc [ ("range", LSP.mk_range range); ("kind", `Int kind) ]) - progress - in - let params = - [ ( "textDocument" - , `Assoc [ ("uri", `String uri); ("version", `Int version) ] ) - ; ("processing", `List progress) + `Assoc + [ ("capabilities", `Assoc capabilities) + ; ( "serverInfo" + , `Assoc + [ ("name", `String "coq-lsp (C) Inria 2023") + ; ("version", `String Version.server) + ] ) ] - in - LSP.mk_notification ~method_:"$/coq/fileProgress" ~params - -let asts_of_doc doc = - List.filter_map (fun v -> v.Fleche.Doc.ast) doc.Fleche.Doc.nodes - -let diags_of_doc doc = - List.concat_map (fun node -> node.Fleche.Doc.diags) doc.Fleche.Doc.nodes - -module Check = struct - let pending = ref None + |> RResult.ok - (* Notification handling; reply is optional / asynchronous *) - let do_check ofmt ~fb_queue ~uri = - let handle = DocHandle.find ~uri in - let doc = Fleche.Doc.check ~ofmt ~doc:handle.doc ~fb_queue in - DocHandle.update_doc_info ~handle ~doc; - let diags = diags_of_doc doc in - let diags = lsp_of_diags ~uri:doc.uri ~version:doc.version diags in - LIO.send_json ofmt @@ diags +let rtable : (int, PendingRequest.t) Hashtbl.t = Hashtbl.create 673 - let completed uri = - let doc = DocHandle.find_doc ~uri in - match doc.completed with - | Yes _ -> true - | _ -> false +let rec answer_request ~ofmt ~id result = + match result with + | RResult.Ok result -> LSP.mk_reply ~id ~result |> LIO.send_json ofmt + | Error (code, message) -> + LSP.mk_request_error ~id ~code ~message |> LIO.send_json ofmt + | Postpone (DocRequest { uri; _ } as pr) -> + if Fleche.Debug.request_delay then + LIO.trace "request" ("postponing rq : " ^ string_of_int id); + Doc_manager.serve_on_completion ~uri ~id; + Hashtbl.add rtable id pr + | Postpone (PosRequest { uri; point; _ } as pr) -> + if Fleche.Debug.request_delay then + LIO.trace "request" ("postponing rq : " ^ string_of_int id); + (* This will go away once we have a proper location request queue in + Doc_manager *) + (match Doc_manager.serve_if_point ~uri ~id ~point with + | None -> () + | Some id_to_cancel -> + (* -32802 = RequestFailed | -32803 = ServerCancelled ; *) + let code = -32802 in + let message = "Request got old in server" in + answer_request ~ofmt ~id:id_to_cancel (Error (code, message))); + Hashtbl.add rtable id pr + +let cancel_rq ~ofmt ~code ~message id = + match Hashtbl.find_opt rtable id with + | None -> + (* Request already served or cancelled *) + () + | Some _ -> + Hashtbl.remove rtable id; + answer_request ~ofmt ~id (Error (code, message)) - let schedule ~uri = pending := Some uri -end +let do_shutdown ~params:_ = RResult.Ok `Null let do_open ~state params = let document = dict_field "textDocument" params in @@ -209,48 +177,38 @@ let do_open ~state params = , string_field "text" document ) in let root_state, workspace = State.(state.root_state, state.workspace) in - let doc = - Fleche.Doc.create ~state:root_state ~workspace ~uri ~contents ~version - in - DocHandle.create ~uri ~doc; - Check.schedule ~uri + Doc_manager.create ~root_state ~workspace ~uri ~contents ~version -let do_change params = +let do_change ~ofmt params = let document = dict_field "textDocument" params in let uri, version = (string_field "uri" document, int_field "version" document) in let changes = List.map U.to_assoc @@ list_field "contentChanges" params in match changes with - | [] -> () + | [] -> + LIO.trace "do_change" "no change in changes? ignoring"; + () | _ :: _ :: _ -> - LIO.trace "do_change" "more than one change unsupported due to sync method"; - assert false + LIO.trace "do_change" + "more than one change unsupported due to sync method, ignoring"; + () | change :: _ -> let contents = string_field "text" change in - let doc = DocHandle.find_doc ~uri in - if version > doc.version then ( - LIO.trace "bump file" (uri ^ " / version: " ^ string_of_int version); - let tb = Unix.gettimeofday () in - let doc = Fleche.Doc.bump_version ~version ~contents doc in - let diff = Unix.gettimeofday () -. tb in - LIO.trace "bump file took" (Format.asprintf "%f" diff); - let () = DocHandle.update_doc_version ~doc in - Check.schedule ~uri) - else - (* That's a weird case, get got changes without a version bump? Do nothing - for now *) - () - -let do_close _ofmt params = + let invalid_rq = Doc_manager.change ~uri ~version ~contents in + let code = -32802 in + let message = "Request got old in server" in + Int.Set.iter (cancel_rq ~ofmt ~code ~message) invalid_rq + +let do_close ~ofmt:_ params = let document = dict_field "textDocument" params in let uri = string_field "uri" document in - DocHandle.close ~uri + Doc_manager.close ~uri let get_textDocument params = let document = dict_field "textDocument" params in let uri = string_field "uri" document in - let doc = DocHandle.find_doc ~uri in + let doc = Doc_manager.find_doc ~uri in (uri, doc) let get_position params = @@ -258,263 +216,248 @@ let get_position params = let line, character = (int_field "line" pos, int_field "character" pos) in (line, character) -let mk_syminfo file (name, _path, kind, pos) : J.t = - `Assoc - [ ("name", `String name) - ; ("kind", `Int kind) - ; (* function *) - ( "location" - , `Assoc - [ ("uri", `String file) - ; ("range", LSP.mk_range Fleche.Types.(to_range pos)) - ] ) - ] - -let _kind_of_type _tm = 13 -(* let open Terms in let open Timed in let is_undef = option_empty !(tm.sym_def) - && List.length !(tm.sym_rules) = 0 in match !(tm.sym_type) with | Vari _ -> - 13 (* Variable *) | Type | Kind | Symb _ | _ when is_undef -> 14 (* Constant - *) | _ -> 12 (* Function *) *) - -let do_symbols ofmt ~id params = +let do_position_request ~postpone ~params ~handler = let uri, doc = get_textDocument params in - match doc.completed with - | Yes _ -> - let f loc id = mk_syminfo uri (Names.Id.to_string id, "", 12, loc) in - let ast = asts_of_doc doc in - 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 _ -> - (* -32802 = RequestFailed | -32803 = ServerCancelled ; *) - let code = -32802 in - let message = "Document is not ready" in - LSP.mk_request_error ~id ~code ~message |> LIO.send_json ofmt - -let do_position_request ofmt ~id params ~handler = - let _uri, doc = get_textDocument params in + let version = dict_field "textDocument" params |> oint_field "version" in let point = get_position params in let line, col = point in + (* XXX: The logic here is shared by the wake-up code in Doc_manager, it should + be refactored, and in fact it should be the Doc_manager (which manages the + request wake-up queue) who should take this decision. + + Actually the owner of the doc ready data is Fleche.Doc, but for now we + approximate that until we can chat directly with Flèche *) let in_range = match doc.completed with | Yes _ -> true - | Stopped loc -> - line < loc.line_nb_last - || (line = loc.line_nb_last && col <= loc.ep - loc.bol_pos_last) + | Failed loc | Stopped loc -> + let proc_line = loc.line_nb_last - 1 in + line < proc_line || (line = proc_line && col < loc.ep - loc.bol_pos_last) + in + let in_range = + match version with + | None -> in_range + | Some version -> doc.version >= version && in_range in - if in_range then - let result = handler ~doc ~point in - LSP.mk_reply ~id ~result |> LIO.send_json ofmt + if in_range then RResult.Ok (handler ~doc ~point) + else if postpone then Postpone (PosRequest { uri; point; handler }) else - (* -32802 = RequestFailed | -32803 = ServerCancelled ; *) let code = -32802 in let message = "Document is not ready" in - LSP.mk_request_error ~id ~code ~message |> LIO.send_json ofmt + Error (code, message) -let hover_handler ~doc ~point = - let show_loc_info = true in - let loc_span = Fleche.Info.LC.loc ~doc ~point Exact in - let loc_string = - Option.map Coq.Ast.pr_loc loc_span |> Option.default "no ast" - in - let info_string = - Fleche.Info.LC.info ~doc ~point Exact |> Option.default "no info" - in - let hover_string = - if show_loc_info then loc_string ^ "\n___\n" ^ info_string else info_string - in - `Assoc - ([ ( "contents" - , `Assoc - [ ("kind", `String "markdown"); ("value", `String hover_string) ] ) - ] - @ Option.cata - (fun loc -> [ ("range", LSP.mk_range (Fleche.Types.to_range loc)) ]) - [] loc_span) +let do_hover = do_position_request ~postpone:false ~handler:Requests.hover +let do_goals = do_position_request ~postpone:true ~handler:Requests.goals -let do_hover ofmt = do_position_request ofmt ~handler:hover_handler +let do_completion = + do_position_request ~postpone:false ~handler:Requests.completion -let do_trace params = - let trace = string_field "value" params in - LIO.set_trace_value (LIO.TraceValue.parse trace) - -(* Replace by ppx when we can print goals properly in the client *) -let mk_hyp { Coq.Goals.names; def = _; ty } : Yojson.Safe.t = - let names = List.map (fun id -> `String (Names.Id.to_string id)) names in - let ty = Pp.string_of_ppcmds ty in - `Assoc [ ("names", `List names); ("ty", `String ty) ] - -let mk_goal { Coq.Goals.info = _; ty; hyps } : Yojson.Safe.t = - let ty = Pp.string_of_ppcmds ty in - `Assoc [ ("ty", `String ty); ("hyps", `List (List.map mk_hyp hyps)) ] - -let mk_goals { Coq.Goals.goals; _ } = List.map mk_goal goals -let mk_goals = Option.cata mk_goals [] -let mk_message (_loc, _lvl, msg) = `String (Pp.string_of_ppcmds msg) -let mk_messages m = List.map mk_message m -let mk_messages = Option.cata mk_messages [] - -let mk_error node = - let open Fleche in - let open Fleche.Types in - match List.filter (fun d -> d.Diagnostic.severity < 2) node.Doc.diags with - | [] -> [] - | e :: _ -> [ ("error", `String e.Diagnostic.message) ] - -let goals_mode = - if !Fleche.Config.v.goal_after_tactic then Fleche.Info.PrevIfEmpty - else Fleche.Info.Prev - -let goals_handler ~doc ~point = - let open Fleche in - let goals = Info.LC.goals ~doc ~point goals_mode in - let node = Info.LC.node ~doc ~point Exact in - let messages = Option.map (fun node -> node.Doc.messages) node in - let error = Option.cata mk_error [] node in - `Assoc - ([ ( "textDocument" - , `Assoc [ ("uri", `String doc.uri); ("version", `Int doc.version) ] ) - ; ( "position" - , `Assoc [ ("line", `Int (fst point)); ("character", `Int (snd point)) ] - ) - ; ("goals", `List (mk_goals goals)) - ; ("messages", `List (mk_messages messages)) - ] - @ error) - -let do_goals ofmt = do_position_request ofmt ~handler:goals_handler - -let completion_handler ~doc ~point:_ = - let f _loc id = `Assoc [ ("label", `String Names.Id.(to_string id)) ] in - let ast = asts_of_doc doc in - let clist = Coq.Ast.grab_definitions f ast in - `List clist - -let do_completion ofmt = do_position_request ofmt ~handler:completion_handler -let memo_cache_file = ".coq-lsp.cache" - -let memo_save_to_disk () = - try - Fleche.Memo.save_to_disk ~file:memo_cache_file; - LIO.trace "memo" "cache saved to disk" - with exn -> - LIO.trace "memo" (Printexc.to_string exn); - Sys.remove memo_cache_file; - () - -(* We disable it for now, see todo.org for more information *) -let memo_save_to_disk () = if false then memo_save_to_disk () - -let memo_read_from_disk () = - try - if Sys.file_exists memo_cache_file then ( - LIO.trace "memo" "trying to load cache file"; - Fleche.Memo.load_from_disk ~file:memo_cache_file; - LIO.trace "memo" "cache file loaded") - else LIO.trace "memo" "cache file not present" - with exn -> - LIO.trace "memo" ("loading cache failed: " ^ Printexc.to_string exn); - Sys.remove memo_cache_file; - () - -let memo_read_from_disk () = if false then memo_read_from_disk () - -(* The rule is: we keep the latest change check notification in the variable; it - is only served when the rest of requests are served. - - Note that we should add a method to detect stale requests; maybe cancel them - when a new edit comes. - - Also, this should eventually become a queue, instead of a single - change_pending setup. *) -let request_queue = Queue.create () +(* Requires the full document to be processed *) +let do_document_request ~params ~handler = + let uri, doc = get_textDocument params in + match doc.completed with + | Yes _ -> RResult.Ok (handler ~doc) + | Stopped _ | Failed _ -> + Postpone (PendingRequest.DocRequest { uri; handler }) -let process_input (com : J.t) = - if Fleche.Debug.sched_wakeup then - LIO.trace "-> enqueue" (Format.asprintf "%.2f" (Unix.gettimeofday ())); - (* TODO: this is the place to cancel pending requests that are invalid, and in - general, to perform queue optimizations *) - Queue.push com request_queue; - Control.interrupt := true +let do_symbols = do_document_request ~handler:Requests.symbols +let do_trace params = + let trace = string_field "value" params in + LIO.set_trace_value (LIO.TraceValue.of_string trace) + +(***********************************************************************) + +(** Misc helpers *) +let rec read_request ic = + let com = LIO.read_request ic in + if Fleche.Debug.read then LIO.trace_object "read" com; + match LSP.Message.from_yojson com with + | Ok msg -> msg + | Error msg -> + LIO.trace "read_request" ("error: " ^ msg); + read_request ic + +let do_cancel ~ofmt ~params = + let id = int_field "id" params in + let code = -32800 in + let message = "Cancelled by client" in + cancel_rq ~ofmt ~code ~message id + +let serve_postponed_request id = + match Hashtbl.find_opt rtable id with + | None -> + LIO.trace "can't wake up cancelled request: " (string_of_int id); + None + | Some (DocRequest { uri; handler }) -> + if Fleche.Debug.request_delay then + LIO.trace "wake up doc rq: " (string_of_int id); + Hashtbl.remove rtable id; + let doc = Doc_manager.find_doc ~uri in + Some (RResult.Ok (handler ~doc)) + | Some (PosRequest { uri; point; handler }) -> + if Fleche.Debug.request_delay then + LIO.trace "wake up pos rq: " + (Format.asprintf "%d | pos: (%d,%d)" id (fst point) (snd point)); + Hashtbl.remove rtable id; + let doc = Doc_manager.find_doc ~uri in + Some (RResult.Ok (handler ~point ~doc)) + +let serve_postponed_request ~ofmt id = + serve_postponed_request id |> Option.iter (answer_request ~ofmt ~id) + +let serve_postponed_requests ~ofmt rl = + Int.Set.iter (serve_postponed_request ~ofmt) rl + +(***********************************************************************) + +(** LSP Init routine *) exception Lsp_exit -(* XXX: We could split requests and notifications but with the OCaml theading - model there is not a lot of difference yet; something to think for the - future. *) -let dispatch_message ofmt ~state dict = - let id = oint_field "id" dict in - let params = odict_field "params" dict in - match string_field "method" dict with - (* Requests *) - | "initialize" -> do_initialize ofmt ~id params - | "shutdown" -> do_shutdown ofmt ~id - (* Symbols and info about the document *) - | "textDocument/completion" -> do_completion ofmt ~id params - | "textDocument/documentSymbol" -> do_symbols ofmt ~id params - | "textDocument/hover" -> do_hover ofmt ~id params +let log_workspace w = + let message, extra = Coq.Workspace.describe w in + LIO.trace "workspace" "initialized" ~extra; + LIO.logMessage ~lvl:3 ~message + +let rec lsp_init_loop ic ofmt ~cmdline : Coq.Workspace.t = + match read_request ic with + | LSP.Message.Request { method_ = "initialize"; id; params } -> + (* At this point logging is allowed per LSP spec *) + LIO.logMessage ~lvl:3 ~message:"Initializing server"; + let result = do_initialize ~params in + answer_request ~ofmt ~id result; + LIO.logMessage ~lvl:3 ~message:"Server initialized"; + (* Workspace initialization *) + let workspace = Coq.Workspace.guess ~cmdline in + log_workspace workspace; + workspace + | LSP.Message.Request { id; _ } -> + (* per spec *) + LSP.mk_request_error ~id ~code:(-32002) ~message:"server not initialized" + |> LIO.send_json ofmt; + lsp_init_loop ic ofmt ~cmdline + | LSP.Message.Notification { method_ = "exit"; params = _ } -> raise Lsp_exit + | LSP.Message.Notification _ -> + (* We can't log before getting the initialize message *) + lsp_init_loop ic ofmt ~cmdline + +(** Dispatching *) +let dispatch_notification ofmt ~state ~method_ ~params = + match method_ with + (* Lifecycle *) + | "exit" -> raise Lsp_exit (* setTrace *) | "$/setTrace" -> do_trace params - (* Proof-specific stuff *) - | "proof/goals" -> do_goals ofmt ~id params - (* Notifications *) + (* Document lifetime *) | "textDocument/didOpen" -> do_open ~state params - | "textDocument/didChange" -> do_change params - | "textDocument/didClose" -> do_close ofmt params - | "textDocument/didSave" -> memo_save_to_disk () - | "exit" -> raise Lsp_exit + | "textDocument/didChange" -> do_change ~ofmt params + | "textDocument/didClose" -> do_close ~ofmt params + | "textDocument/didSave" -> Cache.save_to_disk () + (* Cancel Request *) + | "$/cancelRequest" -> do_cancel ~ofmt ~params (* NOOPs *) - | "initialized" | "workspace/didChangeWatchedFiles" -> () + | "initialized" -> () + (* Generic handler *) | msg -> LIO.trace "no_handler" msg -let dispatch_message ofmt ~state dict = - try dispatch_message ofmt ~state dict with +let dispatch_request ~method_ ~params = + match method_ with + (* Lifecyle *) + | "initialize" -> + LIO.trace "dispatch_request" "duplicate initialize request! Rejecting"; + (* XXX what's the error code here *) + RResult.Error (-32600, "Invalid Request: server already initialized") + | "shutdown" -> do_shutdown ~params + (* Symbols and info about the document *) + | "textDocument/completion" -> do_completion ~params + | "textDocument/documentSymbol" -> do_symbols ~params + | "textDocument/hover" -> do_hover ~params + (* Proof-specific stuff *) + | "proof/goals" -> do_goals ~params + (* Generic handler *) + | msg -> + LIO.trace "no_handler" msg; + Error (-32601, "method not found") + +let dispatch_request ofmt ~id ~method_ ~params = + dispatch_request ~method_ ~params |> answer_request ~ofmt ~id + +let dispatch_message ofmt ~state (com : LSP.Message.t) = + match com with + | Notification { method_; params } -> + dispatch_notification ofmt ~state ~method_ ~params + | Request { id; method_; params } -> + dispatch_request ofmt ~id ~method_ ~params + +let dispatch_message ofmt ~state com = + try dispatch_message ofmt ~state com with | U.Type_error (msg, obj) -> LIO.trace_object msg obj | Lsp_exit -> raise Lsp_exit + | Doc_manager.AbortRequest -> + () (* XXX: Separate requests from notifications, handle this better *) | exn -> + (* Note: We should never arrive here from Coq, as every call to Coq should + be wrapper in Coq.Protect. So hitting this codepath, is effectively a + coq-lsp internal error and should be fixed *) let bt = Printexc.get_backtrace () in let iexn = Exninfo.capture exn in LIO.trace "process_queue" (if Printexc.backtrace_status () then "bt=true" else "bt=false"); - let method_name = string_field "method" dict in + let method_name = LSP.Message.method_ com in LIO.trace "process_queue" ("exn in method: " ^ method_name); LIO.trace "process_queue" (Printexc.to_string exn); LIO.trace "process_queue" Pp.(string_of_ppcmds CErrors.(iprint iexn)); LIO.trace "BT" bt -let rec process_queue ofmt ~state = - if Fleche.Debug.sched_wakeup then - LIO.trace "<- dequeue" (Format.asprintf "%.2f" (Unix.gettimeofday ())); - (match Queue.peek_opt request_queue with - | None -> ( - match !Check.pending with - | Some uri -> - LIO.trace "process_queue" "resuming document checking"; - Control.interrupt := false; - Check.do_check ofmt ~fb_queue:state.State.fb_queue ~uri; - (* Only if completed! *) - if Check.completed uri then Check.pending := None - | None -> Thread.delay 0.1) +(***********************************************************************) +(* The queue strategy is: we keep pending document checks in Doc_manager, they + are only resumed when the rest of requests in the queue are served. + + Note that we should add a method to detect stale requests; maybe cancel them + when a new edit comes. *) + +(** Main event queue *) +let request_queue = Queue.create () + +let dispatch_or_resume_check ofmt ~state = + match Queue.peek_opt request_queue with + | None -> + Control.interrupt := false; + let ready = Check.check_or_yield ~ofmt in + serve_postponed_requests ~ofmt ready | Some com -> - (* TODO we should optimize the queue *) + (* TODO: optimize the queue? *) ignore (Queue.pop request_queue); - let dict = U.to_assoc com in - let m = string_field "method" dict in - LIO.trace "process_queue" ("Serving Request: " ^ m); + LIO.trace "process_queue" ("Serving Request: " ^ LSP.Message.method_ com); (* We let Coq work normally now *) Control.interrupt := false; - dispatch_message ofmt ~state dict); + dispatch_message ofmt ~state com + +let rec process_queue ofmt ~state = + if Fleche.Debug.sched_wakeup then + LIO.trace "<- dequeue" (Format.asprintf "%.2f" (Unix.gettimeofday ())); + dispatch_or_resume_check ofmt ~state; process_queue ofmt ~state -let lsp_cb oc = +let process_input (com : LSP.Message.t) = + if Fleche.Debug.sched_wakeup then + LIO.trace "-> enqueue" (Format.asprintf "%.2f" (Unix.gettimeofday ())); + (* TODO: this is the place to cancel pending requests that are invalid, and in + general, to perform queue optimizations *) + Queue.push com request_queue; + Control.interrupt := true + +(* Main loop *) +let lsp_cb = Fleche.Io.CallBack. { trace = LIO.trace ; send_diagnostics = - (fun ~uri ~version diags -> - lsp_of_diags ~uri ~version diags |> Lsp.Io.send_json oc) + (fun ~ofmt ~uri ~version diags -> + Lsp_util.lsp_of_diags ~uri ~version diags |> Lsp.Io.send_json ofmt) ; send_fileProgress = - (fun ~uri ~version progress -> - lsp_of_progress ~uri ~version progress |> Lsp.Io.send_json oc) + (fun ~ofmt ~uri ~version progress -> + Lsp_util.lsp_of_progress ~uri ~version progress + |> Lsp.Io.send_json ofmt) } let lvl_to_severity (lvl : Feedback.level) = @@ -529,67 +472,66 @@ let add_message lvl loc msg q = let lvl = lvl_to_severity lvl in q := (loc, lvl, msg) :: !q -let mk_fb_handler () = - let q = ref [] in - ( (fun Feedback.{ contents; _ } -> - match contents with - | Message (((Error | Warning | Notice) as lvl), loc, msg) -> - add_message lvl loc msg q - | Message ((Info as lvl), loc, msg) -> - if !Fleche.Config.v.show_coq_info_messages then - add_message lvl loc msg q - else () - | Message (Debug, _loc, _msg) -> () - | _ -> ()) - , q ) - -let log_workspace w = - let message = Coq.Workspace.describe w in - LIO.logMessage ~lvl:3 ~message +let mk_fb_handler q Feedback.{ contents; _ } = + match contents with + | Message (((Error | Warning | Notice) as lvl), loc, msg) -> + add_message lvl loc msg q + | Message ((Info as lvl), loc, msg) -> + if !Fleche.Config.v.show_coq_info_messages then add_message lvl loc msg q + else () + | Message (Debug, _loc, _msg) -> () + | _ -> () + +let coq_init ~fb_queue ~bt = + let fb_handler = mk_fb_handler fb_queue in + let debug = bt || Fleche.Debug.backtraces in + let load_module = Dynlink.loadfile in + let load_plugin = Coq.Loader.plugin_handler None in + Coq.Init.(coq_init { fb_handler; debug; load_module; load_plugin }) let lsp_main bt std coqlib vo_load_path ml_include_path = LSP.std_protocol := std; - Exninfo.record_backtrace true; + (* We output to stdout *) + let ic = stdin in let oc = F.std_formatter in - (* Send a log message *) + (* Set log channel *) LIO.set_log_channel oc; - LIO.logMessage ~lvl:3 ~message:"Server started"; + Fleche.Io.CallBack.set lsp_cb; - Fleche.Io.CallBack.set (lsp_cb oc); + (* IMPORTANT: LSP spec forbids any message from server to client before + initialize is received *) (* Core Coq initialization *) - let fb_handler, fb_queue = mk_fb_handler () in - let debug = bt || Fleche.Debug.backtraces in - let load_module = Dynlink.loadfile in - let load_plugin = Coq.Loader.plugin_handler None in - let root_state = - Coq.Init.(coq_init { fb_handler; debug; load_module; load_plugin }) - in - - (* Workspace initialization *) + let fb_queue = Coq.Protect.fb_queue in + let root_state = coq_init ~fb_queue ~bt in let cmdline = { Coq.Workspace.CmdLine.coqlib; vo_load_path; ml_include_path } in - let workspace = Coq.Workspace.guess ~cmdline in - log_workspace workspace; - (* Core LSP loop context *) - let state = { State.root_state; workspace; fb_queue } in + (* Read JSON-RPC messages and push them to the queue *) + let rec read_loop () = + let msg = read_request ic in + process_input msg; + read_loop () + in + + (* Input/output will happen now *) + try + (* LSP Server server initialization *) + let workspace = lsp_init_loop ic oc ~cmdline in + + (* Core LSP loop context *) + let state = { State.root_state; workspace } in - memo_read_from_disk (); + (* Read workspace state (noop for now) *) + Cache.read_from_disk (); - let (_ : Thread.t) = Thread.create (fun () -> process_queue oc ~state) () in + let (_ : Thread.t) = Thread.create (fun () -> process_queue oc ~state) () in - let rec loop () = - (* XXX: Implement a queue, compact *) - let com = LIO.read_request stdin in - if Fleche.Debug.read then LIO.trace_object "read" com; - process_input com; - loop () - in - try loop () with + read_loop () + with | (LIO.ReadError "EOF" | Lsp_exit) as exn -> let message = "server exiting" @@ -676,7 +618,7 @@ let lsp_cmd : unit Cmd.t = let vo_load_path = term_append [ rload_path; load_path ] in Cmd.( v - (Cmd.info "coq-lsp" ~version:"0.01" ~doc ~man) + (Cmd.info "coq-lsp" ~version:Version.server ~doc ~man) Term.(const lsp_main $ bt $ std $ coqlib $ vo_load_path $ ml_include_path)) let main () = diff --git a/controller/doc_manager.ml b/controller/doc_manager.ml new file mode 100644 index 000000000..ba5ff9a8d --- /dev/null +++ b/controller/doc_manager.ml @@ -0,0 +1,225 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* () + | Some _ -> + LIO.trace "do_open" ("file " ^ uri ^ " not properly closed by client")); + Hashtbl.add doc_table uri + { doc; cp_requests = Int.Set.empty; pt_request = None } + + let close ~uri = Hashtbl.remove doc_table uri + + let find ~uri = + match Hashtbl.find_opt doc_table uri with + | Some h -> h + | None -> + LIO.trace "DocHandle.find" ("file " ^ uri ^ " not available"); + raise AbortRequest + + let find_opt ~uri = Hashtbl.find_opt doc_table uri + let find_doc ~uri = (find ~uri).doc + + let _update_doc ~handle ~(doc : Fleche.Doc.t) = + Hashtbl.replace doc_table doc.uri { handle with doc } + + (* Clear requests *) + let update_doc_version ~(doc : Fleche.Doc.t) = + let invalid_reqs = + match Hashtbl.find_opt doc_table doc.uri with + | None -> Int.Set.empty + | Some { cp_requests; pt_request = Some pt_id; _ } -> + Int.Set.add (fst pt_id) cp_requests + | Some { cp_requests; pt_request = None; _ } -> cp_requests + in + Hashtbl.replace doc_table doc.uri + { doc; cp_requests = Int.Set.empty; pt_request = None }; + invalid_reqs + + let attach_cp_request ~uri ~id = + match Hashtbl.find_opt doc_table uri with + | Some { doc; cp_requests; pt_request } -> + let cp_requests = Int.Set.add id cp_requests in + Hashtbl.replace doc_table uri { doc; cp_requests; pt_request } + | None -> () + + let attach_pt_request ~uri ~id ~point = + match Hashtbl.find_opt doc_table uri with + | Some { doc; cp_requests; pt_request = old_request } -> + let pt_request = Some (id, point) in + Hashtbl.replace doc_table uri { doc; cp_requests; pt_request }; + Option.map (fun (id, _) -> id) old_request + | None -> None + + (* For now only on completion, I think we want check to return the list of + requests that can be served / woken up *) + let do_requests ~doc ~handle = + let handle = { handle with doc } in + match doc.completed with + | Yes _ -> + let pt_id = + match handle.pt_request with + | None -> Int.Set.empty + | Some (id, _) -> Int.Set.singleton id + in + let wake_up = Int.Set.union pt_id handle.cp_requests in + let pt_request = None in + let cp_requests = Int.Set.empty in + ({ handle with cp_requests; pt_request }, wake_up) + | Stopped stop_loc -> + let handle, pt_id = + match handle.pt_request with + | None -> (handle, Int.Set.empty) + | Some (id, (req_line, req_col)) -> + (* XXX: Same code than in doc.ml *) + let stop_line = stop_loc.line_nb_last - 1 in + let stop_col = stop_loc.ep - stop_loc.bol_pos_last in + if + stop_line > req_line || (stop_line = req_line && stop_col >= req_col) + then ({ handle with pt_request = None }, Int.Set.singleton id) + else (handle, Int.Set.empty) + in + (handle, pt_id) + | Failed _ -> (handle, Int.Set.empty) + + (* trigger pending incremental requests *) + let update_doc_info ~handle ~(doc : Fleche.Doc.t) = + let handle, requests = do_requests ~doc ~handle in + Hashtbl.replace doc_table doc.uri handle; + requests +end + +let diags_of_doc doc = + List.concat_map Fleche.Doc.Node.diags doc.Fleche.Doc.nodes + +module Check = struct + let pending = ref None + + let completed ~uri = + let doc = Handle.find_doc ~uri in + match doc.completed with + | Yes _ | Failed _ -> true + | Stopped _ -> false + + (* Notification handling; reply is optional / asynchronous *) + let check ofmt ~uri = + LIO.trace "process_queue" "resuming document checking"; + match Handle.find_opt ~uri with + | Some handle -> + let target_of_pt_handle (_, (l, c)) = Fleche.Doc.Target.Position (l, c) in + let target = + Option.cata target_of_pt_handle Fleche.Doc.Target.End handle.pt_request + in + let doc = Fleche.Doc.check ~ofmt ~target ~doc:handle.doc () in + let requests = Handle.update_doc_info ~handle ~doc in + let diags = diags_of_doc doc in + let diags = + Lsp_util.lsp_of_diags ~uri:doc.uri ~version:doc.version diags + in + LIO.send_json ofmt @@ diags; + (* Only if completed! *) + if completed ~uri then pending := None; + requests + | None -> + LIO.trace "Check.check" ("file " ^ uri ^ " not available"); + Int.Set.empty + + let check_or_yield ~ofmt = + match !pending with + | None -> + Thread.delay 0.1; + Int.Set.empty + | Some uri -> check ofmt ~uri + + let schedule ~uri = pending := Some uri +end + +let create ~root_state ~workspace ~uri ~contents ~version = + let r = + Fleche.Doc.create ~state:root_state ~workspace ~uri ~contents ~version + in + match r with + | Completed (Result.Ok doc) -> + Handle.create ~uri ~doc; + Check.schedule ~uri + | Completed (Result.Error (Anomaly (_, msg))) + | Completed (Result.Error (User (_, msg))) -> + (* For now we inform the user of the problem, we could be finer and create a + ghost node for the implicit import, but we will phase that out in Coq + upstream at some point. *) + let message = + Format.asprintf "Fleche.Doc.create, internal error: @[%a@]" Pp.pp_with msg + in + LIO.logMessage ~lvl:1 ~message + | Interrupted -> () + +(* Can't wait for the day this goes away *) +let tainted = ref false + +let create ~root_state ~workspace ~uri ~contents ~version = + if !tainted then + (* Warn about Coq bug *) + let message = + "You have opened two or more Coq files simultaneously in the server\n\ + Unfortunately Coq's parser doesn't properly support that setup yet\n\ + If you see some strange parsing errors please close all files but one\n\ + Then restart the coq-lsp server; sorry for the inconveniencies" + in + LIO.logMessage ~lvl:2 ~message + else tainted := true; + create ~root_state ~workspace ~uri ~contents ~version + +let change ~uri ~version ~contents = + let doc = Handle.find_doc ~uri in + if version > doc.version then ( + LIO.trace "bump file" (uri ^ " / version: " ^ string_of_int version); + let tb = Unix.gettimeofday () in + let doc = Fleche.Doc.bump_version ~version ~contents doc in + let diff = Unix.gettimeofday () -. tb in + LIO.trace "bump file took" (Format.asprintf "%f" diff); + let invalid_reqs = Handle.update_doc_version ~doc in + Check.schedule ~uri; + invalid_reqs) + else + (* That's a weird case, get got changes without a version bump? Do nothing + for now *) + Int.Set.empty + +let close = Handle.close +let find_doc = Handle.find_doc +let serve_on_completion ~uri ~id = Handle.attach_cp_request ~uri ~id +let serve_if_point ~uri ~id ~point = Handle.attach_pt_request ~uri ~id ~point diff --git a/controller/doc_manager.mli b/controller/doc_manager.mli new file mode 100644 index 000000000..8bfbe5d2d --- /dev/null +++ b/controller/doc_manager.mli @@ -0,0 +1,51 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* Int.Set.t +end + +(** Create a document *) +val create : + root_state:Coq.State.t + -> workspace:Coq.Workspace.t + -> uri:string + -> contents:string + -> version:int + -> unit + +(** Update a document, returns the list of not valid requests *) +val change : uri:string -> version:int -> contents:string -> Int.Set.t + +(** Close a document *) +val close : uri:string -> unit + +exception AbortRequest + +(** [find_doc ~uri] , raises AbortRequest if [uri] is invalid *) +val find_doc : uri:string -> Fleche.Doc.t + +(** Add a request to be served when the document is completed *) +val serve_on_completion : uri:string -> id:int -> unit + +(** Add a request to be served when the document point data is available, for + now, we allow a single request like that. Maybe returns the id of the + previous request which should now be cancelled. *) +val serve_if_point : uri:string -> id:int -> point:int * int -> int option diff --git a/controller/dune b/controller/dune index e4f264226..e379444f6 100644 --- a/controller/dune +++ b/controller/dune @@ -1,6 +1,6 @@ (executable (name coq_lsp) - (modules coq_lsp) + (modules version cache requests lsp_util doc_manager coq_lsp) (public_name coq-lsp) (preprocess (staged_pps ppx_import ppx_deriving_yojson)) diff --git a/controller/lsp_util.ml b/controller/lsp_util.ml new file mode 100644 index 000000000..a64fca087 --- /dev/null +++ b/controller/lsp_util.ml @@ -0,0 +1,40 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* + (range, severity, message, None)) + diags + |> Lsp.Base.mk_diagnostics ~uri ~version + +let lsp_of_progress ~uri ~version progress = + let progress = + List.map + (fun (range, kind) -> + `Assoc [ ("range", LSP.mk_range range); ("kind", `Int kind) ]) + progress + in + let params = + [ ( "textDocument" + , `Assoc [ ("uri", `String uri); ("version", `Int version) ] ) + ; ("processing", `List progress) + ] + in + LSP.mk_notification ~method_:"$/coq/fileProgress" ~params diff --git a/controller/lsp_util.mli b/controller/lsp_util.mli new file mode 100644 index 000000000..b082e5e4b --- /dev/null +++ b/controller/lsp_util.mli @@ -0,0 +1,25 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* version:int -> Fleche.Types.Diagnostic.t list -> Yojson.Safe.t + +val lsp_of_progress : + uri:string + -> version:int + -> (Fleche.Types.Range.t * int) list + -> Yojson.Safe.t diff --git a/controller/requests.ml b/controller/requests.ml new file mode 100644 index 000000000..9c20090c4 --- /dev/null +++ b/controller/requests.ml @@ -0,0 +1,133 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* Yojson.Safe.t +type position_request = doc:Fleche.Doc.t -> point:int * int -> Yojson.Safe.t + +module Util = struct + let asts_of_doc doc = List.filter_map Fleche.Doc.Node.ast doc.Fleche.Doc.nodes +end + +let mk_syminfo file (name, _path, kind, pos) : Yojson.Safe.t = + `Assoc + [ ("name", `String name) + ; ("kind", `Int kind) + ; (* function *) + ( "location" + , `Assoc + [ ("uri", `String file) + ; ("range", Lsp.Base.mk_range Fleche.Types.(to_range pos)) + ] ) + ] + +let _kind_of_type _tm = 13 +(* let open Terms in let open Timed in let is_undef = option_empty !(tm.sym_def) + && List.length !(tm.sym_rules) = 0 in match !(tm.sym_type) with | Vari _ -> + 13 (* Variable *) | Type | Kind | Symb _ | _ when is_undef -> 14 (* Constant + *) | _ -> 12 (* Function *) *) + +let symbols ~(doc : Fleche.Doc.t) = + let uri = doc.uri in + let f loc id = mk_syminfo uri (Names.Id.to_string id, "", 12, loc) in + let ast = Util.asts_of_doc doc in + let slist = Coq.Ast.grab_definitions f ast in + `List slist + +let hover ~doc ~point = + let show_loc_info = true in + let loc_span = Fleche.Info.LC.loc ~doc ~point Exact in + let loc_string = + Option.map Coq.Ast.pr_loc loc_span |> Option.default "no ast" + in + let stats = doc.stats in + let info_string = + Fleche.Info.LC.info ~doc ~point Exact + |> Option.map (Fleche.Doc.Node.Info.print ~stats) + |> Option.default "no info" + in + let hover_string = + if show_loc_info then loc_string ^ "\n___\n" ^ info_string else info_string + in + `Assoc + ([ ( "contents" + , `Assoc + [ ("kind", `String "markdown"); ("value", `String hover_string) ] ) + ] + @ Option.cata + (fun loc -> + [ ("range", Lsp.Base.mk_range (Fleche.Types.to_range loc)) ]) + [] loc_span) + +(* Replace by ppx when we can print goals properly in the client *) +let mk_hyp { Coq.Goals.names; def = _; ty } : Yojson.Safe.t = + let names = List.map (fun id -> `String (Names.Id.to_string id)) names in + let ty = Pp.string_of_ppcmds ty in + `Assoc [ ("names", `List names); ("ty", `String ty) ] + +let mk_goal { Coq.Goals.info = _; ty; hyps } : Yojson.Safe.t = + let ty = Pp.string_of_ppcmds ty in + `Assoc [ ("ty", `String ty); ("hyps", `List (List.map mk_hyp hyps)) ] + +let mk_goals { Coq.Goals.goals; stack = _; bullet = _; shelf; given_up } = + `Assoc + [ ("goals", `List (List.map mk_goal goals)) + ; ("stack", `Null) + ; ("bullet", `Null) + ; ("shelf", `List (List.map mk_goal shelf)) + ; ("given_up", `List (List.map mk_goal given_up)) + ] + +let mk_goals = Option.cata mk_goals `Null +let mk_message (_loc, _lvl, msg) = `String (Pp.string_of_ppcmds msg) +let mk_messages m = List.map mk_message m +let mk_messages = Option.cata mk_messages [] + +let mk_error node = + let open Fleche in + let open Fleche.Types in + match + List.filter (fun d -> d.Diagnostic.severity < 2) node.Doc.Node.diags + with + | [] -> [] + | e :: _ -> [ ("error", `String e.Diagnostic.message) ] + +let goals_mode = + if !Fleche.Config.v.goal_after_tactic then Fleche.Info.PrevIfEmpty + else Fleche.Info.Prev + +let goals ~doc ~point = + let open Fleche in + let goals = Info.LC.goals ~doc ~point goals_mode in + let node = Info.LC.node ~doc ~point Exact in + let messages = Option.map Doc.Node.messages node in + let error = Option.cata mk_error [] node in + `Assoc + ([ ( "textDocument" + , `Assoc [ ("uri", `String doc.uri); ("version", `Int doc.version) ] ) + ; ( "position" + , `Assoc [ ("line", `Int (fst point)); ("character", `Int (snd point)) ] + ) + ; ("goals", mk_goals goals) + ; ("messages", `List (mk_messages messages)) + ] + @ error) + +let completion ~doc ~point:_ = + let f _loc id = `Assoc [ ("label", `String Names.Id.(to_string id)) ] in + let ast = Util.asts_of_doc doc in + let clist = Coq.Ast.grab_definitions f ast in + `List clist diff --git a/controller/requests.mli b/controller/requests.mli new file mode 100644 index 000000000..427383429 --- /dev/null +++ b/controller/requests.mli @@ -0,0 +1,24 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* Yojson.Safe.t +type position_request = doc:Fleche.Doc.t -> point:int * int -> Yojson.Safe.t + +val symbols : document_request +val hover : position_request +val goals : position_request +val completion : position_request diff --git a/controller/version.ml b/controller/version.ml new file mode 100644 index 000000000..b8646e478 --- /dev/null +++ b/controller/version.ml @@ -0,0 +1,17 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* " + "Ali Caglayan " + "Shachar Itzhaky " + "Ramkumar Ramachandra " ] license: "LGPL-2.1-or-later" doc: "https://ejgallego.github.io/coq-lsp/" @@ -18,14 +21,14 @@ depends: [ "ocaml" { >= "4.12.0" } "dune" { >= "3.2" } + # lsp dependencies + "cmdliner" { >= "1.1.0" } + "yojson" { >= "1.7.0" } + # Not yet required, install Coq deps instead "coq" { >= "8.16.0" & < "8.17" } "coq-serapi" { >= "8.16.2" & < "8.17" } "camlp-streams" { >= "5.0" } - - # lsp dependencies - "cmdliner" { >= "1.1.0" } - "yojson" { >= "1.7.0" } ] build: [ [ "dune" "build" "-p" name "-j" jobs ] ] diff --git a/coq/ast.ml b/coq/ast.ml index 91baf3d6f..3c1b3011c 100644 --- a/coq/ast.ml +++ b/coq/ast.ml @@ -86,6 +86,6 @@ let pr_loc ?(print_file = false) loc = else "loc" in Format.asprintf "%s: line: %d, col: %d -- line: %d, col: %d / {%d-%d}" file - loc.line_nb (loc.bp - loc.bol_pos) loc.line_nb_last + (loc.line_nb - 1) (loc.bp - loc.bol_pos) (loc.line_nb_last - 1) (loc.ep - loc.bol_pos_last) loc.bp loc.ep diff --git a/coq/dune b/coq/dune index 524f96a94..07b7f5424 100644 --- a/coq/dune +++ b/coq/dune @@ -3,4 +3,4 @@ (public_name coq-lsp.coq) ; Unfortunate we have to link the STM due to the LTAC plugin ; depending on it, we should fix this upstream - (libraries coq-core.vernac coq-core.stm coq-serapi.serlib)) + (libraries coq-core.vernac coq-core.stm coq-serapi.serlib camlp-streams)) diff --git a/coq/goals.ml b/coq/goals.ml index 40ede8e11..50577da87 100644 --- a/coq/goals.ml +++ b/coq/goals.ml @@ -50,6 +50,7 @@ type cdcl = Constr.compacted_declaration let to_tuple ppx : cdcl -> 'pc hyp = let open CDC in + let ppx t = ppx (EConstr.of_constr t) in function | LocalAssum (idl, tm) -> { names = List.map Context.binder_name idl; def = None; ty = ppx tm } @@ -60,16 +61,15 @@ let to_tuple ppx : cdcl -> 'pc hyp = } (** gets a hypothesis *) -let get_hyp (ppx : Constr.t -> 'pc) (_sigma : Evd.evar_map) (hdecl : cdcl) : +let get_hyp (ppx : EConstr.t -> 'pc) (_sigma : Evd.evar_map) (hdecl : cdcl) : 'pc hyp = to_tuple ppx hdecl (** gets the constr associated to the type of the current goal *) -let get_goal_type (ppx : Constr.t -> 'pc) (sigma : Evd.evar_map) (g : Evar.t) : +let get_goal_type (ppx : EConstr.t -> 'pc) (sigma : Evd.evar_map) (g : Evar.t) : _ = - ppx - @@ EConstr.to_constr ~abort_on_undefined_evars:false sigma - Evd.(evar_concl (find sigma g)) + let evi = Evd.find sigma g in + ppx Evd.(evar_concl evi) let build_info sigma g = { evar = g; name = Evd.evar_ident g sigma } @@ -86,30 +86,20 @@ let process_goal_gen ppx sigma g : 'a reified_goal = let info = build_info sigma g in { info; ty = get_goal_type ppx sigma g; hyps } -(* let if_not_empty (pp : Pp.t) = if Pp.(repr pp = Ppcmd_empty) then None else - Some pp *) - -let pr_hyp (h : _ hyp) = - let { names; ty; def = _ } = h in - Pp.(prlist Names.Id.print names ++ str " : " ++ ty) - -let pr_hyps hyps = - Pp.( - pr_vertical_list pr_hyp hyps - ++ fnl () - ++ str "============================================" - ++ fnl ()) - -let pr_goal ~hyps (g : _ reified_goal) = - let hyps = if hyps then pr_hyps g.hyps else Pp.mt () in - Pp.(hyps ++ g.ty) - -let pp_goals (g : _ goals) = - let { goals; stack = _; bullet = _; shelf = _; given_up = _ } = g in - match goals with - | [] -> Pp.str "No goals left" - | g :: gs -> - Pp.( - v 0 (pr_goal ~hyps:true g) - ++ cut () - ++ prlist_with_sep cut (pr_goal ~hyps:false) gs) +let if_not_empty (pp : Pp.t) = + if Pp.(repr pp = Ppcmd_empty) then None else Some pp + +let reify ~ppx lemmas = + let lemmas = State.Proof.to_coq lemmas in + let proof = + Vernacstate.LemmaStack.with_top lemmas ~f:(fun pstate -> + Declare.Proof.get pstate) + in + let { Proof.goals; stack; sigma; _ } = Proof.data proof in + let ppx = List.map (process_goal_gen ppx sigma) in + { goals = ppx goals + ; stack = List.map (fun (g1, g2) -> (ppx g1, ppx g2)) stack + ; bullet = if_not_empty @@ Proof_bullet.suggest proof + ; shelf = Evd.shelf sigma |> ppx + ; given_up = Evd.given_up sigma |> Evar.Set.elements |> ppx + } diff --git a/coq/goals.mli b/coq/goals.mli index 7c22bb5f3..e49af19a0 100644 --- a/coq/goals.mli +++ b/coq/goals.mli @@ -40,13 +40,10 @@ type 'a goals = ; given_up : 'a list } -(** Stm-independent goal processor *) -val process_goal_gen : - (Environ.env -> Evd.evar_map -> Constr.t -> 'a) - -> Evd.evar_map - -> Evar.t - -> 'a reified_goal - type reified_pp = Pp.t reified_goal goals -val pp_goals : reified_pp -> Pp.t +(** Stm-independent goal processor *) +val reify : + ppx:(Environ.env -> Evd.evar_map -> EConstr.t -> 'a) + -> State.Proof.t + -> 'a reified_goal goals diff --git a/coq/init.ml b/coq/init.ml index 3c1d2ec63..09462b026 100644 --- a/coq/init.ml +++ b/coq/init.ml @@ -73,7 +73,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); @@ -84,3 +84,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..a5603838f 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.E.t diff --git a/coq/interp.ml b/coq/interp.ml index 784bbb1ae..f74c84fcc 100644 --- a/coq/interp.ml +++ b/coq/interp.ml @@ -16,52 +16,17 @@ (************************************************************************) module Info = struct - type 'a t = - { res : 'a - ; feedback : Message.t list - } + type 'a t = { res : 'a } end -let get_feedback fb_queue = - let res = !fb_queue in - fb_queue := []; - res - -type 'a interp_result = 'a Info.t Protect.R.t +type 'a interp_result = 'a Info.t Protect.E.t let coq_interp ~st cmd = let st = State.to_coq st in let cmd = Ast.to_coq cmd in Vernacinterp.interp ~st cmd |> State.of_coq -let interp ~st ~fb_queue cmd = +let interp ~st cmd = Protect.eval cmd ~f:(fun cmd -> let res = coq_interp ~st cmd in - (* It is safe to call the printer here as the state is guaranteed to be - the right one after `coq_interp`, but beware! *) - let feedback = List.rev @@ get_feedback fb_queue in - { Info.res; feedback }) - -let marshal_out f oc res = - match res with - | Protect.R.Interrupted -> () - | Protect.R.Completed res -> ( - match res with - | Ok res -> - Marshal.to_channel oc 0 []; - f oc res.Info.res - | Error (loc, msg) -> - Marshal.to_channel oc 1 []; - 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)) + { Info.res }) diff --git a/coq/interp.mli b/coq/interp.mli index 3cf11a2a0..5b37fa927 100644 --- a/coq/interp.mli +++ b/coq/interp.mli @@ -16,18 +16,9 @@ (************************************************************************) module Info : sig - type 'a t = - { res : 'a - ; feedback : Message.t list - } + type 'a t = { res : 'a } end -type 'a interp_result = 'a Info.t Protect.R.t +type 'a interp_result = 'a Info.t Protect.E.t -val interp : - st:State.t -> fb_queue:Message.t list ref -> Ast.t -> State.t interp_result - -val marshal_in : (in_channel -> 'a) -> in_channel -> 'a interp_result - -val marshal_out : - (out_channel -> 'a -> unit) -> out_channel -> 'a interp_result -> unit +val interp : st:State.t -> Ast.t -> State.t interp_result diff --git a/coq/loader.ml b/coq/loader.ml index ae5359fdc..7f0e60a4e 100644 --- a/coq/loader.ml +++ b/coq/loader.ml @@ -22,13 +22,19 @@ let list_last l = List.(nth l (length l - 1)) let map_serlib fl_pkg = let supported = match fl_pkg with (* Supported by serlib *) (* directory *) - | "coq-core.plugins.ltac" (* ltac *) + | "coq-core.plugins.cc" (* cc *) + | "coq-core.plugins.extraction" (* extraction *) | "coq-core.plugins.firstorder" (* firstorder *) | "coq-core.plugins.funind" (* funind *) + | "coq-core.plugins.ltac" (* ltac *) + | "coq-core.plugins.ltac2" (* ltac2 *) + | "coq-core.plugins.micromega" (* micromega *) | "coq-core.plugins.ring" (* ring *) - | "coq-core.plugins.extraction" (* extraction *) + | "coq-core.plugins.ssreflect" (* ssreflect *) | "coq-core.plugins.ssrmatching" (* ssrmatching *) - | "coq-core.plugins.ssreflect" (* ssr *) + | "coq-core.plugins.number_string_notation" (* syntax *) + | "coq-core.plugins.tauto" (* tauto *) + | "coq-core.plugins.zify" (* zify *) -> true | _ -> Feedback.msg_warning Pp.(str "Missing serlib plugin: " ++ str fl_pkg); diff --git a/coq/parsing.ml b/coq/parsing.ml new file mode 100644 index 000000000..ae26a3c48 --- /dev/null +++ b/coq/parsing.ml @@ -0,0 +1,59 @@ +let bp_ = ref 0 +let undamage_jf loc = + Loc. + { loc with + bol_pos = loc.bol_pos - !bp_ + ; bp = loc.bp - !bp_ + ; ep = loc.ep - !bp_ + } + +let undamage_jf_opt loc = Option.map undamage_jf loc + +module PCoqHack = struct + type t = + { pa_tok_strm : Tok.t LStream.t + ; lexer_state : CLexer.Lexer.State.t ref + } + + let loc (p : Pcoq.Parsable.t) : Loc.t = + let p : t = Obj.magic p in + LStream.current_loc p.pa_tok_strm |> undamage_jf +end + +module Parsable = struct + include Pcoq.Parsable + let loc = PCoqHack.loc +end + +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 (fun { CAst.loc; v } -> + CAst.make ?loc:(undamage_jf_opt loc) v) + |> Option.map Ast.of_coq + +let parse ~st ps = Protect.eval ~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 = + (* type 'a parser_fun = { parser_fun : te LStream.t -> 'a } *) + let rec dot st = + match LStream.next st with + | Tok.KEYWORD ("." | "..." | "Qed" | "Defined" | "Admitted") | Tok.BULLET _ + -> () + | Tok.EOI -> () + | _ -> dot st + in + Pcoq.Entry.of_parser "Coqtoplevel.dot" { parser_fun = dot } + +(* If an error occurred while parsing, we try to read the input until a dot + token is encountered. We assume that when a lexer error occurs, at least one + char was eaten *) +let rec discard_to_dot ps = + try Pcoq.Entry.parse parse_to_terminator ps with + | CLexer.Error.E _ -> discard_to_dot ps + | e when CErrors.noncritical e -> () diff --git a/coq/parsing.mli b/coq/parsing.mli new file mode 100644 index 000000000..87343c474 --- /dev/null +++ b/coq/parsing.mli @@ -0,0 +1,11 @@ +module Parsable : sig + type t + + val make : ?loc:Loc.t -> char Stream.t -> t + val loc : t -> Loc.t +end + +val parse : st:State.t -> Parsable.t -> Ast.t option Protect.E.t +val discard_to_dot : Parsable.t -> unit + +val bp_ : int ref diff --git a/coq/print.ml b/coq/print.ml new file mode 100644 index 000000000..ac4bf3a99 --- /dev/null +++ b/coq/print.ml @@ -0,0 +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 f = pr_letype_env ~goal_concl_style env sigma in + Protect.eval ~f x diff --git a/coq/print.mli b/coq/print.mli new file mode 100644 index 000000000..dec808c32 --- /dev/null +++ b/coq/print.mli @@ -0,0 +1,6 @@ +val pr_letype_env : + goal_concl_style:bool + -> Environ.env + -> Evd.evar_map + -> EConstr.t + -> Pp.t Protect.E.t diff --git a/coq/protect.ml b/coq/protect.ml index cd3b2b619..e3cf04c1b 100644 --- a/coq/protect.ml +++ b/coq/protect.ml @@ -1,15 +1,36 @@ +module Error = struct + 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 type 'a t = - | Completed of ('a, Loc.t option * Pp.t) result + | Completed of ('a, Error.t) result | Interrupted (* signal sent, eval didn't complete *) -end -let map_loc ~f = function - | R.Completed (Error (loc, msg)) -> - R.Completed (Error (Option.map f loc, msg)) - | res -> res + let map ~f = function + | Completed (Result.Ok r) -> Completed (Result.Ok (f r)) + | Completed (Result.Error r) -> Completed (Result.Error r) + | Interrupted -> Interrupted -let eval ~f x = + let map_error ~f = function + | Completed (Error e) -> Completed (Error (Error.map ~f e)) + | res -> res + + let map_loc ~f = + let f (loc, msg) = (Option.map f loc, msg) in + map_error ~f +end + +(* Eval and reify exceptions *) +let eval_exn ~f x = try let res = f x in R.Completed (Ok res) @@ -19,4 +40,27 @@ 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))) + +module E = struct + type 'a t = + { r : 'a R.t + ; feedback : Message.t list + } + + let map ~f { r; feedback } = { r = R.map ~f r; feedback } + let map_message ~f (loc, lvl, msg) = (Option.map f loc, lvl, msg) + + let map_loc ~f { r; feedback } = + { r = R.map_loc ~f r; feedback = List.map (map_message ~f) feedback } +end + +let fb_queue : Message.t list ref = ref [] + +(* Eval with reified exceptions and feedback *) +let eval ~f x = + let r = eval_exn ~f x in + let feedback = List.rev !fb_queue in + let () = fb_queue := [] in + { E.r; feedback } diff --git a/coq/protect.mli b/coq/protect.mli index 4b9b8ee74..c477da339 100644 --- a/coq/protect.mli +++ b/coq/protect.mli @@ -1,11 +1,43 @@ +(** This modules reifies Coq side effects into an algebraic structure. + + This is obviously very convenient for upper layer programming. + + As of today this includes feedback and exceptions. *) +module Error : sig + type payload = Loc.t option * Pp.t + + type t = private + | User of payload + | Anomaly of payload +end + module R : sig - type 'a t = - | Completed of ('a, Loc.t option * Pp.t) result + 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.payload -> Error.payload) -> 'a t -> 'a t + + (** Update the loc stored in the result, this is used by our cache-aware + location *) + val map_loc : f:(Loc.t -> Loc.t) -> 'a t -> 'a t +end + +module E : sig + type 'a t = + { r : 'a R.t + ; feedback : Message.t list + } + + val map : f:('a -> 'b) -> 'a t -> 'b t + val map_loc : f:(Loc.t -> Loc.t) -> 'a t -> 'a t end -val eval : f:('i -> 'o) -> 'i -> 'o R.t +(** Must be hooked to allow [Protect] to capture the feedback. *) +val fb_queue : Message.t list ref -(** Update the loc stored in the result, this is used by our cache-aware - location *) -val map_loc : f:(Loc.t -> Loc.t) -> 'a R.t -> 'a R.t +(** 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 E.t diff --git a/coq/state.ml b/coq/state.ml index 368ccdd4c..01ea22a36 100644 --- a/coq/state.ml +++ b/coq/state.ml @@ -75,11 +75,14 @@ let mode ~st = st.Vernacstate.lemmas 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 +module Proof = struct + type t = Vernacstate.LemmaStack.t + + let to_coq x = x +end + +let lemmas ~st = st.Vernacstate.lemmas let drop_proofs ~st = let open Vernacstate in @@ -88,6 +91,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 +109,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) () *) diff --git a/coq/state.mli b/coq/state.mli index d1fbea864..1e2baa5b5 100644 --- a/coq/state.mli +++ b/coq/state.mli @@ -1,19 +1,32 @@ type t -val marshal_in : in_channel -> t -val marshal_out : out_channel -> t -> unit -val of_coq : Vernacstate.t -> t -val to_coq : t -> Vernacstate.t val compare : t -> t -> int val equal : t -> t -> bool 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 + +(** Proof states *) +module Proof : sig + type t + + val to_coq : t -> Vernacstate.LemmaStack.t +end + +val lemmas : st:t -> Proof.t option + +(** 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.E.t (** Drop the proofs from the state *) val drop_proofs : st:t -> t (** Admit an ongoing proof *) val admit : st:t -> t + +(* Extra *) +val marshal_in : in_channel -> t +val marshal_out : out_channel -> t -> unit +val of_coq : Vernacstate.t -> t +val to_coq : t -> Vernacstate.t diff --git a/coq/workspace.ml b/coq/workspace.ml index a27df975d..63dd12fc7 100644 --- a/coq/workspace.ml +++ b/coq/workspace.ml @@ -16,7 +16,8 @@ (************************************************************************) type t = - { vo_load_path : Loadpath.vo_path list + { coqlib : string + ; vo_load_path : Loadpath.vo_path list ; ml_include_path : string list ; require_libs : (string * string option * Vernacexpr.export_with_cats option) list @@ -38,7 +39,8 @@ let default ~implicit ~coqlib ~kind = let coq_root = Names.DirPath.make [ Libnames.coq_root ] in let default_root = Libnames.default_root_prefix in let require_libs = [ ("Coq.Init.Prelude", None, Some (Lib.Import, None)) ] in - { vo_load_path = + { coqlib + ; vo_load_path = [ mk_lp ~ml:false ~root:coq_root ~implicit ~dir:"theories" ; mk_lp ~ml:true ~root:default_root ~implicit:false ~dir:"user-contrib" ] @@ -57,17 +59,33 @@ let add_loadpaths base ~vo_load_path ~ml_include_path = ; ml_include_path = base.ml_include_path @ ml_include_path } -let describe { kind; vo_load_path; ml_include_path; require_libs; _ } = +let pp_load_path fmt + { Loadpath.unix_path; coq_path; implicit = _; has_ml = _; recursive = _ } = + Format.fprintf fmt "Path %s ---> %s" + (Names.DirPath.to_string coq_path) + unix_path + +let describe { coqlib; kind; vo_load_path; ml_include_path; require_libs; _ } = let require_msg = String.concat " " (List.map (fun (s, _, _) -> s) require_libs) in let n_vo = List.length vo_load_path in let n_ml = List.length ml_include_path in - Format.asprintf - "@[Configuration loaded from %s@\n\ - - Modules [%s] will be loaded by default; %d Coq path directory bindings \ - in scope; %d Coq plugin directory bindings in scope@]" - kind require_msg n_vo n_ml + let extra = + Format.asprintf "@[vo_paths:@\n @[%a@]@\nml_paths:@\n @[%a@]@]" + (Format.pp_print_list pp_load_path) + vo_load_path + Format.(pp_print_list pp_print_string) + ml_include_path + in + ( Format.asprintf + "@[Configuration loaded from %s@\n\ + \ - coqlib is at: %s@\n\ + \ - Modules [%s] will be loaded by default@\n\ + \ - %d Coq path directory bindings in scope; %d Coq plugin directory \ + bindings in scope@]" + kind coqlib require_msg n_vo n_ml + , extra ) let rec parse_args args init w = match args with @@ -94,7 +112,8 @@ let load_objs libs = (* NOTE: Use exhaustive match below to avoid bugs by skipping fields *) let apply ~libname - { vo_load_path + { coqlib = _ + ; vo_load_path ; ml_include_path ; require_libs ; indices_matter diff --git a/coq/workspace.mli b/coq/workspace.mli index acc3940af..5e6198643 100644 --- a/coq/workspace.mli +++ b/coq/workspace.mli @@ -16,7 +16,8 @@ (************************************************************************) type t = private - { vo_load_path : Loadpath.vo_path list + { coqlib : string + ; vo_load_path : Loadpath.vo_path list ; ml_include_path : string list ; require_libs : (string * string option * Vernacexpr.export_with_cats option) list @@ -25,7 +26,8 @@ type t = private ; kind : string (** How was the workspace built *) } -val describe : t -> string +(** user message, debug extra data *) +val describe : t -> string * string module CmdLine : sig type t = diff --git a/editor/code/CHANGELOG.md b/editor/code/CHANGELOG.md index e97b4affc..c03d8a7b5 100644 --- a/editor/code/CHANGELOG.md +++ b/editor/code/CHANGELOG.md @@ -1,5 +1,5 @@ -# coq-lsp 0.1.2: ----------------- +# coq-lsp 0.1.2: Message +------------------------ - Requires coq-lsp server 0.1.2, see full changelog at https://github.com/ejgallego/coq-lsp/releases/tag/0.1.2 @@ -7,6 +7,7 @@ - The Coq LSP server output window will now show trace information - Coq Info Panel will now show messages coming from commands such as `About` or `Search` +- Coq Info Panel will now show detailed error information. # coq-lsp 0.1.1: Location ------------------------- diff --git a/editor/code/README.md b/editor/code/README.md index 9ac797f44..cb2c7649d 100644 --- a/editor/code/README.md +++ b/editor/code/README.md @@ -1,12 +1,34 @@ -# Coq LSP VSCode client +# Welcome to coq-lsp, a Language Server Protocol-based extension for the Coq Interactive Proof Assistant -This is an experimental, pure-LSP client for Coq. +`coq-lsp` aims to provide a modern and streamlined experience for +VSCode users, relying on the new [coq-lsp language +server](https://github.com/ejgallego/coq-lsp). -You will need to install the server: +The server provides many nice features such as incremental checking, +advanced error recovery, document information, ... See the server +documentation for more information. + +## Features + +The `coq-lsp` VSCode extension relies on the standard VSCode LSP +client by Microsoft, with 2 main addons: + +- information / goal panel: this will display goals, messages, and + errors at point. It does also support client-side rendering. By + default, Cmd-Enter and mouse click will enable the panel for the + current point. +- document checking progress, using the right lane decoration. + +See the extension configuration options for more information. + +## How to install the server: + +To install the server please do: ``` opam install coq-lsp ``` -Only Linux and OSX are supported for now; Windows support is hopefully -coming soon. +The server should also appear in the Coq Platform, and likely by other +channels. + diff --git a/editor/code/package-lock.json b/editor/code/package-lock.json index c99edfe63..95a744510 100644 --- a/editor/code/package-lock.json +++ b/editor/code/package-lock.json @@ -1,12 +1,12 @@ { "name": "coq-lsp", - "version": "0.1.2", + "version": "0.1.3", "lockfileVersion": 2, "requires": true, "packages": { "": { "name": "coq-lsp", - "version": "0.1.2", + "version": "0.1.3", "dependencies": { "throttle-debounce": "^5.0.0", "vscode-languageclient": "^8.0.2" diff --git a/editor/code/package.json b/editor/code/package.json index 3659bc297..479ede979 100644 --- a/editor/code/package.json +++ b/editor/code/package.json @@ -2,7 +2,7 @@ "name": "coq-lsp", "displayName": "coq-lsp", "description": "Coq LSP provides native vsCode support for checking Coq proof documents", - "version": "0.1.2", + "version": "0.1.3", "contributors": [ "Emilio Jesús Gallego Arias ", "Ali Caglayan ", @@ -131,17 +131,19 @@ }, "coq-lsp.show_goals_on": { "type": "number", - "default": 1, + "default": 3, "description": "When to show goals and information about the current cursor", "enum": [ 0, 1, - 2 + 2, + 3 ], "enumItemLabels": [ "Don't follow cursor", "Show on click", - "Show on click and on cursor movement" + "Show on click and on cursor movement", + "Show on click, cursor, and command movement" ] }, "coq-lsp.admit_on_bad_qed": { diff --git a/editor/code/src/client.ts b/editor/code/src/client.ts index 87c3ce3d3..7a80c54a3 100644 --- a/editor/code/src/client.ts +++ b/editor/code/src/client.ts @@ -25,6 +25,7 @@ enum ShowGoalsOnCursorChange { Never = 0, OnMouse = 1, OnMouseAndKeyboard = 2, + OnMouseKeyboardCommand = 3, } interface CoqLspServerConfig { @@ -154,9 +155,10 @@ export function activate(context: ExtensionContext): void { const goals = (editor: TextEditor) => { checkPanelAlive(); let uri = editor.document.uri; + let version = editor.document.version; let position = editor.selection.active; if (goalPanel) { - goalPanel.update(uri, position); + goalPanel.update(uri, version, position); } }; @@ -164,13 +166,18 @@ export function activate(context: ExtensionContext): void { (evt: vscode.TextEditorSelectionChangeEvent) => { if (evt.textEditor.document.languageId != "coq") return; - const show = - (evt.kind == vscode.TextEditorSelectionChangeKind.Keyboard && - config.show_goals_on == ShowGoalsOnCursorChange.OnMouseAndKeyboard) || - (evt.kind == vscode.TextEditorSelectionChangeKind.Mouse && - (config.show_goals_on == ShowGoalsOnCursorChange.OnMouse || - config.show_goals_on == - ShowGoalsOnCursorChange.OnMouseAndKeyboard)); + const kind = + evt.kind == vscode.TextEditorSelectionChangeKind.Mouse + ? 1 + : evt.kind == vscode.TextEditorSelectionChangeKind.Keyboard + ? 2 + : evt.kind + ? evt.kind + : 3; + // When evt.kind is null, it often means it was due to an + // edit, we want to re-trigger in that case + + const show = kind <= config.show_goals_on; if (show) { goals(evt.textEditor); diff --git a/editor/code/src/goals.ts b/editor/code/src/goals.ts index d8c63056d..c0254411f 100644 --- a/editor/code/src/goals.ts +++ b/editor/code/src/goals.ts @@ -17,14 +17,21 @@ interface Goal { } interface GoalRequest { - textDocument: TextDocumentIdentifier; + textDocument: VersionedTextDocumentIdentifier; position: Position; } +interface GoalConfig { + goals: Goal[]; + stack: undefined; + bullet?: string; + shelf: Goal[]; + given_up: Goal[]; +} interface GoalAnswer { textDocument: VersionedTextDocumentIdentifier; position: Position; - goals: Goal[]; + goals?: GoalConfig; messages: string[]; error?: string; } @@ -46,11 +53,16 @@ function htmlOfHyp(hyp: Hyp) { return `
${hypBody}
`; } -function detailsOfList(elems: any[], summary: string, inner: string) { - let detailsStatus = elems.length == 0 ? "closed" : "open"; +function detailsOfList( + open: boolean, + elems: any[], + summary: string, + inner: string +) { + let detailsStatus = elems.length > 0 && open ? "open" : "closed"; return `
- ${summary} (${elems.length}) + ${summary} [${elems.length}]
${inner}
`; } @@ -74,23 +86,47 @@ function htmlOfGoals(goals: Goal[]) { else return goals.map(htmlOfGoal).join(" "); } +function detailsOfGoalList(open: boolean, name: string, goals: Goal[]) { + let goalsInner: string = htmlOfGoals(goals); + return detailsOfList(open, goals, name, goalsInner); +} + +function buildGoalsContent(g: GoalConfig) { + let goalsBody = detailsOfGoalList(true, "Goals", g.goals); + let shelfBody = + g.shelf.length > 0 ? detailsOfGoalList(false, "Shelf", g.shelf) : ""; + let givenBody = + g.given_up.length > 0 + ? detailsOfGoalList(false, "Given Up", g.given_up) + : ""; + return ` + ${goalsBody} +
+ ${shelfBody} + ${givenBody} +
`; +} + // Returns the HTML code of the panel and the inset ccontent -function buildGoalsContent(goals: GoalAnswer, styleUri: Uri) { +function buildInfoContent(goals: GoalAnswer, styleUri: Uri) { // get the HTML code of goals environment let vsUri = Uri.parse(goals.textDocument.uri); let uriBase = basename(vsUri.path); - let goalsInner: string = htmlOfGoals(goals.goals); - let goalsBody = detailsOfList(goals.goals, "Goals", goalsInner); + let goalsBody = goals.goals ? buildGoalsContent(goals.goals) : ""; let messageBody = detailsOfList( + true, goals.messages, "Messages", goals.messages.map(htmlOfCoqBlock).join(" ") ); let errorBody = goals.error - ? detailsOfList([0], "Error Browser", htmlOfCoqBlock(goals.error)) + ? detailsOfList(true, [0], "Error Browser", htmlOfCoqBlock(goals.error)) : ""; + let line = goals.position.line + 1; + let character = goals.position.character + 1; + // Use #FA8072 color too? return ` @@ -103,8 +139,8 @@ function buildGoalsContent(goals: GoalAnswer, styleUri: Uri) {
- ${uriBase}:${goals.position.line}:${goals.position.character} -
+ ${uriBase}:${line}:${character} +
${goalsBody}
@@ -129,17 +165,17 @@ class GoalView { this.styleUri = styleUri; } - update(uri: Uri, position: Position) { - this.sendGoalsRequest(uri, position); + update(uri: Uri, version: number, position: Position) { + this.sendGoalsRequest(uri, version, position); } display(goals: GoalAnswer) { - this.view.html = buildGoalsContent(goals, this.styleUri); + this.view.html = buildInfoContent(goals, this.styleUri); } // LSP Protocol extension for Goals - sendGoalsRequest(uri: Uri, position: Position) { - let doc = { uri: uri.toString() }; + sendGoalsRequest(uri: Uri, version: number, position: Position) { + let doc = { uri: uri.toString(), version }; let cursor: GoalRequest = { textDocument: doc, position: position }; const req = new RequestType("proof/goals"); this.client.sendRequest(req, cursor).then( @@ -159,8 +195,8 @@ export class GoalPanel { this.panel = panel; this.view = new GoalView(client, panel.webview, styleUri); } - update(uri: Uri, position: Position) { - this.view.update(uri, position); + update(uri: Uri, version: number, position: Position) { + this.view.update(uri, version, position); } dispose() { this.panel.dispose(); diff --git a/etc/FAQ.md b/etc/FAQ.md new file mode 100644 index 000000000..9ffe0ff65 --- /dev/null +++ b/etc/FAQ.md @@ -0,0 +1,113 @@ +# `coq-lsp` frequently asked questions + +## Why do you say so often "client" and "server", what does it mean? + +In the world of user interfaces for programming languages +(a.k.a. IDEs), "client/server" refer respectively to the editor and +the compiler of language checker which provides feedback to the +editor, that is to say, errors, warnings, syntax highlighting +information, etc... + +This way, the editor don't need to know a lot about the language. + +Thus, in `coq-lsp` case we have: + +- the client is Visual Studio Code plus the `coq-lsp` extension, or + some other editors such as Emacs or vim, +- the server is an extended Coq binary `coq-lsp`, which takes care of + running and checking Coq commands, among other tasks. + +The client and the server communicate using the [Language Server +Protocol](https://microsoft.github.io/language-server-protocol/) +standard, thus, the `coq-lsp` language server can be used from any +editor supporting this protocol. + +## How is `coq-lsp` different from VSCoq? + +[VSCoq](https://github.com/coq-community/vscoq) was developed by C.J. +Siegbell and at the time was an impressive achievement. The key +difference between `VSCoq` and `coq-lsp` is how the VSCode client +communicates with Coq. + +`VSCoq` communicates with Coq using the `coqidetop` server, which +implements a XML protocol providing basic operations over documents. + +In `coq-lsp` case, VSCode and Coq communicate using the LSP protocol, +plus a set of custom extensions. This is possible thanks to a new +`coq-lsp` language server, which is an extended Coq binary taking +advantage of improved Coq APIs. + +The XML protocol design dates back to 10 years ago, and it makes hard +to support some nice features. Moreover, development of VSCoq and +`coqidetop` is not coupled, so it is not easy to add new features. + +VSCoq went to significant effort to workaround these deficits +client-side, but that came with its own set of technical and +maintenance challenges. + +A key problem when implementing a language server for Coq is the fact +that Coq APIs were not meant for reactive UIs. + +For `coq-lsp`, we have done a year-long effort to significantly +improve Coq's base APIs, which has resulted in a much more lightweight +client implementation and a more capable server. + +Moreover, `coq-lsp` development is active while VSCoq is mostly in +maintenance mode due to the limitations outlined above. In a sense, +you could think of `coq-lsp` as a full rewrite of VSCoq, using the +experience we have accumulated over years of work in related projects +(such as jsCoq), and the experience in state-of-the art UI design and +implementation in other systems (Rust, Lean, Isabelle). + +We didn't pick `VSCoq 2` as a project name given than `coq-lsp` +follows the LSP standard and is not specific to Visual Studio code, in +fact, it works great on other editors such as vim or Emacs. + +## Is `coq-lsp` limited to VSCode? + +No! See above! + +While VSCode is for now the primary client development platform, +we fully intend the `coq-lsp` server to be usable from other editors. + +In particular, we have already ported jsCoq to work as a `coq-lsp` +client. + +Please get in touch if you would like to contribute support for your +favorite editor! + +## What part of the LSP protocol does `coq-lsp` support? + +See the [PROTOCOL.md](./doc/PROTOCOL.md) file. `coq-lsp` provides some +minimal extensions to the `coq-lsp` protocol as to adapt to the needs +of interactive proof checking, see [this +issue](https://github.com/microsoft/language-server-protocol/issues/1414) +for more information about proof assistants and LSP. + +## What is `coq-lsp` roadmap? + +The short-term roadmap is to support the full LSP protocol, and to +focus on core issues related to the needs of Coq users. + +## How is `coq-lsp` developed? + +`coq-lsp` is developed collaboratively, by a [team of +contributors](https://github.com/ejgallego/coq-lsp#team). + +The development is coordinated by Emilio J. Gallego Arias, who is also +the technical lead for the project. + +## Is there more information about `coq-lsp` design? + +Yes! There are a couple of presentations related to development +methodology and internals. We will upload the presentations here +shortly. We also hope to publish a paper soon. + +Is not easy to describe an evolving system, we like this quote [from Twitter](https://twitter.com/notypes/status/1610279076320923650): + +> Papers sometimes feel like a terrible way to communicate systems +> research; systems continue evolving but papers are static +> +> Our compiler (https://calyxir.org) is three years into development +> but people keep citing the paper and discussing limitations that +> have been addressed diff --git a/etc/doc/PROTOCOL.md b/etc/doc/PROTOCOL.md index f16688507..226ae0fd9 100644 --- a/etc/doc/PROTOCOL.md +++ b/etc/doc/PROTOCOL.md @@ -68,19 +68,29 @@ interface GoalRequest { Answer to the request is a `Goal[]` object, where ```typescript interface Hyp { - names: string; - ty: string; + names: string; + ty: string; } interface Goal { - ty: string; - hyps: Hyp[]; + ty: string; + hyps: Hyp[]; +} + +interface GoalConfig { + goals : Goal[]; + stack : undefined; + bullet ?: string; + shelf : Goal[]; + given_up : Goal[]; } interface GoalAnswer { - textDocument: VersionedTextDocumentIdentifier; - position: Position; - goals : Goal[]; + textDocument: VersionedTextDocumentIdentifier; + position: Position; + goals?: GoalConfig; + messages: string[]; + error?: string; } ``` @@ -91,6 +101,8 @@ which can be then rendered by the client in way that is desired. #### Changelog +- v4: send full goal configuration with shelf, given_up +- v3: include messages and optional error in the request response - v2: include position and document in the request response - v1: initial version, imported from lambdapi-lsp diff --git a/fleche/debug.ml b/fleche/debug.ml index 2677fd77b..278065fbe 100644 --- a/fleche/debug.ml +++ b/fleche/debug.ml @@ -22,3 +22,6 @@ let backtraces = false || all (* Sched wakeup *) let sched_wakeup = false || all + +(* Request event queue *) +let request_delay = true || all diff --git a/fleche/doc.ml b/fleche/doc.ml index d3886c02e..62ff9a525 100644 --- a/fleche/doc.ml +++ b/fleche/doc.ml @@ -7,26 +7,169 @@ (* Status: Experimental *) (************************************************************************) -let hd_opt ~default l = - match l with - | [] -> default - | h :: _ -> h +(* Should be moved to the right place *) +module Util = struct + let hd_opt ~default l = + match l with + | [] -> default + | h :: _ -> h + + let mk_diag ?(extra = []) range severity message = + let range = Types.to_range range in + let message = Pp.string_of_ppcmds message in + Types.Diagnostic.{ range; severity; message; extra } + + (* ast-dependent error diagnostic generation *) + let mk_error_diagnostic ~loc ~msg ~ast = + match (Coq.Ast.to_coq ast).v with + | Vernacexpr.{ expr = VernacRequire (prefix, _export, module_refs); _ } -> + let refs = List.map fst module_refs in + let extra = [ Types.Diagnostic.Extra.FailedRequire { prefix; refs } ] in + mk_diag ~extra loc 1 msg + | _ -> mk_diag loc 1 msg + + let feed_to_diag ~loc (range, severity, message) = + let range = Option.default loc range in + mk_diag range severity message + + let diags_of_feedback ~loc fbs = + let diags, messages = List.partition (fun (_, lvl, _) -> lvl < 3) fbs in + let diags = + if !Config.v.show_notices_as_diagnostics then + diags @ List.filter (fun (_, lvl, _) -> lvl = 3) fbs + else diags + in + (List.map (feed_to_diag ~loc) diags, messages) + + let build_span start_loc end_loc = + Loc. + { start_loc with + line_nb_last = end_loc.line_nb_last + ; bol_pos_last = end_loc.bol_pos_last + ; ep = end_loc.ep + } + + let print_stats () = + (if !Config.v.mem_stats then + let size = Memo.mem_stats () in + Io.Log.trace "stats" (string_of_int size)); + + Io.Log.trace "cache" (Stats.to_string ()); + Io.Log.trace "cache" (Memo.CacheStats.stats ()); + (* this requires patches to Coq *) + (* Io.Log.error "coq parsing" (Cstats.dump ()); *) + (* Cstats.reset (); *) + Memo.CacheStats.reset (); + Stats.reset () + + let gen l = String.make (String.length l) ' ' + + let rec md_map_lines coq l = + match l with + | [] -> [] + | l :: ls -> + if String.equal "```" l then gen l :: md_map_lines (not coq) ls + else (if coq then l else gen l) :: md_map_lines coq ls + + let markdown_process text = + let lines = String.split_on_char '\n' text in + let lines = md_map_lines false lines in + String.concat "\n" lines + + let process_contents ~uri ~contents = + let ext = Filename.extension uri in + let is_markdown = String.equal ext ".mv" in + if is_markdown then markdown_process contents else contents + + let safe_sub s pos len = + if pos < 0 || len < 0 || pos > String.length s - len then ( + let s = String.sub s 0 (Stdlib.min 20 String.(length s - 1)) in + Io.Log.trace "string_sub" + (Format.asprintf "error for pos: %d len: %d str: %s" pos len s); + None) + else Some (String.sub s pos len) + + let pp_words fmt w = + if w < 1024.0 then Format.fprintf fmt "%.0f w" w + else if w < 1024.0 *. 1024.0 then Format.fprintf fmt "%.2f Kw" (w /. 1024.0) + else Format.fprintf fmt "%.2f Mw" (w /. (1024.0 *. 1024.0)) +end + +module DDebug = struct + let parsed_sentence ~ast = + let loc = Coq.Ast.loc ast |> Option.get in + let line = "[l: " ^ string_of_int (loc.Loc.line_nb - 1) ^ "] " in + Io.Log.trace "coq" + ("parsed sentence: " ^ line ^ Pp.string_of_ppcmds (Coq.Ast.print ast)) + + let resume last_tok version = + Io.Log.trace "check" + Format.( + asprintf "resuming [v: %d], from: %d l: %d" version last_tok.Loc.ep + (last_tok.Loc.line_nb_last - 1)) +end (* [node list] is a very crude form of a meta-data map "loc -> data" , where for now [data] is only the goals. *) -type node = - { loc : Loc.t - ; ast : Coq.Ast.t option (** Ast of node *) - ; state : Coq.State.t (** (Full) State of node *) - ; diags : Types.Diagnostic.t list - ; messages : Coq.Message.t list - ; memo_info : string - } +module Node = struct + module Info = struct + type t = + { cache_hit : bool + ; parsing_time : float + ; time : float option + ; mw_prev : float + ; mw_after : float + } + + let make ?(cache_hit = false) ~parsing_time ?time ~mw_prev ~mw_after () = + { cache_hit; parsing_time; time; mw_prev; mw_after } + + (* let { Gc.major_words = mw_after; _ } = Gc.quick_stat () in *) + + let pp_time fmt = function + | None -> Format.fprintf fmt "N/A" + | Some time -> Format.fprintf fmt "%.4f" time + + let print ~stats { cache_hit; parsing_time; time; mw_prev; mw_after } = + let cptime = Stats.get_f stats ~kind:Stats.Kind.Parsing in + let cetime = Stats.get_f stats ~kind:Stats.Kind.Exec in + let memo_info = + Format.asprintf + "Cache Hit: %b | Parse (s/c): %.4f / %.2f | Exec (s/c): %a / %.2f" + cache_hit parsing_time cptime pp_time time cetime + in + let mem_info = + Format.asprintf "major words: %a | diff %a" Util.pp_words mw_after + Util.pp_words (mw_after -. mw_prev) + in + memo_info ^ "\n___\n" ^ mem_info + end + + type t = + { loc : Loc.t + ; ast : Coq.Ast.t option (** Ast of node *) + ; state : Coq.State.t (** (Full) State of node *) + ; diags : Types.Diagnostic.t list + ; messages : Coq.Message.t list + ; info : Info.t + } + + let loc { loc; _ } = loc + let ast { ast; _ } = ast + let state { state; _ } = state + let diags { diags; _ } = diags + let messages { messages; _ } = messages + let info { info; _ } = info +end 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 @@ -36,11 +179,12 @@ type t = { uri : string ; version : int ; contents : string - ; end_loc : int * int * int + ; end_loc : Types.Point.t ; root : Coq.State.t - ; nodes : node list + ; nodes : Node.t list ; diags_dirty : bool (** Used to optimize `eager_diagnostics` *) ; completed : Completion.t + ; stats : Stats.t (** Info about cumulative stats *) } let mk_doc root_state workspace = @@ -52,20 +196,41 @@ let init_loc ~uri = Loc.initial (InFile { dirpath = None; file = uri }) let get_last_text text = let lines = CString.split_on_char '\n' text in - let last_line = hd_opt ~default:"" (List.rev lines) in - (List.length lines, String.length last_line, String.length text) + let last_line = Util.hd_opt ~default:"" (List.rev lines) in + Types.Point. + { line = List.length lines - 1 + ; character = String.length last_line + ; offset = String.length text + } + +let process_init_feedback loc state feedback = + if not (CList.is_empty feedback) then + let diags, messages = Util.diags_of_feedback ~loc feedback in + let parsing_time = 0.0 in + let { Gc.major_words = mw_prev; _ } = Gc.quick_stat () in + let info = Node.Info.make ~parsing_time ~mw_prev ~mw_after:mw_prev () in + [ { Node.loc; ast = None; state; diags; messages; info } ] + else [] let create ~state ~workspace ~uri ~version ~contents = - let end_loc = get_last_text contents in - { uri - ; contents - ; end_loc - ; version - ; root = mk_doc state workspace - ; nodes = [] - ; diags_dirty = false - ; completed = Stopped (init_loc ~uri) - } + let { Coq.Protect.E.r; feedback } = mk_doc state workspace in + Coq.Protect.R.map r ~f:(fun root -> + Stats.reset (); + let stats = Stats.dump () in + let init_loc = init_loc ~uri in + let nodes = process_init_feedback init_loc root feedback in + let diags_dirty = not (CList.is_empty nodes) in + let end_loc = get_last_text contents in + { uri + ; contents + ; end_loc + ; version + ; root + ; nodes + ; diags_dirty + ; completed = Stopped init_loc + ; stats + }) let recover_up_to_offset doc offset = Io.Log.trace "prefix" @@ -76,7 +241,7 @@ let recover_up_to_offset doc offset = | n :: ns -> if Debug.scan then Io.Log.trace "scan" - (Format.asprintf "consider node at %s" (Coq.Ast.pr_loc n.loc)); + (Format.asprintf "consider node at %s" (Coq.Ast.pr_loc n.Node.loc)); if n.loc.Loc.ep >= offset then (List.rev acc_nodes, acc_loc) else find (n :: acc_nodes) n.loc ns in @@ -99,10 +264,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 @@ -112,23 +276,40 @@ 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 + let diags_dirty = if node.Node.diags <> [] then true else doc.diags_dirty in { doc with nodes = node :: doc.nodes; diags_dirty } -let concat_diags doc = List.concat_map (fun node -> node.diags) doc.nodes +let concat_diags doc = List.concat_map (fun node -> node.Node.diags) doc.nodes -let send_eager_diagnostics ~uri ~version ~doc = +let send_eager_diagnostics ~ofmt ~uri ~version ~doc = (* this is too noisy *) (* let proc_diag = mk_diag loc 3 (Pp.str "Processing") in *) (* Io.Report.diagnostics ~uri ~version (proc_diag :: doc.diags)); *) if doc.diags_dirty && !Config.v.eager_diagnostics then ( let diags = concat_diags doc in - Io.Report.diagnostics ~uri ~version diags; + Io.Report.diagnostics ~ofmt ~uri ~version diags; { doc with diags_dirty = false }) else doc let set_completion ~completed doc = { doc with completed } +let set_stats ~stats doc = { doc with stats } (* We approximate the remnants of the document. It would be easier if instead of reporting what is missing, we would report what is done, but for now we are @@ -137,20 +318,13 @@ let set_completion ~completed doc = { doc with completed } As we are quite dynamic (for now) in terms of what we observe of the document (basically we observe it linearly), we must compute the final position with a bit of a hack. *) -let compute_progress end_loc last_done = +let compute_progress end_ last_done = let start = { Types.Point.line = last_done.Loc.line_nb_last - 1 ; character = last_done.ep - last_done.bol_pos_last ; offset = last_done.ep } in - let end_line, end_col, end_offset = end_loc in - let end_ = - { Types.Point.line = end_line - 1 - ; character = end_col - ; offset = end_offset - } - in let range = Types.Range.{ start; end_ } in (range, 1) @@ -161,56 +335,14 @@ let report_progress ~doc last_tok = (* XXX: Save on close? *) (* let close_doc _modname = () *) -let bp_ = ref 0 - -let undamage_jf loc = - Loc. - { loc with - bol_pos = loc.bol_pos - !bp_ - ; bp = loc.bp - !bp_ - ; ep = loc.ep - !bp_ - } - -let undamage_jf_opt loc = Option.map undamage_jf loc - 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 (fun { CAst.loc; v } -> - CAst.make ?loc:(undamage_jf_opt loc) v) - |> Option.map Coq.Ast.of_coq - in - Stats.record ~kind:Stats.Kind.Parsing ~f:(Coq.Protect.eval ~f:parse) ps - -(* Read the input stream until a dot or a "end of proof" token is encountered *) -let parse_to_terminator : unit Pcoq.Entry.t = - (* type 'a parser_fun = { parser_fun : te LStream.t -> 'a } *) - let rec dot st = - match LStream.next st with - | Tok.KEYWORD ("." | "..." | "Qed" | "Defined" | "Admitted") | Tok.BULLET _ - -> () - | Tok.EOI -> () - | _ -> dot st - in - Pcoq.Entry.of_parser "Coqtoplevel.dot" { parser_fun = dot } - -(* If an error occurred while parsing, we try to read the input until a dot - token is encountered. We assume that when a lexer error occurs, at least one - char was eaten *) -let rec discard_to_dot ps = - try Pcoq.Entry.parse parse_to_terminator ps with - | CLexer.Error.E _ -> discard_to_dot ps - | e when CErrors.noncritical e -> () + let f ps = Coq.Parsing.parse ~st ps in + Stats.record ~kind:Stats.Kind.Parsing ~f ps let rec find_recovery_for_failed_qed ~default nodes = match nodes with | [] -> (default, None) - | { ast = None; _ } :: ns -> find_recovery_for_failed_qed ~default ns + | { Node.ast = None; _ } :: ns -> find_recovery_for_failed_qed ~default ns | { ast = Some ast; state; loc; _ } :: ns -> ( match (Coq.Ast.to_coq ast).CAst.v.Vernacexpr.expr with | Vernacexpr.VernacStartTheoremProof _ -> ( @@ -234,79 +366,17 @@ let state_recovery_heuristic doc st v = st | _ -> st -let debug_parsed_sentence ~ast = - let loc = Coq.Ast.loc ast |> Option.get in - let line = "[l: " ^ string_of_int loc.Loc.line_nb ^ "] " in - Io.Log.trace "coq" - ("parsed sentence: " ^ line ^ Pp.string_of_ppcmds (Coq.Ast.print ast)) - -type process_action = - | EOF of Completion.t (* completed *) - | Skip of Loc.t * Loc.t (* span of the skipped sentence + last valid token *) - | Process of Coq.Ast.t (* ast to process *) - -(* Make each fb a diag *) -let _pp_located fmt (_loc, pp) = Pp.pp_with fmt pp - -let pp_words fmt w = - if w < 1024.0 then Format.fprintf fmt "%.0f w" w - else if w < 1024.0 *. 1024.0 then Format.fprintf fmt "%.2f Kw" (w /. 1024.0) - else Format.fprintf fmt "%.2f Mw" (w /. (1024.0 *. 1024.0)) - -let mk_diag ?(extra = []) range severity message = - let range = Types.to_range range in - let message = Pp.string_of_ppcmds message in - Types.Diagnostic.{ range; severity; message; extra } - -(* modular error diagnostic generation *) -let mk_error_diagnostic ~loc ~msg ~ast = - match (Coq.Ast.to_coq ast).v with - | Vernacexpr.{ expr = VernacRequire (prefix, _export, module_refs); _ } -> - let refs = List.map fst module_refs in - let extra = [ Types.Diagnostic.Extra.FailedRequire { prefix; refs } ] in - mk_diag ~extra loc 1 msg - | _ -> mk_diag loc 1 msg - -let feed_to_diag ~loc (range, severity, message) = - let range = Option.default loc range in - mk_diag range severity message - -let process_feedback ~loc fbs = - let diags, messages = List.partition (fun (_, lvl, _) -> lvl < 3) fbs in - let diags = - if !Config.v.show_notices_as_diagnostics then - diags @ List.filter (fun (_, lvl, _) -> lvl = 3) fbs - else diags - in - (List.map (feed_to_diag ~loc) diags, messages) - -let interp_and_info ~parsing_time ~st ~fb_queue ast = +let interp_and_info ~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_command ~st ~fb_queue ast + Memo.interp_command ~st ast in - let cptime = Stats.get ~kind:Stats.Kind.Parsing in - let cetime = Stats.get ~kind:Stats.Kind.Exec in let { Gc.major_words = mw_after; _ } = Gc.quick_stat () in - let memo_info = - Format.asprintf - "Cache Hit: %b | Parse (s/c): %.4f / %.2f | Exec (s/c): %.4f / %.2f" - cache_hit parsing_time cptime time cetime - in - let mem_info = - Format.asprintf "major words: %a | diff %a" pp_words mw_after pp_words - (mw_after -. mw_prev) + let info = + Node.Info.make ~cache_hit ~parsing_time ~time ~mw_prev ~mw_after () in - (res, memo_info ^ "\n___\n" ^ mem_info) - -let build_span start_loc end_loc = - Loc. - { start_loc with - line_nb_last = end_loc.line_nb_last - ; bol_pos_last = end_loc.bol_pos_last - ; ep = end_loc.ep - } + (res, info) (* Copied from CLexer *) let clexer_after loc = @@ -317,6 +387,75 @@ let clexer_after loc = ; bp = loc.ep } +type parse_action = + | EOF of Completion.t (* completed *) + | Skip of Loc.t * Loc.t (* span of the skipped sentence + last valid token *) + | Process of Coq.Ast.t (* success! *) + +(* Returns parse_action, diags, parsing_time *) +let parse_action ~st last_tok doc_handle = + let start_loc = Coq.Parsing.Parsable.loc doc_handle |> clexer_after in + let { Coq.Protect.E.r; feedback }, time = parse_stm ~st doc_handle in + match r with + | Coq.Protect.R.Interrupted -> (EOF (Stopped last_tok), [], feedback, time) + | Coq.Protect.R.Completed res -> ( + match res with + | Ok None -> + (* We actually need to fix Coq to return the location of the true file + EOF, the below trick doesn't work. That will involved updating the type + of `main_entry` *) + let last_tok = Coq.Parsing.Parsable.loc doc_handle in + (EOF (Yes last_tok), [], feedback, time) + | Ok (Some ast) -> + let () = if Debug.parsing then DDebug.parsed_sentence ~ast in + (Process ast, [], feedback, time) + | 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 parse_diags = [ Util.mk_diag err_loc 1 msg ] in + (EOF (Failed last_tok), parse_diags, feedback, time) + | Error (User (Some err_loc, msg)) -> + let parse_diags = [ Util.mk_diag err_loc 1 msg ] in + Coq.Parsing.discard_to_dot doc_handle; + let last_tok = Coq.Parsing.Parsable.loc doc_handle in + let span_loc = Util.build_span start_loc last_tok in + (Skip (span_loc, last_tok), parse_diags, feedback, time)) + +(* Result of node-building action *) +type document_action = + | Stop of Completion.t * Node.t + | Continue of + { state : Coq.State.t + ; last_tok : Loc.t + ; node : Node.t + } + | Interrupted of Loc.t + +let unparseable_node ~loc ~parsing_diags ~parsing_feedback ~state ~parsing_time + = + let fb_diags, messages = Util.diags_of_feedback ~loc parsing_feedback in + let diags = fb_diags @ parsing_diags in + let { Gc.major_words = mw_prev; _ } = Gc.quick_stat () in + let info = Node.Info.make ~parsing_time ~mw_prev ~mw_after:mw_prev () in + { Node.loc; ast = None; diags; messages; state; info } + +let assemble_diags ~loc ~parsing_diags ~parsing_feedback ~diags ~feedback = + let parsing_fb_diags, parsing_messages = + Util.diags_of_feedback ~loc parsing_feedback + in + let fb_diags, fb_messages = Util.diags_of_feedback ~loc feedback in + let diags = parsing_diags @ parsing_fb_diags @ fb_diags @ diags in + let messages = parsing_messages @ fb_messages in + (diags, messages) + +let parsed_node ~loc ~ast ~state ~parsing_diags ~parsing_feedback ~diags + ~feedback ~info = + let diags, messages = + assemble_diags ~loc ~parsing_diags ~parsing_feedback ~diags ~feedback + in + { Node.loc; ast = Some ast; diags; messages; state; info } + let stream_of_string ~offset text = let pad = String.make offset ' ' in let str = Stream.of_string (pad ^ text) in @@ -325,200 +464,200 @@ let stream_of_string ~offset text = done; str -module PCoqHack = struct +let maybe_ok_diagnostics ~loc = + if !Config.v.ok_diagnostics then + let ok_diag = Util.mk_diag loc 3 (Pp.str "OK") in + [ ok_diag ] + else [] + +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 ~parsing_diags ~parsing_feedback ~ast ~st ~feedback + ~info last_tok res = + let ast_loc = Coq.Ast.loc ast |> Option.get in + match res with + | Ok { Coq.Interp.Info.res = state } -> + let ok_diags = maybe_ok_diagnostics ~loc:ast_loc in + let node = + parsed_node ~loc:ast_loc ~ast ~state ~parsing_diags ~parsing_feedback + ~diags:ok_diags ~feedback ~info + in + Continue { state; last_tok; node } + | Error (Coq.Protect.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 err_diags = [ Util.mk_error_diagnostic ~loc:err_loc ~msg ~ast ] in + let recovery_st = state_recovery_heuristic doc st ast in + let node = + parsed_node ~loc:ast_loc ~ast ~state:recovery_st ~parsing_diags + ~parsing_feedback ~diags:err_diags ~feedback ~info + in + 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 = + match action with + (* End of file *) + | EOF completed -> + let loc = Completion.loc completed in + let node = + unparseable_node ~loc ~parsing_diags ~parsing_feedback ~state:st + ~parsing_time + in + Stop (completed, node) + (* Parsing error *) + | Skip (span_loc, last_tok) -> + let node = + unparseable_node ~loc:span_loc ~parsing_diags ~parsing_feedback ~state:st + ~parsing_time + in + Continue { state = st; last_tok; node } + (* We can interpret the command now *) + | Process ast -> ( + let { Coq.Protect.E.r; feedback }, info = + interp_and_info ~parsing_time ~st ast + in + match r with + | Coq.Protect.R.Interrupted -> + (* Exit *) + Interrupted last_tok + | Coq.Protect.R.Completed res -> + (* The evaluation by Coq fully completed, then we can resume checking from + this point then, hence the new last valid token last_tok_new *) + let last_tok_new = Coq.Parsing.Parsable.loc doc_handle in + node_of_coq_result ~doc ~ast ~st ~parsing_diags ~parsing_feedback + ~feedback ~info last_tok_new res) + +module Target = struct type t = - { pa_tok_strm : Tok.t LStream.t - ; lexer_state : CLexer.Lexer.State.t ref - } - - let loc (p : Pcoq.Parsable.t) : Loc.t = - let p : t = Obj.magic p in - LStream.current_loc p.pa_tok_strm |> undamage_jf + | End + | Position of int * int end -(* XXX: Imperative problem *) -let process_and_parse ~uri ~version ~fb_queue doc last_tok doc_handle = +let beyond_target pos target = + match target with + | Target.End -> false + | Position (cut_line, cut_col) -> + (* This needs careful thinking as to help with the show goals postponement + case. *) + let pos_line = pos.Loc.line_nb_last - 1 in + let pos_col = Loc.(pos.ep - pos.bol_pos_last) in + pos_line > cut_line || (pos_line = cut_line && pos_col > cut_col) + +let pr_target = function + | Target.End -> "end" + | Target.Position (l, c) -> Format.asprintf "{cutpoint l: %02d | c: %02d" l c + +let log_beyond_target last_tok target = + Io.Log.trace "beyond_target" ("target reached " ^ Coq.Ast.pr_loc last_tok); + Io.Log.trace "beyond_target" ("target is " ^ pr_target target) + +(* main interpretation loop *) +let process_and_parse ~ofmt ~target ~uri ~version doc last_tok doc_handle = let rec stm doc st last_tok = - let doc = send_eager_diagnostics ~uri ~version ~doc in - report_progress ~doc last_tok; + (* Reporting of progress and diagnostics (if dirty) *) + let doc = send_eager_diagnostics ~ofmt ~uri ~version ~doc in + report_progress ~ofmt ~doc last_tok; if Debug.parsing then Io.Log.trace "coq" "parsing sentence"; - (* Parsing *) - let action, parsing_diags, parsing_time = - let start_loc = PCoqHack.loc doc_handle |> clexer_after in - match parse_stm ~st doc_handle with - | Coq.Protect.R.Interrupted, time -> (EOF (Stopped last_tok), [], time) - | Coq.Protect.R.Completed res, time -> ( - match res with - | Ok None -> - (* We actually need to fix Coq to return the location of the true file - EOF, the below trick doesn't work. That will involved updating the - type of `main_entry` *) - let last_tok = PCoqHack.loc doc_handle in - (EOF (Yes last_tok), [], time) - | 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 - (* let err_loc = undamage_jf err_loc in *) - let diags = [ mk_diag err_loc 1 msg ] in - discard_to_dot doc_handle; - let last_tok = PCoqHack.loc doc_handle in - let span_loc = build_span start_loc last_tok in - (Skip (span_loc, last_tok), diags, time)) - in - (* Execution *) - match action with - (* End of file *) - | EOF completed -> set_completion ~completed doc - | Skip (span_loc, last_tok) -> - (* We add the parsing diags *) - let node = - { loc = span_loc - ; ast = None - ; diags = parsing_diags - ; messages = [] - ; state = st - ; memo_info = "" - } + if beyond_target last_tok target then + let () = log_beyond_target last_tok target in + (* We set to Completed.Yes when we have reached the EOI *) + let completed = + if last_tok.Loc.ep >= doc.end_loc.offset then Completion.Yes last_tok + else Completion.Stopped last_tok + in + set_completion ~completed doc + else + (* Parsing *) + let action, parsing_diags, parsing_feedback, parsing_time = + parse_action ~st last_tok doc_handle + in + (* Execution *) + let action = + document_action ~st ~parsing_diags ~parsing_feedback ~parsing_time ~doc + last_tok doc_handle action in - let doc = add_node ~node doc in - stm doc st last_tok - (* We interpret the command now *) - | Process ast -> ( - let ast_loc = Coq.Ast.loc ast |> Option.get in - let res, memo_info = interp_and_info ~parsing_time ~st ~fb_queue ast in - match res with - | Coq.Protect.R.Interrupted -> - (* Exit *) - set_completion ~completed:(Stopped last_tok) doc - | Coq.Protect.R.Completed res -> ( - (* We can resume checking from this point then *) - let last_tok_new = PCoqHack.loc doc_handle in - match res with - | Ok { res = state; feedback } -> - let diags = - if !Config.v.ok_diagnostics then - let ok_diag = mk_diag ast_loc 3 (Pp.str "OK") in - [ ok_diag ] - else [] - in - let fb_diags, messages = process_feedback ~loc:ast_loc feedback in - let diags = parsing_diags @ fb_diags @ diags in - let node = - { loc = ast_loc; ast = Some ast; diags; messages; state; memo_info } - in - let doc = add_node ~node doc in - stm doc state last_tok_new - | Error (err_loc, msg) -> - let err_loc = Option.default ast_loc err_loc in - (* let err_loc = undamage_jf err_loc in *) - let diags = [ mk_error_diagnostic ~loc:err_loc ~msg ~ast ] in - (* FB should be handled by Coq.Protect.eval XXX *) - let fb_diags, messages = - List.rev !fb_queue |> process_feedback ~loc:err_loc - in - fb_queue := []; - let diags = parsing_diags @ fb_diags @ diags in - let st = state_recovery_heuristic doc st ast in - let node = - { loc = ast_loc - ; ast = Some ast - ; diags - ; messages - ; state = st - ; memo_info - } - in - let doc = add_node ~node doc in - stm doc st last_tok_new)) + match action with + | Interrupted last_tok -> set_completion ~completed:(Stopped last_tok) doc + | Stop (completed, node) -> + let doc = add_node ~node doc in + set_completion ~completed doc + | Continue { state; last_tok; node } -> + let doc = add_node ~node doc in + stm doc state last_tok in + (* Set the document to "internal" mode, stm expects the node list to be in + reveresed order *) + let doc = { doc with nodes = List.rev doc.nodes } in (* Note that nodes and diags in reversed order here *) (match doc.nodes with | [] -> () | n :: _ -> Io.Log.trace "resume" ("last node :" ^ Coq.Ast.pr_loc n.loc)); let st = - hd_opt ~default:doc.root (List.map (fun { state; _ } -> state) doc.nodes) + Util.hd_opt ~default:doc.root + (List.map (fun { Node.state; _ } -> state) doc.nodes) in - stm doc st last_tok - -let print_stats () = - (if !Config.v.mem_stats then - let size = Memo.mem_stats () in - Io.Log.trace "stats" (string_of_int size)); - - Io.Log.trace "cache" (Stats.dump ()); - Io.Log.trace "cache" (Memo.CacheStats.stats ()); - (* this requires patches to Coq *) - (* Io.Log.error "coq parsing" (Cstats.dump ()); *) - (* Cstats.reset (); *) - Memo.CacheStats.reset (); - Stats.reset () - -let gen l = String.make (String.length l) ' ' - -let rec md_map_lines coq l = - match l with - | [] -> [] - | l :: ls -> - if String.equal "```" l then gen l :: md_map_lines (not coq) ls - else (if coq then l else gen l) :: md_map_lines coq ls - -let markdown_process text = - let lines = String.split_on_char '\n' text in - let lines = md_map_lines false lines in - String.concat "\n" lines - -let process_contents ~uri ~contents = - let ext = Filename.extension uri in - let is_markdown = String.equal ext ".mv" in - if is_markdown then markdown_process contents else contents - -let log_resume last_tok = - Io.Log.trace "check" - Format.( - asprintf "resuming, from: %d l: %d" last_tok.Loc.ep - last_tok.Loc.line_nb_last) - -let check ~ofmt:_ ~doc ~fb_queue = - match doc.completed with - | Yes _ -> - Io.Log.trace "check" "resuming, completed=yes, nothing to do"; - doc - | Stopped last_tok -> - log_resume last_tok; - let uri, version, contents = (doc.uri, doc.version, doc.contents) in - (* Process markdown *) - let processed_content = process_contents ~uri ~contents in - (* Compute resume point, basically [CLexer.after] + stream setup *) - 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)) - in - bp_ := resume_loc.bp; + Stats.restore doc.stats; + let doc = stm doc st last_tok in + let stats = Stats.dump () in + let doc = set_stats ~stats doc in + (* Set the document to "finished" mode: reverse the node list *) + let doc = { doc with nodes = List.rev doc.nodes } in + doc + +let log_doc_completion (completed : Completion.t) = + let timestamp = Unix.gettimeofday () in + let loc, status = + match completed with + | Yes loc -> (loc, "fully checked") + | Stopped loc -> (loc, "stopped") + | Failed loc -> (loc, "failed") + in + Format.asprintf "done [%.2f]: document %s with pos %s" timestamp status + (Coq.Ast.pr_loc loc) + |> Io.Log.trace "check" + +let resume_check ~ofmt ~last_tok ~doc ~target = + let uri, version, contents = (doc.uri, doc.version, doc.contents) in + (* Process markdown *) + let processed_content = Util.process_contents ~uri ~contents in + (* Compute resume point, basically [CLexer.after] + stream setup *) + let resume_loc = clexer_after last_tok in + let offset = resume_loc.bp in + Coq.Parsing.bp_ := resume_loc.bp; + let pcontent_len = String.length processed_content in + match Util.safe_sub processed_content offset (pcontent_len - offset) with + | None -> + (* Guard against internal tricky eof errors *) + let completed = Completion.Failed last_tok in + set_completion ~completed doc + | Some processed_content -> let handle = - Pcoq.Parsable.make ~loc:resume_loc + Coq.Parsing.Parsable.make ~loc:resume_loc (stream_of_string ~offset processed_content) in - (* Set the document to "internal" mode *) + (* Set the content to the padded version if neccesary *) + let doc = { doc with contents = processed_content } in let doc = - { doc with contents = processed_content; nodes = List.rev doc.nodes } + process_and_parse ~ofmt ~target ~uri ~version doc last_tok handle in - let doc = process_and_parse ~uri ~version ~fb_queue doc last_tok handle in - (* Set the document to "finished" mode: Restore the original contents, - reverse the accumulators *) - let doc = { doc with nodes = List.rev doc.nodes; contents } in - let end_msg = - let timestamp = Unix.gettimeofday () in - let loc = - match doc.completed with - | Yes loc -> loc - | Stopped loc -> loc - in - Format.asprintf "done [%.2f]: document fully checked %s" timestamp - (Coq.Ast.pr_loc loc) - in - Io.Log.trace "check" end_msg; - print_stats (); + (* Restore the original contents *) + { doc with contents } + +let check ~ofmt ~target ~doc () = + 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 -> + DDebug.resume last_tok doc.version; + let doc = resume_check ~ofmt ~last_tok ~doc ~target in + log_doc_completion doc.completed; + Util.print_stats (); doc diff --git a/fleche/doc.mli b/fleche/doc.mli index c621bf991..0bb01ce2d 100644 --- a/fleche/doc.mli +++ b/fleche/doc.mli @@ -16,43 +16,78 @@ (* Status: Experimental *) (************************************************************************) -(* [node list] is a very crude form of a meta-data map "loc -> data" , where for - now [data] is only the goals. *) -type node = - { loc : Loc.t - ; ast : Coq.Ast.t option (** Ast of node *) - ; state : Coq.State.t (** (Full) State of node *) - ; diags : Types.Diagnostic.t list (** Diagnostics associated to the node *) - ; messages : Coq.Message.t list - ; memo_info : string - } +module Node : sig + module Info : sig + type t = private + { cache_hit : bool + ; parsing_time : float + ; time : float option + ; mw_prev : float + ; mw_after : float + } + + val print : stats:Stats.t -> t -> string + end + + type t = private + { loc : Loc.t + ; ast : Coq.Ast.t option (** Ast of node *) + ; state : Coq.State.t (** (Full) State of node *) + ; diags : Types.Diagnostic.t list (** Diagnostics associated to the node *) + ; messages : Coq.Message.t list + ; info : Info.t + } + + val loc : t -> Loc.t + val ast : t -> Coq.Ast.t option + val state : t -> Coq.State.t + val diags : t -> Types.Diagnostic.t list + val messages : t -> Coq.Message.t list + val info : t -> Info.t +end module Completion : sig - type t = + type t = private | 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 *) end +(** A Flèche document is basically a [node list], which is a crude form of a + meta-data map [Loc.t -> data], where for now [data] is the contents of + [Node.t]. *) type t = private { uri : string ; version : int ; contents : string - ; end_loc : int * int * int + ; end_loc : Types.Point.t ; root : Coq.State.t - ; nodes : node list + ; nodes : Node.t list ; diags_dirty : bool ; completed : Completion.t + ; stats : Stats.t (** Info about cumulative document stats *) } +(** Note, [create] calls Coq but it is not cached in the Memo.t table *) val create : state:Coq.State.t -> workspace:Coq.Workspace.t -> uri:string -> version:int -> contents:string - -> t + -> t Coq.Protect.R.t +(** Update the contents of a document, updating the right structures for + incremental checking. *) val bump_version : version:int -> contents:string -> t -> t -val check : - ofmt:Format.formatter -> doc:t -> fb_queue:Coq.Message.t list ref -> t +(** Checking targets, this specifies what we expect check to reach *) +module Target : sig + type t = + | End + | Position of int * int +end + +(** [check ofmt ~fb_queue ?cutpoint ~doc] if set, [cutpoint] will have Flèche + stop after the point specified there has been reached. *) +val check : ofmt:Format.formatter -> target:Target.t -> doc:t -> unit -> t diff --git a/fleche/info.ml b/fleche/info.ml index 7b88aa561..b0d76f9dd 100644 --- a/fleche/info.ml +++ b/fleche/info.ml @@ -113,12 +113,12 @@ module type S = sig type ('a, 'r) query = doc:Doc.t -> point:P.t -> 'a -> 'r option - val node : (approx, Doc.node) query + val node : (approx, Doc.Node.t) query val loc : (approx, Loc.t) query val ast : (approx, Coq.Ast.t) query val goals : (approx, Coq.Goals.reified_pp) query val messages : (approx, Coq.Message.t list) query - val info : (approx, string) query + val info : (approx, Doc.Node.Info.t) query val completion : (string, string list) query end @@ -133,7 +133,7 @@ module Make (P : Point) : S with module P := P = struct match l with | [] -> prev | node :: xs -> ( - let loc = node.Doc.loc in + let loc = node.Doc.Node.loc in match approx with | Exact -> if P.in_range ~loc point then Some node else find None xs | PrevIfEmpty -> @@ -146,51 +146,50 @@ module Make (P : Point) : S with module P := P = struct let node = find - let if_not_empty (pp : Pp.t) = - if Pp.(repr pp = Ppcmd_empty) then None else Some pp - - let reify_goals ppx lemmas = - let open Coq.Goals in - let proof = - Vernacstate.LemmaStack.with_top lemmas ~f:(fun pstate -> - Declare.Proof.get pstate) - in - let { Proof.goals; stack; sigma; _ } = Proof.data proof in - let ppx = List.map (Coq.Goals.process_goal_gen ppx sigma) in - Some - { goals = ppx goals - ; stack = List.map (fun (g1, g2) -> (ppx g1, ppx g2)) stack - ; bullet = if_not_empty @@ Proof_bullet.suggest proof - ; shelf = Evd.shelf sigma |> ppx - ; given_up = Evd.given_up sigma |> Evar.Set.elements |> ppx - } - let pr_goal st = let ppx env sigma x = - (* It is conveneint to optimize the Pp.t type, see [Jscoq_util.pp_opt] *) - Printer.pr_ltype_env ~goal_concl_style:true env sigma x + let { Coq.Protect.E.r; feedback } = + Coq.Print.pr_letype_env ~goal_concl_style:true env sigma x + in + Io.Log.feedback feedback; + match r with + | Coq.Protect.R.Completed (Ok pr) -> pr + | Coq.Protect.R.Completed (Error _pr) -> Pp.str "printer failed!" + | Interrupted -> Pp.str "printer interrupted!" in let lemmas = Coq.State.lemmas ~st in - Option.cata (reify_goals ppx) None lemmas + Option.map (Coq.Goals.reify ~ppx) lemmas let loc ~doc ~point approx = let node = find ~doc ~point approx in - Option.map (fun node -> node.Doc.loc) node + Option.map Doc.Node.loc node let ast ~doc ~point approx = let node = find ~doc ~point approx in - Option.bind node (fun node -> node.Doc.ast) + Option.bind node Doc.Node.ast + + let in_state ~st ~f node = + match Coq.State.in_state ~st ~f node with + | { r = Coq.Protect.R.Completed (Result.Ok res); feedback } -> + Io.Log.feedback feedback; + res + | { r = Coq.Protect.R.Completed (Result.Error _) | Coq.Protect.R.Interrupted + ; feedback + } -> + Io.Log.feedback feedback; + 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) + let st = node.Doc.Node.state in + in_state ~st ~f:pr_goal st) let messages ~doc ~point approx = - find ~doc ~point approx |> Option.map (fun node -> node.Doc.messages) + find ~doc ~point approx |> Option.map Doc.Node.messages let info ~doc ~point approx = - find ~doc ~point approx |> Option.map (fun node -> node.Doc.memo_info) + find ~doc ~point approx |> Option.map Doc.Node.info (* XXX: This belongs in Coq *) let pr_extref gr = @@ -205,7 +204,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.Node.state prefix ~f:(fun prefix -> to_qualid prefix |> obind (fun p -> Nametab.completion_canditates p diff --git a/fleche/info.mli b/fleche/info.mli index a8e275721..a19448fc4 100644 --- a/fleche/info.mli +++ b/fleche/info.mli @@ -44,12 +44,12 @@ module type S = sig type ('a, 'r) query = doc:Doc.t -> point:P.t -> 'a -> 'r option - val node : (approx, Doc.node) query + val node : (approx, Doc.Node.t) query val loc : (approx, Loc.t) query val ast : (approx, Coq.Ast.t) query val goals : (approx, Coq.Goals.reified_pp) query val messages : (approx, Coq.Message.t list) query - val info : (approx, string) query + val info : (approx, Doc.Node.Info.t) query val completion : (string, string list) query end diff --git a/fleche/io.ml b/fleche/io.ml index a815162b0..b3cd34c45 100644 --- a/fleche/io.ml +++ b/fleche/io.ml @@ -2,15 +2,23 @@ module CallBack = struct type t = { trace : string -> ?extra:string -> string -> unit ; send_diagnostics : - uri:string -> version:int -> Types.Diagnostic.t list -> unit + ofmt:Format.formatter + -> uri:string + -> version:int + -> Types.Diagnostic.t list + -> unit ; send_fileProgress : - uri:string -> version:int -> (Types.Range.t * int) list -> unit + ofmt:Format.formatter + -> uri:string + -> version:int + -> (Types.Range.t * int) list + -> unit } let default = { trace = (fun _ ?extra:_ _ -> ()) - ; send_diagnostics = (fun ~uri:_ ~version:_ _ -> ()) - ; send_fileProgress = (fun ~uri:_ ~version:_ _ -> ()) + ; send_diagnostics = (fun ~ofmt:_ ~uri:_ ~version:_ _ -> ()) + ; send_fileProgress = (fun ~ofmt:_ ~uri:_ ~version:_ _ -> ()) } let cb = ref default @@ -19,12 +27,19 @@ end module Log = struct let trace d ?extra m = !CallBack.cb.trace d ?extra m + + let feedback feedback = + if not (CList.is_empty feedback) then + (* Put feedbacks content here? *) + let extra = None in + !CallBack.cb.trace "feedback" ?extra + "feedback received in non-user facing place" end module Report = struct - let diagnostics ~uri ~version d = - !CallBack.cb.send_diagnostics ~uri ~version d + let diagnostics ~ofmt ~uri ~version d = + !CallBack.cb.send_diagnostics ~ofmt ~uri ~version d - let fileProgress ~uri ~version d = - !CallBack.cb.send_fileProgress ~uri ~version d + let fileProgress ~ofmt ~uri ~version d = + !CallBack.cb.send_fileProgress ~ofmt ~uri ~version d end diff --git a/fleche/io.mli b/fleche/io.mli index be3613970..dcdeb1ae7 100644 --- a/fleche/io.mli +++ b/fleche/io.mli @@ -4,9 +4,17 @@ module CallBack : sig (** Send a log message, [extra] may contain information to be shown in verbose mode *) ; send_diagnostics : - uri:string -> version:int -> Types.Diagnostic.t list -> unit + ofmt:Format.formatter + -> uri:string + -> version:int + -> Types.Diagnostic.t list + -> unit ; send_fileProgress : - uri:string -> version:int -> (Types.Range.t * int) list -> unit + ofmt:Format.formatter + -> uri:string + -> version:int + -> (Types.Range.t * int) list + -> unit } val set : t -> unit @@ -14,11 +22,23 @@ end module Log : sig val trace : string -> ?extra:string -> string -> unit + + (** For unexpected feedback *) + val feedback : Coq.Message.t list -> unit end module Report : sig - val diagnostics : uri:string -> version:int -> Types.Diagnostic.t list -> unit + val diagnostics : + ofmt:Format.formatter + -> uri:string + -> version:int + -> Types.Diagnostic.t list + -> unit val fileProgress : - uri:string -> version:int -> (Types.Range.t * int) list -> unit + ofmt:Format.formatter + -> uri:string + -> version:int + -> (Types.Range.t * int) list + -> unit end diff --git a/fleche/memo.ml b/fleche/memo.ml index 256b55fc9..b6c51568f 100644 --- a/fleche/memo.ml +++ b/fleche/memo.ml @@ -25,16 +25,6 @@ module VernacInput = struct else false let hash (v, st) = Hashtbl.hash (Coq.Ast.hash v, st) - - let marshal_out oc (v, st) = - Coq.Ast.marshal_out oc v; - Coq.State.marshal_out oc st; - () - - let marshal_in ic = - let v = Coq.Ast.marshal_in ic in - let st = Coq.State.marshal_in ic in - (v, st) end module CacheStats = struct @@ -67,15 +57,6 @@ module HC = Hashtbl.Make (VernacInput) module Result = struct (* We store the location as to compute an offset for cached results *) type t = Loc.t * Coq.State.t Coq.Interp.interp_result - - (* XXX *) - let marshal_in ic : t = - let loc = Marshal.from_channel ic in - (loc, Coq.Interp.marshal_in Coq.State.marshal_in ic) - - let marshal_out oc (loc, t) = - Marshal.to_channel oc loc []; - Coq.Interp.marshal_out Coq.State.marshal_out oc t end type cache = Result.t HC.t @@ -120,9 +101,9 @@ let loc_apply_offset let adjust_offset ~stm_loc ~cached_loc res = let offset = loc_offset cached_loc stm_loc in let f = loc_apply_offset offset in - Coq.Protect.map_loc ~f res + Coq.Protect.E.map_loc ~f res -let interp_command ~st ~fb_queue stm : _ Stats.t = +let interp_command ~st stm : _ Stats.t = let stm_loc = Coq.Ast.loc stm |> Option.get in match in_cache st stm with | Some (cached_loc, res), time -> @@ -134,16 +115,13 @@ let interp_command ~st ~fb_queue stm : _ Stats.t = 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:(Coq.Interp.interp ~st ~fb_queue) stm - in + let res, time_interp = CS.record ~kind ~f:(Coq.Interp.interp ~st) stm in let time = time_hash +. time_interp in - match res with - | Coq.Protect.R.Interrupted as res -> + match res.r with + | Coq.Protect.R.Interrupted -> (* Don't cache interruptions *) - fb_queue := []; Stats.make ~time res - | Coq.Protect.R.Completed _ as res -> + | Coq.Protect.R.Completed _ -> let () = HC.add !cache (stm, st) (stm_loc, res) in let time = time_hash +. time_interp in Stats.make ~time res) @@ -162,23 +140,23 @@ let interp_admitted ~st = let mem_stats () = Obj.reachable_words (Obj.magic cache) -let _hashtbl_out oc t = - Marshal.to_channel oc (HC.length t) []; - HC.iter - (fun vi res -> - VernacInput.marshal_out oc vi; - Result.marshal_out oc res) - t - -let _hashtbl_in ic = - let ht = HC.create 1000 in - let count : int = Marshal.from_channel ic in - for _i = 0 to count - 1 do - let vi = VernacInput.marshal_in ic in - let res = Result.marshal_in ic in - HC.add ht vi res - done; - ht +(* let _hashtbl_out oc t = () *) +(* Marshal.to_channel oc (HC.length t) []; *) +(* HC.iter *) +(* (fun vi res -> *) +(* VernacInput.marshal_out oc vi; *) +(* Result.marshal_out oc res) *) +(* t *) + +(* let _hashtbl_in ic = *) +(* let ht = HC.create 1000 in *) +(* let count : int = Marshal.from_channel ic in *) +(* for _i = 0 to count - 1 do *) +(* let vi = VernacInput.marshal_in ic in *) +(* let res = Result.marshal_in ic in *) +(* HC.add ht vi res *) +(* done; *) +(* ht *) let load_from_disk ~file = let ic = open_in_bin file in diff --git a/fleche/memo.mli b/fleche/memo.mli index c28bc1b6a..8e12f5ae0 100644 --- a/fleche/memo.mli +++ b/fleche/memo.mli @@ -7,21 +7,24 @@ module Stats : sig } end -(* debug *) -val input_info : Coq.Ast.t * Coq.State.t -> string - +(** Interpret a command, possibly memoizing it *) val interp_command : - st:Coq.State.t - -> fb_queue:Coq.Message.t list ref - -> Coq.Ast.t - -> Coq.State.t Coq.Interp.interp_result Stats.t + st:Coq.State.t -> Coq.Ast.t -> Coq.State.t Coq.Interp.interp_result Stats.t val interp_admitted : st:Coq.State.t -> Coq.State.t + +(** Stats *) val mem_stats : unit -> int -val load_from_disk : file:string -> unit -val save_to_disk : file:string -> unit module CacheStats : sig val reset : unit -> unit val stats : unit -> string end + +(** Not working yet *) +val load_from_disk : file:string -> unit + +val save_to_disk : file:string -> unit + +(** debug *) +val input_info : Coq.Ast.t * Coq.State.t -> string diff --git a/fleche/stats.ml b/fleche/stats.ml index ff2ed3da9..9ded94ac9 100644 --- a/fleche/stats.ml +++ b/fleche/stats.ml @@ -17,6 +17,21 @@ end let stats = Hashtbl.create 1000 let find kind = Hashtbl.find_opt stats kind |> Option.default 0.0 +type t = float * float * float + +let dump () = (find Kind.Hashing, find Kind.Parsing, find Kind.Exec) + +let restore (h, p, e) = + Hashtbl.replace stats Kind.Hashing h; + Hashtbl.replace stats Kind.Parsing p; + Hashtbl.replace stats Kind.Exec e + +let get_f (h, p, e) ~kind = + match kind with + | Kind.Hashing -> h + | Parsing -> p + | Exec -> e + let bump kind time = let acc = find kind in Hashtbl.replace stats kind (acc +. time) @@ -34,7 +49,7 @@ let record ~kind ~f x = let get ~kind = find kind -let dump () = +let to_string () = Format.asprintf "hashing: %f | parsing: %f | exec: %f" (find Kind.Hashing) (find Kind.Parsing) (find Kind.Exec) diff --git a/fleche/stats.mli b/fleche/stats.mli index c514d947c..78258fd62 100644 --- a/fleche/stats.mli +++ b/fleche/stats.mli @@ -8,5 +8,11 @@ end val get : kind:Kind.t -> float val record : kind:Kind.t -> f:('a -> 'b) -> 'a -> 'b * float -val dump : unit -> string +val to_string : unit -> string val reset : unit -> unit + +type t + +val dump : unit -> t +val restore : t -> unit +val get_f : t -> kind:Kind.t -> float diff --git a/lsp/base.ml b/lsp/base.ml index 7188ad7db..bf1cee1c3 100644 --- a/lsp/base.ml +++ b/lsp/base.ml @@ -21,9 +21,6 @@ (* Whether to send extended lsp messages *) let std_protocol = ref true - -module J = Yojson.Safe - let _mk_extra l = if !std_protocol then [] else l (* Ad-hoc parsing for file:///foo... *) @@ -31,6 +28,48 @@ let _parse_uri str = let l = String.length str - 7 in String.(sub str 7 l) +module J = Yojson.Safe +module U = Yojson.Safe.Util + +let string_field name dict = U.to_string List.(assoc name dict) +let dict_field name dict = U.to_assoc (List.assoc name dict) + +module Message = struct + type t = + | Notification of + { method_ : string + ; params : (string * Yojson.Safe.t) list + } + | Request of + { id : int + ; method_ : string + ; params : (string * Yojson.Safe.t) list + } + + (** Reify an incoming message *) + let from_yojson msg = + try + let dict = U.to_assoc msg in + let method_ = string_field "method" dict in + let params = dict_field "params" dict in + (match List.assoc_opt "id" dict with + | None -> Notification { method_; params } + | Some id -> + let id = U.to_int id in + Request { id; method_; params }) + |> Result.ok + with + | Not_found -> Error ("missing parameter: " ^ J.to_string msg) + | U.Type_error (msg, obj) -> + Error (Format.asprintf "msg: %s; obj: %s" msg (J.to_string obj)) + + let method_ = function + | Notification { method_; _ } | Request { method_; _ } -> method_ + + let params = function + | Notification { params; _ } | Request { params; _ } -> params +end + let mk_reply ~id ~result = `Assoc [ ("jsonrpc", `String "2.0"); ("id", `Int id); ("result", result) ] diff --git a/lsp/base.mli b/lsp/base.mli index 3f84fb891..789723683 100644 --- a/lsp/base.mli +++ b/lsp/base.mli @@ -15,6 +15,26 @@ (* Written by: Emilio J. Gallego Arias *) (************************************************************************) +(** Basic JSON-RPC Incoming Messages *) +module Message : sig + type t = + | Notification of + { method_ : string + ; params : (string * Yojson.Safe.t) list + } + | Request of + { id : int + ; method_ : string + ; params : (string * Yojson.Safe.t) list + } + + (** Reify an incoming message *) + val from_yojson : Yojson.Safe.t -> (t, string) Result.t + + val method_ : t -> string + val params : t -> (string * Yojson.Safe.t) list +end + val mk_range : Fleche.Types.Range.t -> Yojson.Safe.t (** Build notification *) diff --git a/lsp/io.ml b/lsp/io.ml index a13bfd411..4f32a0cc6 100644 --- a/lsp/io.ml +++ b/lsp/io.ml @@ -18,29 +18,6 @@ module F = Format module J = Yojson.Safe -module TraceValue = struct - type t = - | Off - | Messages - | Verbose - - let parse = function - | "messages" -> Messages - | "verbose" -> Verbose - | "off" -> Off - | _ -> raise (Invalid_argument "TraceValue.parse") - - let to_string = function - | Off -> "off" - | Messages -> "messages" - | Verbose -> "verbose" -end - -let oc = ref F.std_formatter -let set_log_channel c = oc := c -let trace_value = ref TraceValue.Off -let set_trace_value value = trace_value := value - let read_request_raw ic = let cl = input_line ic in let sin = Scanf.Scanning.from_string cl in @@ -86,6 +63,31 @@ let send_json fmt obj = F.fprintf fmt "Content-Length: %d\r\n\r\n%s%!" size msg; Mutex.unlock mut +(** Logging *) + +module TraceValue = struct + type t = + | Off + | Messages + | Verbose + + let of_string = function + | "messages" -> Messages + | "verbose" -> Verbose + | "off" -> Off + | _ -> raise (Invalid_argument "TraceValue.parse") + + let to_string = function + | Off -> "off" + | Messages -> "messages" + | Verbose -> "verbose" +end + +let oc = ref F.std_formatter +let set_log_channel c = oc := c +let trace_value = ref TraceValue.Off +let set_trace_value value = trace_value := value + let logMessage ~lvl ~message = let method_ = "window/logMessage" in let params = [ ("type", `Int lvl); ("message", `String message) ] in diff --git a/lsp/io.mli b/lsp/io.mli index dcdf72664..241eea5fe 100644 --- a/lsp/io.mli +++ b/lsp/io.mli @@ -15,27 +15,32 @@ (* Written by: Emilio J. Gallego Arias *) (************************************************************************) -(* We export this module *) +(** JSON-RPC input/output *) + +(** Read a JSON-RPC request from channel *) +val read_request : in_channel -> Yojson.Safe.t + +exception ReadError of string + +(** Send a JSON-RPC request to channel *) +val send_json : Format.formatter -> Yojson.Safe.t -> unit + +(** Logging *) + +(** Trace values *) module TraceValue : sig type t = | Off | Messages | Verbose - val parse : string -> t + val of_string : string -> t val to_string : t -> string end +(** Set the trace value *) val set_trace_value : TraceValue.t -> unit -(** Read a JSON-RPC request from channel *) -val read_request : in_channel -> Yojson.Safe.t - -exception ReadError of string - -(** Send a JSON-RPC request to channel *) -val send_json : Format.formatter -> Yojson.Safe.t -> unit - (** Set the log channel *) val set_log_channel : Format.formatter -> unit diff --git a/vendor/coq b/vendor/coq deleted file mode 160000 index 036eafab7..000000000 --- a/vendor/coq +++ /dev/null @@ -1 +0,0 @@ -Subproject commit 036eafab7934343a99d184740526675854ab977b diff --git a/vendor/coq-serapi b/vendor/coq-serapi deleted file mode 160000 index 6db3b1706..000000000 --- a/vendor/coq-serapi +++ /dev/null @@ -1 +0,0 @@ -Subproject commit 6db3b17068f4a71111da82cdf756b97243be4696