From 6d403d8004a1c03bef1901cf1918f375b975c11b Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Sat, 7 Jan 2023 19:53:17 +0100 Subject: [PATCH 01/39] [code] Improve client README and changelog. --- editor/code/CHANGELOG.md | 5 +++-- editor/code/README.md | 32 +++++++++++++++++++++++++++----- 2 files changed, 30 insertions(+), 7 deletions(-) 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. + From a50e3d601a46f48ab4beb41eebbfcdfdc70a3b08 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Sun, 8 Jan 2023 16:28:21 +0100 Subject: [PATCH 02/39] [controller] Handle failing requests better. This is a start to handle Coq Internal errors better. Some changes were already in different form in the first versions of #145 c.f. #91 --- controller/coq_lsp.ml | 31 ++++++++++++++++++++++++------- 1 file changed, 24 insertions(+), 7 deletions(-) diff --git a/controller/coq_lsp.ml b/controller/coq_lsp.ml index a91d613cb..d30a6d023 100644 --- a/controller/coq_lsp.ml +++ b/controller/coq_lsp.ml @@ -120,6 +120,9 @@ let do_shutdown ofmt ~id = let msg = LSP.mk_reply ~id ~result:`Null in LIO.send_json ofmt msg +(* XXX: We need to handle this better *) +exception AbortRequest + (* Handler for document *) module DocHandle = struct type t = @@ -137,7 +140,15 @@ module DocHandle = struct 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 ~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 ~handle ~(doc : Fleche.Doc.t) = @@ -185,12 +196,16 @@ module Check = struct (* 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 + match DocHandle.find_opt ~uri with + | Some handle -> + 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 + | None -> + LIO.trace "Check.do_check" ("file " ^ uri ^ " not available"); + () let completed uri = let doc = DocHandle.find_doc ~uri in @@ -471,6 +486,8 @@ let dispatch_message ofmt ~state dict = try dispatch_message ofmt ~state dict with | U.Type_error (msg, obj) -> LIO.trace_object msg obj | Lsp_exit -> raise Lsp_exit + | AbortRequest -> + () (* XXX: Separate requests from notifications, handle this better *) | exn -> let bt = Printexc.get_backtrace () in let iexn = Exninfo.capture exn in From 838656792667c0d5b109ddf7710e631edc7ffcb5 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Sun, 8 Jan 2023 16:34:47 +0100 Subject: [PATCH 03/39] [controller] Better log for failed Doc.create. --- controller/coq_lsp.ml | 18 +++++++++++++----- 1 file changed, 13 insertions(+), 5 deletions(-) diff --git a/controller/coq_lsp.ml b/controller/coq_lsp.ml index d30a6d023..d74adf8d8 100644 --- a/controller/coq_lsp.ml +++ b/controller/coq_lsp.ml @@ -224,11 +224,19 @@ 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 + try + let doc = + Fleche.Doc.create ~state:root_state ~workspace ~uri ~contents ~version + in + DocHandle.create ~uri ~doc; + Check.schedule ~uri + with + (* Fleche.Doc.create failed due to some Coq Internal Error, we need to use + Coq.Protect on that call *) + | exn -> + let iexn = Exninfo.capture exn in + LIO.trace "Fleche.Doc.create" "internal error"; + Exninfo.iraise iexn let do_change params = let document = dict_field "textDocument" params in From 25135ba653096d8e1eb172afed1f0fcc7e0b253f Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Sat, 7 Jan 2023 20:36:52 +0100 Subject: [PATCH 04/39] [faq] Preliminary FAQ --- README.md | 4 ++ etc/FAQ.md | 113 +++++++++++++++++++++++++++++++++++++++++++++++++++++ 2 files changed, 117 insertions(+) create mode 100644 etc/FAQ.md diff --git a/README.md b/README.md index e7ddcf5d9..e99c4dbcb 100644 --- a/README.md +++ b/README.md @@ -27,6 +27,10 @@ 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, 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 From 68c227c9008f786adb919990032a5392c3b5fd8b Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Sun, 8 Jan 2023 20:19:05 +0100 Subject: [PATCH 05/39] [fleche] Protect Coq document creation `Coq.Init` will actually often `Require` Coq's prelude and perform arbitrary actions, we now reflect this on the type. We still have a way to improve here, but for now the code is clear and the server should not crash anymore unless there is a real bug in coq-lsp. Closes #91 --- controller/coq_lsp.ml | 23 ++++++++++++----------- coq/protect.ml | 24 ++++++++++++++++++------ coq/protect.mli | 19 ++++++++++++++----- fleche/doc.ml | 24 +++++++++++++----------- fleche/doc.mli | 3 ++- fleche/memo.ml | 2 +- 6 files changed, 60 insertions(+), 35 deletions(-) diff --git a/controller/coq_lsp.ml b/controller/coq_lsp.ml index d74adf8d8..502b57225 100644 --- a/controller/coq_lsp.ml +++ b/controller/coq_lsp.ml @@ -224,19 +224,17 @@ let do_open ~state params = , string_field "text" document ) in let root_state, workspace = State.(state.root_state, state.workspace) in - try - let doc = - Fleche.Doc.create ~state:root_state ~workspace ~uri ~contents ~version - in + match + Fleche.Doc.create ~state:root_state ~workspace ~uri ~contents ~version + with + | Coq.Protect.R.Completed (Result.Ok doc) -> DocHandle.create ~uri ~doc; Check.schedule ~uri - with - (* Fleche.Doc.create failed due to some Coq Internal Error, we need to use - Coq.Protect on that call *) - | exn -> - let iexn = Exninfo.capture exn in - LIO.trace "Fleche.Doc.create" "internal error"; - Exninfo.iraise iexn + (* Maybe send some diagnostics in this case? *) + | Coq.Protect.R.Completed (Result.Error (_, msg)) -> + let msg = Pp.string_of_ppcmds msg in + LIO.trace "Fleche.Doc.create" ("internal error" ^ msg) + | Coq.Protect.R.Interrupted -> () let do_change params = let document = dict_field "textDocument" params in @@ -497,6 +495,9 @@ let dispatch_message ofmt ~state dict = | 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" diff --git a/coq/protect.ml b/coq/protect.ml index cd3b2b619..f166e8eca 100644 --- a/coq/protect.ml +++ b/coq/protect.ml @@ -1,13 +1,25 @@ +module Error = struct + type t = Loc.t option * Pp.t +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 map_error ~f = function + | Completed (Error (loc, msg)) -> Completed (Error (f (loc, msg))) + | res -> res + + let map_loc ~f = + let f (loc, msg) = (Option.map f loc, msg) in + map_error ~f +end let eval ~f x = try diff --git a/coq/protect.mli b/coq/protect.mli index 4b9b8ee74..3fc28a46a 100644 --- a/coq/protect.mli +++ b/coq/protect.mli @@ -1,11 +1,20 @@ +module Error : sig + type t = Loc.t option * Pp.t +end + module R : sig 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 *) + + val map : f:('a -> 'b) -> 'a t -> 'b t + val map_error : f:(Error.t -> Error.t) -> '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 +(** 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. *) val eval : f:('i -> 'o) -> 'i -> 'o R.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 R.t -> 'a R.t diff --git a/fleche/doc.ml b/fleche/doc.ml index 08d7a4e77..baa1810e8 100644 --- a/fleche/doc.ml +++ b/fleche/doc.ml @@ -46,7 +46,8 @@ type t = let mk_doc root_state workspace = (* XXX This shouldn't be foo *) let libname = Names.(DirPath.make [ Id.of_string "foo" ]) in - Coq.Init.doc_init ~root_state ~workspace ~libname + let f () = Coq.Init.doc_init ~root_state ~workspace ~libname in + Coq.Protect.eval ~f () let init_loc ~uri = Loc.initial (InFile { dirpath = None; file = uri }) @@ -56,16 +57,17 @@ let get_last_text text = (List.length lines, String.length last_line, String.length text) 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) - } + Coq.Protect.R.map (mk_doc state workspace) ~f:(fun root -> + let end_loc = get_last_text contents in + { uri + ; contents + ; end_loc + ; version + ; root + ; nodes = [] + ; diags_dirty = false + ; completed = Stopped (init_loc ~uri) + }) let recover_up_to_offset doc offset = Io.Log.trace "prefix" diff --git a/fleche/doc.mli b/fleche/doc.mli index c621bf991..59b2ef254 100644 --- a/fleche/doc.mli +++ b/fleche/doc.mli @@ -44,13 +44,14 @@ type t = private ; completed : Completion.t } +(** Note, [create] 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 val bump_version : version:int -> contents:string -> t -> t diff --git a/fleche/memo.ml b/fleche/memo.ml index 256b55fc9..c5de049bf 100644 --- a/fleche/memo.ml +++ b/fleche/memo.ml @@ -120,7 +120,7 @@ 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.R.map_loc ~f res let interp_command ~st ~fb_queue stm : _ Stats.t = let stm_loc = Coq.Ast.loc stm |> Option.get in From 81061cbaea17255dddb9856495ed2b2e25a98dc8 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Sun, 8 Jan 2023 20:43:09 +0100 Subject: [PATCH 06/39] [meta] Bump coq-lsp version in server and client. --- controller/coq_lsp.ml | 2 +- editor/code/package.json | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/controller/coq_lsp.ml b/controller/coq_lsp.ml index d74adf8d8..4d6491cc0 100644 --- a/controller/coq_lsp.ml +++ b/controller/coq_lsp.ml @@ -77,7 +77,7 @@ let do_client_options coq_lsp_options = let check_client_version version : unit = LIO.trace "version" version; match version with - | "any" | "0.1.2" -> () + | "any" | "0.1.3" -> () | v -> let message = Format.asprintf "Incorrect version: %s , expected 0.1.2" v in LIO.logMessage ~lvl:1 ~message diff --git a/editor/code/package.json b/editor/code/package.json index 3659bc297..51eb153fa 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 ", From 5435734b2d3ac5fd472de6c00834b3f61d1af2c9 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Mon, 9 Jan 2023 00:00:59 +0100 Subject: [PATCH 07/39] [coq] Protect all base API calls, stop checking on anomaly Work on tricky issues made me realize that we don't handle anomalies and Coq errors still in the best way, thus #91 is not really solved. There are 2 issues this PR solves: - goal printing can raise an anomalies and errors, due to setting state and printing, - it is safer to stop checking and set the document to failed when an anomaly happens (tho we could make this configurable). Thus, we go full principled in terms of API and make `Protect` mandatory on the exported APIs from `coq` library. We also introduce a `Failed` state that prevents further checking of that document without having finished it. Really fixes #91, and a step towards #153 TODO: protect calls to admit, but we leave this for a further PR as it is quite tricky due to error recovery needing rework to fully account for `Protect.R` results. --- CHANGES.md | 6 +++ controller/coq_lsp.ml | 11 +++--- coq/init.ml | 5 ++- coq/init.mli | 2 +- coq/interp.ml | 21 +++++----- coq/parsing.ml | 10 +++++ coq/parsing.mli | 1 + coq/print.ml | 8 ++++ coq/print.mli | 2 + coq/protect.ml | 15 ++++++-- coq/protect.mli | 10 +++-- coq/state.ml | 15 ++++++-- coq/state.mli | 5 ++- fleche/doc.ml | 89 +++++++++++++++++++++++++++++++------------ fleche/doc.mli | 1 + fleche/info.ml | 13 +++++-- 16 files changed, 156 insertions(+), 58 deletions(-) create mode 100644 coq/parsing.ml create mode 100644 coq/parsing.mli create mode 100644 coq/print.ml create mode 100644 coq/print.mli diff --git a/CHANGES.md b/CHANGES.md index b92be3152..5489615cb 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -1,3 +1,9 @@ +# coq-lsp 0.1.3: +------------------------ + + - Much improved handling of Coq fatal errors, the server is now + hardened against them (@ejgallego, #155, #157, #160, fixes #91) + # coq-lsp 0.1.2: Message ------------------------ diff --git a/controller/coq_lsp.ml b/controller/coq_lsp.ml index 2edae0a4d..1d8bf9a5c 100644 --- a/controller/coq_lsp.ml +++ b/controller/coq_lsp.ml @@ -210,8 +210,8 @@ module Check = struct let completed uri = let doc = DocHandle.find_doc ~uri in match doc.completed with - | Yes _ -> true - | _ -> false + | Yes _ | Failed _ -> true + | Stopped _ -> false let schedule ~uri = pending := Some uri end @@ -231,7 +231,8 @@ let do_open ~state params = DocHandle.create ~uri ~doc; Check.schedule ~uri (* Maybe send some diagnostics in this case? *) - | Coq.Protect.R.Completed (Result.Error (_, msg)) -> + | Coq.Protect.R.Completed (Result.Error (Anomaly (_, msg))) + | Coq.Protect.R.Completed (Result.Error (User (_, msg))) -> let msg = Pp.string_of_ppcmds msg in LIO.trace "Fleche.Doc.create" ("internal error" ^ msg) | Coq.Protect.R.Interrupted -> () @@ -306,7 +307,7 @@ let do_symbols ofmt ~id params = let slist = Coq.Ast.grab_definitions f ast in let msg = LSP.mk_reply ~id ~result:(`List slist) in LIO.send_json ofmt msg - | Stopped _ -> + | Stopped _ | Failed _ -> (* -32802 = RequestFailed | -32803 = ServerCancelled ; *) let code = -32802 in let message = "Document is not ready" in @@ -319,7 +320,7 @@ let do_position_request ofmt ~id params ~handler = let in_range = match doc.completed with | Yes _ -> true - | Stopped loc -> + | Failed loc | Stopped loc -> line < loc.line_nb_last || (line = loc.line_nb_last && col <= loc.ep - loc.bol_pos_last) in diff --git a/coq/init.ml b/coq/init.ml index c33a9685f..91de9ffbd 100644 --- a/coq/init.ml +++ b/coq/init.ml @@ -72,7 +72,7 @@ let coq_init opts = (**************************************************************************) (* Inits the context for a document *) -let doc_init ~root_state ~workspace ~libname = +let doc_init ~root_state ~workspace ~libname () = (* Lsp.Io.log_error "init" "starting"; *) Vernacstate.unfreeze_interp_state (State.to_coq root_state); @@ -83,3 +83,6 @@ let doc_init ~root_state ~workspace ~libname = (* We return the state at this point! *) Vernacstate.freeze_interp_state ~marshallable:false |> State.of_coq + +let doc_init ~root_state ~workspace ~libname = + Protect.eval ~f:(doc_init ~root_state ~workspace ~libname) () diff --git a/coq/init.mli b/coq/init.mli index 2358bf1a1..42351de8d 100644 --- a/coq/init.mli +++ b/coq/init.mli @@ -33,4 +33,4 @@ val doc_init : root_state:State.t -> workspace:Workspace.t -> libname:Names.DirPath.t - -> State.t + -> State.t Protect.R.t diff --git a/coq/interp.ml b/coq/interp.ml index 784bbb1ae..ff3f261c4 100644 --- a/coq/interp.ml +++ b/coq/interp.ml @@ -50,18 +50,15 @@ let marshal_out f oc res = | Ok res -> Marshal.to_channel oc 0 []; f oc res.Info.res - | Error (loc, msg) -> + | Error _err -> Marshal.to_channel oc 1 []; - Marshal.to_channel oc loc []; - Marshal.to_channel oc msg []; + (* Marshal.to_channel oc loc []; *) + (* Marshal.to_channel oc msg []; *) ()) -let marshal_in f ic = - let tag : int = Marshal.from_channel ic in - if tag = 0 then - let res = f ic in - Protect.R.Completed (Ok { Info.res; feedback = [] }) - else - let loc : Loc.t option = Marshal.from_channel ic in - let msg : Pp.t = Marshal.from_channel ic in - Protect.R.Completed (Error (loc, msg)) +(* Needs to be implemeted by Protect.marshal_in *) +let marshal_in _f _ic = Obj.magic 0 +(* let tag : int = Marshal.from_channel ic in if tag = 0 then let res = f ic in + Protect.R.Completed (Ok { Info.res; feedback = [] }) else let loc : Loc.t + option = Marshal.from_channel ic in let msg : Pp.t = Marshal.from_channel ic + in Protect.R.Completed (Error (User (loc, msg))) *) diff --git a/coq/parsing.ml b/coq/parsing.ml new file mode 100644 index 000000000..9f396c887 --- /dev/null +++ b/coq/parsing.ml @@ -0,0 +1,10 @@ +let parse ~st ps = + let mode = State.mode ~st in + let st = State.parsing ~st in + (* Coq is missing this, so we add it here. Note that this MUST run inside + coq_protect *) + Control.check_for_interrupt (); + Vernacstate.Parser.parse st Pvernac.(main_entry mode) ps + |> Option.map Ast.of_coq + +let parse ~st ps = Protect.eval ~f:(parse ~st) ps diff --git a/coq/parsing.mli b/coq/parsing.mli new file mode 100644 index 000000000..aba4a267b --- /dev/null +++ b/coq/parsing.mli @@ -0,0 +1 @@ +val parse : st:State.t -> Pcoq.Parsable.t -> Ast.t option Protect.R.t diff --git a/coq/print.ml b/coq/print.ml new file mode 100644 index 000000000..4c8de0a4f --- /dev/null +++ b/coq/print.ml @@ -0,0 +1,8 @@ +let pr_ltype_env ~goal_concl_style env sigma x = + Printer.pr_ltype_env ~goal_concl_style env sigma x + +let pr_ltype_env ~goal_concl_style env sigma x = + let f = pr_ltype_env ~goal_concl_style env sigma in + match Protect.eval ~f x with + | Protect.R.Completed (Ok pr) -> pr + | _ -> Pp.str "printer failed!" diff --git a/coq/print.mli b/coq/print.mli new file mode 100644 index 000000000..6caa3f407 --- /dev/null +++ b/coq/print.mli @@ -0,0 +1,2 @@ +val pr_ltype_env : + goal_concl_style:bool -> Environ.env -> Evd.evar_map -> Constr.t -> Pp.t diff --git a/coq/protect.ml b/coq/protect.ml index f166e8eca..5e221add4 100644 --- a/coq/protect.ml +++ b/coq/protect.ml @@ -1,5 +1,13 @@ module Error = struct - type t = Loc.t option * Pp.t + type payload = Loc.t option * Pp.t + + type t = + | User of payload + | Anomaly of payload + + let map ~f = function + | User e -> User (f e) + | Anomaly e -> Anomaly (f e) end module R = struct @@ -13,7 +21,7 @@ module R = struct | Interrupted -> Interrupted let map_error ~f = function - | Completed (Error (loc, msg)) -> Completed (Error (f (loc, msg))) + | Completed (Error e) -> Completed (Error (Error.map ~f e)) | res -> res let map_loc ~f = @@ -31,4 +39,5 @@ let eval ~f x = let e, info = Exninfo.capture exn in let loc = Loc.(get_loc info) in let msg = CErrors.iprint (e, info) in - R.Completed (Error (loc, msg)) + if CErrors.is_anomaly e then R.Completed (Error (Anomaly (loc, msg))) + else R.Completed (Error (User (loc, msg))) diff --git a/coq/protect.mli b/coq/protect.mli index 3fc28a46a..5cb645056 100644 --- a/coq/protect.mli +++ b/coq/protect.mli @@ -1,14 +1,18 @@ module Error : sig - type t = Loc.t option * Pp.t + type payload = Loc.t option * Pp.t + + type t = private + | User of payload + | Anomaly of payload end module R : sig - type 'a t = + type 'a t = private | Completed of ('a, Error.t) result | Interrupted (* signal sent, eval didn't complete *) val map : f:('a -> 'b) -> 'a t -> 'b t - val map_error : f:(Error.t -> Error.t) -> 'a t -> 'a t + val map_error : f:(Error.payload -> Error.payload) -> 'a t -> 'a t (** Update the loc stored in the result, this is used by our cache-aware location *) diff --git a/coq/state.ml b/coq/state.ml index 368ccdd4c..4b07f5029 100644 --- a/coq/state.ml +++ b/coq/state.ml @@ -77,10 +77,6 @@ let mode ~st = let parsing ~st = st.Vernacstate.parsing let lemmas ~st = st.Vernacstate.lemmas -let in_state ~st ~f a = - Vernacstate.unfreeze_interp_state st; - f a - let drop_proofs ~st = let open Vernacstate in { st with @@ -88,6 +84,13 @@ let drop_proofs ~st = Option.cata (fun s -> snd @@ Vernacstate.LemmaStack.pop s) None st.lemmas } +let in_state ~st ~f a = + let f a = + Vernacstate.unfreeze_interp_state st; + f a + in + Protect.eval ~f a + let admit ~st = let () = Vernacstate.unfreeze_interp_state st in match st.Vernacstate.lemmas with @@ -99,3 +102,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..f747e0bdf 100644 --- a/coq/state.mli +++ b/coq/state.mli @@ -10,7 +10,10 @@ val hash : t -> int val mode : st:t -> Pvernac.proof_mode option val parsing : st:t -> Vernacstate.Parser.t val lemmas : st:t -> Vernacstate.LemmaStack.t option -val in_state : st:t -> f:('a -> 'b) -> 'a -> 'b + +(** Execute a command in state [st]. Unfortunately this can produce anomalies as + Coq state setting is imperative, so we need to wrap it in protect. *) +val in_state : st:t -> f:('a -> 'b) -> 'a -> 'b Protect.R.t (** Drop the proofs from the state *) val drop_proofs : st:t -> t diff --git a/fleche/doc.ml b/fleche/doc.ml index baa1810e8..14cbb65e7 100644 --- a/fleche/doc.ml +++ b/fleche/doc.ml @@ -27,6 +27,10 @@ module Completion = struct type t = | Yes of Loc.t (** Location of the last token in the document *) | Stopped of Loc.t (** Location of the last valid token *) + | Failed of Loc.t (** Critical failure, like an anomaly *) + + let loc = function + | Yes loc | Stopped loc | Failed loc -> loc end (* Private. A doc is a list of nodes for now. The first element in the list is @@ -46,8 +50,7 @@ type t = let mk_doc root_state workspace = (* XXX This shouldn't be foo *) let libname = Names.(DirPath.make [ Id.of_string "foo" ]) in - let f () = Coq.Init.doc_init ~root_state ~workspace ~libname in - Coq.Protect.eval ~f () + Coq.Init.doc_init ~root_state ~workspace ~libname let init_loc ~uri = Loc.initial (InFile { dirpath = None; file = uri }) @@ -101,10 +104,9 @@ let compute_common_prefix ~contents doc = let completed = Completion.Stopped loc in (nodes, completed) -let bump_version ~version ~contents doc = +let bump_version ~version ~contents ~end_loc doc = (* When a new document, we resume checking from a common prefix *) let nodes, completed = compute_common_prefix ~contents doc in - let end_loc = get_last_text contents in { doc with version ; nodes @@ -114,6 +116,22 @@ let bump_version ~version ~contents doc = ; completed } +let bump_version ~version ~contents doc = + let end_loc = get_last_text contents in + match doc.completed with + (* We can do better, but we need to handle the case where the anomaly is when + restoring / executing the first sentence *) + | Failed _ -> + { doc with + version + ; nodes = [] + ; contents + ; end_loc + ; diags_dirty = true + ; completed = Stopped (init_loc ~uri:doc.uri) + } + | Stopped _ | Yes _ -> bump_version ~version ~contents ~end_loc doc + let add_node ~node doc = let diags_dirty = if node.diags <> [] then true else doc.diags_dirty in { doc with nodes = node :: doc.nodes; diags_dirty } @@ -164,16 +182,8 @@ let report_progress ~doc last_tok = (* let close_doc _modname = () *) let parse_stm ~st ps = - let mode = Coq.State.mode ~st in - let st = Coq.State.parsing ~st in - let parse ps = - (* Coq is missing this, so we add it here. Note that this MUST run inside - coq_protect *) - Control.check_for_interrupt (); - Vernacstate.Parser.parse st Pvernac.(main_entry mode) ps - |> Option.map Coq.Ast.of_coq - in - Stats.record ~kind:Stats.Kind.Parsing ~f:(Coq.Protect.eval ~f:parse) ps + let f ps = Coq.Parsing.parse ~st ps in + Stats.record ~kind:Stats.Kind.Parsing ~f ps (* Read the input stream until a dot or a "end of proof" token is encountered *) let parse_to_terminator : unit Pcoq.Entry.t = @@ -318,8 +328,13 @@ let process_and_parse ~uri ~version ~fb_queue doc last_tok doc_handle = | Ok (Some ast) -> let () = if Debug.parsing then debug_parsed_sentence ~ast in (Process ast, [], time) - | Error (loc, msg) -> - let err_loc = Option.get loc in + | Error (Anomaly (_, msg)) | Error (User (None, msg)) -> + (* We don't have a better altenative :(, usually missing error loc + here means an anomaly, so we stop *) + let err_loc = last_tok in + let diags = [ mk_diag err_loc 1 msg ] in + (EOF (Failed last_tok), diags, time) + | Error (User (Some err_loc, msg)) -> let diags = [ mk_diag err_loc 1 msg ] in discard_to_dot doc_handle; let last_tok = Pcoq.Parsable.loc doc_handle in @@ -329,7 +344,18 @@ let process_and_parse ~uri ~version ~fb_queue doc last_tok doc_handle = (* Execution *) match action with (* End of file *) - | EOF completed -> set_completion ~completed doc + | EOF completed -> + let node = + { loc = Completion.loc completed + ; ast = None + ; diags = parsing_diags + ; messages = [] + ; state = st + ; memo_info = "" + } + in + let doc = add_node ~node doc in + set_completion ~completed doc | Skip (span_loc, last_tok) -> (* We add the parsing diags *) let node = @@ -370,7 +396,8 @@ let process_and_parse ~uri ~version ~fb_queue doc last_tok doc_handle = in let doc = add_node ~node doc in stm doc state last_tok_new - | Error (err_loc, msg) -> + | Error (Anomaly (err_loc, msg) as coq_err) + | Error (User (err_loc, msg) as coq_err) -> ( let err_loc = Option.default ast_loc err_loc in let diags = [ mk_error_diagnostic ~loc:err_loc ~msg ~ast ] in (* FB should be handled by Coq.Protect.eval XXX *) @@ -390,7 +417,9 @@ let process_and_parse ~uri ~version ~fb_queue doc last_tok doc_handle = } in let doc = add_node ~node doc in - stm doc st last_tok_new)) + match coq_err with + | Anomaly _ -> set_completion ~completed:(Failed last_tok_new) doc + | User _ -> stm doc st last_tok_new))) in (* Note that nodes and diags in reversed order here *) (match doc.nodes with @@ -439,11 +468,21 @@ let log_resume last_tok = asprintf "resuming, from: %d l: %d" last_tok.Loc.ep last_tok.Loc.line_nb_last) +let safe_sub s pos len = + if pos < 0 || len < 0 || pos > String.length s - len then ( + Io.Log.trace "string_sub" + (Format.asprintf "error for pos: %d len: %d str: %s" pos len s); + s) + else String.sub s pos len + let check ~ofmt:_ ~doc ~fb_queue = match doc.completed with | Yes _ -> Io.Log.trace "check" "resuming, completed=yes, nothing to do"; doc + | Failed _ -> + Io.Log.trace "check" "can't resume, failed=yes, nothing to do"; + doc | Stopped last_tok -> log_resume last_tok; let uri, version, contents = (doc.uri, doc.version, doc.contents) in @@ -453,7 +492,8 @@ let check ~ofmt:_ ~doc ~fb_queue = let resume_loc = CLexer.after last_tok in let offset = resume_loc.bp in let processed_content = - String.(sub processed_content offset (length processed_content - offset)) + safe_sub processed_content offset + (String.length processed_content - offset) in let handle = Pcoq.Parsable.make ~loc:resume_loc @@ -469,12 +509,13 @@ let check ~ofmt:_ ~doc ~fb_queue = let doc = { doc with nodes = List.rev doc.nodes; contents } in let end_msg = let timestamp = Unix.gettimeofday () in - let loc = + let loc, status = match doc.completed with - | Yes loc -> loc - | Stopped loc -> loc + | Yes loc -> (loc, "fully checked") + | Stopped loc -> (loc, "stopped") + | Failed loc -> (loc, "failed") in - Format.asprintf "done [%.2f]: document fully checked %s" timestamp + Format.asprintf "done [%.2f]: document %s with pos %s" timestamp status (Coq.Ast.pr_loc loc) in Io.Log.trace "check" end_msg; diff --git a/fleche/doc.mli b/fleche/doc.mli index 59b2ef254..d8c60f840 100644 --- a/fleche/doc.mli +++ b/fleche/doc.mli @@ -31,6 +31,7 @@ module Completion : sig 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 *) end type t = private diff --git a/fleche/info.ml b/fleche/info.ml index 7b88aa561..60a8cd175 100644 --- a/fleche/info.ml +++ b/fleche/info.ml @@ -168,7 +168,7 @@ module Make (P : Point) : S with module P := P = struct 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 + Coq.Print.pr_ltype_env ~goal_concl_style:true env sigma x in let lemmas = Coq.State.lemmas ~st in Option.cata (reify_goals ppx) None lemmas @@ -181,10 +181,15 @@ module Make (P : Point) : S with module P := P = struct let node = find ~doc ~point approx in Option.bind node (fun node -> node.Doc.ast) + let in_state ~st ~f node = + match Coq.State.in_state ~st ~f node with + | Coq.Protect.R.Completed (Result.Ok res) -> res + | Coq.Protect.R.Completed (Result.Error _) | Coq.Protect.R.Interrupted -> + None + let goals ~doc ~point approx = find ~doc ~point approx - |> obind (fun node -> - Coq.State.in_state ~st:node.Doc.state ~f:pr_goal node.Doc.state) + |> obind (fun node -> in_state ~st:node.Doc.state ~f:pr_goal node.Doc.state) let messages ~doc ~point approx = find ~doc ~point approx |> Option.map (fun node -> node.Doc.messages) @@ -205,7 +210,7 @@ module Make (P : Point) : S with module P := P = struct let completion ~doc ~point prefix = find ~doc ~point Exact |> obind (fun node -> - Coq.State.in_state ~st:node.Doc.state prefix ~f:(fun prefix -> + in_state ~st:node.Doc.state prefix ~f:(fun prefix -> to_qualid prefix |> obind (fun p -> Nametab.completion_canditates p From 9349b1da2cac7d227dc92891299e476dc7f16f58 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Sun, 8 Jan 2023 21:48:09 +0100 Subject: [PATCH 08/39] [opam] Some fixes to opam. --- coq-lsp.opam | 40 ++++++++++++++++++++++------------------ 1 file changed, 22 insertions(+), 18 deletions(-) diff --git a/coq-lsp.opam b/coq-lsp.opam index 7d98aded4..691e3ade3 100644 --- a/coq-lsp.opam +++ b/coq-lsp.opam @@ -10,33 +10,37 @@ homepage: "https://github.com/ejgallego/coq-lsp" dev-repo: "git+https://github.com/ejgallego/coq-lsp.git" authors: [ "Emilio Jesús Gallego Arias " + "Ali Caglayan " + "Shachar Itzhaky " + "Ramkumar Ramachandra " ] -license: "LGPL-2.1" +license: "LGPL-2.1-or-later" doc: "https://ejgallego.github.io/coq-lsp/" depends: [ - "ocaml" { >= "4.12.0" } - "dune" { build & >= "3.5.0" } + "ocaml" { >= "4.12.0" } + "dune" { >= "3.5.0" } - # Not yet required, install Coq deps instead - # "coq" { >= "8.17" } + # lsp dependencies + "cmdliner" { >= "1.1.0" } + "yojson" { >= "1.7.0" } + + # Uncomment this for releases + # "coq" { >= "8.17" < "8.18" } + # "coq-serapi" { >= "8.17" < "8.18" } - # coq deps + # coq deps: remove this for releases "ocamlfind" {>= "1.8.1"} "zarith" {>= "1.11"} - # serapi deps - "sexplib" { >= "v0.13.0" } - "ppx_deriving" { >= "4.2.1" } - "ppx_sexp_conv" { >= "v0.13.0" } - "ppx_compare" { >= "v0.13.0" } - "ppx_hash" { >= "v0.13.0" } - "ppx_import" { build & >= "1.5-3" } - "ppx_deriving_yojson" { >= "3.4" } - - # lsp dependencies - "cmdliner" { >= "1.1.0" } - "yojson" { >= "1.7.0" } + # serapi deps: remove this for releases + "sexplib" { >= "v0.13.0" } + "ppx_deriving" { >= "4.2.1" } + "ppx_sexp_conv" { >= "v0.13.0" } + "ppx_compare" { >= "v0.13.0" } + "ppx_hash" { >= "v0.13.0" } + "ppx_import" { >= "1.5-3" } + "ppx_deriving_yojson" { >= "3.4" } ] build: [ [ "dune" "build" "-p" name "-j" jobs ] ] From 30430d5671a811cc0504d824043cd52fdbf716c2 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Mon, 9 Jan 2023 01:58:07 +0100 Subject: [PATCH 09/39] [readme] [nit] Some fixes and comments. --- README.md | 9 ++++++++- 1 file changed, 8 insertions(+), 1 deletion(-) diff --git a/README.md b/README.md index e99c4dbcb..ba6cb4b56 100644 --- a/README.md +++ b/README.md @@ -37,6 +37,9 @@ See our [list of frequently-asked questions](./etc/FAQ.md). `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 @@ -56,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. @@ -256,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! + + From b8f0a63deffbc1037eb43bb1ae63564c41518a83 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Tue, 10 Jan 2023 21:39:16 +0100 Subject: [PATCH 10/39] [controller] Print coqlib and verbose loadpath info This is useful for debugging. --- controller/coq_lsp.ml | 3 ++- coq/workspace.ml | 37 ++++++++++++++++++++++++++++--------- coq/workspace.mli | 6 ++++-- 3 files changed, 34 insertions(+), 12 deletions(-) diff --git a/controller/coq_lsp.ml b/controller/coq_lsp.ml index 1d8bf9a5c..0e01e7d68 100644 --- a/controller/coq_lsp.ml +++ b/controller/coq_lsp.ml @@ -571,7 +571,8 @@ let mk_fb_handler () = , q ) let log_workspace w = - let message = Coq.Workspace.describe w in + let message, extra = Coq.Workspace.describe w in + LIO.trace "workspace" "initialized" ~extra; LIO.logMessage ~lvl:3 ~message let lsp_main bt std coqlib vo_load_path ml_include_path = diff --git a/coq/workspace.ml b/coq/workspace.ml index a27df975d..679894c42 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_print_string) + ml_include_path + (Format.pp_print_list pp_load_path) + vo_load_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 = From 54a7e83600578f073765219703c7a5964b74ac18 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Tue, 10 Jan 2023 22:15:13 +0100 Subject: [PATCH 11/39] [lsp/io] Refactor JSON-RPC from logging code We better organize logging and JSON-RPC code as they are not related. --- controller/coq_lsp.ml | 4 ++-- coq/workspace.ml | 8 ++++---- lsp/io.ml | 48 ++++++++++++++++++++++--------------------- lsp/io.mli | 25 +++++++++++++--------- 4 files changed, 46 insertions(+), 39 deletions(-) diff --git a/controller/coq_lsp.ml b/controller/coq_lsp.ml index 0e01e7d68..616c1c7c7 100644 --- a/controller/coq_lsp.ml +++ b/controller/coq_lsp.ml @@ -85,7 +85,7 @@ let check_client_version version : unit = let do_initialize ofmt ~id 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 @@ -358,7 +358,7 @@ let do_hover ofmt = do_position_request ofmt ~handler:hover_handler let do_trace params = let trace = string_field "value" params in - LIO.set_trace_value (LIO.TraceValue.parse trace) + LIO.set_trace_value (LIO.TraceValue.of_string trace) (* Replace by ppx when we can print goals properly in the client *) let mk_hyp { Coq.Goals.names; def = _; ty } : Yojson.Safe.t = diff --git a/coq/workspace.ml b/coq/workspace.ml index 679894c42..7f7bad1b6 100644 --- a/coq/workspace.ml +++ b/coq/workspace.ml @@ -79,10 +79,10 @@ let describe { coqlib; kind; vo_load_path; ml_include_path; require_libs; _ } = vo_load_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 \ + "@[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 ) 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 From 0d5d1d900ea73aba68da251319aab11d1d6ca37a Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Tue, 10 Jan 2023 22:56:20 +0100 Subject: [PATCH 12/39] [controller] Separate dispatching of notifications and requests This was long overdue, so we can now start to handle better some critical stuff, such as request cancellation, proper LSP initialization sequence, and principled request response (both immediate and delayed). --- controller/coq_lsp.ml | 69 ++++++++++++++++++++++--------------------- lsp/base.ml | 45 ++++++++++++++++++++++++++-- lsp/base.mli | 20 +++++++++++++ 3 files changed, 98 insertions(+), 36 deletions(-) diff --git a/controller/coq_lsp.ml b/controller/coq_lsp.ml index 616c1c7c7..56f4fa65e 100644 --- a/controller/coq_lsp.ml +++ b/controller/coq_lsp.ml @@ -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,7 +35,6 @@ 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 odict_field name dict = @@ -451,7 +445,7 @@ let memo_read_from_disk () = if false then memo_read_from_disk () change_pending setup. *) let request_queue = Queue.create () -let process_input (com : J.t) = +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 @@ -461,36 +455,45 @@ let process_input (com : J.t) = 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 *) +let dispatch_notification ofmt ~state ~method_ ~params = + match method_ with + (* Lifecycle *) + | "exit" -> raise Lsp_exit + (* setTrace *) + | "$/setTrace" -> do_trace params + (* 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 () + (* NOOPs *) + | "initialized" -> () + (* Generic handler *) + | msg -> LIO.trace "no_handler" msg + +let dispatch_request ofmt ~id ~method_ ~params = + match method_ with + (* Lifecyle *) | "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 - (* setTrace *) - | "$/setTrace" -> do_trace params (* Proof-specific stuff *) | "proof/goals" -> do_goals ofmt ~id params - (* Notifications *) - | "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 - (* NOOPs *) - | "initialized" | "workspace/didChangeWatchedFiles" -> () + (* Generic handler *) | msg -> LIO.trace "no_handler" msg -let dispatch_message ofmt ~state dict = - try dispatch_message ofmt ~state dict with +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 | AbortRequest -> @@ -503,7 +506,7 @@ let dispatch_message ofmt ~state dict = 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)); @@ -525,12 +528,10 @@ let rec process_queue ofmt ~state = | Some com -> (* TODO we should 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); process_queue ofmt ~state let lsp_cb oc = @@ -614,7 +615,9 @@ let lsp_main bt std coqlib vo_load_path ml_include_path = (* 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; + (match LSP.Message.from_yojson com with + | Ok msg -> process_input msg + | Error msg -> LIO.trace "read_request" ("error: " ^ msg)); loop () in try loop () with diff --git a/lsp/base.ml b/lsp/base.ml index 7188ad7db..060f8a28d 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" + | 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 *) From b1590073d3daa8ce4424b9511d0b6d4bf2ed8bf2 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Tue, 10 Jan 2023 23:06:36 +0100 Subject: [PATCH 13/39] [controller] Handle requests response uniformly. Another step towards better request handling, we should be able next to attach requests to a document handler. --- controller/coq_lsp.ml | 74 ++++++++++++++++++++++--------------------- 1 file changed, 38 insertions(+), 36 deletions(-) diff --git a/controller/coq_lsp.ml b/controller/coq_lsp.ml index 56f4fa65e..ab49a4984 100644 --- a/controller/coq_lsp.ml +++ b/controller/coq_lsp.ml @@ -76,7 +76,7 @@ let check_client_version version : unit = let message = Format.asprintf "Incorrect version: %s , expected 0.1.2" v 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.of_string LIO.TraceValue.Off @@ -96,23 +96,19 @@ 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") - ] ) - ]) + let 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 + Ok result -let do_shutdown ofmt ~id = - let msg = LSP.mk_reply ~id ~result:`Null in - LIO.send_json ofmt msg +let do_shutdown ~params:_ = Ok `Null (* XXX: We need to handle this better *) exception AbortRequest @@ -292,22 +288,22 @@ let _kind_of_type _tm = 13 13 (* Variable *) | Type | Kind | Symb _ | _ when is_undef -> 14 (* Constant *) | _ -> 12 (* Function *) *) -let do_symbols ofmt ~id params = +let do_symbols ~params = 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 + let result = `List slist in + Ok result | Stopped _ | Failed _ -> (* -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 do_position_request ofmt ~id params ~handler = +let do_position_request ~params ~handler = let _uri, doc = get_textDocument params in let point = get_position params in let line, col = point in @@ -318,14 +314,12 @@ let do_position_request ofmt ~id params ~handler = line < loc.line_nb_last || (line = loc.line_nb_last && col <= loc.ep - loc.bol_pos_last) in - if in_range then - let result = handler ~doc ~point in - LSP.mk_reply ~id ~result |> LIO.send_json ofmt + if in_range then Result.Ok (handler ~doc ~point) 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 + Result.Error (code, message) let hover_handler ~doc ~point = let show_loc_info = true in @@ -348,7 +342,7 @@ let hover_handler ~doc ~point = (fun loc -> [ ("range", LSP.mk_range (Fleche.Types.to_range loc)) ]) [] loc_span) -let do_hover ofmt = do_position_request ofmt ~handler:hover_handler +let do_hover = do_position_request ~handler:hover_handler let do_trace params = let trace = string_field "value" params in @@ -398,7 +392,7 @@ let goals_handler ~doc ~point = ] @ error) -let do_goals ofmt = do_position_request ofmt ~handler:goals_handler +let do_goals = do_position_request ~handler:goals_handler let completion_handler ~doc ~point:_ = let f _loc id = `Assoc [ ("label", `String Names.Id.(to_string id)) ] in @@ -406,7 +400,7 @@ let completion_handler ~doc ~point:_ = let clist = Coq.Ast.grab_definitions f ast in `List clist -let do_completion ofmt = do_position_request ofmt ~handler:completion_handler +let do_completion = do_position_request ~handler:completion_handler let memo_cache_file = ".coq-lsp.cache" let memo_save_to_disk () = @@ -471,19 +465,27 @@ let dispatch_notification ofmt ~state ~method_ ~params = (* Generic handler *) | msg -> LIO.trace "no_handler" msg -let dispatch_request ofmt ~id ~method_ ~params = +let dispatch_request ~method_ ~params = match method_ with (* Lifecyle *) - | "initialize" -> do_initialize ofmt ~id params - | "shutdown" -> do_shutdown ofmt ~id + | "initialize" -> do_initialize ~params + | "shutdown" -> do_shutdown ~params (* 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 + | "textDocument/completion" -> do_completion ~params + | "textDocument/documentSymbol" -> do_symbols ~params + | "textDocument/hover" -> do_hover ~params (* Proof-specific stuff *) - | "proof/goals" -> do_goals ofmt ~id params + | "proof/goals" -> do_goals ~params (* Generic handler *) - | msg -> LIO.trace "no_handler" msg + | msg -> + LIO.trace "no_handler" msg; + Ok `Null + +let dispatch_request ofmt ~id ~method_ ~params = + (match dispatch_request ~method_ ~params with + | Ok result -> LSP.mk_reply ~id ~result + | Error (code, message) -> LSP.mk_request_error ~id ~code ~message) + |> LIO.send_json ofmt let dispatch_message ofmt ~state (com : LSP.Message.t) = match com with From 9dd61552ad1c70dd86185a302fb8a6fa3236e680 Mon Sep 17 00:00:00 2001 From: Ali Caglayan Date: Mon, 9 Jan 2023 14:36:12 +0100 Subject: [PATCH 14/39] [server] Add version string in separate file, update version This should make it easier to update the version when doing a release, and fixes a bug. Signed-off-by: Ali Caglayan --- controller/coq_lsp.ml | 17 ++++++++++------- controller/dune | 2 +- controller/version.ml | 17 +++++++++++++++++ controller/version.mli | 15 +++++++++++++++ 4 files changed, 43 insertions(+), 8 deletions(-) create mode 100644 controller/version.ml create mode 100644 controller/version.mli diff --git a/controller/coq_lsp.ml b/controller/coq_lsp.ml index 616c1c7c7..7ca0bf51a 100644 --- a/controller/coq_lsp.ml +++ b/controller/coq_lsp.ml @@ -74,12 +74,15 @@ let do_client_options coq_lsp_options = | 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.3" -> () - | 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 = @@ -704,7 +707,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/dune b/controller/dune index e4f264226..61d482987 100644 --- a/controller/dune +++ b/controller/dune @@ -1,6 +1,6 @@ (executable (name coq_lsp) - (modules coq_lsp) + (modules coq_lsp version) (public_name coq-lsp) (preprocess (staged_pps ppx_import ppx_deriving_yojson)) 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 *) +(* Date: Tue, 10 Jan 2023 23:45:57 +0100 Subject: [PATCH 15/39] [controller] Refactor requests, move to their own file. --- controller/coq_lsp.ml | 116 +++-------------------------------- controller/dune | 2 +- controller/requests.ml | 130 ++++++++++++++++++++++++++++++++++++++++ controller/requests.mli | 26 ++++++++ 4 files changed, 164 insertions(+), 110 deletions(-) create mode 100644 controller/requests.ml create mode 100644 controller/requests.mli diff --git a/controller/coq_lsp.ml b/controller/coq_lsp.ml index 43a697489..166dee273 100644 --- a/controller/coq_lsp.ml +++ b/controller/coq_lsp.ml @@ -178,9 +178,6 @@ let lsp_of_progress ~uri ~version progress = 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 @@ -273,38 +270,9 @@ 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 ~params = +let do_document_request ~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 result = `List slist in - Ok result - | Stopped _ | Failed _ -> - (* -32802 = RequestFailed | -32803 = ServerCancelled ; *) - let code = -32802 in - let message = "Document is not ready" in - Error (code, message) + handler ~uri ~doc let do_position_request ~params ~handler = let _uri, doc = get_textDocument params in @@ -324,86 +292,16 @@ let do_position_request ~params ~handler = let message = "Document is not ready" in Result.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 ~handler:hover_handler +let do_symbols = do_document_request ~handler:Requests.symbols +let do_hover = do_position_request ~handler:Requests.hover +let do_goals = do_position_request ~handler:Requests.goals +let do_completion = do_position_request ~handler:Requests.completion let do_trace params = let trace = string_field "value" params in LIO.set_trace_value (LIO.TraceValue.of_string 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 = do_position_request ~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 = do_position_request ~handler:completion_handler +(* Memo stuff *) let memo_cache_file = ".coq-lsp.cache" let memo_save_to_disk () = diff --git a/controller/dune b/controller/dune index 61d482987..ff0d6be99 100644 --- a/controller/dune +++ b/controller/dune @@ -1,6 +1,6 @@ (executable (name coq_lsp) - (modules coq_lsp version) + (modules version requests coq_lsp) (public_name coq-lsp) (preprocess (staged_pps ppx_import ppx_deriving_yojson)) diff --git a/controller/requests.ml b/controller/requests.ml new file mode 100644 index 000000000..68b200e0d --- /dev/null +++ b/controller/requests.ml @@ -0,0 +1,130 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* doc:Fleche.Doc.t -> (Yojson.Safe.t, int * string) Result.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 (fun v -> v.Fleche.Doc.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 ~uri ~(doc : Fleche.Doc.t) = + match doc.completed with + | Yes _ -> + 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 + let result = `List slist in + Ok result + | Stopped _ | Failed _ -> + (* -32802 = RequestFailed | -32803 = ServerCancelled ; *) + let code = -32802 in + let message = "Document is not ready" in + Error (code, message) + +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 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.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; _ } = 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 ~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 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..723d680fd --- /dev/null +++ b/controller/requests.mli @@ -0,0 +1,26 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* doc:Fleche.Doc.t -> (Yojson.Safe.t, int * string) Result.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 From 38fe8e1aea791856c3c655b6ddb12e4f3da319b2 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Tue, 10 Jan 2023 23:48:56 +0100 Subject: [PATCH 16/39] [controller] Refactor memo cache, move to its own file. --- controller/cache.ml | 47 +++++++++++++++++++++++++++++++++++++++++++ controller/cache.mli | 19 +++++++++++++++++ controller/coq_lsp.ml | 35 +++----------------------------- controller/dune | 2 +- 4 files changed, 70 insertions(+), 33 deletions(-) create mode 100644 controller/cache.ml create mode 100644 controller/cache.mli 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 166dee273..95c570c1f 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 *) (************************************************************************) @@ -301,35 +301,6 @@ let do_trace params = let trace = string_field "value" params in LIO.set_trace_value (LIO.TraceValue.of_string trace) -(* Memo stuff *) -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. @@ -360,7 +331,7 @@ let dispatch_notification ofmt ~state ~method_ ~params = | "textDocument/didOpen" -> do_open ~state params | "textDocument/didChange" -> do_change params | "textDocument/didClose" -> do_close ofmt params - | "textDocument/didSave" -> memo_save_to_disk () + | "textDocument/didSave" -> Cache.save_to_disk () (* NOOPs *) | "initialized" -> () (* Generic handler *) @@ -510,7 +481,7 @@ let lsp_main bt std coqlib vo_load_path ml_include_path = (* Core LSP loop context *) let state = { State.root_state; workspace; fb_queue } in - memo_read_from_disk (); + Cache.read_from_disk (); let (_ : Thread.t) = Thread.create (fun () -> process_queue oc ~state) () in diff --git a/controller/dune b/controller/dune index ff0d6be99..64ee60896 100644 --- a/controller/dune +++ b/controller/dune @@ -1,6 +1,6 @@ (executable (name coq_lsp) - (modules version requests coq_lsp) + (modules version cache requests coq_lsp) (public_name coq-lsp) (preprocess (staged_pps ppx_import ppx_deriving_yojson)) From 798c06c202895767fa8f37984e1d5e00a3236425 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Wed, 11 Jan 2023 00:33:32 +0100 Subject: [PATCH 17/39] [controller] Refactor document handling, move to its own file. --- controller/coq_lsp.ml | 145 +++---------------------------------- controller/doc_manager.ml | 131 +++++++++++++++++++++++++++++++++ controller/doc_manager.mli | 43 +++++++++++ controller/dune | 2 +- controller/lsp_util.ml | 40 ++++++++++ controller/lsp_util.mli | 25 +++++++ 6 files changed, 252 insertions(+), 134 deletions(-) create mode 100644 controller/doc_manager.ml create mode 100644 controller/doc_manager.mli create mode 100644 controller/lsp_util.ml create mode 100644 controller/lsp_util.mli diff --git a/controller/coq_lsp.ml b/controller/coq_lsp.ml index 95c570c1f..4d6236abd 100644 --- a/controller/coq_lsp.ml +++ b/controller/coq_lsp.ml @@ -55,6 +55,7 @@ end module LIO = Lsp.Io module LSP = Lsp.Base +module Check = Doc_manager.Check (* Request Handling: The client expects a reply *) module CoqLspOption = struct @@ -113,99 +114,6 @@ let do_initialize ~params = let do_shutdown ~params:_ = Ok `Null -(* XXX: We need to handle this better *) -exception AbortRequest - -(* 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 = - 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 ~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) - ] - in - LSP.mk_notification ~method_:"$/coq/fileProgress" ~params - -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 - - (* Notification handling; reply is optional / asynchronous *) - let do_check ofmt ~fb_queue ~uri = - match DocHandle.find_opt ~uri with - | Some handle -> - 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 - | None -> - LIO.trace "Check.do_check" ("file " ^ uri ^ " not available"); - () - - let completed uri = - let doc = DocHandle.find_doc ~uri in - match doc.completed with - | Yes _ | Failed _ -> true - | Stopped _ -> false - - let schedule ~uri = pending := Some uri -end - let do_open ~state params = let document = dict_field "textDocument" params in let uri, version, contents = @@ -214,18 +122,7 @@ let do_open ~state params = , string_field "text" document ) in let root_state, workspace = State.(state.root_state, state.workspace) in - match - Fleche.Doc.create ~state:root_state ~workspace ~uri ~contents ~version - with - | Coq.Protect.R.Completed (Result.Ok doc) -> - DocHandle.create ~uri ~doc; - Check.schedule ~uri - (* Maybe send some diagnostics in this case? *) - | Coq.Protect.R.Completed (Result.Error (Anomaly (_, msg))) - | Coq.Protect.R.Completed (Result.Error (User (_, msg))) -> - let msg = Pp.string_of_ppcmds msg in - LIO.trace "Fleche.Doc.create" ("internal error" ^ msg) - | Coq.Protect.R.Interrupted -> () + Doc_manager.create ~root_state ~workspace ~uri ~contents ~version let do_change params = let document = dict_field "textDocument" params in @@ -240,29 +137,17 @@ let do_change params = assert false | 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 *) - () + Doc_manager.change ~uri ~version ~contents 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 = @@ -370,7 +255,7 @@ 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 - | AbortRequest -> + | 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 @@ -390,17 +275,11 @@ 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) + | None -> + Control.interrupt := false; + Check.check_or_yield ofmt ~fb_queue:state.State.fb_queue | Some com -> - (* TODO we should optimize the queue *) + (* TODO: optimize the queue? *) ignore (Queue.pop request_queue); LIO.trace "process_queue" ("Serving Request: " ^ LSP.Message.method_ com); (* We let Coq work normally now *) @@ -413,10 +292,10 @@ let lsp_cb oc = { trace = LIO.trace ; send_diagnostics = (fun ~uri ~version diags -> - lsp_of_diags ~uri ~version diags |> Lsp.Io.send_json oc) + Lsp_util.lsp_of_diags ~uri ~version diags |> Lsp.Io.send_json oc) ; send_fileProgress = (fun ~uri ~version progress -> - lsp_of_progress ~uri ~version progress |> Lsp.Io.send_json oc) + Lsp_util.lsp_of_progress ~uri ~version progress |> Lsp.Io.send_json oc) } let lvl_to_severity (lvl : Feedback.level) = diff --git a/controller/doc_manager.ml b/controller/doc_manager.ml new file mode 100644 index 000000000..1cce55433 --- /dev/null +++ b/controller/doc_manager.ml @@ -0,0 +1,131 @@ +(************************************************************************) +(* * 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; requests = () } + + 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 ~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 diags_of_doc doc = + List.concat_map (fun node -> node.Fleche.Doc.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 ~fb_queue ~uri = + LIO.trace "process_queue" "resuming document checking"; + match Handle.find_opt ~uri with + | Some handle -> + let doc = Fleche.Doc.check ~ofmt ~doc:handle.doc ~fb_queue in + Handle.update_doc_info ~handle ~doc; + 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 + | None -> + LIO.trace "Check.check" ("file " ^ uri ^ " not available"); + () + + let check_or_yield ofmt ~fb_queue = + match !pending with + | None -> Thread.delay 0.1 + | Some uri -> check ofmt ~fb_queue ~uri + + let schedule ~uri = pending := Some uri +end + +let create ~root_state ~workspace ~uri ~contents ~version = + match + Fleche.Doc.create ~state:root_state ~workspace ~uri ~contents ~version + with + | Coq.Protect.R.Completed (Result.Ok doc) -> + Handle.create ~uri ~doc; + Check.schedule ~uri + (* Maybe send some diagnostics in this case? *) + | Coq.Protect.R.Completed (Result.Error (Anomaly (_, msg))) + | Coq.Protect.R.Completed (Result.Error (User (_, msg))) -> + let msg = Pp.string_of_ppcmds msg in + LIO.trace "Fleche.Doc.create" ("internal error" ^ msg) + | Coq.Protect.R.Interrupted -> () + +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 () = Handle.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 close = Handle.close +let find_doc = Handle.find_doc diff --git a/controller/doc_manager.mli b/controller/doc_manager.mli new file mode 100644 index 000000000..2978afa52 --- /dev/null +++ b/controller/doc_manager.mli @@ -0,0 +1,43 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* fb_queue:Coq.Message.t list ref -> unit +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 *) +val change : uri:string -> version:int -> contents:string -> unit + +(** 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 diff --git a/controller/dune b/controller/dune index 64ee60896..e379444f6 100644 --- a/controller/dune +++ b/controller/dune @@ -1,6 +1,6 @@ (executable (name coq_lsp) - (modules version cache requests 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 From 9c13d4998478a7e0e21d4f0671fb1fdb0b0daa4d Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Tue, 10 Jan 2023 22:23:21 +0100 Subject: [PATCH 18/39] [controller] Follow the initialize specification better. To that extent we introduce a special init loop for server initialization. See: https://microsoft.github.io/language-server-protocol/specifications/lsp/3.17/specification/#initialize --- CHANGES.md | 2 + controller/coq_lsp.ml | 176 ++++++++++++++++++++++++++---------------- coq/workspace.ml | 4 +- 3 files changed, 115 insertions(+), 67 deletions(-) diff --git a/CHANGES.md b/CHANGES.md index 5489615cb..d17d963ee 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -3,6 +3,8 @@ - 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) # coq-lsp 0.1.2: Message ------------------------ diff --git a/controller/coq_lsp.ml b/controller/coq_lsp.ml index 4d6236abd..cf50ee5a6 100644 --- a/controller/coq_lsp.ml +++ b/controller/coq_lsp.ml @@ -62,7 +62,7 @@ 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 @@ -100,17 +100,15 @@ let do_initialize ~params = ; ("codeActionProvider", `Bool false) ] in - let result = - `Assoc - [ ("capabilities", `Assoc capabilities) - ; ( "serverInfo" - , `Assoc - [ ("name", `String "coq-lsp (C) Inria 2022") - ; ("version", `String "0.1+alpha") - ] ) - ] - in - Ok result + `Assoc + [ ("capabilities", `Assoc capabilities) + ; ( "serverInfo" + , `Assoc + [ ("name", `String "coq-lsp (C) Inria 2023") + ; ("version", `String Version.server) + ] ) + ] + |> Result.ok let do_shutdown ~params:_ = Ok `Null @@ -186,26 +184,57 @@ let do_trace params = let trace = string_field "value" params in LIO.set_trace_value (LIO.TraceValue.of_string trace) -(* 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. +(** 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 - Also, this should eventually become a queue, instead of a single - change_pending setup. *) -let request_queue = Queue.create () +let answer_request ofmt ~id result = + (match result with + | Ok result -> LSP.mk_reply ~id ~result + | Error (code, message) -> LSP.mk_request_error ~id ~code ~message) + |> LIO.send_json ofmt -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 +(***********************************************************************) +(** LSP Init routine *) exception Lsp_exit +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 *) @@ -225,7 +254,9 @@ let dispatch_notification ofmt ~state ~method_ ~params = let dispatch_request ~method_ ~params = match method_ with (* Lifecyle *) - | "initialize" -> do_initialize ~params + | "initialize" -> + (* XXX This can't happen here *) + do_initialize ~params | "shutdown" -> do_shutdown ~params (* Symbols and info about the document *) | "textDocument/completion" -> do_completion ~params @@ -236,13 +267,10 @@ let dispatch_request ~method_ ~params = (* Generic handler *) | msg -> LIO.trace "no_handler" msg; - Ok `Null + Error (-32601, "method not found") let dispatch_request ofmt ~id ~method_ ~params = - (match dispatch_request ~method_ ~params with - | Ok result -> LSP.mk_reply ~id ~result - | Error (code, message) -> LSP.mk_request_error ~id ~code ~message) - |> LIO.send_json ofmt + dispatch_request ~method_ ~params |> answer_request ofmt ~id let dispatch_message ofmt ~state (com : LSP.Message.t) = match com with @@ -271,6 +299,16 @@ let dispatch_message ofmt ~state com = LIO.trace "process_queue" Pp.(string_of_ppcmds CErrors.(iprint iexn)); LIO.trace "BT" bt +(***********************************************************************) +(* 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 rec process_queue ofmt ~state = if Fleche.Debug.sched_wakeup then LIO.trace "<- dequeue" (Format.asprintf "%.2f" (Unix.gettimeofday ())); @@ -287,6 +325,15 @@ let rec process_queue ofmt ~state = dispatch_message ofmt ~state com); process_queue ofmt ~state +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 oc = Fleche.Io.CallBack. { trace = LIO.trace @@ -324,56 +371,55 @@ let mk_fb_handler () = | _ -> ()) , q ) -let log_workspace w = - let message, extra = Coq.Workspace.describe w in - LIO.trace "workspace" "initialized" ~extra; - LIO.logMessage ~lvl:3 ~message +let coq_init bt = + 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 + (Coq.Init.(coq_init { fb_handler; debug; load_module; load_plugin }), fb_queue) 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 oc); - (* 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 + (* IMPORTANT: LSP spec forbids any message from server to client before + initialize is received *) - (* Workspace initialization *) + (* Core Coq initialization *) + let root_state, fb_queue = coq_init 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 - Cache.read_from_disk (); + (* Core LSP loop context *) + let state = { State.root_state; workspace; fb_queue } in - let (_ : Thread.t) = Thread.create (fun () -> process_queue oc ~state) () in + (* Read workspace state (noop for now) *) + Cache.read_from_disk (); - 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; - (match LSP.Message.from_yojson com with - | Ok msg -> process_input msg - | Error msg -> LIO.trace "read_request" ("error: " ^ msg)); - loop () - in - try loop () with + let (_ : Thread.t) = Thread.create (fun () -> process_queue oc ~state) () in + + read_loop () + with | (LIO.ReadError "EOF" | Lsp_exit) as exn -> let message = "server exiting" diff --git a/coq/workspace.ml b/coq/workspace.ml index 7f7bad1b6..63dd12fc7 100644 --- a/coq/workspace.ml +++ b/coq/workspace.ml @@ -73,10 +73,10 @@ let describe { coqlib; kind; vo_load_path; ml_include_path; require_libs; _ } = let n_ml = List.length ml_include_path in let extra = Format.asprintf "@[vo_paths:@\n @[%a@]@\nml_paths:@\n @[%a@]@]" - Format.(pp_print_list pp_print_string) - ml_include_path (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\ From 2ed5daf7a8b9308f6ca603241539c615969f03bb Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Wed, 11 Jan 2023 02:00:14 +0100 Subject: [PATCH 19/39] [code] Allow goals to follow selection update by a command Fixes #163 This makes VsCodeVim cursor tracking work; thanks to Cactus (Anton) Golov for detailed bug reporting and testing. --- CHANGES.md | 4 ++++ editor/code/package.json | 6 ++++-- editor/code/src/client.ts | 17 ++++++++++------- 3 files changed, 18 insertions(+), 9 deletions(-) diff --git a/CHANGES.md b/CHANGES.md index d17d963ee..96f33e7b5 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -5,6 +5,10 @@ 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 0.1.2: Message ------------------------ diff --git a/editor/code/package.json b/editor/code/package.json index 51eb153fa..dca40d7c8 100644 --- a/editor/code/package.json +++ b/editor/code/package.json @@ -136,12 +136,14 @@ "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..3c1f59d39 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 { @@ -164,13 +165,15 @@ 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 + : 1000; + const show = kind <= config.show_goals_on; if (show) { goals(evt.textEditor); From 1eb593bbd4ac68cf429315b7cf1ce94f531c7cb4 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Wed, 11 Jan 2023 01:32:28 +0100 Subject: [PATCH 20/39] [server] Warn the user of possible problems when >= 2 files are open. --- CHANGES.md | 7 +++++-- controller/doc_manager.ml | 16 ++++++++++++++++ 2 files changed, 21 insertions(+), 2 deletions(-) diff --git a/CHANGES.md b/CHANGES.md index 96f33e7b5..8fd2cde2a 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -1,5 +1,5 @@ -# coq-lsp 0.1.3: ------------------------- +# coq-lsp 0.1.3: View +--------------------- - Much improved handling of Coq fatal errors, the server is now hardened against them (@ejgallego, #155, #157, #160, fixes #91) @@ -9,6 +9,9 @@ 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) # coq-lsp 0.1.2: Message ------------------------ diff --git a/controller/doc_manager.ml b/controller/doc_manager.ml index 1cce55433..165bd2157 100644 --- a/controller/doc_manager.ml +++ b/controller/doc_manager.ml @@ -112,6 +112,22 @@ let create ~root_state ~workspace ~uri ~contents ~version = LIO.trace "Fleche.Doc.create" ("internal error" ^ msg) | Coq.Protect.R.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 ( From d14ab9c2940e34e0ee2026b10ce1aa421afc9542 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Wed, 11 Jan 2023 19:48:40 +0100 Subject: [PATCH 21/39] [code] [build] Update package-lock.json --- editor/code/package-lock.json | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) 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" From 2ce9b24300ebe78018b77684574811f2de24cb5d Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Tue, 3 Jan 2023 17:09:35 +0100 Subject: [PATCH 22/39] [controller] Allow to postpone and cancel requests Some requests need to be delayed until the document is ready, such as `documentSymbols`. In order to do this, we allow to postpone requests, and `Doc_manager.check` will now return the list of requests pending for a given document. The implementation is lightweight and quite a prototype, but should serve as a basis for more advanced stuff. Closes #124. --- CHANGES.md | 3 ++ controller/coq_lsp.ml | 101 +++++++++++++++++++++++++++++-------- controller/doc_manager.ml | 44 ++++++++++++---- controller/doc_manager.mli | 8 ++- controller/requests.ml | 20 ++------ controller/requests.mli | 4 +- 6 files changed, 130 insertions(+), 50 deletions(-) diff --git a/CHANGES.md b/CHANGES.md index 8fd2cde2a..d5c8363e7 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -12,6 +12,9 @@ - `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) # coq-lsp 0.1.2: Message ------------------------ diff --git a/controller/coq_lsp.ml b/controller/coq_lsp.ml index cf50ee5a6..31ca4f6f6 100644 --- a/controller/coq_lsp.ml +++ b/controller/coq_lsp.ml @@ -57,6 +57,22 @@ module LIO = Lsp.Io module LSP = Lsp.Base module Check = Doc_manager.Check +module PendingRequest = struct + type t = + { uri : string + ; handler : uri:string -> doc:Fleche.Doc.t -> 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] @@ -108,9 +124,9 @@ let do_initialize ~params = ; ("version", `String Version.server) ] ) ] - |> Result.ok + |> RResult.ok -let do_shutdown ~params:_ = Ok `Null +let do_shutdown ~params:_ = RResult.Ok `Null let do_open ~state params = let document = dict_field "textDocument" params in @@ -153,10 +169,6 @@ let get_position params = let line, character = (int_field "line" pos, int_field "character" pos) in (line, character) -let do_document_request ~params ~handler = - let uri, doc = get_textDocument params in - handler ~uri ~doc - let do_position_request ~params ~handler = let _uri, doc = get_textDocument params in let point = get_position params in @@ -168,18 +180,26 @@ let do_position_request ~params ~handler = line < loc.line_nb_last || (line = loc.line_nb_last && col <= loc.ep - loc.bol_pos_last) in - if in_range then Result.Ok (handler ~doc ~point) + if in_range then RResult.Ok (handler ~doc ~point) else (* -32802 = RequestFailed | -32803 = ServerCancelled ; *) let code = -32802 in let message = "Document is not ready" in - Result.Error (code, message) + RResult.Error (code, message) -let do_symbols = do_document_request ~handler:Requests.symbols let do_hover = do_position_request ~handler:Requests.hover let do_goals = do_position_request ~handler:Requests.goals let do_completion = do_position_request ~handler:Requests.completion +(* 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 ~uri ~doc) + | Stopped _ | Failed _ -> Postpone { uri; handler } + +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) @@ -196,11 +216,43 @@ let rec read_request ic = LIO.trace "read_request" ("error: " ^ msg); read_request ic +let rtable : (int, PendingRequest.t) Hashtbl.t = Hashtbl.create 673 + let answer_request ofmt ~id result = - (match result with - | Ok result -> LSP.mk_reply ~id ~result - | Error (code, message) -> LSP.mk_request_error ~id ~code ~message) - |> LIO.send_json ofmt + 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 ({ uri; _ } as pr) -> + Doc_manager.serve_on_completion ~uri ~id; + Hashtbl.add rtable id pr + +let do_cancel ofmt ~params = + let id = int_field "id" params in + match Hashtbl.find_opt rtable id with + | None -> + (* Request is not pending *) + () + | Some _ -> + Hashtbl.remove rtable id; + answer_request ofmt ~id (Error (-32800, "Cancelled by client")) + +let serve_postponed_request id = + match Hashtbl.find_opt rtable id with + | None -> + LIO.trace "can't serve cancelled request: " (string_of_int id); + None + | Some { uri; handler } -> + LIO.trace "serving rq: " (string_of_int id ^ " uri: " ^ uri); + Hashtbl.remove rtable id; + let doc = Doc_manager.find_doc ~uri in + Some (RResult.Ok (handler ~uri ~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 (***********************************************************************) @@ -246,6 +298,8 @@ let dispatch_notification ofmt ~state ~method_ ~params = | "textDocument/didChange" -> do_change params | "textDocument/didClose" -> do_close ofmt params | "textDocument/didSave" -> Cache.save_to_disk () + (* Cancel Request *) + | "$/cancelRequest" -> do_cancel ofmt ~params (* NOOPs *) | "initialized" -> () (* Generic handler *) @@ -255,8 +309,9 @@ let dispatch_request ~method_ ~params = match method_ with (* Lifecyle *) | "initialize" -> - (* XXX This can't happen here *) - do_initialize ~params + 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 @@ -309,20 +364,24 @@ let dispatch_message ofmt ~state com = (** Main event queue *) let request_queue = Queue.create () -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 +let dispatch_or_resume_check ofmt ~state = + match Queue.peek_opt request_queue with | None -> Control.interrupt := false; - Check.check_or_yield ofmt ~fb_queue:state.State.fb_queue + let ready = Check.check_or_yield ofmt ~fb_queue:state.State.fb_queue in + serve_postponed_requests ofmt ready | Some com -> (* TODO: optimize the queue? *) ignore (Queue.pop request_queue); LIO.trace "process_queue" ("Serving Request: " ^ LSP.Message.method_ com); (* We let Coq work normally now *) Control.interrupt := false; - dispatch_message ofmt ~state com); + 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 process_input (com : LSP.Message.t) = diff --git a/controller/doc_manager.ml b/controller/doc_manager.ml index 165bd2157..24af93210 100644 --- a/controller/doc_manager.ml +++ b/controller/doc_manager.ml @@ -24,7 +24,11 @@ exception AbortRequest module Handle = struct type t = { doc : Fleche.Doc.t - ; requests : unit (* placeholder for requests attached to a document *) + ; requests : Int.Set.t + (* For now we just store the request id to wake up on completion, + later on we may want to store a more interesting type, for example + "wake up when a location is reached", or always to continue the + streaming *) } let doc_table : (string, t) Hashtbl.t = Hashtbl.create 39 @@ -34,7 +38,7 @@ module Handle = struct | None -> () | Some _ -> LIO.trace "do_open" ("file " ^ uri ^ " not properly closed by client")); - Hashtbl.add doc_table uri { doc; requests = () } + Hashtbl.add doc_table uri { doc; requests = Int.Set.empty } let close ~uri = Hashtbl.remove doc_table uri @@ -48,16 +52,34 @@ module Handle = struct let find_opt ~uri = Hashtbl.find_opt doc_table uri let find_doc ~uri = (find ~uri).doc - let _update ~handle ~(doc : Fleche.Doc.t) = + 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) = - Hashtbl.replace doc_table doc.uri { doc; requests = () } + Hashtbl.replace doc_table doc.uri { doc; requests = Int.Set.empty } + + let attach_request ~uri ~id = + match Hashtbl.find_opt doc_table uri with + | Some { doc; requests } -> + let requests = Int.Set.add id requests in + Hashtbl.replace doc_table uri { doc; requests } + | 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 _ -> ({ doc; requests = Int.Set.empty }, handle.requests) + | Stopped _ -> (handle, Int.Set.empty) + | Failed _ -> (handle, Int.Set.empty) (* trigger pending incremental requests *) let update_doc_info ~handle ~(doc : Fleche.Doc.t) = - Hashtbl.replace doc_table doc.uri { handle with doc } + let handle, requests = do_requests ~doc ~handle in + Hashtbl.replace doc_table doc.uri handle; + requests end let diags_of_doc doc = @@ -78,21 +100,24 @@ module Check = struct match Handle.find_opt ~uri with | Some handle -> let doc = Fleche.Doc.check ~ofmt ~doc:handle.doc ~fb_queue in - Handle.update_doc_info ~handle ~doc; + 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 + if completed ~uri then pending := None; + requests | None -> LIO.trace "Check.check" ("file " ^ uri ^ " not available"); - () + Int.Set.empty let check_or_yield ofmt ~fb_queue = match !pending with - | None -> Thread.delay 0.1 + | None -> + Thread.delay 0.1; + Int.Set.empty | Some uri -> check ofmt ~fb_queue ~uri let schedule ~uri = pending := Some uri @@ -145,3 +170,4 @@ let change ~uri ~version ~contents = let close = Handle.close let find_doc = Handle.find_doc +let serve_on_completion ~uri ~id = Handle.attach_request ~uri ~id diff --git a/controller/doc_manager.mli b/controller/doc_manager.mli index 2978afa52..77ab1102c 100644 --- a/controller/doc_manager.mli +++ b/controller/doc_manager.mli @@ -17,9 +17,10 @@ module Check : sig (** Check a document, or yield if there is none pending; it will send progress - and diagnostics notifications to [ofmt] *) + and diagnostics notifications to [ofmt]. Will return the list of requests + that are ready to execute. *) val check_or_yield : - Format.formatter -> fb_queue:Coq.Message.t list ref -> unit + Format.formatter -> fb_queue:Coq.Message.t list ref -> Int.Set.t end (** Create a document *) @@ -41,3 +42,6 @@ exception AbortRequest (** [find_doc ~uri] , raises AbortRequest if [uri] is invalid *) val find_doc : uri:string -> Fleche.Doc.t + +(** Request support *) +val serve_on_completion : uri:string -> id:int -> unit diff --git a/controller/requests.ml b/controller/requests.ml index 68b200e0d..259649a46 100644 --- a/controller/requests.ml +++ b/controller/requests.ml @@ -15,9 +15,7 @@ (* Written by: Emilio J. Gallego Arias *) (************************************************************************) -type document_request = - uri:string -> doc:Fleche.Doc.t -> (Yojson.Safe.t, int * string) Result.t - +type document_request = uri:string -> doc:Fleche.Doc.t -> Yojson.Safe.t type position_request = doc:Fleche.Doc.t -> point:int * int -> Yojson.Safe.t module Util = struct @@ -44,18 +42,10 @@ let _kind_of_type _tm = 13 *) | _ -> 12 (* Function *) *) let symbols ~uri ~(doc : Fleche.Doc.t) = - match doc.completed with - | Yes _ -> - 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 - let result = `List slist in - Ok result - | Stopped _ | Failed _ -> - (* -32802 = RequestFailed | -32803 = ServerCancelled ; *) - let code = -32802 in - let message = "Document is not ready" in - Error (code, message) + 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 diff --git a/controller/requests.mli b/controller/requests.mli index 723d680fd..ae90dc2ea 100644 --- a/controller/requests.mli +++ b/controller/requests.mli @@ -15,9 +15,7 @@ (* Written by: Emilio J. Gallego Arias *) (************************************************************************) -type document_request = - uri:string -> doc:Fleche.Doc.t -> (Yojson.Safe.t, int * string) Result.t - +type document_request = uri:string -> doc:Fleche.Doc.t -> Yojson.Safe.t type position_request = doc:Fleche.Doc.t -> point:int * int -> Yojson.Safe.t val symbols : document_request From bd53b9564d1d3b5a61124948821c563ca92fc128 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Wed, 11 Jan 2023 21:53:48 +0100 Subject: [PATCH 23/39] [deps] Bump Coq and SerAPI to newer versions. Closes #88 --- coq/goals.ml | 5 +++-- coq/loader.ml | 12 +++++++++--- vendor/coq | 2 +- vendor/coq-serapi | 2 +- 4 files changed, 14 insertions(+), 7 deletions(-) diff --git a/coq/goals.ml b/coq/goals.ml index 40ede8e11..3fb9daf39 100644 --- a/coq/goals.ml +++ b/coq/goals.ml @@ -67,9 +67,10 @@ let get_hyp (ppx : Constr.t -> 'pc) (_sigma : Evd.evar_map) (hdecl : cdcl) : (** 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 (EvarInfo evi) = Evd.find sigma g in ppx @@ EConstr.to_constr ~abort_on_undefined_evars:false sigma - Evd.(evar_concl (find sigma g)) + Evd.(evar_concl evi) let build_info sigma g = { evar = g; name = Evd.evar_ident g sigma } @@ -77,7 +78,7 @@ let build_info sigma g = { evar = g; name = Evd.evar_ident g sigma } let process_goal_gen ppx sigma g : 'a reified_goal = (* XXX This looks cumbersome *) let env = Global.env () in - let evi = Evd.find sigma g in + let (EvarInfo evi) = Evd.find sigma g in let env = Evd.evar_filtered_env env evi in (* why is compaction neccesary... ? [eg for better display] *) let ctx = Termops.compact_named_context (Environ.named_context env) in 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/vendor/coq b/vendor/coq index 0b30c2161..34b1ee696 160000 --- a/vendor/coq +++ b/vendor/coq @@ -1 +1 @@ -Subproject commit 0b30c2161c7221e6269d1d8fa28dd92b75b118aa +Subproject commit 34b1ee696a8dab756a82859105d6338678e90ad0 diff --git a/vendor/coq-serapi b/vendor/coq-serapi index b532c6abb..dd9e3fbf7 160000 --- a/vendor/coq-serapi +++ b/vendor/coq-serapi @@ -1 +1 @@ -Subproject commit b532c6abb809e4e6f37d77234d4d10c51834a90c +Subproject commit dd9e3fbf7faaf3bf365fa3eff134641055151a9b From d0a66ed4d729279c94eb5c7ebb36dceb7e82196d Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Thu, 12 Jan 2023 19:57:32 +0100 Subject: [PATCH 24/39] [fleche] Some refactoring in preparation for a more controlled interp loop. Next step is to control not only resumption, but ending, to which extent a refactoring is convenient as to separate concerns of what the document can do vs what the user desires to do. --- controller/doc_manager.ml | 4 +- controller/requests.ml | 9 +- fleche/doc.ml | 274 +++++++++++++++++++++----------------- fleche/doc.mli | 38 ++++-- fleche/info.ml | 19 +-- fleche/info.mli | 2 +- 6 files changed, 197 insertions(+), 149 deletions(-) diff --git a/controller/doc_manager.ml b/controller/doc_manager.ml index 24af93210..8ab9d633a 100644 --- a/controller/doc_manager.ml +++ b/controller/doc_manager.ml @@ -83,7 +83,7 @@ module Handle = struct end let diags_of_doc doc = - List.concat_map (fun node -> node.Fleche.Doc.diags) doc.Fleche.Doc.nodes + List.concat_map Fleche.Doc.Node.diags doc.Fleche.Doc.nodes module Check = struct let pending = ref None @@ -99,7 +99,7 @@ module Check = struct LIO.trace "process_queue" "resuming document checking"; match Handle.find_opt ~uri with | Some handle -> - let doc = Fleche.Doc.check ~ofmt ~doc:handle.doc ~fb_queue in + let doc = Fleche.Doc.check ~ofmt ~doc:handle.doc ~fb_queue () in let requests = Handle.update_doc_info ~handle ~doc in let diags = diags_of_doc doc in let diags = diff --git a/controller/requests.ml b/controller/requests.ml index 259649a46..dc46fc64e 100644 --- a/controller/requests.ml +++ b/controller/requests.ml @@ -19,8 +19,7 @@ type document_request = uri:string -> doc:Fleche.Doc.t -> 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 (fun v -> v.Fleche.Doc.ast) doc.Fleche.Doc.nodes + 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 = @@ -88,7 +87,9 @@ 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 + match + List.filter (fun d -> d.Diagnostic.severity < 2) node.Doc.Node.diags + with | [] -> [] | e :: _ -> [ ("error", `String e.Diagnostic.message) ] @@ -100,7 +101,7 @@ 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 (fun node -> node.Doc.messages) node in + let messages = Option.map (fun node -> node.Doc.Node.messages) node in let error = Option.cata mk_error [] node in `Assoc ([ ( "textDocument" diff --git a/fleche/doc.ml b/fleche/doc.ml index 14cbb65e7..2f55c8dc9 100644 --- a/fleche/doc.ml +++ b/fleche/doc.ml @@ -14,14 +14,23 @@ let hd_opt ~default l = (* [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 + 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 + ; memo_info : string + } + + let loc { loc; _ } = loc + let ast { ast; _ } = ast + let state { state; _ } = state + let diags { diags; _ } = diags + let messages { messages; _ } = messages + let memo_info { memo_info; _ } = memo_info +end module Completion = struct type t = @@ -42,7 +51,7 @@ type t = ; contents : string ; end_loc : int * int * int ; root : Coq.State.t - ; nodes : node list + ; nodes : Node.t list ; diags_dirty : bool (** Used to optimize `eager_diagnostics` *) ; completed : Completion.t } @@ -81,7 +90,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 @@ -133,10 +142,10 @@ let bump_version ~version ~contents doc = | 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 = (* this is too noisy *) @@ -208,7 +217,7 @@ let rec discard_to_dot 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 _ -> ( @@ -238,11 +247,6 @@ let debug_parsed_sentence ~ast = 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 @@ -306,127 +310,151 @@ let build_span start_loc end_loc = ; ep = end_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 (* ast to process *) + +let parse_action ~st last_tok doc_handle = + let start_loc = Pcoq.Parsable.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 = Pcoq.Parsable.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 (Anomaly (_, msg)) | Error (User (None, msg)) -> + (* We don't have a better altenative :(, usually missing error loc here + means an anomaly, so we stop *) + let err_loc = last_tok in + let diags = [ mk_diag err_loc 1 msg ] in + (EOF (Failed last_tok), diags, time) + | Error (User (Some err_loc, msg)) -> + let diags = [ mk_diag err_loc 1 msg ] in + discard_to_dot doc_handle; + let last_tok = Pcoq.Parsable.loc doc_handle in + let span_loc = build_span start_loc last_tok in + (Skip (span_loc, last_tok), diags, time)) + +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 ~diags ~state = + { Node.loc; ast = None; diags; messages = []; state; memo_info = "" } + +let parsed_node ~loc ~ast ~diags ~messages ~state ~memo_info = + { Node.loc; ast = Some ast; diags; messages; state; memo_info } + +let maybe_ok_diagnostics ~loc = + if !Config.v.ok_diagnostics then + let ok_diag = mk_diag loc 3 (Pp.str "OK") in + [ ok_diag ] + else [] + +let node_of_coq_result ~fb_queue ~parsing_diags ~ast ~ast_loc ~doc ~st + ~memo_info last_tok res = + match res with + | Ok { Coq.Interp.Info.res = state; feedback } -> + let diags = maybe_ok_diagnostics ~loc:ast_loc in + let fb_diags, messages = process_feedback ~loc:ast_loc feedback in + let diags = parsing_diags @ fb_diags @ diags in + let node = + parsed_node ~loc:ast_loc ~ast ~diags ~messages ~state ~memo_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 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 recovery_st = state_recovery_heuristic doc st ast in + let node = + parsed_node ~loc:ast_loc ~ast ~diags ~messages ~state:recovery_st + ~memo_info + in + match coq_err with + | Anomaly _ -> Stop (Failed last_tok, node) + | User _ -> Continue { state = recovery_st; last_tok; node }) + +(* *) +let document_action ~fb_queue ~st ~parsing_diags ~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 ~diags:parsing_diags ~state:st in + Stop (completed, node) + (* Parsing error *) + | Skip (span_loc, last_tok) -> + let node = unparseable_node ~loc:span_loc ~diags:parsing_diags ~state:st in + Continue { state = st; last_tok; node } + (* We interpret the command now *) + | Process ast -> ( + let ast_loc = Coq.Ast.loc ast |> Option.get in + (* We register pre-interp for now *) + let res, memo_info = interp_and_info ~parsing_time ~st ~fb_queue ast in + match res 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 = Pcoq.Parsable.loc doc_handle in + node_of_coq_result ~fb_queue ~parsing_diags ~ast ~ast_loc ~doc ~st + ~memo_info last_tok_new res) + (* XXX: Imperative problem *) -let process_and_parse ~uri ~version ~fb_queue doc last_tok doc_handle = +let process_and_parse ?cutpoint:_ ~uri ~version ~fb_queue 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; if Debug.parsing then Io.Log.trace "coq" "parsing sentence"; (* Parsing *) let action, parsing_diags, parsing_time = - let start_loc = Pcoq.Parsable.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 = Pcoq.Parsable.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 (Anomaly (_, msg)) | Error (User (None, msg)) -> - (* We don't have a better altenative :(, usually missing error loc - here means an anomaly, so we stop *) - let err_loc = last_tok in - let diags = [ mk_diag err_loc 1 msg ] in - (EOF (Failed last_tok), diags, time) - | Error (User (Some err_loc, msg)) -> - let diags = [ mk_diag err_loc 1 msg ] in - discard_to_dot doc_handle; - let last_tok = Pcoq.Parsable.loc doc_handle in - let span_loc = build_span start_loc last_tok in - (Skip (span_loc, last_tok), diags, time)) + parse_action ~st last_tok doc_handle in (* Execution *) + let action = + document_action ~fb_queue ~st ~parsing_diags ~parsing_time ~doc last_tok + doc_handle action + in match action with - (* End of file *) - | EOF completed -> - let node = - { loc = Completion.loc completed - ; ast = None - ; diags = parsing_diags - ; messages = [] - ; state = st - ; memo_info = "" - } - in + | Interrupted last_tok -> set_completion ~completed:(Stopped last_tok) doc + | Stop (completed, node) -> let doc = add_node ~node doc in 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 = "" - } - in + | Continue { state; last_tok; node } -> 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 - (* We register pre-interp for now *) - 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 = Pcoq.Parsable.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 (Anomaly (err_loc, msg) as coq_err) - | Error (User (err_loc, msg) as coq_err) -> ( - let err_loc = Option.default ast_loc err_loc in - let diags = [ mk_error_diagnostic ~loc:err_loc ~msg ~ast ] in - (* FB should be handled by Coq.Protect.eval XXX *) - 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 - match coq_err with - | Anomaly _ -> set_completion ~completed:(Failed last_tok_new) doc - | User _ -> stm doc st last_tok_new))) + stm doc state last_tok 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) + hd_opt ~default:doc.root + (List.map (fun { Node.state; _ } -> state) doc.nodes) in stm doc st last_tok @@ -475,7 +503,7 @@ let safe_sub s pos len = s) else String.sub s pos len -let check ~ofmt:_ ~doc ~fb_queue = +let check ~ofmt:_ ~fb_queue ?cutpoint ~doc () = match doc.completed with | Yes _ -> Io.Log.trace "check" "resuming, completed=yes, nothing to do"; @@ -503,7 +531,9 @@ let check ~ofmt:_ ~doc ~fb_queue = let doc = { doc with contents = processed_content; nodes = List.rev doc.nodes } in - let doc = process_and_parse ~uri ~version ~fb_queue doc last_tok handle in + let doc = + process_and_parse ?cutpoint ~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 diff --git a/fleche/doc.mli b/fleche/doc.mli index d8c60f840..5183ad66f 100644 --- a/fleche/doc.mli +++ b/fleche/doc.mli @@ -18,17 +18,26 @@ (* [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 + 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 + ; memo_info : string + } + + 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 memo_info : t -> string +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 *) @@ -40,7 +49,7 @@ type t = private ; contents : string ; end_loc : int * int * int ; root : Coq.State.t - ; nodes : node list + ; nodes : Node.t list ; diags_dirty : bool ; completed : Completion.t } @@ -56,5 +65,12 @@ val create : val bump_version : version:int -> contents:string -> t -> t +(** [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 -> doc:t -> fb_queue:Coq.Message.t list ref -> t + ofmt:Format.formatter + -> fb_queue:Coq.Message.t list ref + -> ?cutpoint:int * int + -> doc:t + -> unit + -> t diff --git a/fleche/info.ml b/fleche/info.ml index 60a8cd175..78850b42e 100644 --- a/fleche/info.ml +++ b/fleche/info.ml @@ -113,7 +113,7 @@ 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 @@ -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 -> @@ -167,7 +167,6 @@ module Make (P : Point) : S with module P := P = struct let pr_goal st = let ppx env sigma x = - (* It is conveneint to optimize the Pp.t type, see [Jscoq_util.pp_opt] *) Coq.Print.pr_ltype_env ~goal_concl_style:true env sigma x in let lemmas = Coq.State.lemmas ~st in @@ -175,11 +174,11 @@ module Make (P : Point) : S with module P := P = struct 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 @@ -189,13 +188,15 @@ module Make (P : Point) : S with module P := P = struct let goals ~doc ~point approx = find ~doc ~point approx - |> obind (fun node -> in_state ~st:node.Doc.state ~f:pr_goal node.Doc.state) + |> obind (fun node -> + 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.memo_info (* XXX: This belongs in Coq *) let pr_extref gr = @@ -210,7 +211,7 @@ module Make (P : Point) : S with module P := P = struct let completion ~doc ~point prefix = find ~doc ~point Exact |> obind (fun node -> - 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..fdfe9bc70 100644 --- a/fleche/info.mli +++ b/fleche/info.mli @@ -44,7 +44,7 @@ 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 From 588cc4769a56f4f0b5f6c58e6cdd33f17bef88f5 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Thu, 12 Jan 2023 21:05:17 +0100 Subject: [PATCH 25/39] [coq] Capture all feedback as a side-effect in protect. This is way more principled and avoids the Coq-specific `fb_queue` propagating along most of the API. Downside: we are now more exposed to the lack of thread-safety of the feedback approach. --- controller/coq_lsp.ml | 51 +++++---- controller/doc_manager.ml | 31 +++--- controller/doc_manager.mli | 3 +- coq/init.mli | 2 +- coq/interp.ml | 40 +------ coq/interp.mli | 15 +-- coq/parsing.mli | 2 +- coq/print.ml | 4 +- coq/print.mli | 6 +- coq/protect.ml | 25 ++++- coq/protect.mli | 23 +++- coq/state.mli | 2 +- fleche/doc.ml | 213 ++++++++++++++++++++----------------- fleche/doc.mli | 8 +- fleche/info.ml | 18 +++- fleche/io.ml | 31 ++++-- fleche/io.mli | 28 ++++- fleche/memo.ml | 68 ++++-------- fleche/memo.mli | 21 ++-- 19 files changed, 320 insertions(+), 271 deletions(-) diff --git a/controller/coq_lsp.ml b/controller/coq_lsp.ml index 31ca4f6f6..3facc4fdc 100644 --- a/controller/coq_lsp.ml +++ b/controller/coq_lsp.ml @@ -49,7 +49,6 @@ module State = struct type t = { root_state : Coq.State.t ; workspace : Coq.Workspace.t - ; fb_queue : Coq.Message.t list ref } end @@ -368,7 +367,7 @@ 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 ~fb_queue:state.State.fb_queue in + let ready = Check.check_or_yield ~ofmt in serve_postponed_requests ofmt ready | Some com -> (* TODO: optimize the queue? *) @@ -393,15 +392,16 @@ let process_input (com : LSP.Message.t) = Control.interrupt := true (* Main loop *) -let lsp_cb oc = +let lsp_cb = Fleche.Io.CallBack. { trace = LIO.trace ; send_diagnostics = - (fun ~uri ~version diags -> - Lsp_util.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_util.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) = @@ -416,26 +416,22 @@ 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 coq_init bt = - let fb_handler, fb_queue = mk_fb_handler () in +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 }), fb_queue) + 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; @@ -446,13 +442,14 @@ let lsp_main bt std coqlib vo_load_path ml_include_path = (* Set log channel *) LIO.set_log_channel oc; - Fleche.Io.CallBack.set (lsp_cb oc); + Fleche.Io.CallBack.set lsp_cb; (* IMPORTANT: LSP spec forbids any message from server to client before initialize is received *) (* Core Coq initialization *) - let root_state, fb_queue = coq_init bt in + 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 @@ -470,7 +467,7 @@ let lsp_main bt std coqlib vo_load_path ml_include_path = let workspace = lsp_init_loop ic oc ~cmdline in (* Core LSP loop context *) - let state = { State.root_state; workspace; fb_queue } in + let state = { State.root_state; workspace } in (* Read workspace state (noop for now) *) Cache.read_from_disk (); diff --git a/controller/doc_manager.ml b/controller/doc_manager.ml index 8ab9d633a..dfcd14bf6 100644 --- a/controller/doc_manager.ml +++ b/controller/doc_manager.ml @@ -95,11 +95,11 @@ module Check = struct | Stopped _ -> false (* Notification handling; reply is optional / asynchronous *) - let check ofmt ~fb_queue ~uri = + let check ofmt ~uri = LIO.trace "process_queue" "resuming document checking"; match Handle.find_opt ~uri with | Some handle -> - let doc = Fleche.Doc.check ~ofmt ~doc:handle.doc ~fb_queue () in + let doc = Fleche.Doc.check ~ofmt ~doc:handle.doc () in let requests = Handle.update_doc_info ~handle ~doc in let diags = diags_of_doc doc in let diags = @@ -113,29 +113,34 @@ module Check = struct LIO.trace "Check.check" ("file " ^ uri ^ " not available"); Int.Set.empty - let check_or_yield ofmt ~fb_queue = + let check_or_yield ~ofmt = match !pending with | None -> Thread.delay 0.1; Int.Set.empty - | Some uri -> check ofmt ~fb_queue ~uri + | Some uri -> check ofmt ~uri let schedule ~uri = pending := Some uri end let create ~root_state ~workspace ~uri ~contents ~version = - match + let r = Fleche.Doc.create ~state:root_state ~workspace ~uri ~contents ~version - with - | Coq.Protect.R.Completed (Result.Ok doc) -> + in + match r with + | Completed (Result.Ok doc) -> Handle.create ~uri ~doc; Check.schedule ~uri - (* Maybe send some diagnostics in this case? *) - | Coq.Protect.R.Completed (Result.Error (Anomaly (_, msg))) - | Coq.Protect.R.Completed (Result.Error (User (_, msg))) -> - let msg = Pp.string_of_ppcmds msg in - LIO.trace "Fleche.Doc.create" ("internal error" ^ msg) - | Coq.Protect.R.Interrupted -> () + | 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 diff --git a/controller/doc_manager.mli b/controller/doc_manager.mli index 77ab1102c..aacf04e01 100644 --- a/controller/doc_manager.mli +++ b/controller/doc_manager.mli @@ -19,8 +19,7 @@ module Check : sig (** Check a document, or yield if there is none pending; it will send progress and diagnostics notifications to [ofmt]. Will return the list of requests that are ready to execute. *) - val check_or_yield : - Format.formatter -> fb_queue:Coq.Message.t list ref -> Int.Set.t + val check_or_yield : ofmt:Format.formatter -> Int.Set.t end (** Create a document *) diff --git a/coq/init.mli b/coq/init.mli index 42351de8d..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 Protect.R.t + -> State.t Protect.E.t diff --git a/coq/interp.ml b/coq/interp.ml index ff3f261c4..f74c84fcc 100644 --- a/coq/interp.ml +++ b/coq/interp.ml @@ -16,49 +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 _err -> - Marshal.to_channel oc 1 []; - (* Marshal.to_channel oc loc []; *) - (* Marshal.to_channel oc msg []; *) - ()) - -(* Needs to be implemeted by Protect.marshal_in *) -let marshal_in _f _ic = Obj.magic 0 -(* let tag : int = Marshal.from_channel ic in if tag = 0 then let res = f ic in - Protect.R.Completed (Ok { Info.res; feedback = [] }) else let loc : Loc.t - option = Marshal.from_channel ic in let msg : Pp.t = Marshal.from_channel ic - in Protect.R.Completed (Error (User (loc, msg))) *) + { 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/parsing.mli b/coq/parsing.mli index aba4a267b..35b81377d 100644 --- a/coq/parsing.mli +++ b/coq/parsing.mli @@ -1 +1 @@ -val parse : st:State.t -> Pcoq.Parsable.t -> Ast.t option Protect.R.t +val parse : st:State.t -> Pcoq.Parsable.t -> Ast.t option Protect.E.t diff --git a/coq/print.ml b/coq/print.ml index 4c8de0a4f..43aaa9d62 100644 --- a/coq/print.ml +++ b/coq/print.ml @@ -3,6 +3,4 @@ let pr_ltype_env ~goal_concl_style env sigma x = let pr_ltype_env ~goal_concl_style env sigma x = let f = pr_ltype_env ~goal_concl_style env sigma in - match Protect.eval ~f x with - | Protect.R.Completed (Ok pr) -> pr - | _ -> Pp.str "printer failed!" + Protect.eval ~f x diff --git a/coq/print.mli b/coq/print.mli index 6caa3f407..e4ad9c818 100644 --- a/coq/print.mli +++ b/coq/print.mli @@ -1,2 +1,6 @@ val pr_ltype_env : - goal_concl_style:bool -> Environ.env -> Evd.evar_map -> Constr.t -> Pp.t + goal_concl_style:bool + -> Environ.env + -> Evd.evar_map + -> Constr.t + -> Pp.t Protect.E.t diff --git a/coq/protect.ml b/coq/protect.ml index 5e221add4..e3cf04c1b 100644 --- a/coq/protect.ml +++ b/coq/protect.ml @@ -29,7 +29,8 @@ module R = struct map_error ~f end -let eval ~f x = +(* Eval and reify exceptions *) +let eval_exn ~f x = try let res = f x in R.Completed (Ok res) @@ -41,3 +42,25 @@ let eval ~f x = let msg = CErrors.iprint (e, info) in 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 5cb645056..c477da339 100644 --- a/coq/protect.mli +++ b/coq/protect.mli @@ -1,3 +1,8 @@ +(** 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 @@ -19,6 +24,20 @@ module R : sig 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 + +(** Must be hooked to allow [Protect] to capture the feedback. *) +val fb_queue : Message.t list ref + (** Eval a function and reify the exceptions. Note [f] _must_ be pure, as in - case of anomaly [f] may be re-executed with debug options. *) -val eval : f:('i -> 'o) -> 'i -> 'o R.t + 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.mli b/coq/state.mli index f747e0bdf..e918a5634 100644 --- a/coq/state.mli +++ b/coq/state.mli @@ -13,7 +13,7 @@ val lemmas : st:t -> Vernacstate.LemmaStack.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.R.t +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 diff --git a/fleche/doc.ml b/fleche/doc.ml index 2f55c8dc9..c8e954313 100644 --- a/fleche/doc.ml +++ b/fleche/doc.ml @@ -7,10 +7,48 @@ (* 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 + } +end (* [node list] is a very crude form of a meta-data map "loc -> data" , where for now [data] is only the goals. *) @@ -65,20 +103,30 @@ 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 + let last_line = Util.hd_opt ~default:"" (List.rev lines) in (List.length lines, String.length last_line, 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 + [ { Node.loc; ast = None; state; diags; messages; memo_info = "" } ] + else [] + let create ~state ~workspace ~uri ~version ~contents = - Coq.Protect.R.map (mk_doc state workspace) ~f:(fun root -> + let { Coq.Protect.E.r; feedback } = mk_doc state workspace in + Coq.Protect.R.map r ~f:(fun root -> + 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 = false - ; completed = Stopped (init_loc ~uri) + ; nodes + ; diags_dirty + ; completed = Stopped init_loc }) let recover_up_to_offset doc offset = @@ -147,13 +195,13 @@ let add_node ~node doc = 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 @@ -247,46 +295,16 @@ let debug_parsed_sentence ~ast = Io.Log.trace "coq" ("parsed sentence: " ^ line ^ Pp.string_of_ppcmds (Coq.Ast.print ast)) -(* 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 @@ -302,46 +320,40 @@ let interp_and_info ~parsing_time ~st ~fb_queue ast = 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 - } - 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 (* ast to process *) +(* Returns parse_action, diags, parsing_time *) let parse_action ~st last_tok doc_handle = let start_loc = Pcoq.Parsable.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 -> ( + 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 = Pcoq.Parsable.loc doc_handle in - (EOF (Yes last_tok), [], time) + (EOF (Yes last_tok), [], feedback, time) | Ok (Some ast) -> let () = if Debug.parsing then debug_parsed_sentence ~ast in - (Process ast, [], time) + (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 diags = [ mk_diag err_loc 1 msg ] in - (EOF (Failed last_tok), diags, time) + 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 diags = [ mk_diag err_loc 1 msg ] in + let parse_diags = [ Util.mk_diag err_loc 1 msg ] in discard_to_dot doc_handle; let last_tok = Pcoq.Parsable.loc doc_handle in - let span_loc = build_span start_loc last_tok in - (Skip (span_loc, last_tok), diags, time)) + let span_loc = Util.build_span start_loc last_tok in + (Skip (span_loc, last_tok), parse_diags, feedback, time)) type document_action = | Stop of Completion.t * Node.t @@ -352,25 +364,32 @@ type document_action = } | Interrupted of Loc.t -let unparseable_node ~loc ~diags ~state = - { Node.loc; ast = None; diags; messages = []; state; memo_info = "" } +let unparseable_node ~loc ~parsing_diags ~parsing_feedback ~state = + let fb_diags, messages = Util.diags_of_feedback ~loc parsing_feedback in + let diags = fb_diags @ parsing_diags in + { Node.loc; ast = None; diags; messages; state; memo_info = "" } let parsed_node ~loc ~ast ~diags ~messages ~state ~memo_info = { Node.loc; ast = Some ast; diags; messages; state; memo_info } let maybe_ok_diagnostics ~loc = if !Config.v.ok_diagnostics then - let ok_diag = mk_diag loc 3 (Pp.str "OK") in + let ok_diag = Util.mk_diag loc 3 (Pp.str "OK") in [ ok_diag ] else [] -let node_of_coq_result ~fb_queue ~parsing_diags ~ast ~ast_loc ~doc ~st - ~memo_info last_tok res = +let node_of_coq_result ~feedback ~parsing_feedback ~ast ~doc ~st ~memo_info + last_tok res = + let ast_loc = Coq.Ast.loc ast |> Option.get in match res with - | Ok { Coq.Interp.Info.res = state; feedback } -> - let diags = maybe_ok_diagnostics ~loc:ast_loc in - let fb_diags, messages = process_feedback ~loc:ast_loc feedback in - let diags = parsing_diags @ fb_diags @ diags in + | Ok { Coq.Interp.Info.res = state } -> + let parsing_diags, parsing_messages = + Util.diags_of_feedback ~loc:ast_loc parsing_feedback + in + let fb_diags, fb_messages = Util.diags_of_feedback ~loc:ast_loc feedback in + let ok_diags = maybe_ok_diagnostics ~loc:ast_loc in + let diags = parsing_diags @ fb_diags @ ok_diags in + let messages = parsing_messages @ fb_messages in let node = parsed_node ~loc:ast_loc ~ast ~diags ~messages ~state ~memo_info in @@ -378,13 +397,13 @@ let node_of_coq_result ~fb_queue ~parsing_diags ~ast ~ast_loc ~doc ~st | 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 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 + let err_diags = [ Util.mk_error_diagnostic ~loc:err_loc ~msg ~ast ] in + let parsing_diags, parsing_messages = + Util.diags_of_feedback ~loc:ast_loc parsing_feedback in - fb_queue := []; - let diags = parsing_diags @ fb_diags @ diags in + let fb_diags, fb_messages = Util.diags_of_feedback ~loc:err_loc feedback in + let diags = parsing_diags @ fb_diags @ err_diags in + let messages = parsing_messages @ fb_messages in let recovery_st = state_recovery_heuristic doc st ast in let node = parsed_node ~loc:ast_loc ~ast ~diags ~messages ~state:recovery_st @@ -395,24 +414,29 @@ let node_of_coq_result ~fb_queue ~parsing_diags ~ast ~ast_loc ~doc ~st | User _ -> Continue { state = recovery_st; last_tok; node }) (* *) -let document_action ~fb_queue ~st ~parsing_diags ~parsing_time ~doc last_tok - doc_handle action = +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 ~diags:parsing_diags ~state:st in + let node = + unparseable_node ~loc ~parsing_diags ~parsing_feedback ~state:st + in Stop (completed, node) (* Parsing error *) | Skip (span_loc, last_tok) -> - let node = unparseable_node ~loc:span_loc ~diags:parsing_diags ~state:st in + let node = + unparseable_node ~loc:span_loc ~parsing_diags ~parsing_feedback ~state:st + in Continue { state = st; last_tok; node } (* We interpret the command now *) | Process ast -> ( - let ast_loc = Coq.Ast.loc ast |> Option.get in (* We register pre-interp for now *) - let res, memo_info = interp_and_info ~parsing_time ~st ~fb_queue ast in - match res with + let { Coq.Protect.E.r; feedback }, memo_info = + interp_and_info ~parsing_time ~st ast + in + match r with | Coq.Protect.R.Interrupted -> (* Exit *) Interrupted last_tok @@ -420,24 +444,23 @@ let document_action ~fb_queue ~st ~parsing_diags ~parsing_time ~doc last_tok (* 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 = Pcoq.Parsable.loc doc_handle in - node_of_coq_result ~fb_queue ~parsing_diags ~ast ~ast_loc ~doc ~st - ~memo_info last_tok_new res) + node_of_coq_result ~doc ~ast ~st ~parsing_feedback ~feedback ~memo_info + last_tok_new res) (* XXX: Imperative problem *) -let process_and_parse ?cutpoint:_ ~uri ~version ~fb_queue doc last_tok - doc_handle = +let process_and_parse ~ofmt ?cutpoint:_ ~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; + 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 action, parsing_diags, parsing_feedback, parsing_time = parse_action ~st last_tok doc_handle in (* Execution *) let action = - document_action ~fb_queue ~st ~parsing_diags ~parsing_time ~doc last_tok - doc_handle action + document_action ~st ~parsing_diags ~parsing_feedback ~parsing_time ~doc + last_tok doc_handle action in match action with | Interrupted last_tok -> set_completion ~completed:(Stopped last_tok) doc @@ -453,7 +476,7 @@ let process_and_parse ?cutpoint:_ ~uri ~version ~fb_queue doc last_tok | [] -> () | n :: _ -> Io.Log.trace "resume" ("last node :" ^ Coq.Ast.pr_loc n.loc)); let st = - hd_opt ~default:doc.root + Util.hd_opt ~default:doc.root (List.map (fun { Node.state; _ } -> state) doc.nodes) in stm doc st last_tok @@ -503,7 +526,7 @@ let safe_sub s pos len = s) else String.sub s pos len -let check ~ofmt:_ ~fb_queue ?cutpoint ~doc () = +let check ~ofmt ?cutpoint ~doc () = match doc.completed with | Yes _ -> Io.Log.trace "check" "resuming, completed=yes, nothing to do"; @@ -532,7 +555,7 @@ let check ~ofmt:_ ~fb_queue ?cutpoint ~doc () = { doc with contents = processed_content; nodes = List.rev doc.nodes } in let doc = - process_and_parse ?cutpoint ~uri ~version ~fb_queue doc last_tok handle + process_and_parse ~ofmt ?cutpoint ~uri ~version doc last_tok handle in (* Set the document to "finished" mode: Restore the original contents, reverse the accumulators *) diff --git a/fleche/doc.mli b/fleche/doc.mli index 5183ad66f..2c4011c32 100644 --- a/fleche/doc.mli +++ b/fleche/doc.mli @@ -67,10 +67,4 @@ val bump_version : version:int -> contents:string -> t -> t (** [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 - -> fb_queue:Coq.Message.t list ref - -> ?cutpoint:int * int - -> doc:t - -> unit - -> t +val check : ofmt:Format.formatter -> ?cutpoint:int * int -> doc:t -> unit -> t diff --git a/fleche/info.ml b/fleche/info.ml index 78850b42e..c421f3de9 100644 --- a/fleche/info.ml +++ b/fleche/info.ml @@ -167,7 +167,14 @@ module Make (P : Point) : S with module P := P = struct let pr_goal st = let ppx env sigma x = - Coq.Print.pr_ltype_env ~goal_concl_style:true env sigma x + let { Coq.Protect.E.r; feedback } = + Coq.Print.pr_ltype_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 @@ -182,8 +189,13 @@ module Make (P : Point) : S with module P := P = struct let in_state ~st ~f node = match Coq.State.in_state ~st ~f node with - | Coq.Protect.R.Completed (Result.Ok res) -> res - | Coq.Protect.R.Completed (Result.Error _) | Coq.Protect.R.Interrupted -> + | { 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 = 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 c5de049bf..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.R.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 From 61a75b35fcade517ffd7c84e2876ea2693d3d1a6 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Thu, 12 Jan 2023 22:14:28 +0100 Subject: [PATCH 26/39] [fleche] Refactor doc a bit, no important change. --- fleche/doc.ml | 160 ++++++++++++++++++++++++++------------------------ 1 file changed, 83 insertions(+), 77 deletions(-) diff --git a/fleche/doc.ml b/fleche/doc.ml index c8e954313..72ca77137 100644 --- a/fleche/doc.ml +++ b/fleche/doc.ml @@ -48,6 +48,79 @@ module Util = struct ; 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.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 safe_sub s pos len = + if pos < 0 || len < 0 || pos > String.length s - len then ( + Io.Log.trace "string_sub" + (Format.asprintf "error for pos: %d len: %d str: %s" pos len s); + s) + else String.sub s pos len + + let 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 memo_info ~cache_hit ~parsing_time ~time ~mw_prev = + 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) + in + memo_info ^ "\n___\n" ^ mem_info +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 ^ "] " in + Io.Log.trace "coq" + ("parsed sentence: " ^ line ^ Pp.string_of_ppcmds (Coq.Ast.print ast)) + + let resume last_tok = + Io.Log.trace "check" + Format.( + asprintf "resuming, from: %d l: %d" last_tok.Loc.ep + last_tok.Loc.line_nb_last) end (* [node list] is a very crude form of a meta-data map "loc -> data" , where for @@ -289,36 +362,14 @@ 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)) - -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 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 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) - in - (res, memo_info ^ "\n___\n" ^ mem_info) + let memo_info = Util.memo_info ~cache_hit ~parsing_time ~time ~mw_prev in + (res, memo_info) type parse_action = | EOF of Completion.t (* completed *) @@ -340,7 +391,7 @@ let parse_action ~st last_tok doc_handle = let last_tok = Pcoq.Parsable.loc doc_handle in (EOF (Yes last_tok), [], feedback, time) | Ok (Some ast) -> - let () = if Debug.parsing then debug_parsed_sentence ~ast in + 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 @@ -430,9 +481,8 @@ let document_action ~st ~parsing_diags ~parsing_feedback ~parsing_time ~doc unparseable_node ~loc:span_loc ~parsing_diags ~parsing_feedback ~state:st in Continue { state = st; last_tok; node } - (* We interpret the command now *) + (* We can interpret the command now *) | Process ast -> ( - (* We register pre-interp for now *) let { Coq.Protect.E.r; feedback }, memo_info = interp_and_info ~parsing_time ~st ast in @@ -447,9 +497,10 @@ let document_action ~st ~parsing_diags ~parsing_feedback ~parsing_time ~doc node_of_coq_result ~doc ~ast ~st ~parsing_feedback ~feedback ~memo_info last_tok_new res) -(* XXX: Imperative problem *) +(* main interpretation loop *) let process_and_parse ~ofmt ?cutpoint:_ ~uri ~version doc last_tok doc_handle = let rec stm doc st 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"; @@ -481,51 +532,6 @@ let process_and_parse ~ofmt ?cutpoint:_ ~uri ~version doc last_tok doc_handle = 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 safe_sub s pos len = - if pos < 0 || len < 0 || pos > String.length s - len then ( - Io.Log.trace "string_sub" - (Format.asprintf "error for pos: %d len: %d str: %s" pos len s); - s) - else String.sub s pos len - let check ~ofmt ?cutpoint ~doc () = match doc.completed with | Yes _ -> @@ -535,15 +541,15 @@ let check ~ofmt ?cutpoint ~doc () = Io.Log.trace "check" "can't resume, failed=yes, nothing to do"; doc | Stopped last_tok -> - log_resume last_tok; + DDebug.resume last_tok; let uri, version, contents = (doc.uri, doc.version, doc.contents) in (* Process markdown *) - let processed_content = process_contents ~uri ~contents in + 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 let processed_content = - safe_sub processed_content offset + Util.safe_sub processed_content offset (String.length processed_content - offset) in let handle = @@ -572,5 +578,5 @@ let check ~ofmt ?cutpoint ~doc () = (Coq.Ast.pr_loc loc) in Io.Log.trace "check" end_msg; - print_stats (); + Util.print_stats (); doc From 90fbaed3f80c17b600468fd1e156c1c4ff8d55f4 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Thu, 12 Jan 2023 18:17:53 +0100 Subject: [PATCH 27/39] [goals] Send and display information about shelved and given up goals. --- CHANGES.md | 6 +++-- Makefile | 5 ++++ controller/requests.ml | 14 ++++++++--- editor/code/src/goals.ts | 53 ++++++++++++++++++++++++++++++++-------- etc/doc/PROTOCOL.md | 26 ++++++++++++++------ 5 files changed, 82 insertions(+), 22 deletions(-) diff --git a/CHANGES.md b/CHANGES.md index d5c8363e7..3f6dbe894 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -11,10 +11,12 @@ (@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) + (@ejgallego, #169) - Implement request postponement and cancellation. Thus `documentSymbols` will now be postponed until the document is - ready, (@ejgallego #141, #146, fixes #124) + ready, (@ejgallego, #141, #146, fixes #124) + - Protocol and VS Code interfaces now support shelved and given_up + goals (@ejgallego, #175) # coq-lsp 0.1.2: Message ------------------------ diff --git a/Makefile b/Makefile index 525b69e85..2473a5774 100644 --- a/Makefile +++ b/Makefile @@ -83,3 +83,8 @@ 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 . diff --git a/controller/requests.ml b/controller/requests.ml index dc46fc64e..0bd67c08c 100644 --- a/controller/requests.ml +++ b/controller/requests.ml @@ -78,8 +78,16 @@ 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_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 [] @@ -109,7 +117,7 @@ let goals ~doc ~point = ; ( "position" , `Assoc [ ("line", `Int (fst point)); ("character", `Int (snd point)) ] ) - ; ("goals", `List (mk_goals goals)) + ; ("goals", mk_goals goals) ; ("messages", `List (mk_messages messages)) ] @ error) diff --git a/editor/code/src/goals.ts b/editor/code/src/goals.ts index d8c63056d..6be7a56b2 100644 --- a/editor/code/src/goals.ts +++ b/editor/code/src/goals.ts @@ -20,11 +20,18 @@ interface GoalRequest { textDocument: TextDocumentIdentifier; 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,21 +86,42 @@ 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)) : ""; // Use #FA8072 color too? @@ -104,7 +137,7 @@ function buildGoalsContent(goals: GoalAnswer, styleUri: Uri) {
${uriBase}:${goals.position.line}:${goals.position.character} -
+
${goalsBody}
@@ -134,7 +167,7 @@ class GoalView { } display(goals: GoalAnswer) { - this.view.html = buildGoalsContent(goals, this.styleUri); + this.view.html = buildInfoContent(goals, this.styleUri); } // LSP Protocol extension for Goals 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 From 40ca573920a1709848b5f5ca395e198c260a1aaf Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Thu, 12 Jan 2023 23:34:10 +0100 Subject: [PATCH 28/39] [coq] Minor refactoring on the type of goal printing. --- coq/goals.ml | 9 ++++----- coq/goals.mli | 2 +- coq/print.ml | 8 ++++---- coq/print.mli | 4 ++-- fleche/info.ml | 2 +- 5 files changed, 12 insertions(+), 13 deletions(-) diff --git a/coq/goals.ml b/coq/goals.ml index 3fb9daf39..9e6a5a35e 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,17 +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) : _ = let (EvarInfo evi) = Evd.find sigma g in - ppx - @@ EConstr.to_constr ~abort_on_undefined_evars:false sigma - Evd.(evar_concl evi) + ppx Evd.(evar_concl evi) let build_info sigma g = { evar = g; name = Evd.evar_ident g sigma } diff --git a/coq/goals.mli b/coq/goals.mli index 7c22bb5f3..4b3ec62c8 100644 --- a/coq/goals.mli +++ b/coq/goals.mli @@ -42,7 +42,7 @@ type 'a goals = (** Stm-independent goal processor *) val process_goal_gen : - (Environ.env -> Evd.evar_map -> Constr.t -> 'a) + (Environ.env -> Evd.evar_map -> EConstr.t -> 'a) -> Evd.evar_map -> Evar.t -> 'a reified_goal diff --git a/coq/print.ml b/coq/print.ml index 43aaa9d62..ac4bf3a99 100644 --- a/coq/print.ml +++ b/coq/print.ml @@ -1,6 +1,6 @@ -let pr_ltype_env ~goal_concl_style env sigma x = - Printer.pr_ltype_env ~goal_concl_style env sigma x +let pr_letype_env ~goal_concl_style env sigma x = + Printer.pr_letype_env ~goal_concl_style env sigma x -let pr_ltype_env ~goal_concl_style env sigma x = - let f = pr_ltype_env ~goal_concl_style env sigma in +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 index e4ad9c818..dec808c32 100644 --- a/coq/print.mli +++ b/coq/print.mli @@ -1,6 +1,6 @@ -val pr_ltype_env : +val pr_letype_env : goal_concl_style:bool -> Environ.env -> Evd.evar_map - -> Constr.t + -> EConstr.t -> Pp.t Protect.E.t diff --git a/fleche/info.ml b/fleche/info.ml index c421f3de9..a6525d28b 100644 --- a/fleche/info.ml +++ b/fleche/info.ml @@ -168,7 +168,7 @@ module Make (P : Point) : S with module P := P = struct let pr_goal st = let ppx env sigma x = let { Coq.Protect.E.r; feedback } = - Coq.Print.pr_ltype_env ~goal_concl_style:true env sigma x + Coq.Print.pr_letype_env ~goal_concl_style:true env sigma x in Io.Log.feedback feedback; match r with From 42cbbe836cc5a9edbff0de8ac6b2870d12f1c0b2 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Fri, 13 Jan 2023 03:22:22 +0100 Subject: [PATCH 29/39] [fleche] Debug print document version on resumption. --- fleche/doc.ml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/fleche/doc.ml b/fleche/doc.ml index 72ca77137..11637c95a 100644 --- a/fleche/doc.ml +++ b/fleche/doc.ml @@ -116,10 +116,10 @@ module DDebug = struct Io.Log.trace "coq" ("parsed sentence: " ^ line ^ Pp.string_of_ppcmds (Coq.Ast.print ast)) - let resume last_tok = + let resume last_tok version = Io.Log.trace "check" Format.( - asprintf "resuming, from: %d l: %d" last_tok.Loc.ep + asprintf "resuming [v: %d], from: %d l: %d" version last_tok.Loc.ep last_tok.Loc.line_nb_last) end @@ -541,7 +541,7 @@ let check ~ofmt ?cutpoint ~doc () = Io.Log.trace "check" "can't resume, failed=yes, nothing to do"; doc | Stopped last_tok -> - DDebug.resume last_tok; + DDebug.resume last_tok doc.version; let uri, version, contents = (doc.uri, doc.version, doc.contents) in (* Process markdown *) let processed_content = Util.process_contents ~uri ~contents in From cde83ef93edf44d9957573ec6b9f2bd75fff7918 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Fri, 13 Jan 2023 03:22:42 +0100 Subject: [PATCH 30/39] [goals] Fix position-based display (LSP is zero-based). --- editor/code/src/goals.ts | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/editor/code/src/goals.ts b/editor/code/src/goals.ts index 6be7a56b2..076b786a6 100644 --- a/editor/code/src/goals.ts +++ b/editor/code/src/goals.ts @@ -136,7 +136,7 @@ function buildInfoContent(goals: GoalAnswer, styleUri: Uri) {
- ${uriBase}:${goals.position.line}:${goals.position.character} + ${uriBase}:${goals.position.line+1}:${goals.position.character+1}
${goalsBody}
From e3987f2a60cfaef97f9f3b6e23f68111aac15e27 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Fri, 13 Jan 2023 03:23:19 +0100 Subject: [PATCH 31/39] [goals] Show goals in all selection change events. This fixes the event not triggering on deletion for example. --- editor/code/src/client.ts | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/editor/code/src/client.ts b/editor/code/src/client.ts index 3c1f59d39..4155d2a2a 100644 --- a/editor/code/src/client.ts +++ b/editor/code/src/client.ts @@ -172,7 +172,10 @@ export function activate(context: ExtensionContext): void { ? 2 : evt.kind ? evt.kind - : 1000; + : 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) { From eaf401085a48d4a34621e14f8d9998eca2032ba6 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Fri, 13 Jan 2023 03:26:57 +0100 Subject: [PATCH 32/39] [typescript] Workaround horrible prettier behavior here. --- editor/code/src/goals.ts | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/editor/code/src/goals.ts b/editor/code/src/goals.ts index 076b786a6..d0a6ed04e 100644 --- a/editor/code/src/goals.ts +++ b/editor/code/src/goals.ts @@ -124,6 +124,9 @@ function buildInfoContent(goals: GoalAnswer, styleUri: Uri) { ? 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 ` @@ -136,7 +139,7 @@ function buildInfoContent(goals: GoalAnswer, styleUri: Uri) {
- ${uriBase}:${goals.position.line+1}:${goals.position.character+1} + ${uriBase}:${line}:${character}
${goalsBody}
From 8f594f663ecd2f5649fe3adba58f50399eaed2a3 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Fri, 13 Jan 2023 16:40:41 +0100 Subject: [PATCH 33/39] [controller] Patch obvious DOS hole. That was there from a very early prototype, for no good reason. --- Makefile | 3 +++ controller/coq_lsp.ml | 9 ++++++--- 2 files changed, 9 insertions(+), 3 deletions(-) diff --git a/Makefile b/Makefile index 2473a5774..ce9a1a0a4 100644 --- a/Makefile +++ b/Makefile @@ -88,3 +88,6 @@ extension: .PHONY: ts-fmt ts-fmt: cd editor/code && npx prettier -w . + +.PHONY: make-fmt +make-fmt: build fmt diff --git a/controller/coq_lsp.ml b/controller/coq_lsp.ml index 3facc4fdc..dc7bb4f8b 100644 --- a/controller/coq_lsp.ml +++ b/controller/coq_lsp.ml @@ -144,10 +144,13 @@ let do_change params = 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 Doc_manager.change ~uri ~version ~contents From 58ace6081f77b23ad238f366796e2c9b7f97cc77 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Fri, 13 Jan 2023 04:45:50 +0100 Subject: [PATCH 34/39] [api] Improvements on Coq API encapsulation. This is much improved. --- coq/goals.ml | 44 +++++++++++++++++--------------------------- coq/goals.mli | 13 +++++-------- coq/parsing.ml | 22 ++++++++++++++++++++++ coq/parsing.mli | 10 +++++++++- coq/state.ml | 7 +++++++ coq/state.mli | 20 +++++++++++++++----- fleche/doc.ml | 32 ++++++-------------------------- fleche/info.ml | 21 +-------------------- 8 files changed, 82 insertions(+), 87 deletions(-) diff --git a/coq/goals.ml b/coq/goals.ml index 9e6a5a35e..8a0fa9501 100644 --- a/coq/goals.ml +++ b/coq/goals.ml @@ -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 4b3ec62c8..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 -> EConstr.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/parsing.ml b/coq/parsing.ml index 9f396c887..8113657b9 100644 --- a/coq/parsing.ml +++ b/coq/parsing.ml @@ -1,3 +1,5 @@ +module Parsable = Pcoq.Parsable + let parse ~st ps = let mode = State.mode ~st in let st = State.parsing ~st in @@ -8,3 +10,23 @@ let parse ~st ps = |> 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 Gramlib.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 index 35b81377d..c721a2112 100644 --- a/coq/parsing.mli +++ b/coq/parsing.mli @@ -1 +1,9 @@ -val parse : st:State.t -> Pcoq.Parsable.t -> Ast.t option Protect.E.t +module Parsable : sig + type t + + val make : ?loc:Loc.t -> char Gramlib.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 diff --git a/coq/state.ml b/coq/state.ml index 4b07f5029..01ea22a36 100644 --- a/coq/state.ml +++ b/coq/state.ml @@ -75,6 +75,13 @@ let mode ~st = st.Vernacstate.lemmas let parsing ~st = st.Vernacstate.parsing + +module Proof = struct + type t = Vernacstate.LemmaStack.t + + let to_coq x = x +end + let lemmas ~st = st.Vernacstate.lemmas let drop_proofs ~st = diff --git a/coq/state.mli b/coq/state.mli index e918a5634..1e2baa5b5 100644 --- a/coq/state.mli +++ b/coq/state.mli @@ -1,15 +1,19 @@ 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 + +(** 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. *) @@ -20,3 +24,9 @@ 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/fleche/doc.ml b/fleche/doc.ml index 11637c95a..3541400fa 100644 --- a/fleche/doc.ml +++ b/fleche/doc.ml @@ -315,26 +315,6 @@ let parse_stm ~st ps = let f ps = Coq.Parsing.parse ~st ps in Stats.record ~kind:Stats.Kind.Parsing ~f ps -(* Read the input stream until a dot or a "end of proof" token is encountered *) -let parse_to_terminator : unit Pcoq.Entry.t = - (* type 'a parser_fun = { parser_fun : te LStream.t -> 'a } *) - let rec dot st = - match Gramlib.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 rec find_recovery_for_failed_qed ~default nodes = match nodes with | [] -> (default, None) @@ -378,7 +358,7 @@ type parse_action = (* Returns parse_action, diags, parsing_time *) let parse_action ~st last_tok doc_handle = - let start_loc = Pcoq.Parsable.loc doc_handle |> CLexer.after in + 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) @@ -388,7 +368,7 @@ let parse_action ~st last_tok doc_handle = (* 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 = Pcoq.Parsable.loc doc_handle in + 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 @@ -401,8 +381,8 @@ let parse_action ~st last_tok doc_handle = (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 - discard_to_dot doc_handle; - let last_tok = Pcoq.Parsable.loc doc_handle 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)) @@ -493,7 +473,7 @@ let document_action ~st ~parsing_diags ~parsing_feedback ~parsing_time ~doc | 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 = Pcoq.Parsable.loc doc_handle in + let last_tok_new = Coq.Parsing.Parsable.loc doc_handle in node_of_coq_result ~doc ~ast ~st ~parsing_feedback ~feedback ~memo_info last_tok_new res) @@ -553,7 +533,7 @@ let check ~ofmt ?cutpoint ~doc () = (String.length processed_content - offset) in let handle = - Pcoq.Parsable.make ~loc:resume_loc + Coq.Parsing.Parsable.make ~loc:resume_loc Gramlib.Stream.(of_string ~offset processed_content) in (* Set the document to "internal" mode *) diff --git a/fleche/info.ml b/fleche/info.ml index a6525d28b..81c4f21f5 100644 --- a/fleche/info.ml +++ b/fleche/info.ml @@ -146,25 +146,6 @@ 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 = let { Coq.Protect.E.r; feedback } = @@ -177,7 +158,7 @@ module Make (P : Point) : S with module P := P = struct | 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 From 7f14019d12cdbf657a5ca0df9b2c45cc84dd5f3b Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Thu, 12 Jan 2023 22:23:45 +0100 Subject: [PATCH 35/39] [fleche] Allow to set cutoff point. We will use this to wake up the current goal request. We fix a few line use by the way, the internal standard of fleche is 0-based for both line and column (as in the LSP spec) --- controller/coq_lsp.ml | 4 +- controller/doc_manager.ml | 3 +- controller/requests.ml | 2 +- coq/ast.ml | 2 +- fleche/doc.ml | 144 ++++++++++++++++++++++---------------- fleche/doc.mli | 18 +++-- 6 files changed, 105 insertions(+), 68 deletions(-) diff --git a/controller/coq_lsp.ml b/controller/coq_lsp.ml index dc7bb4f8b..c53da38b1 100644 --- a/controller/coq_lsp.ml +++ b/controller/coq_lsp.ml @@ -179,8 +179,8 @@ let do_position_request ~params ~handler = match doc.completed with | Yes _ -> true | Failed loc | Stopped loc -> - line < loc.line_nb_last - || (line = loc.line_nb_last && col <= loc.ep - loc.bol_pos_last) + let proc_line = loc.line_nb_last - 1 in + line < proc_line || (line = proc_line && col < loc.ep - loc.bol_pos_last) in if in_range then RResult.Ok (handler ~doc ~point) else diff --git a/controller/doc_manager.ml b/controller/doc_manager.ml index dfcd14bf6..09e9cd284 100644 --- a/controller/doc_manager.ml +++ b/controller/doc_manager.ml @@ -99,7 +99,8 @@ module Check = struct LIO.trace "process_queue" "resuming document checking"; match Handle.find_opt ~uri with | Some handle -> - let doc = Fleche.Doc.check ~ofmt ~doc:handle.doc () in + let target = Fleche.Doc.Target.End 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 = diff --git a/controller/requests.ml b/controller/requests.ml index 0bd67c08c..9297b3f21 100644 --- a/controller/requests.ml +++ b/controller/requests.ml @@ -109,7 +109,7 @@ 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 (fun node -> node.Doc.Node.messages) node in + let messages = Option.map Doc.Node.messages node in let error = Option.cata mk_error [] node in `Assoc ([ ( "textDocument" 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/fleche/doc.ml b/fleche/doc.ml index 3541400fa..aa54c67de 100644 --- a/fleche/doc.ml +++ b/fleche/doc.ml @@ -112,7 +112,7 @@ 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 ^ "] " 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)) @@ -120,7 +120,7 @@ module DDebug = struct Io.Log.trace "check" Format.( asprintf "resuming [v: %d], from: %d l: %d" version last_tok.Loc.ep - last_tok.Loc.line_nb_last) + (last_tok.Loc.line_nb_last - 1)) end (* [node list] is a very crude form of a meta-data map "loc -> data" , where for @@ -354,7 +354,7 @@ let interp_and_info ~parsing_time ~st ast = 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 (* ast to process *) + | Process of Coq.Ast.t (* success! *) (* Returns parse_action, diags, parsing_time *) let parse_action ~st last_tok doc_handle = @@ -386,6 +386,7 @@ let parse_action ~st last_tok doc_handle = 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 @@ -400,7 +401,20 @@ let unparseable_node ~loc ~parsing_diags ~parsing_feedback ~state = let diags = fb_diags @ parsing_diags in { Node.loc; ast = None; diags; messages; state; memo_info = "" } -let parsed_node ~loc ~ast ~diags ~messages ~state ~memo_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 ~memo_info = + let diags, messages = + assemble_diags ~loc ~parsing_diags ~parsing_feedback ~diags ~feedback + in { Node.loc; ast = Some ast; diags; messages; state; memo_info } let maybe_ok_diagnostics ~loc = @@ -409,42 +423,33 @@ let maybe_ok_diagnostics ~loc = [ ok_diag ] else [] -let node_of_coq_result ~feedback ~parsing_feedback ~ast ~doc ~st ~memo_info - last_tok res = +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 + ~memo_info last_tok res = let ast_loc = Coq.Ast.loc ast |> Option.get in match res with | Ok { Coq.Interp.Info.res = state } -> - let parsing_diags, parsing_messages = - Util.diags_of_feedback ~loc:ast_loc parsing_feedback - in - let fb_diags, fb_messages = Util.diags_of_feedback ~loc:ast_loc feedback in let ok_diags = maybe_ok_diagnostics ~loc:ast_loc in - let diags = parsing_diags @ fb_diags @ ok_diags in - let messages = parsing_messages @ fb_messages in let node = - parsed_node ~loc:ast_loc ~ast ~diags ~messages ~state ~memo_info + parsed_node ~loc:ast_loc ~ast ~state ~parsing_diags ~parsing_feedback + ~diags:ok_diags ~feedback ~memo_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) -> ( + | 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 parsing_diags, parsing_messages = - Util.diags_of_feedback ~loc:ast_loc parsing_feedback - in - let fb_diags, fb_messages = Util.diags_of_feedback ~loc:err_loc feedback in - let diags = parsing_diags @ fb_diags @ err_diags in - let messages = parsing_messages @ fb_messages in let recovery_st = state_recovery_heuristic doc st ast in let node = - parsed_node ~loc:ast_loc ~ast ~diags ~messages ~state:recovery_st - ~memo_info + parsed_node ~loc:ast_loc ~ast ~state:recovery_st ~parsing_diags + ~parsing_feedback ~diags:err_diags ~feedback ~memo_info in - match coq_err with - | Anomaly _ -> Stop (Failed last_tok, node) - | User _ -> Continue { state = recovery_st; last_tok; node }) + 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 @@ -474,33 +479,53 @@ let document_action ~st ~parsing_diags ~parsing_feedback ~parsing_time ~doc (* 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_feedback ~feedback ~memo_info - last_tok_new res) + node_of_coq_result ~doc ~ast ~st ~parsing_diags ~parsing_feedback + ~feedback ~memo_info last_tok_new res) + +module Target = struct + type t = + | End + | Position of int * int +end + +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) (* main interpretation loop *) -let process_and_parse ~ofmt ?cutpoint:_ ~uri ~version doc last_tok doc_handle = +let process_and_parse ~ofmt ~target ~uri ~version doc last_tok doc_handle = let rec stm doc st 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_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 - match action with - | Interrupted last_tok -> set_completion ~completed:(Stopped last_tok) doc - | Stop (completed, node) -> - let doc = add_node ~node doc in + if beyond_target last_tok target then + let completed = Completion.Stopped last_tok in set_completion ~completed doc - | Continue { state; last_tok; node } -> - let doc = add_node ~node doc in - stm doc state last_tok + 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 + 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 (* Note that nodes and diags in reversed order here *) (match doc.nodes with @@ -512,7 +537,19 @@ let process_and_parse ~ofmt ?cutpoint:_ ~uri ~version doc last_tok doc_handle = in stm doc st last_tok -let check ~ofmt ?cutpoint ~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 check ~ofmt ~target ~doc () = match doc.completed with | Yes _ -> Io.Log.trace "check" "resuming, completed=yes, nothing to do"; @@ -541,22 +578,11 @@ let check ~ofmt ?cutpoint ~doc () = { doc with contents = processed_content; nodes = List.rev doc.nodes } in let doc = - process_and_parse ~ofmt ?cutpoint ~uri ~version doc last_tok handle + process_and_parse ~ofmt ~target ~uri ~version 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, status = - match doc.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) - in - Io.Log.trace "check" end_msg; + log_doc_completion doc.completed; Util.print_stats (); doc diff --git a/fleche/doc.mli b/fleche/doc.mli index 2c4011c32..7edf06fa2 100644 --- a/fleche/doc.mli +++ b/fleche/doc.mli @@ -16,8 +16,6 @@ (* Status: Experimental *) (************************************************************************) -(* [node list] is a very crude form of a meta-data map "loc -> data" , where for - now [data] is only the goals. *) module Node : sig type t = private { loc : Loc.t @@ -43,6 +41,9 @@ module Completion : sig | 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 @@ -54,7 +55,7 @@ type t = private ; completed : Completion.t } -(** Note, [create] is not cached in the Memo.t table *) +(** Note, [create] calls Coq but it is not cached in the Memo.t table *) val create : state:Coq.State.t -> workspace:Coq.Workspace.t @@ -63,8 +64,17 @@ val create : -> contents:string -> 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 +(** 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 -> ?cutpoint:int * int -> doc:t -> unit -> t +val check : ofmt:Format.formatter -> target:Target.t -> doc:t -> unit -> t From 39ec767536741ac25b9a1759d08186b8e69fadb7 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Fri, 13 Jan 2023 00:03:29 +0100 Subject: [PATCH 36/39] [controller] Postpone position requests until doc checking catches up. This provides a much nicer typing and navigation experience, basically if some data about the document is not ready, the request is postponed and will be served when such data becames available. We also switch the default for the client as to show goals on typing / movement of the cursor. With the new delay capability, this gives the user usually what they want in terms of the goal panel being up-to-date. Some notes: - For now we only postpone goal requests, we should implement a proper queue (in next PRs). One pending goal request works pretty well for interactive use. - `Doc.Target.t` can be more refined, as to support `Info.find` `Prev` behavior (but this is a bit complex due to the way both searches interact) --- CHANGES.md | 9 ++- controller/coq_lsp.ml | 149 +++++++++++++++++++++++++------------ controller/doc_manager.ml | 74 ++++++++++++++---- controller/doc_manager.mli | 11 ++- controller/requests.ml | 5 +- controller/requests.mli | 2 +- editor/code/package.json | 2 +- editor/code/src/client.ts | 3 +- editor/code/src/goals.ts | 14 ++-- fleche/debug.ml | 3 + fleche/doc.ml | 87 +++++++++++++--------- fleche/doc.mli | 2 +- lsp/base.ml | 2 +- 13 files changed, 247 insertions(+), 116 deletions(-) diff --git a/CHANGES.md b/CHANGES.md index 3f6dbe894..513e562cd 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -1,5 +1,5 @@ -# coq-lsp 0.1.3: View ---------------------- +# 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) @@ -17,6 +17,11 @@ 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) # coq-lsp 0.1.2: Message ------------------------ diff --git a/controller/coq_lsp.ml b/controller/coq_lsp.ml index c53da38b1..a84d5ec68 100644 --- a/controller/coq_lsp.ml +++ b/controller/coq_lsp.ml @@ -36,6 +36,7 @@ let option_default x d = | Some x -> x 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 @@ -58,9 +59,15 @@ module Check = Doc_manager.Check module PendingRequest = struct type t = - { uri : string - ; handler : uri:string -> doc:Fleche.Doc.t -> J.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 @@ -125,6 +132,41 @@ let do_initialize ~params = ] |> RResult.ok +let rtable : (int, PendingRequest.t) Hashtbl.t = Hashtbl.create 673 + +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 do_shutdown ~params:_ = RResult.Ok `Null let do_open ~state params = @@ -137,7 +179,7 @@ let do_open ~state params = let root_state, workspace = State.(state.root_state, state.workspace) in 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) @@ -153,9 +195,12 @@ let do_change params = () | change :: _ -> let contents = string_field "text" change in - Doc_manager.change ~uri ~version ~contents + 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 do_close ~ofmt:_ params = let document = dict_field "textDocument" params in let uri = string_field "uri" document in Doc_manager.close ~uri @@ -171,10 +216,17 @@ let get_position params = let line, character = (int_field "line" pos, int_field "character" pos) in (line, character) -let do_position_request ~params ~handler = - let _uri, doc = get_textDocument params in +let do_position_request ~postpone ~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 @@ -182,23 +234,31 @@ let do_position_request ~params ~handler = 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 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 - RResult.Error (code, message) + Error (code, message) + +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 = do_position_request ~handler:Requests.hover -let do_goals = do_position_request ~handler:Requests.goals -let do_completion = do_position_request ~handler:Requests.completion +let do_completion = + do_position_request ~postpone:false ~handler:Requests.completion (* 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 ~uri ~doc) - | Stopped _ | Failed _ -> Postpone { uri; handler } + | Yes _ -> RResult.Ok (handler ~doc) + | Stopped _ | Failed _ -> + Postpone (PendingRequest.DocRequest { uri; handler }) let do_symbols = do_document_request ~handler:Requests.symbols @@ -218,43 +278,36 @@ let rec read_request ic = LIO.trace "read_request" ("error: " ^ msg); read_request ic -let rtable : (int, PendingRequest.t) Hashtbl.t = Hashtbl.create 673 - -let 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 ({ uri; _ } as pr) -> - Doc_manager.serve_on_completion ~uri ~id; - Hashtbl.add rtable id pr - -let do_cancel ofmt ~params = +let do_cancel ~ofmt ~params = let id = int_field "id" params in - match Hashtbl.find_opt rtable id with - | None -> - (* Request is not pending *) - () - | Some _ -> - Hashtbl.remove rtable id; - answer_request ofmt ~id (Error (-32800, "Cancelled by client")) + 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 serve cancelled request: " (string_of_int id); + LIO.trace "can't wake up cancelled request: " (string_of_int id); None - | Some { uri; handler } -> - LIO.trace "serving rq: " (string_of_int id ^ " uri: " ^ uri); + | 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 ~uri ~doc)) + 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_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 +let serve_postponed_requests ~ofmt rl = + Int.Set.iter (serve_postponed_request ~ofmt) rl (***********************************************************************) @@ -272,7 +325,7 @@ let rec lsp_init_loop ic ofmt ~cmdline : Coq.Workspace.t = (* 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; + answer_request ~ofmt ~id result; LIO.logMessage ~lvl:3 ~message:"Server initialized"; (* Workspace initialization *) let workspace = Coq.Workspace.guess ~cmdline in @@ -297,11 +350,11 @@ let dispatch_notification ofmt ~state ~method_ ~params = | "$/setTrace" -> do_trace params (* Document lifetime *) | "textDocument/didOpen" -> do_open ~state params - | "textDocument/didChange" -> do_change params - | "textDocument/didClose" -> do_close ofmt params + | "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 + | "$/cancelRequest" -> do_cancel ~ofmt ~params (* NOOPs *) | "initialized" -> () (* Generic handler *) @@ -327,7 +380,7 @@ let dispatch_request ~method_ ~params = Error (-32601, "method not found") let dispatch_request ofmt ~id ~method_ ~params = - dispatch_request ~method_ ~params |> answer_request ofmt ~id + dispatch_request ~method_ ~params |> answer_request ~ofmt ~id let dispatch_message ofmt ~state (com : LSP.Message.t) = match com with @@ -371,7 +424,7 @@ let dispatch_or_resume_check ofmt ~state = | None -> Control.interrupt := false; let ready = Check.check_or_yield ~ofmt in - serve_postponed_requests ofmt ready + serve_postponed_requests ~ofmt ready | Some com -> (* TODO: optimize the queue? *) ignore (Queue.pop request_queue); diff --git a/controller/doc_manager.ml b/controller/doc_manager.ml index 09e9cd284..ba5ff9a8d 100644 --- a/controller/doc_manager.ml +++ b/controller/doc_manager.ml @@ -24,11 +24,12 @@ exception AbortRequest module Handle = struct type t = { doc : Fleche.Doc.t - ; requests : Int.Set.t + ; cp_requests : Int.Set.t (* For now we just store the request id to wake up on completion, later on we may want to store a more interesting type, for example "wake up when a location is reached", or always to continue the streaming *) + ; pt_request : (int * (int * int)) option (* id, point *) } let doc_table : (string, t) Hashtbl.t = Hashtbl.create 39 @@ -38,7 +39,8 @@ module Handle = struct | None -> () | Some _ -> LIO.trace "do_open" ("file " ^ uri ^ " not properly closed by client")); - Hashtbl.add doc_table uri { doc; requests = Int.Set.empty } + Hashtbl.add doc_table uri + { doc; cp_requests = Int.Set.empty; pt_request = None } let close ~uri = Hashtbl.remove doc_table uri @@ -57,22 +59,61 @@ module Handle = struct (* Clear requests *) let update_doc_version ~(doc : Fleche.Doc.t) = - Hashtbl.replace doc_table doc.uri { doc; requests = Int.Set.empty } + 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_request ~uri ~id = + let attach_cp_request ~uri ~id = match Hashtbl.find_opt doc_table uri with - | Some { doc; requests } -> - let requests = Int.Set.add id requests in - Hashtbl.replace doc_table uri { doc; requests } + | 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 _ -> ({ doc; requests = Int.Set.empty }, handle.requests) - | Stopped _ -> (handle, Int.Set.empty) + | 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 *) @@ -99,7 +140,10 @@ module Check = struct LIO.trace "process_queue" "resuming document checking"; match Handle.find_opt ~uri with | Some handle -> - let target = Fleche.Doc.Target.End in + 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 @@ -167,13 +211,15 @@ let change ~uri ~version ~contents = 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 () = Handle.update_doc_version ~doc in - Check.schedule ~uri) + 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_request ~uri ~id +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 index aacf04e01..8bfbe5d2d 100644 --- a/controller/doc_manager.mli +++ b/controller/doc_manager.mli @@ -31,8 +31,8 @@ val create : -> version:int -> unit -(** Update a document *) -val change : uri:string -> version:int -> contents:string -> 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 @@ -42,5 +42,10 @@ exception AbortRequest (** [find_doc ~uri] , raises AbortRequest if [uri] is invalid *) val find_doc : uri:string -> Fleche.Doc.t -(** Request support *) +(** 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/requests.ml b/controller/requests.ml index 9297b3f21..97434f2ec 100644 --- a/controller/requests.ml +++ b/controller/requests.ml @@ -15,7 +15,7 @@ (* Written by: Emilio J. Gallego Arias *) (************************************************************************) -type document_request = uri:string -> doc:Fleche.Doc.t -> Yojson.Safe.t +type document_request = doc:Fleche.Doc.t -> Yojson.Safe.t type position_request = doc:Fleche.Doc.t -> point:int * int -> Yojson.Safe.t module Util = struct @@ -40,7 +40,8 @@ let _kind_of_type _tm = 13 13 (* Variable *) | Type | Kind | Symb _ | _ when is_undef -> 14 (* Constant *) | _ -> 12 (* Function *) *) -let symbols ~uri ~(doc : Fleche.Doc.t) = +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 diff --git a/controller/requests.mli b/controller/requests.mli index ae90dc2ea..427383429 100644 --- a/controller/requests.mli +++ b/controller/requests.mli @@ -15,7 +15,7 @@ (* Written by: Emilio J. Gallego Arias *) (************************************************************************) -type document_request = uri:string -> doc:Fleche.Doc.t -> Yojson.Safe.t +type document_request = doc:Fleche.Doc.t -> Yojson.Safe.t type position_request = doc:Fleche.Doc.t -> point:int * int -> Yojson.Safe.t val symbols : document_request diff --git a/editor/code/package.json b/editor/code/package.json index dca40d7c8..479ede979 100644 --- a/editor/code/package.json +++ b/editor/code/package.json @@ -131,7 +131,7 @@ }, "coq-lsp.show_goals_on": { "type": "number", - "default": 1, + "default": 3, "description": "When to show goals and information about the current cursor", "enum": [ 0, diff --git a/editor/code/src/client.ts b/editor/code/src/client.ts index 4155d2a2a..7a80c54a3 100644 --- a/editor/code/src/client.ts +++ b/editor/code/src/client.ts @@ -155,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); } }; diff --git a/editor/code/src/goals.ts b/editor/code/src/goals.ts index d0a6ed04e..c0254411f 100644 --- a/editor/code/src/goals.ts +++ b/editor/code/src/goals.ts @@ -17,7 +17,7 @@ interface Goal { } interface GoalRequest { - textDocument: TextDocumentIdentifier; + textDocument: VersionedTextDocumentIdentifier; position: Position; } interface GoalConfig { @@ -165,8 +165,8 @@ 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) { @@ -174,8 +174,8 @@ class GoalView { } // 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( @@ -195,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/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 aa54c67de..d3cb90883 100644 --- a/fleche/doc.ml +++ b/fleche/doc.ml @@ -83,10 +83,11 @@ module Util = struct 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); - s) - else String.sub s pos len + None) + else Some (String.sub s pos len) let pp_words fmt w = if w < 1024.0 then Format.fprintf fmt "%.0f w" w @@ -160,7 +161,7 @@ type t = { uri : string ; version : int ; contents : string - ; end_loc : int * int * int + ; end_loc : Types.Point.t ; root : Coq.State.t ; nodes : Node.t list ; diags_dirty : bool (** Used to optimize `eager_diagnostics` *) @@ -177,7 +178,11 @@ 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 = Util.hd_opt ~default:"" (List.rev lines) in - (List.length lines, String.length last_line, String.length text) + 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 @@ -287,20 +292,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) @@ -498,6 +496,14 @@ let beyond_target pos target = 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 = @@ -506,7 +512,12 @@ let process_and_parse ~ofmt ~target ~uri ~version doc last_tok doc_handle = report_progress ~ofmt ~doc last_tok; if Debug.parsing then Io.Log.trace "coq" "parsing sentence"; if beyond_target last_tok target then - let completed = Completion.Stopped last_tok in + 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 *) @@ -527,7 +538,7 @@ let process_and_parse ~ofmt ~target ~uri ~version doc last_tok doc_handle = let doc = add_node ~node doc in stm doc state last_tok in - (* Note that nodes and diags in reversed order here *) + (* Note that nodes and diags are expected in reversed order here *) (match doc.nodes with | [] -> () | n :: _ -> Io.Log.trace "resume" ("last node :" ^ Coq.Ast.pr_loc n.loc)); @@ -549,26 +560,20 @@ let log_doc_completion (completed : Completion.t) = (Coq.Ast.pr_loc loc) |> Io.Log.trace "check" -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 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 - let processed_content = - Util.safe_sub processed_content offset - (String.length processed_content - offset) - in +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 + 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 = Coq.Parsing.Parsable.make ~loc:resume_loc Gramlib.Stream.(of_string ~offset processed_content) @@ -582,7 +587,19 @@ let check ~ofmt ~target ~doc () = 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 + { doc with nodes = List.rev doc.nodes; 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 7edf06fa2..39a8ae2fb 100644 --- a/fleche/doc.mli +++ b/fleche/doc.mli @@ -48,7 +48,7 @@ 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.t list ; diags_dirty : bool diff --git a/lsp/base.ml b/lsp/base.ml index 060f8a28d..bf1cee1c3 100644 --- a/lsp/base.ml +++ b/lsp/base.ml @@ -59,7 +59,7 @@ module Message = struct Request { id; method_; params }) |> Result.ok with - | Not_found -> Error "missing parameter" + | 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)) From a2d0a115529eaeed24bb48ffc58f7c14f56cf4f5 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Fri, 13 Jan 2023 20:25:17 +0100 Subject: [PATCH 37/39] [fleche] Store (and restore) global stats per-document. Fixes #173 There are many improvements that we could do here. --- CHANGES.md | 1 + fleche/doc.ml | 31 +++++++++++++++++++++---------- fleche/doc.mli | 1 + fleche/stats.ml | 11 ++++++++++- fleche/stats.mli | 7 ++++++- 5 files changed, 39 insertions(+), 12 deletions(-) diff --git a/CHANGES.md b/CHANGES.md index 513e562cd..4ca9c3a24 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -22,6 +22,7 @@ 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/fleche/doc.ml b/fleche/doc.ml index d3cb90883..78bdf13f5 100644 --- a/fleche/doc.ml +++ b/fleche/doc.ml @@ -54,7 +54,7 @@ module Util = struct let size = Memo.mem_stats () in Io.Log.trace "stats" (string_of_int size)); - Io.Log.trace "cache" (Stats.dump ()); + 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 ()); *) @@ -166,6 +166,7 @@ type t = ; 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 = @@ -193,6 +194,8 @@ let process_init_feedback loc state feedback = let create ~state ~workspace ~uri ~version ~contents = 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 @@ -205,6 +208,7 @@ let create ~state ~workspace ~uri ~version ~contents = ; nodes ; diags_dirty ; completed = Stopped init_loc + ; stats }) let recover_up_to_offset doc offset = @@ -284,6 +288,7 @@ let send_eager_diagnostics ~ofmt ~uri ~version ~doc = 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 @@ -538,7 +543,10 @@ let process_and_parse ~ofmt ~target ~uri ~version doc last_tok doc_handle = let doc = add_node ~node doc in stm doc state last_tok in - (* Note that nodes and diags are expected in reversed order here *) + (* 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)); @@ -546,7 +554,13 @@ let process_and_parse ~ofmt ~target ~uri ~version doc last_tok doc_handle = Util.hd_opt ~default:doc.root (List.map (fun { Node.state; _ } -> state) doc.nodes) in - stm doc st last_tok + 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 @@ -578,16 +592,13 @@ let resume_check ~ofmt ~last_tok ~doc ~target = Coq.Parsing.Parsable.make ~loc:resume_loc Gramlib.Stream.(of_string ~offset processed_content) in - (* Set the document to "internal" mode *) - let doc = - { doc with contents = processed_content; nodes = List.rev doc.nodes } - in + (* Set the content to the padded version if neccesary *) + let doc = { doc with contents = processed_content } in let doc = process_and_parse ~ofmt ~target ~uri ~version doc last_tok handle in - (* Set the document to "finished" mode: Restore the original contents, - reverse the accumulators *) - { doc with nodes = List.rev doc.nodes; contents } + (* Restore the original contents *) + { doc with contents } let check ~ofmt ~target ~doc () = match doc.completed with diff --git a/fleche/doc.mli b/fleche/doc.mli index 39a8ae2fb..eaaf78927 100644 --- a/fleche/doc.mli +++ b/fleche/doc.mli @@ -53,6 +53,7 @@ type t = private ; nodes : Node.t list ; diags_dirty : bool ; completed : Completion.t + ; stats : Stats.t (** Info about cumulative stats *) } (** Note, [create] calls Coq but it is not cached in the Memo.t table *) diff --git a/fleche/stats.ml b/fleche/stats.ml index ff2ed3da9..61c7629d7 100644 --- a/fleche/stats.ml +++ b/fleche/stats.ml @@ -17,6 +17,15 @@ 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 bump kind time = let acc = find kind in Hashtbl.replace stats kind (acc +. time) @@ -34,7 +43,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..932c38ffe 100644 --- a/fleche/stats.mli +++ b/fleche/stats.mli @@ -8,5 +8,10 @@ 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 From d674f867c30eadce8d418732eae0aca6bc27bfa2 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Fri, 13 Jan 2023 20:30:35 +0100 Subject: [PATCH 38/39] [doc] Turn node info into a proper data structure. --- fleche/doc.ml | 60 +++++++++++++++++++++++++++----------------------- fleche/doc.mli | 10 ++++++--- fleche/info.ml | 2 +- 3 files changed, 40 insertions(+), 32 deletions(-) diff --git a/fleche/doc.ml b/fleche/doc.ml index 78bdf13f5..93b35a603 100644 --- a/fleche/doc.ml +++ b/fleche/doc.ml @@ -93,21 +93,6 @@ module Util = struct 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 memo_info ~cache_hit ~parsing_time ~time ~mw_prev = - 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) - in - memo_info ^ "\n___\n" ^ mem_info end module DDebug = struct @@ -127,13 +112,32 @@ end (* [node list] is a very crude form of a meta-data map "loc -> data" , where for now [data] is only the goals. *) module Node = struct + module Info = struct + type t = string + + let make ~cache_hit ~parsing_time ~time ~mw_prev = + 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" 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 - ; memo_info : string + ; info : Info.t } let loc { loc; _ } = loc @@ -141,7 +145,7 @@ module Node = struct let state { state; _ } = state let diags { diags; _ } = diags let messages { messages; _ } = messages - let memo_info { memo_info; _ } = memo_info + let info { info; _ } = info end module Completion = struct @@ -188,7 +192,7 @@ let get_last_text 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 - [ { Node.loc; ast = None; state; diags; messages; memo_info = "" } ] + [ { Node.loc; ast = None; state; diags; messages; info = "" } ] else [] let create ~state ~workspace ~uri ~version ~contents = @@ -351,8 +355,8 @@ let interp_and_info ~parsing_time ~st ast = let { Memo.Stats.res; cache_hit; memory = _; time } = Memo.interp_command ~st ast in - let memo_info = Util.memo_info ~cache_hit ~parsing_time ~time ~mw_prev in - (res, memo_info) + let info = Node.Info.make ~cache_hit ~parsing_time ~time ~mw_prev in + (res, info) type parse_action = | EOF of Completion.t (* completed *) @@ -402,7 +406,7 @@ type document_action = let unparseable_node ~loc ~parsing_diags ~parsing_feedback ~state = let fb_diags, messages = Util.diags_of_feedback ~loc parsing_feedback in let diags = fb_diags @ parsing_diags in - { Node.loc; ast = None; diags; messages; state; memo_info = "" } + { Node.loc; ast = None; diags; messages; state; info = "" } let assemble_diags ~loc ~parsing_diags ~parsing_feedback ~diags ~feedback = let parsing_fb_diags, parsing_messages = @@ -414,11 +418,11 @@ let assemble_diags ~loc ~parsing_diags ~parsing_feedback ~diags ~feedback = (diags, messages) let parsed_node ~loc ~ast ~state ~parsing_diags ~parsing_feedback ~diags - ~feedback ~memo_info = + ~feedback ~info = let diags, messages = assemble_diags ~loc ~parsing_diags ~parsing_feedback ~diags ~feedback in - { Node.loc; ast = Some ast; diags; messages; state; memo_info } + { Node.loc; ast = Some ast; diags; messages; state; info } let maybe_ok_diagnostics ~loc = if !Config.v.ok_diagnostics then @@ -431,14 +435,14 @@ let strategy_of_coq_err ~node ~state ~last_tok = function | User _ -> Continue { state; last_tok; node } let node_of_coq_result ~doc ~parsing_diags ~parsing_feedback ~ast ~st ~feedback - ~memo_info last_tok res = + ~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 ~memo_info + ~diags:ok_diags ~feedback ~info in Continue { state; last_tok; node } | Error (Coq.Protect.Error.Anomaly (err_loc, msg) as coq_err) @@ -448,7 +452,7 @@ let node_of_coq_result ~doc ~parsing_diags ~parsing_feedback ~ast ~st ~feedback 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 ~memo_info + ~parsing_feedback ~diags:err_diags ~feedback ~info in strategy_of_coq_err ~node ~state:recovery_st ~last_tok coq_err @@ -471,7 +475,7 @@ let document_action ~st ~parsing_diags ~parsing_feedback ~parsing_time ~doc Continue { state = st; last_tok; node } (* We can interpret the command now *) | Process ast -> ( - let { Coq.Protect.E.r; feedback }, memo_info = + let { Coq.Protect.E.r; feedback }, info = interp_and_info ~parsing_time ~st ast in match r with @@ -483,7 +487,7 @@ let document_action ~st ~parsing_diags ~parsing_feedback ~parsing_time ~doc this point then, hence the new last valid token last_tok_new *) let last_tok_new = Coq.Parsing.Parsable.loc doc_handle in node_of_coq_result ~doc ~ast ~st ~parsing_diags ~parsing_feedback - ~feedback ~memo_info last_tok_new res) + ~feedback ~info last_tok_new res) module Target = struct type t = diff --git a/fleche/doc.mli b/fleche/doc.mli index eaaf78927..182fb5702 100644 --- a/fleche/doc.mli +++ b/fleche/doc.mli @@ -17,13 +17,17 @@ (************************************************************************) module Node : sig + module Info : sig + type 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 - ; memo_info : string + ; info : Info.t } val loc : t -> Loc.t @@ -31,7 +35,7 @@ module Node : sig val state : t -> Coq.State.t val diags : t -> Types.Diagnostic.t list val messages : t -> Coq.Message.t list - val memo_info : t -> string + val info : t -> string end module Completion : sig @@ -53,7 +57,7 @@ type t = private ; nodes : Node.t list ; diags_dirty : bool ; completed : Completion.t - ; stats : Stats.t (** Info about cumulative stats *) + ; stats : Stats.t (** Info about cumulative document stats *) } (** Note, [create] calls Coq but it is not cached in the Memo.t table *) diff --git a/fleche/info.ml b/fleche/info.ml index 81c4f21f5..9bbd294bd 100644 --- a/fleche/info.ml +++ b/fleche/info.ml @@ -189,7 +189,7 @@ module Make (P : Point) : S with module P := P = struct find ~doc ~point approx |> Option.map Doc.Node.messages let info ~doc ~point approx = - find ~doc ~point approx |> Option.map Doc.Node.memo_info + find ~doc ~point approx |> Option.map Doc.Node.info (* XXX: This belongs in Coq *) let pr_extref gr = From b3cece3a49b23d879851ca78bc153ebcfcf1ecbc Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Fri, 13 Jan 2023 20:47:23 +0100 Subject: [PATCH 39/39] [fleche] Store stats in raw form. This way we can process them for a document and determine who are the most expensive sentences, etc... --- controller/requests.ml | 5 ++++- fleche/doc.ml | 47 ++++++++++++++++++++++++++++++++---------- fleche/doc.mli | 12 +++++++++-- fleche/info.ml | 2 +- fleche/info.mli | 2 +- fleche/stats.ml | 6 ++++++ fleche/stats.mli | 1 + 7 files changed, 59 insertions(+), 16 deletions(-) diff --git a/controller/requests.ml b/controller/requests.ml index 97434f2ec..9c20090c4 100644 --- a/controller/requests.ml +++ b/controller/requests.ml @@ -53,8 +53,11 @@ let hover ~doc ~point = 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.default "no info" + 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 diff --git a/fleche/doc.ml b/fleche/doc.ml index 93b35a603..da8475ccd 100644 --- a/fleche/doc.ml +++ b/fleche/doc.ml @@ -113,16 +113,30 @@ end now [data] is only the goals. *) module Node = struct module Info = struct - type t = string + 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 make ~cache_hit ~parsing_time ~time ~mw_prev = - 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 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): %.4f / %.2f" - cache_hit parsing_time cptime time cetime + "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 @@ -192,7 +206,10 @@ let get_last_text 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 - [ { Node.loc; ast = None; state; diags; messages; info = "" } ] + 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 = @@ -355,7 +372,10 @@ let interp_and_info ~parsing_time ~st ast = let { Memo.Stats.res; cache_hit; memory = _; time } = Memo.interp_command ~st ast in - let info = Node.Info.make ~cache_hit ~parsing_time ~time ~mw_prev in + let { Gc.major_words = mw_after; _ } = Gc.quick_stat () in + let info = + Node.Info.make ~cache_hit ~parsing_time ~time ~mw_prev ~mw_after () + in (res, info) type parse_action = @@ -403,10 +423,13 @@ type document_action = } | Interrupted of Loc.t -let unparseable_node ~loc ~parsing_diags ~parsing_feedback ~state = +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 - { Node.loc; ast = None; diags; messages; state; info = "" } + 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 = @@ -465,12 +488,14 @@ let document_action ~st ~parsing_diags ~parsing_feedback ~parsing_time ~doc 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 *) diff --git a/fleche/doc.mli b/fleche/doc.mli index 182fb5702..0bb01ce2d 100644 --- a/fleche/doc.mli +++ b/fleche/doc.mli @@ -18,7 +18,15 @@ module Node : sig module Info : sig - type t = string + 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 @@ -35,7 +43,7 @@ module Node : sig val state : t -> Coq.State.t val diags : t -> Types.Diagnostic.t list val messages : t -> Coq.Message.t list - val info : t -> string + val info : t -> Info.t end module Completion : sig diff --git a/fleche/info.ml b/fleche/info.ml index 9bbd294bd..b0d76f9dd 100644 --- a/fleche/info.ml +++ b/fleche/info.ml @@ -118,7 +118,7 @@ module type S = sig 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/info.mli b/fleche/info.mli index fdfe9bc70..a19448fc4 100644 --- a/fleche/info.mli +++ b/fleche/info.mli @@ -49,7 +49,7 @@ module type S = sig 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/stats.ml b/fleche/stats.ml index 61c7629d7..9ded94ac9 100644 --- a/fleche/stats.ml +++ b/fleche/stats.ml @@ -26,6 +26,12 @@ let restore (h, p, e) = 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) diff --git a/fleche/stats.mli b/fleche/stats.mli index 932c38ffe..78258fd62 100644 --- a/fleche/stats.mli +++ b/fleche/stats.mli @@ -15,3 +15,4 @@ type t val dump : unit -> t val restore : t -> unit +val get_f : t -> kind:Kind.t -> float