diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml index 1d7c9e81..0494a8ba 100644 --- a/.github/workflows/build.yml +++ b/.github/workflows/build.yml @@ -40,6 +40,8 @@ jobs: ocaml: 5.0.x - os: ubuntu-latest ocaml: 5.1.x + - os: ubuntu-latest + ocaml: 5.2.x - os: macos-latest ocaml: 4.14.x - name: Windows Latest @@ -79,6 +81,39 @@ jobs: - name: 🐛 Test fcc run: opam exec -- make test-compiler + build-opam: + name: Opam dev install + strategy: + fail-fast: false + runs-on: ubuntu-latest + steps: + - name: 🔭 Checkout code + uses: actions/checkout@v3 + with: + submodules: recursive + + - name: 🐫 Setup OCaml + uses: ocaml/setup-ocaml@v2 + with: + ocaml-compiler: 4.14.x + dune-cache: true + + - name: Install Coq and SerAPI into OPAM switch + run: | + opam install lwt logs # Also build pet-server + opam install memprof-limits # We need to do this to avoid coq-lsp rebuilding Coq below due to deptops + opam install vendor/coq/{coq-core,coq-stdlib,coqide-server,coq}.opam + opam install vendor/coq-serapi/coq-serapi.opam + + - name: Install `coq-lsp` into OPAM switch + run: opam install . + + - name: Test `coq-lsp` in installed switch + run: opam exec -- fcc examples/Demo.v + + - name: Test `pet-server` is built + run: opam exec -- which pet-server + client-compile: runs-on: ubuntu-latest defaults: diff --git a/.ocamlformat b/.ocamlformat index 16289641..b2257f5a 100644 --- a/.ocamlformat +++ b/.ocamlformat @@ -1,4 +1,4 @@ -version=0.26.0 +version=0.26.1 profile=conventional ocaml-version=4.08.0 break-separators=before diff --git a/CHANGES.md b/CHANGES.md index dac06c04..9bed0d3f 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -1,5 +1,5 @@ -# unreleased ------------- +# coq-lsp 0.1.9: Hasta el 40 de Mayo... +--------------------------------------- - new option `show_loc_info_on_hover` that will display parsing debug information on hover; previous flag was fixed in code, which is way @@ -65,11 +65,19 @@ #348) - fix Coq performance view display (@ejgallego, #663, regression in #513) + - Added new heatmap feature allowing timing data to be seen in the + editor. Can be enabled with the `Coq LSP: Toggle heatmap` + command. Can be configured to show memory usage. Colors and + granularity are configurable. (@Alizter and @ejgallego, #686, + grants #681). - allow more than one input position in `selectionRange` LSP call (@ejgallego, #667, fixes #663) - new VSCode commands to allow to move one sentence backwards / forward, this is particularly useful when combined with lazy checking mode (@ejgallego, #671, fixes #263, fixes #580) + - VSCode commands `coq-lsp.sentenceNext` / `coq-lsp.sentencePrevious` + are now bound by default to `Alt + N` / `Alt + P` keybindings + (@ejgallego, #718) - change diagnostic `extra` field to `data`, so we now conform to the LSP spec, include the data only when the `send_diags_extra_data` server-side option is enabled (@ejgallego, #670) @@ -98,6 +106,81 @@ - Update `package-lock.json` for latest bugfixes (@ejgallego, #687) - Update Nix flake enviroment (@Alizter, #684 #688) - Update `prettier` (@Alizter @ejgallego, #684 #688) + - Store original performance data in the cache, so we now display the + original timing and memory data even for cached commands (@ejgallego, #693) + - Fix type errors in the Performance Data Notifications (@ejgallego, + @Alizter, #689, #693) + - Send performance performance data for the full document + (@ejgallego, @Alizter, #689, #693) + - Better types `coq/perfData` call (@ejgallego @Alizter, #689) + - New server option to enable / disable `coq/perfData` (@ejgallego, #689) + - New client option to enable / disable `coq/perfData` (@ejgallego, #717) + - The `coq-lsp.document` VSCode command will now display the returned + JSON data in a new editor (@ejgallego, #701) + - Update server settings on the fly when tweaking them in VSCode. + Implement `workspace/didChangeConfiguration` (@ejgallego, #702) + - [Coq API] Add functions to retrieve list of declarations done in + .vo files (@ejallego, @eytans, #704) + - New `petanque` API to interact directly with Coq's proof + engine. (@ejgallego, @gbdrt, Laetitia Teodorescu #703, thanks to + Alex Sanchez-Stern for many insightful feedback and testing) + - New `petanque` JSON-RPC `pet.exe`, which can be used à la SerAPI + to perform proof search and more (@ejgallego, @gbdrt, #705) + - New `pet-server.exe` TCP server for keep-alive sessions (@gbdrt, + #697) + - Always dispose UI elements. This should improve some strange + behaviors on extension restart (@ejgallego, #708) + - [code] Added new heatmap feature allowing timing data to be seen in + the editor. Can be enabled with the `Coq LSP: Toggle heatmap` + comamnd. Can be configured to show memory usage. Colors and + granularity are configurable. (@Alizter and @ejgallego, #686, + grants #681). + - [server] Support Coq meta-commands (Reset, Reset Initial, Back) + They are actually pretty useful to hint the incremental engine to + ignore changes in some part of the document (@ejgallego, #709) + - JSON-RPC library now supports all kind of incoming messages + (@ejgallego, #713) + - [code/server] New `coq/viewRange` notification, from client to + server, than hints the scheduler for the visible area of the + document; combined with the new lazy checking mode, this provides + checking on scroll, a feature inspired from Isabelle IDE + (@ejgallego, #717) + - [code] Have VSCode wait for full LSP client shutdown on server + restart. This fixes some bugs on extension restart (finally!) + (@ejgallego, #719) + - [code] Center the view if cursor goes out of scope in + `sentenceNext/sentencePrevious` (@ejgallego, #718) + - Switch Flèche range encoding to protocol native, this means UTF-16 + code points for now (Léo Stefanesco, @ejgallego, #624, fixes #620, + #621) + - Give `Goals` panel focus back if it has lost it (in case of + multiple panels in the second viewColumn of Vscode) whenever + user navigates proofs (@Alidra @ejgallego, #722, #725) + - `fcc`: new option `--diags_level` to control whether Coq's notice + and info messages appear as diagnostics + - [code] Display the continous/on-request checking mode in the status bar, + allow to change it by clicking on it (@ejgallego, #721) + - Add an example of multiple workspaces (@ejgallego, @Blaisorblade, + #611) + - Don't show types of un-expanded goals. We should add an option for + this, but we don't have the cycles (@ejgallego, #730, workarounds + #525 #652) + - Support for `.lv / .v.tex` TeX files with embedded Coq code + (@ejgallego, #727) + - Don't expand bullet goals at previous levels by default + (@ejgallego, @Alizter, #731 cc #525) + - [petanque] Return basic goal information after `run_tac`, so we + avoid a `goals` round-trip for each tactic (@gbdrt, @ejgallego, + #733) + - [coq] Add support for reading glob files metadata (@ejgallego, + #735) + - [petanque] Return extra premise information: file name, position, + raw_text, using the above support for reading .glob files + (@ejgallego, #735) + - [code] Display server status using the `LanguageStatusItem` + facility, for now we display version and checking status + information (moved from #721), and we also allow to toggle the + checking mode from there (@ejgallego, #728) # coq-lsp 0.1.8.1: Spring fix ----------------------------- diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md index 96a07cdb..b4abacf5 100644 --- a/CONTRIBUTING.md +++ b/CONTRIBUTING.md @@ -3,17 +3,23 @@ Contributing to Coq LSP Thank you very much for willing to contribute to coq-lsp! -`coq-lsp` has two components: +The `coq-lsp` repository contains several tightly coupled components +in a single repository, also known as a monorepo, in particular: -- a LSP server for Coq project written in OCaml. -- a `coq-lsp` VS Code extension written in TypeScript and React, in - the `editor/code` directory. +- Flèche: an incremental document engine for Coq supporting literate + programming and programability, written in OCaml +- `fcc`: an extensible command line compiler built on top of Flèche +- `petanque`: direct access to Coq's proof engine +- `coq-lsp`a LSP server for the Coq project, written in OCaml on top of Flèche +- a `coq-lsp/VSCode` extension written in TypeScript and React, in + the `editor/code` directory -Read coq-lsp [FAQ](etc/FAQ.md) for an explanation on what the above mean. +Read coq-lsp [FAQ](etc/FAQ.md) to learn more about LSP and +server/client roles. -It is possible to hack only in the server, on the client, or on both at the same -time. We have thus structured this guide in 3 sections: general guidelines, -server, and VS Code client. +It is possible to hack only in the server, on the client, or on both +at the same time. We have thus structured this guide in 3 sections: +general guidelines, server, and VS Code client. ## General guidelines @@ -184,14 +190,17 @@ coq-lsp.packages.${system}.default The `coq-lsp` server consists of several components, we present them bottom-up +- `vendor/coq`: [vendored] Coq version to build coq-lsp against - `vendor/coq-serapi`: [vendored] improved utility functions to handle Coq AST - `coq`: Utility library / abstracted Coq API. This is the main entry point for communication with Coq, and it reifies Coq calls as to present a purely functional interface to Coq. +- `lang`: base language definitions for Flèche - `fleche`: incremental document processing backend. Exposes a generic API, but closely modelled to match LSP - `lsp`: small generic LSP utilities, at some point to be replaced by a generic library +- `petanque`: low-level access to Coq's API - `controller`: LSP controller, a thin layer translating LSP transport layer to `flèche` surface API, plus some custom event queues for Coq. - `controller-js`: LSP controller for Javascript, used for `vscode.dev` and @@ -209,6 +218,29 @@ Some tips: [ocamlformat]: https://github.com/ocaml-ppx/ocamlformat +### Unicode setup + +Flèche stores locations in the protocol-native format. This has the +advantage that conversion is needed only at range creation point +(where we usually have access to the document to perform the +conversion). + +This way, we can send ranges to the client without conversion. + +Request that work on the raw `Contents.t` buffer must do the inverse +conversion, but we handle this via a proper text API that is aware of +the conversion. + +For now, the setup for Coq is: + +- protocol-level (and Flèche) encoding: UTF-16 (due to LSP) +- `Contents.t`: UTF-8 (sent to Coq) + +It would be very easy to set this parameters at initialization time, +ideal would be for LSP clients to catch up and allow UTF-8 encodings +(so no conversion is needed, at least for Coq), but it seems that we +will take a while to get to this point. + ## Client guide (VS Code Extension) The VS Code extension is setup as a standard `npm` Typescript + React package diff --git a/README.md b/README.md index 19ec0065..e9162961 100644 --- a/README.md +++ b/README.md @@ -20,6 +20,8 @@ document checking, advanced error recovery, hybrid Coq/markdown document support, multiple workspace support, positional goals and information panel, performance data, extensible command-line compiler, plugin system, and more. +See the [coq-lsp User Manual](./etc/doc/USER_MANUAL.md) for more information. + `coq-lsp` aims to provide a seamless, modern interactive theorem proving experience, as well as to serve as a maintainable platform for research and UI integration with other projects. @@ -37,6 +39,7 @@ and web native usage, providing quite a few extra features from vanilla Coq. - [🎁 Features](#-features) - [⏩ Incremental Compilation and Continuous Document Checking](#-incremental-compilation-and-continuous-document-checking) + - [👁 On-demand, Follow The Viewport Document Checking](#-on-demand-follow-the-viewport-document-checking) - [🧠 Smart, Cache-Aware Error Recovery](#-smart-cache-aware-error-recovery) - [🥅 Whole-Document Goal Display](#-whole-document-goal-display) - [🗒️ Markdown Support](#️-markdown-support) @@ -58,6 +61,7 @@ and web native usage, providing quite a few extra features from vanilla Coq. - [✅ Vim](#-vim) - [🩱 Neovim](#-neovim) - [🐍 Python](#-python) +- [⇨ `coq-lsp` users and extensions](#-coq-lsp-users-and-extensions) - [🗣️ Discussion Channel](#️-discussion-channel) - [☎ Weekly Calls](#-weekly-calls) - [❓FAQ](#faq) @@ -87,6 +91,14 @@ restart your proof session where you left it at the last time. Incremental support is undergoing refinement, if `coq-lsp` rechecks when it should not, please file a bug! +### 👁 On-demand, Follow The Viewport Document Checking + +`coq-lsp` does also support on-demand checking. Two modes are available: follow +the cursor, or follow the viewport; the modes can be toggled using the Language +Status Item in Code's bottom right corner: + +On-demand checking + ### 🧠 Smart, Cache-Aware Error Recovery `coq-lsp` won't stop checking on errors, but supports (and encourages) working @@ -182,6 +194,12 @@ fully-fledged LSP client. add your pre/post processing passes, for example to analyze or serialize parts of Coq files. +### 🪄 Advanced APIs for Coq Interaction + +Thanks to Flèche, we provide some APIs on top of it that allow advanced use +cases with Coq. In particular, we provide direct, low-overhead access to Coq's +proof engine using [petanque](./petanque). + ### ♻️ Reusability, Standards, Modularity The incremental document checking library of `coq-lsp` has been designed to be @@ -301,6 +319,17 @@ guide](./CONTRIBUTING.md) - Interact programmatically with Coq files by using the [Python `coq-lsp` client](https://github.com/sr-lab/coq-lsp-pyclient) by Pedro Carrott and Nuno Saavedra. +## ⇨ `coq-lsp` users and extensions + +The below projects are using `coq-lsp`, we recommend you try them! + +- [CoqPilot uses Large Language Models to generate multiple potential proofs and then uses coq-lsp to typecheck them](https://github.com/JetBrains-Research/coqpilot). +- [jsCoq: use Coq from your browser](https://github.com/jscoq/jscoq) +- [Pytanque: a Python library implementing RL Environments](https://github.com/LLM4Coq/pytanque) +- [ViZX: A Visualizer for the ZX Calculus](https://github.com/inQWIRE/ViZX). +- [The Waterproof vscode extension helps students learn how to write mathematical proofs](https://github.com/impermeable/waterproof-vscode). +- [Yade: Support for the YADE diagram editor in VSCode](https://github.com/amblafont/vscode-yade-example). + ## 🗣️ Discussion Channel `coq-lsp` discussion channel it at [Coq's @@ -326,7 +355,7 @@ recommend that if you are installing via opam, you use the following branches that have some fixes backported: - For 8.20: No known problems -- For 8.19: No known problems +- For 8.19: `opam pin add coq-core https://github.com/ejgallego/coq.git#v8.19+lsp` - For 8.18: `opam pin add coq-core https://github.com/ejgallego/coq.git#v8.18+lsp` - For 8.17: `opam pin add coq-core https://github.com/ejgallego/coq.git#v8.17+lsp` - For 8.16: `opam pin add coq https://github.com/ejgallego/coq.git#v8.16+lsp` diff --git a/compiler/args.ml b/compiler/args.ml index ede34c06..b6de9e98 100644 --- a/compiler/args.ml +++ b/compiler/args.ml @@ -14,6 +14,8 @@ type t = ; plugins : string list (** Flèche plugins to load *) ; max_errors : int option (** Maximum erros before aborting the compilation *) + ; coq_diags_level : int + (** Whether to include feedback messages in the diagnostics *) } let compute_default_plugins ~no_vo ~plugins = diff --git a/compiler/compile.ml b/compiler/compile.ml index 059b05ac..263817d0 100644 --- a/compiler/compile.ml +++ b/compiler/compile.ml @@ -22,7 +22,7 @@ let save_diags_file ~(doc : Fleche.Doc.t) = let file = Lang.LUri.File.to_string_file doc.uri in let file = Filename.remove_extension file ^ ".diags" in let diags = Fleche.Doc.diags doc in - Util.format_to_file ~file ~f:Output.pp_diags diags + Coq.Compat.format_to_file ~file ~f:Output.pp_diags diags (** Return: exit status for file: @@ -47,7 +47,7 @@ let compile_file ~cc file : int = let workspace = workspace_of_uri ~io ~workspaces ~uri ~default in let files = Coq.Files.make () in let env = Doc.Env.make ~init:root_state ~workspace ~files in - let raw = Util.input_all file in + let raw = Coq.Compat.Ocaml_414.In_channel.(with_open_bin file input_all) in let () = Theory.create ~io ~token ~env ~uri ~raw ~version:1 in match Theory.Check.maybe_check ~io ~token with | None -> 102 diff --git a/compiler/driver.ml b/compiler/driver.ml index e8d0d94f..20814cc6 100644 --- a/compiler/driver.ml +++ b/compiler/driver.ml @@ -36,18 +36,26 @@ let apply_config ~max_errors = max_errors let go ~int_backend args = - let { Args.cmdline; roots; display; debug; files; plugins; max_errors } = + let { Args.cmdline + ; roots + ; display + ; debug + ; files + ; plugins + ; max_errors + ; coq_diags_level + } = args in (* Initialize event callbacks, in testing don't do perfData *) let perfData = Option.is_empty fcc_test in - let io = Output.init display ~perfData in + let io = Output.init ~display ~perfData ~coq_diags_level in (* Initialize Coq *) let debug = debug || Fleche.Debug.backtraces || !Fleche.Config.v.debug in let root_state = coq_init ~debug in let roots = if List.length roots < 1 then [ Sys.getcwd () ] else roots in let default = Coq.Workspace.default ~debug ~cmdline in - let () = Coq.Limits.select int_backend in + let () = Coq.Limits.select_best int_backend in let () = Coq.Limits.start () in let token = Coq.Limits.Token.create () in let workspaces = diff --git a/compiler/fcc.ml b/compiler/fcc.ml index 8dc8d41d..dd990ad3 100644 --- a/compiler/fcc.ml +++ b/compiler/fcc.ml @@ -3,7 +3,8 @@ open Cmdliner open Fcc_lib let fcc_main int_backend roots display debug plugins files coqlib coqcorelib - ocamlpath rload_path load_path require_libraries no_vo max_errors = + ocamlpath rload_path load_path require_libraries no_vo max_errors + coq_diags_level = let vo_load_path = rload_path @ load_path in let ml_include_path = [] in let args = [] in @@ -19,16 +20,21 @@ let fcc_main int_backend roots display debug plugins files coqlib coqcorelib in let plugins = Args.compute_default_plugins ~no_vo ~plugins in let args = - Args.{ cmdline; roots; display; files; debug; plugins; max_errors } + Args. + { cmdline + ; roots + ; display + ; files + ; debug + ; plugins + ; max_errors + ; coq_diags_level + } in Driver.go ~int_backend args (****************************************************************************) (* Specific to fcc *) -let roots : string list Term.t = - let doc = "Workspace(s) root(s)" in - Arg.(value & opt_all string [] & info [ "root" ] ~docv:"ROOTS" ~doc) - let display : Args.Display.t Term.t = let doc = "Verbosity display settings" in let dparse = @@ -95,7 +101,7 @@ let fcc_cmd : int Cmd.t = Term.( const fcc_main $ int_backend $ roots $ display $ debug $ plugins $ file $ coqlib $ coqcorelib $ ocamlpath $ rload_paths $ qload_paths $ ri_from - $ no_vo $ max_errors) + $ no_vo $ max_errors $ coq_diags_level) in let exits = Exit_codes.[ fatal; stopped; scheduled; uri_failed ] in Cmd.(v (Cmd.info "fcc" ~exits ~version ~doc ~man) fcc_term) diff --git a/compiler/output.ml b/compiler/output.ml index f9f13f4d..bbf66a2a 100644 --- a/compiler/output.ml +++ b/compiler/output.ml @@ -9,7 +9,6 @@ let pp_diags fmt dl = (* We will use this when we set eager diagnotics to true *) let diagnostics ~uri:_ ~version:_ _diags = () let fileProgress ~uri:_ ~version:_ _progress = () -let perfData ~uri:_ ~version:_ _perf = () (* We print trace and messages, and perfData summary *) module Fcc_verbose = struct @@ -24,26 +23,30 @@ module Fcc_verbose = struct let perfData ~uri:_ ~version:_ { Fleche.Perf.summary; _ } = Format.(eprintf "[perfdata]@\n@[%s@]@\n%!" summary) + let serverVersion _ = () + let serverStatus _ = () + let cb = - Fleche.Io.CallBack.{ trace; message; diagnostics; fileProgress; perfData } + Fleche.Io.CallBack. + { trace + ; message + ; diagnostics + ; fileProgress + ; perfData + ; serverVersion + ; serverStatus + } end (* We print trace, messages *) module Fcc_normal = struct let trace _ ?extra:_ _ = () - let message = Fcc_verbose.message - let perfData = Fcc_verbose.perfData - - let cb = - Fleche.Io.CallBack.{ trace; message; diagnostics; fileProgress; perfData } + let cb = { Fcc_verbose.cb with trace } end module Fcc_quiet = struct - let trace _ ?extra:_ _ = () let message ~lvl:_ ~message:_ = () - - let cb = - Fleche.Io.CallBack.{ trace; message; diagnostics; fileProgress; perfData } + let cb = { Fcc_normal.cb with message } end let set_callbacks (display : Args.Display.t) = @@ -56,16 +59,18 @@ let set_callbacks (display : Args.Display.t) = Fleche.Io.CallBack.set cb; cb -let set_config ~perfData = +let set_config ~perfData ~coq_diags_level = + let show_coq_info_messages = coq_diags_level > 1 in + let show_notices_as_diagnostics = coq_diags_level > 0 in Fleche.Config.( v := { !v with send_perf_data = perfData ; eager_diagnostics = false - ; show_coq_info_messages = true - ; show_notices_as_diagnostics = true + ; show_coq_info_messages + ; show_notices_as_diagnostics }) -let init display ~perfData = - set_config ~perfData; +let init ~display ~coq_diags_level ~perfData = + set_config ~perfData ~coq_diags_level; set_callbacks display diff --git a/compiler/output.mli b/compiler/output.mli index 7e643bc0..a4699ef7 100644 --- a/compiler/output.mli +++ b/compiler/output.mli @@ -1,5 +1,9 @@ (** Initialize Console Output System *) -val init : Args.Display.t -> perfData:bool -> Fleche.Io.CallBack.t +val init : + display:Args.Display.t + -> coq_diags_level:int + -> perfData:bool + -> Fleche.Io.CallBack.t (** Report progress on file compilation *) (* val report : unit -> unit *) diff --git a/compiler/util.mli b/compiler/util.mli deleted file mode 100644 index b9eaaf94..00000000 --- a/compiler/util.mli +++ /dev/null @@ -1,4 +0,0 @@ -val input_all : string -> string - -val format_to_file : - file:string -> f:(Format.formatter -> 'a -> unit) -> 'a -> unit diff --git a/controller/coq_lsp.ml b/controller/coq_lsp.ml index 2af1fbc9..25caf87d 100644 --- a/controller/coq_lsp.ml +++ b/controller/coq_lsp.ml @@ -49,35 +49,52 @@ let rec process_queue ~delay ~io ~ofn ~state : unit = | Some (Cont state) -> process_queue ~delay ~io ~ofn ~state let concise_cb ofn = + let send_notification nt = + Lsp.Base.Message.(Notification nt |> to_yojson) |> ofn + in + let diagnostics ~uri ~version diags = + if List.length diags > 0 then + Lsp.JLang.mk_diagnostics ~uri ~version diags |> send_notification + in Fleche.Io.CallBack. { trace = (fun _hdr ?extra:_ _msg -> ()) ; message = (fun ~lvl:_ ~message:_ -> ()) - ; diagnostics = - (fun ~uri ~version diags -> - if List.length diags > 0 then - Lsp.JLang.mk_diagnostics ~uri ~version diags |> ofn) + ; diagnostics ; fileProgress = (fun ~uri:_ ~version:_ _progress -> ()) ; perfData = (fun ~uri:_ ~version:_ _perf -> ()) + ; serverVersion = (fun _ -> ()) + ; serverStatus = (fun _ -> ()) } (* Main loop *) let lsp_cb ofn = + let send_notification nt = + Lsp.Base.Message.(Notification nt |> to_yojson) |> ofn + in + let trace = LIO.trace in let message ~lvl ~message = let lvl = Fleche.Io.Level.to_int lvl in LIO.logMessageInt ~lvl ~message in + let diagnostics ~uri ~version diags = + Lsp.JLang.mk_diagnostics ~uri ~version diags |> send_notification + in + let fileProgress ~uri ~version progress = + Lsp.JFleche.mk_progress ~uri ~version progress |> send_notification + in + let perfData ~uri ~version perf = + Lsp.JFleche.mk_perf ~uri ~version perf |> send_notification + in + let serverVersion vi = Lsp.JFleche.mk_serverVersion vi |> send_notification in + let serverStatus st = Lsp.JFleche.mk_serverStatus st |> send_notification in Fleche.Io.CallBack. - { trace = LIO.trace + { trace ; message - ; diagnostics = - (fun ~uri ~version diags -> - Lsp.JLang.mk_diagnostics ~uri ~version diags |> ofn) - ; fileProgress = - (fun ~uri ~version progress -> - Lsp.JFleche.mk_progress ~uri ~version progress |> ofn) - ; perfData = - (fun ~uri ~version perf -> - Lsp.JFleche.mk_perf ~uri ~version perf |> ofn) + ; diagnostics + ; fileProgress + ; perfData + ; serverVersion + ; serverStatus } let coq_init ~debug = @@ -91,15 +108,18 @@ let exit_notification = let rec lsp_init_loop ~ifn ~ofn ~cmdline ~debug = match ifn () with | None -> raise Lsp_exit - | Some msg -> ( + | Some (Ok msg) -> ( match lsp_init_process ~ofn ~cmdline ~debug msg with | Init_effect.Exit -> raise Lsp_exit | Init_effect.Loop -> lsp_init_loop ~ifn ~ofn ~cmdline ~debug | Init_effect.Success w -> w) + | Some (Error err) -> + Lsp.Io.trace "read_request" ("error: " ^ err); + lsp_init_loop ~ifn ~ofn ~cmdline ~debug let lsp_main bt coqcorelib coqlib ocamlpath vo_load_path ml_include_path require_libraries delay int_backend = - Coq.Limits.select int_backend; + Coq.Limits.select_best int_backend; Coq.Limits.start (); (* Try to be sane w.r.t. \r\n in Windows *) @@ -107,12 +127,19 @@ let lsp_main bt coqcorelib coqlib ocamlpath vo_load_path ml_include_path Stdlib.set_binary_mode_out stdout true; (* We output to stdout *) - let ifn () = LIO.read_request stdin in + let ifn () = LIO.read_message stdin in + (* Set log channels *) - let ofn = LIO.send_json Format.std_formatter in - LIO.set_log_fn ofn; + let json_fn = LIO.send_json Format.std_formatter in + + let ofn response = + let response = Lsp.Base.Message.to_yojson response in + LIO.send_json Format.std_formatter response + in - let io = lsp_cb ofn in + LIO.set_log_fn json_fn; + + let io = lsp_cb json_fn in Fleche.Io.CallBack.set io; (* IMPORTANT: LSP spec forbids any message from server to client before @@ -138,9 +165,12 @@ let lsp_main bt coqcorelib coqlib ocamlpath vo_load_path ml_include_path | None -> (* EOF, push an exit notication to the queue *) enqueue_message exit_notification - | Some msg -> + | Some (Ok msg) -> enqueue_message msg; read_loop () + | Some (Error err) -> + Lsp.Io.trace "read_request" ("error: " ^ err); + read_loop () in (* Input/output will happen now *) @@ -152,7 +182,7 @@ let lsp_main bt coqcorelib coqlib ocamlpath vo_load_path ml_include_path Fleche.Config.( v := { !v with send_diags = false; send_perf_data = false }); LIO.set_log_fn (fun _obj -> ()); - let io = concise_cb ofn in + let io = concise_cb json_fn in Fleche.Io.CallBack.set io; io) else io diff --git a/controller/lsp_core.ml b/controller/lsp_core.ml index c9c36765..abc0c48c 100644 --- a/controller/lsp_core.ml +++ b/controller/lsp_core.ml @@ -164,23 +164,28 @@ module Rq : sig end val serve : - ofn:(J.t -> unit) -> token:Coq.Limits.Token.t -> id:int -> Action.t -> unit + ofn_rq:(LSP.Response.t -> unit) + -> token:Coq.Limits.Token.t + -> id:int + -> Action.t + -> unit - val cancel : ofn:(J.t -> unit) -> code:int -> message:string -> int -> unit + val cancel : + ofn_rq:(LSP.Response.t -> unit) -> code:int -> message:string -> int -> unit val serve_postponed : - ofn:(J.t -> unit) + ofn_rq:(LSP.Response.t -> unit) -> token:Coq.Limits.Token.t -> doc:Fleche.Doc.t -> Int.Set.t -> unit end = struct (* Answer a request, private *) - let answer ~ofn ~id result = + let answer ~ofn_rq ~id result = (match result with - | Result.Ok result -> LSP.mk_reply ~id ~result - | Error (code, message) -> LSP.mk_request_error ~id ~code ~message) - |> ofn + | Result.Ok result -> LSP.Response.mk_ok ~id ~result + | Error (code, message) -> LSP.Response.mk_error ~id ~code ~message) + |> ofn_rq (* private to the Rq module, just used not to retrigger canceled requests *) let _rtable : (int, Request.Data.t) Hashtbl.t = Hashtbl.create 673 @@ -191,16 +196,16 @@ end = struct Hashtbl.add _rtable id pr (* Consumes a request, if alive, it answers mandatorily *) - let consume_ ~ofn ~f id = + let consume_ ~ofn_rq ~f id = match Hashtbl.find_opt _rtable id with | Some pr -> Hashtbl.remove _rtable id; - f pr |> answer ~ofn ~id + f pr |> answer ~ofn_rq ~id | None -> LIO.trace "can't consume cancelled request: " (string_of_int id); () - let cancel ~ofn ~code ~message id : unit = + let cancel ~ofn_rq ~code ~message id : unit = (* fail the request, do cleanup first *) let f pr = let () = @@ -209,30 +214,30 @@ end = struct in Error (code, message) in - consume_ ~ofn ~f id + consume_ ~ofn_rq ~f id let debug_serve id pr = if Fleche.Debug.request_delay then LIO.trace "serving" (Format.asprintf "rq: %d | %a" id Request.Data.data pr) - let serve_postponed ~ofn ~token ~doc id = + let serve_postponed ~ofn_rq ~token ~doc id = let f pr = debug_serve id pr; Request.Data.serve ~token ~doc pr in - consume_ ~ofn ~f id + consume_ ~ofn_rq ~f id - let query ~ofn ~token ~id (pr : Request.Data.t) = + let query ~ofn_rq ~token ~id (pr : Request.Data.t) = let uri, postpone, request = Request.Data.dm_request pr in match Fleche.Theory.Request.add { id; uri; postpone; request } with | Cancel -> let code = -32802 in let message = "Document is not ready" in - Error (code, message) |> answer ~ofn ~id + Error (code, message) |> answer ~ofn_rq ~id | Now doc -> debug_serve id pr; - Request.Data.serve ~token ~doc pr |> answer ~ofn ~id + Request.Data.serve ~token ~doc pr |> answer ~ofn_rq ~id | Postpone -> postpone_ ~id pr module Action = struct @@ -244,13 +249,13 @@ end = struct let error (code, msg) = now (Error (code, msg)) end - let serve ~ofn ~token ~id action = + let serve ~ofn_rq ~token ~id action = match action with - | Action.Immediate r -> answer ~ofn ~id r - | Action.Data p -> query ~ofn ~token ~id p + | Action.Immediate r -> answer ~ofn_rq ~id r + | Action.Data p -> query ~ofn_rq ~token ~id p - let serve_postponed ~ofn ~token ~doc rl = - Int.Set.iter (serve_postponed ~ofn ~token ~doc) rl + let serve_postponed ~ofn_rq ~token ~doc rl = + Int.Set.iter (serve_postponed ~ofn_rq ~token ~doc) rl end (***********************************************************************) @@ -267,7 +272,7 @@ let do_open ~io ~token ~(state : State.t) params = let env = Fleche.Doc.Env.make ~init ~workspace ~files in Fleche.Theory.create ~io ~token ~env ~uri ~raw:text ~version -let do_change ~ofn ~io ~token params = +let do_change ~ofn_rq ~io ~token params = let uri, version = Helpers.get_uri_version params in let changes = List.map U.to_assoc @@ list_field "contentChanges" params in match changes with @@ -283,7 +288,7 @@ let do_change ~ofn ~io ~token params = let invalid_rq = Fleche.Theory.change ~io ~token ~uri ~version ~raw in let code = -32802 in let message = "Request got old in server" in - Int.Set.iter (Rq.cancel ~ofn ~code ~message) invalid_rq + Int.Set.iter (Rq.cancel ~ofn_rq ~code ~message) invalid_rq let do_close ~ofn:_ params = let uri = Helpers.get_uri params in @@ -398,14 +403,32 @@ let do_document = do_document_request_maybe ~handler:Rq_document.request let do_save_vo = do_document_request_maybe ~handler:Rq_save.request let do_lens = do_document_request_maybe ~handler:Rq_lens.request -let do_cancel ~ofn ~params = +let do_cancel ~ofn_rq ~params = let id = int_field "id" params in let code = -32800 in let message = "Cancelled by client" in - Rq.cancel ~ofn ~code ~message id + Rq.cancel ~ofn_rq ~code ~message id let do_cache_trim () = Nt_cache_trim.notification () +let do_viewRange params = + match List.assoc "range" params |> Lsp.JLang.Diagnostic.Range.of_yojson with + | Ok range -> + let { Lsp.JLang.Diagnostic.Range.end_ = { line; character }; _ } = range in + let message = Format.asprintf "l: %d c:%d" line character in + LIO.trace "viewRange" message; + let uri = Helpers.get_uri params in + Fleche.Theory.Check.set_scheduler_hint ~uri ~point:(line, character); + () + | Error err -> LIO.trace "viewRange" ("error in parsing notification: " ^ err) + +let do_changeConfiguration params = + let message = "didChangeReceived" in + let () = LIO.(logMessage ~lvl:Lvl.Info ~message) in + let settings = field "settings" params |> U.to_assoc in + Rq_init.do_settings settings; + () + (***********************************************************************) (** LSP Init routine *) @@ -433,6 +456,7 @@ module Init_effect = struct end let lsp_init_process ~ofn ~cmdline ~debug msg : Init_effect.t = + let ofn_rq r = Lsp.Base.Message.response r |> ofn in match msg with | LSP.Message.Request { method_ = "initialize"; id; params } -> (* At this point logging is allowed per LSP spec *) @@ -440,11 +464,21 @@ let lsp_init_process ~ofn ~cmdline ~debug msg : Init_effect.t = Format.asprintf "Initializing coq-lsp server %s" (version ()) in LIO.logMessage ~lvl:Info ~message; - let result, dirs = Rq_init.do_initialize ~params in - (* We don't need to interrupt this *) let token = Coq.Limits.Token.create () in - Rq.Action.now (Ok result) |> Rq.serve ~ofn ~token ~id; - LIO.logMessage ~lvl:Info ~message:"Server initialized"; + let result, dirs = Rq_init.do_initialize ~params in + Rq.Action.now (Ok result) |> Rq.serve ~ofn_rq ~token ~id; + let vi = + let coq = Coq_config.version in + let ocaml = Sys.ocaml_version in + let coq_lsp = Fleche.Version.server in + Fleche.ServerInfo.Version.{ coq; ocaml; coq_lsp } + in + Lsp.JFleche.mk_serverVersion vi |> Lsp.Base.Message.notification |> ofn; + let message = + Format.asprintf "Server initializing (int_backend: %s)" + (Coq.Limits.name ()) + in + LIO.logMessage ~lvl:Info ~message; (* Workspace initialization *) let debug = debug || !Fleche.Config.v.debug in let workspaces = @@ -456,30 +490,36 @@ let lsp_init_process ~ofn ~cmdline ~debug msg : Init_effect.t = Success workspaces | LSP.Message.Request { id; _ } -> (* per spec *) - LSP.mk_request_error ~id ~code:(-32002) ~message:"server not initialized" - |> ofn; + LSP.Response.mk_error ~id ~code:(-32002) ~message:"server not initialized" + |> ofn_rq; Loop | LSP.Message.Notification { method_ = "exit"; params = _ } -> Exit | LSP.Message.Notification _ -> (* We can't log before getting the initialize message *) Loop + | LSP.Message.Response _ -> + (* O_O *) + Loop (** Dispatching *) let dispatch_notification ~io ~ofn ~token ~state ~method_ ~params : unit = + let ofn_rq r = Lsp.Base.Message.response r |> ofn in match method_ with (* Lifecycle *) | "exit" -> raise Lsp_exit - (* setTrace *) + (* setTrace and settings *) | "$/setTrace" -> do_trace params + | "workspace/didChangeConfiguration" -> do_changeConfiguration params (* Document lifetime *) | "textDocument/didOpen" -> do_open ~io ~token ~state params - | "textDocument/didChange" -> do_change ~io ~ofn ~token params + | "textDocument/didChange" -> do_change ~io ~ofn_rq ~token params | "textDocument/didClose" -> do_close ~ofn params | "textDocument/didSave" -> Cache.save_to_disk () (* Specific to coq-lsp *) + | "coq/viewRange" -> do_viewRange params | "coq/trimCaches" -> do_cache_trim () (* Cancel Request *) - | "$/cancelRequest" -> do_cancel ~ofn ~params + | "$/cancelRequest" -> do_cancel ~ofn_rq ~params (* NOOPs *) | "initialized" -> () (* Generic handler *) @@ -521,15 +561,22 @@ let dispatch_request ~method_ ~params : Rq.Action.t = LIO.trace "no_handler" msg; Rq.Action.error (-32601, "method not found") -let dispatch_request ~ofn ~token ~id ~method_ ~params = - dispatch_request ~method_ ~params |> Rq.serve ~ofn ~token ~id +let dispatch_request ~ofn_rq ~token ~id ~method_ ~params = + dispatch_request ~method_ ~params |> Rq.serve ~ofn_rq ~token ~id let dispatch_message ~io ~ofn ~token ~state (com : LSP.Message.t) : State.t = + let ofn_rq r = Lsp.Base.Message.response r |> ofn in match com with | Notification { method_; params } -> + LIO.trace "process_queue" ("Serving notification: " ^ method_); dispatch_state_notification ~io ~ofn ~token ~state ~method_ ~params | Request { id; method_; params } -> - dispatch_request ~ofn ~token ~id ~method_ ~params; + LIO.trace "process_queue" ("Serving Request: " ^ method_); + dispatch_request ~ofn_rq ~token ~id ~method_ ~params; + state + | Response r -> + LIO.trace "process_queue" + ("Serving response for: " ^ string_of_int (Lsp.Base.Response.id r)); state (* Queue handling *) @@ -560,10 +607,11 @@ type 'a cont = | Yield of 'a let check_or_yield ~io ~ofn ~token ~state = + let ofn_rq r = Lsp.Base.Message.response r |> ofn in match Fleche.Theory.Check.maybe_check ~io ~token with | None -> Yield state | Some (ready, doc) -> - let () = Rq.serve_postponed ~ofn ~token ~doc ready in + let () = Rq.serve_postponed ~ofn_rq ~token ~doc ready in Cont state module LspQueue : sig @@ -603,7 +651,6 @@ let dispatch_or_resume_check ~io ~ofn ~state = let token = token_factory () in check_or_yield ~io ~ofn ~token ~state | Some com -> - LIO.trace "process_queue" ("Serving Request: " ^ LSP.Message.method_ com); (* We let Coq work normally now *) let token = token_factory () in Cont (dispatch_message ~io ~ofn ~token ~state com) diff --git a/controller/lsp_core.mli b/controller/lsp_core.mli index 14bb111f..8581e189 100644 --- a/controller/lsp_core.mli +++ b/controller/lsp_core.mli @@ -41,7 +41,7 @@ module Init_effect : sig end val lsp_init_process : - ofn:(Yojson.Safe.t -> unit) + ofn:(Lsp.Base.Message.t -> unit) -> cmdline:Coq.Workspace.CmdLine.t -> debug:bool -> Lsp.Base.Message.t @@ -56,7 +56,7 @@ type 'a cont = wake up pending requests *) val dispatch_or_resume_check : io:Fleche.Io.CallBack.t - -> ofn:(Yojson.Safe.t -> unit) + -> ofn:(Lsp.Base.Message.t -> unit) -> state:State.t -> State.t cont option diff --git a/controller/rq_common.ml b/controller/rq_common.ml index d1a25be0..2a1627af 100644 --- a/controller/rq_common.ml +++ b/controller/rq_common.ml @@ -44,9 +44,33 @@ let get_id_at_point ~contents ~point = let { Fleche.Contents.lines; _ } = contents in if line <= Array.length lines then let line = Array.get lines line in - (* XXX UTF this will fail on unicode chars that differ among UTF-8/16 (cc - #531) *) - match Coq.Utf8.index_of_char ~line ~char:character with - | None -> None - | Some character -> find_id line character + let character = + Lang.Utf.utf8_offset_of_utf16_offset ~line ~offset:character + in + find_id line character else None + +let validate_line ~(contents : Fleche.Contents.t) ~line = + if Array.length contents.lines > line then + Some (Array.get contents.lines line) + else None + +let validate_column char line = + let length = Lang.Utf.length_utf16 line in + if char < length then + let char = Lang.Utf.utf8_offset_of_utf16_offset ~line ~offset:char in + Some (String.get line char) + else None + +(* This returns a byte-based char offset for the line *) +let validate_position ~contents ~point = + let line, char = point in + validate_line ~contents ~line |> fun l -> Option.bind l (validate_column char) + +let get_char_at_point ~contents ~point = + let line, char = point in + if char >= 1 then + let point = (line, char - 1) in + validate_position ~contents ~point + else (* Can't get previous char *) + None diff --git a/controller/rq_common.mli b/controller/rq_common.mli index 80ab0dde..a7f7bf68 100644 --- a/controller/rq_common.mli +++ b/controller/rq_common.mli @@ -5,5 +5,11 @@ (* Written by: Emilio J. Gallego Arias *) (************************************************************************) +(* Contents utils, should be moved to Contents.t , they mainly handle character + enconding conversiong between protocol and prover positions, if needed *) + val get_id_at_point : contents:Fleche.Contents.t -> point:int * int -> string option + +val get_char_at_point : + contents:Fleche.Contents.t -> point:int * int -> char option diff --git a/controller/rq_completion.ml b/controller/rq_completion.ml index dd7e1243..62a8519e 100644 --- a/controller/rq_completion.ml +++ b/controller/rq_completion.ml @@ -70,31 +70,11 @@ let unicode_list point : Yojson.Safe.t list = (* Coq's CList.map is tail-recursive *) CList.map (mk_unicode_completion_item point) ulist -let validate_line ~(doc : Fleche.Doc.t) ~line = - if Array.length doc.contents.lines > line then - Some (Array.get doc.contents.lines line) - else None - -(* This returns a byte-based char offset for the line *) -let validate_position ~doc ~point = - let line, char = point in - Option.bind (validate_line ~doc ~line) (fun line -> - let char = Coq.Utf8.get_byte_offset_from_utf16_pos line char in - Option.bind char (fun index -> Some (String.get line index))) - -let get_char_at_point ~(doc : Fleche.Doc.t) ~point = - let line, char = point in - if char >= 1 then - let point = (line, char - 1) in - validate_position ~doc ~point - else (* Can't get previous char *) - None - -(* point is a utf char! *) -let completion ~token:_ ~doc ~point = +let completion ~token:_ ~(doc : Fleche.Doc.t) ~point = (* Instead of get_char_at_point we should have a CompletionContext.t, to be addressed in further completion PRs *) - (match get_char_at_point ~doc ~point with + let contents = doc.contents in + (match Rq_common.get_char_at_point ~contents ~point with | None -> let incomplete = true in let items = [] in diff --git a/controller/rq_definition.ml b/controller/rq_definition.ml index 8b29e668..fe7d28cc 100644 --- a/controller/rq_definition.ml +++ b/controller/rq_definition.ml @@ -11,8 +11,9 @@ let request ~token:_ ~(doc : Fleche.Doc.t) ~point = (fun id_at_point -> let { Fleche.Doc.toc; _ } = doc in match CString.Map.find_opt id_at_point toc with - | Some range -> + | Some node -> let uri = doc.uri in + let range = node.range in Lsp.Core.Location.({ uri; range } |> to_yojson) | None -> `Null) `Null diff --git a/controller/rq_hover.ml b/controller/rq_hover.ml index 174a89fd..28b4fd9a 100644 --- a/controller/rq_hover.ml +++ b/controller/rq_hover.ml @@ -238,7 +238,7 @@ end (* Register in-file hover plugins *) let () = List.iter Register.add [ Loc_info.h; Stats.h; Type.h; Notation.h ] -let hover ~token ~doc ~point = +let hover ~token ~(doc : Fleche.Doc.t) ~point = let node = Info.LC.node ~doc ~point Exact in let range = Option.map Doc.Node.range node in let hovers = Register.fire ~token ~doc ~point ~node in diff --git a/controller/rq_init.ml b/controller/rq_init.ml index d0f5f606..d99a4db6 100644 --- a/controller/rq_init.ml +++ b/controller/rq_init.ml @@ -24,9 +24,9 @@ let odict_field name dict = [] (* Request Handling: The client expects a reply *) -let do_client_options coq_lsp_options : unit = - LIO.trace "init" "custom client options:"; - LIO.trace_object "init" (`Assoc coq_lsp_options); +let do_settings coq_lsp_options : unit = + LIO.trace "settings" "setting server options:"; + LIO.trace_object "settings" (`Assoc coq_lsp_options); match Lsp.JFleche.Config.of_yojson (`Assoc coq_lsp_options) with | Ok v -> Fleche.Config.v := v | Error msg -> LIO.trace "CoqLspOption.of_yojson error: " msg @@ -109,8 +109,8 @@ let do_initialize ~params = let dir = determine_workspace_root ~params in let trace = get_trace ~params in LIO.set_trace_value trace; - let coq_lsp_options = odict_field "initializationOptions" params in - do_client_options coq_lsp_options; + let coq_lsp_settings = odict_field "initializationOptions" params in + do_settings coq_lsp_settings; check_client_version !Fleche.Config.v.client_version; let client_capabilities = odict_field "capabilities" params in if Fleche.Debug.lsp_init then ( diff --git a/controller/rq_init.mli b/controller/rq_init.mli index 39909178..c4a424c5 100644 --- a/controller/rq_init.mli +++ b/controller/rq_init.mli @@ -5,6 +5,9 @@ (* Written by: Emilio J. Gallego Arias *) (************************************************************************) +(** Setups the server configuration, takes the list of settings as a JSON dict *) +val do_settings : (string * Yojson.Safe.t) list -> unit + (** Returns answer request + workspace root directory *) val do_initialize : params:(string * Yojson.Safe.t) list -> Yojson.Safe.t * string list diff --git a/coq-lsp.opam b/coq-lsp.opam index bd34db8c..80b6ea0f 100644 --- a/coq-lsp.opam +++ b/coq-lsp.opam @@ -40,6 +40,8 @@ depends: [ "coq-serapi" { >= "8.17.0+0.17.2" < "8.18" } ] +depopts: ["lwt" "logs"] + build: [ [ "rm" "-rf" "vendor" ] [ "dune" "build" "-p" name "-j" jobs ] diff --git a/coq/args.ml b/coq/args.ml index 2eec75ac..d9d5a56a 100644 --- a/coq/args.ml +++ b/coq/args.ml @@ -84,8 +84,22 @@ let ri_from : (string option * string) list Term.t = & info [ "rifrom"; "require-import-from" ] ~docv:"FROM,LIBRARY" ~doc)) let int_backend = - let doc = "Select Interruption Backend" in + let doc = + "Select Interruption Backend, if absent, the best available for your OCaml \ + version will be selected" + in Arg.( value - & opt (enum [ ("Coq", Limits.Coq); ("Mp", Limits.Mp) ]) Limits.Coq + & opt (enum [ ("Coq", Some Limits.Coq); ("Mp", Some Limits.Mp) ]) None & info [ "int_backend" ] ~docv:"INT_BACKEND" ~doc) + +let roots : string list Term.t = + let doc = "Workspace(s) root(s)" in + Arg.(value & opt_all string [] & info [ "root" ] ~docv:"ROOTS" ~doc) + +let coq_diags_level : int Term.t = + let doc = + "Controsl whether Coq Info and Notice message appear in diagnostics.\n\ + \ 0 = None; 1 = Notices, 2 = Notices and Info" + in + Arg.(value & opt int 0 & info [ "diags_level" ] ~docv:"DIAGS_LEVEL" ~doc) diff --git a/coq/args.mli b/coq/args.mli index 58d68a63..0181d2e8 100644 --- a/coq/args.mli +++ b/coq/args.mli @@ -16,4 +16,6 @@ val debug : Bool.t Term.t val bt : Bool.t Term.t val ml_include_path : string list Term.t val ri_from : (string option * string) list Term.t -val int_backend : Limits.backend Term.t +val int_backend : Limits.backend option Term.t +val roots : string list Term.t +val coq_diags_level : int Term.t diff --git a/coq/ast.ml b/coq/ast.ml index 7491e6ec..ab8f8254 100644 --- a/coq/ast.ml +++ b/coq/ast.ml @@ -61,6 +61,51 @@ module Require = struct | _ -> None end +module Meta = struct + type ast = t + + open Ppx_hash_lib.Std.Hash.Builtin + open Ppx_compare_lib.Builtin + module Loc = Serlib.Ser_loc + module Names = Serlib.Ser_names + module Attributes = Serlib.Ser_attributes + module Vernacexpr = Serlib.Ser_vernacexpr + + module Command = struct + type t = + | Back of int + | ResetName of Names.lident + | ResetInitial + [@@deriving hash, compare] + end + + type t = + { command : Command.t + ; loc : Loc.t option + ; attrs : Attributes.vernac_flag list + ; control : Vernacexpr.control_flag list + } + [@@deriving hash, compare] + + (* EJGA: Coq classification puts these commands as pure? Seems like yet + another bug... *) + let extract : ast -> t option = + CAst.with_loc_val (fun ?loc -> function + | { Vernacexpr.expr = Vernacexpr.(VernacResetName id) + ; control + ; attrs + } -> + let command = Command.ResetName id in + Some { command; loc; attrs; control } + | { expr = VernacResetInitial; control; attrs } -> + let command = Command.ResetInitial in + Some { command; loc; attrs; control } + | { expr = (VernacBack num); control; attrs } -> + let command = Command.Back num in + Some { command; loc; attrs; control } + | _ -> None) +end + module Kinds = struct (* LSP kinds *) let _file = 1 diff --git a/coq/ast.mli b/coq/ast.mli index 9a79710a..412d4721 100644 --- a/coq/ast.mli +++ b/coq/ast.mli @@ -32,6 +32,28 @@ module Require : sig val extract : ast -> t option end +module Meta : sig + type ast = t + + module Command : sig + type t = + | Back of int + | ResetName of Names.lident + | ResetInitial + end + + type t = + { command : Command.t + ; loc : Loc.t option + ; attrs : Attributes.vernac_flag list + ; control : Vernacexpr.control_flag list + } + [@@deriving hash, compare] + + (** Determine if we are under a meta-command *) + val extract : ast -> t option +end + (** [make_info ~st ast] Compute info about a possible definition in [ast], we need [~st] to compute the type. *) val make_info : diff --git a/compiler/util.ml b/coq/compat.ml similarity index 87% rename from compiler/util.ml rename to coq/compat.ml index 31745eb1..ea4561c3 100644 --- a/compiler/util.ml +++ b/coq/compat.ml @@ -1,3 +1,5 @@ +(* Compatibility file *) + module Ocaml_414 = struct module In_channel = struct (* 4.14 can do this: In_channel.with_open_bin file In_channel.input_all, so @@ -8,6 +10,7 @@ module Ocaml_414 = struct Fun.protect ~finally:(fun () -> Stdlib.close_in_noerr ic) (fun () -> f ic) let with_open_bin s f = with_open Stdlib.open_in_bin s f + let with_open_text s f = with_open Stdlib.open_in s f (* Read up to [len] bytes into [buf], starting at [ofs]. Return total bytes read. *) @@ -95,9 +98,22 @@ module Ocaml_414 = struct end end -let input_all file = - let open Ocaml_414 in - In_channel.with_open_bin file In_channel.input_all +module Result = struct + include Result + + module O = struct + let ( let+ ) r f = map f r + let ( let* ) r f = bind r f + end + + let split = function + | Ok (x1, x2) -> (Ok x1, Ok x2) + | Error err -> (Error err, Error err) + + let pp pp_r pp_e fmt = function + | Ok r -> Format.fprintf fmt "@[Ok: @[%a@]@]" pp_r r + | Error e -> Format.fprintf fmt "@[Error: @[%a@]@]" pp_e e +end let format_to_file ~file ~f x = let open Ocaml_414 in diff --git a/coq/compat.mli b/coq/compat.mli new file mode 100644 index 00000000..fc56a00c --- /dev/null +++ b/coq/compat.mli @@ -0,0 +1,37 @@ +(* Compatiblity and general utils *) + +(* We should at some point remove all of this file in favor of a standard + library that suits our needs *) +module Ocaml_414 : sig + module In_channel : sig + val with_open_bin : string -> (in_channel -> 'a) -> 'a + val with_open_text : string -> (in_channel -> 'a) -> 'a + val input_all : in_channel -> string + end + + module Out_channel : sig + val with_open : ('a -> out_channel) -> 'a -> (out_channel -> 'b) -> 'b + val with_open_bin : string -> (out_channel -> 'a) -> 'a + end +end + +val format_to_file : + file:string -> f:(Format.formatter -> 'a -> unit) -> 'a -> unit + +module Result : sig + include module type of Result + + module O : sig + val ( let+ ) : ('a, 'l) t -> ('a -> 'b) -> ('b, 'l) t + val ( let* ) : ('a, 'l) t -> ('a -> ('b, 'l) t) -> ('b, 'l) t + end + + val split : ('a * 'b, 'e) t -> ('a, 'e) t * ('b, 'e) t + + val pp : + (Format.formatter -> 'r -> unit) + -> (Format.formatter -> 'e -> unit) + -> Format.formatter + -> ('r, 'e) Result.t + -> unit +end diff --git a/coq/dune b/coq/dune index 15e19a97..7d954f4c 100644 --- a/coq/dune +++ b/coq/dune @@ -1,11 +1,8 @@ (library (name coq) (public_name coq-lsp.coq) - ; Unfortunate we have to link the STM due to the LTAC plugin - ; depending on it, we should fix this upstream - (inline_tests) (preprocess - (pps ppx_compare ppx_hash ppx_inline_test)) + (pps ppx_compare ppx_hash)) (libraries (select limits_mp_impl.ml diff --git a/coq/glob.ml b/coq/glob.ml new file mode 100644 index 00000000..6c9eb714 --- /dev/null +++ b/coq/glob.ml @@ -0,0 +1,190 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* "Ill-formed file: " ^ s + | Outdated -> "Outdated .glob file" +end + +module Info = struct + type t = + { kind : string + ; offset : int * int + } +end + +(* This is taken from coqdoc/glob_file.ml , we should share this code, but no + cycles ATM *) +module Coq = struct + module Entry_type = struct + type t = + | Library + | Module + | Definition + | Inductive + | Constructor + | Lemma + | Record + | Projection + | Instance + | Class + | Method + | Variable + | Axiom + | TacticDefinition + | Abbreviation + | Notation + | Section + | Binder + + let of_string = function + | "def" + | "coe" + | "subclass" + | "canonstruc" + | "fix" + | "cofix" + | "ex" + | "scheme" -> Definition + | "prf" | "thm" -> Lemma + | "ind" | "variant" | "coind" -> Inductive + | "constr" -> Constructor + | "indrec" | "rec" | "corec" -> Record + | "proj" -> Projection + | "class" -> Class + | "meth" -> Method + | "inst" -> Instance + | "var" -> Variable + | "defax" | "prfax" | "ax" -> Axiom + | "abbrev" | "syndef" -> Abbreviation + | "not" -> Notation + | "lib" -> Library + | "mod" | "modtype" -> Module + | "tac" -> TacticDefinition + | "sec" -> Section + | "binder" -> Binder + | s -> invalid_arg ("type_of_string:" ^ s) + end + + let read_dp ic = + let line = input_line ic in + let n = String.length line in + match line.[0] with + | 'F' -> + let lib_name = String.sub line 1 (n - 1) in + Ok lib_name + | _ -> Error (Error.Ill_formed "lib name not found in header") + + let correct_file vfile ic = + let s = input_line ic in + if String.length s < 7 || String.sub s 0 7 <> "DIGEST " then + Error (Error.Ill_formed "DIGEST ill-formed") + else + let s = String.sub s 7 (String.length s - 7) in + match (vfile, s) with + | None, "NO" -> read_dp ic + | Some _, "NO" -> Error (Ill_formed "coming from .v file but no digest") + | None, _ -> Error (Ill_formed "digest but .v source file not available") + | Some vfile, s -> + if s = Digest.to_hex (Digest.file vfile) then + (* XXX Read F line *) + read_dp ic + else Error Outdated + + let parse_ref line = + try + (* Disable for now *) + if false then + let add_ref _ _ _ _ _ = () in + Scanf.sscanf line "R%d:%d %s %s %s %s" (fun loc1 loc2 lib_dp sp id ty -> + for loc = loc1 to loc2 do + add_ref loc lib_dp sp id (Entry_type.of_string ty); + (* Also add an entry for each module mentioned in [lib_dp], * to + use in interpolation. *) + ignore + (List.fold_right + (fun thisPiece priorPieces -> + let newPieces = + match priorPieces with + | "" -> thisPiece + | _ -> thisPiece ^ "." ^ priorPieces + in + add_ref loc "" "" newPieces Entry_type.Library; + newPieces) + (Str.split (Str.regexp_string ".") lib_dp) + "") + done) + with _ -> () + + let parse_def line : _ Result.t = + try + Scanf.sscanf line "%s %d:%d %s %s" + (fun kind loc1 loc2 section_path name -> + Ok (name, section_path, kind, (loc1, loc2))) + with Scanf.Scan_failure err -> Error err + + let process_line dp map line = + match line.[0] with + | 'R' -> + let _reference = parse_ref line in + map + | _ -> ( + match parse_def line with + | Error _ -> map + | Ok (name, section_path, kind, offset) -> + let section_path = + if String.equal "<>" section_path then "" else section_path ^ "." + in + let name = dp ^ "." ^ section_path ^ name in + let info = { Info.kind; offset } in + DefMap.add name info map) + + let read_glob vfile inc = + match correct_file vfile inc with + | Error e -> Error (Error.to_string e) + | Ok dp -> ( + let map = ref DefMap.empty in + try + while true do + let line = input_line inc in + let n = String.length line in + if n > 0 then map := process_line dp !map line + done; + assert false + with End_of_file -> Ok !map) +end + +(* Glob file that was read and parsed successfully *) +type t = Info.t DefMap.t + +let open_file file = + if Sys.file_exists file then + let vfile = Filename.remove_extension file ^ ".v" in + Compat.Ocaml_414.In_channel.with_open_text file (Coq.read_glob (Some vfile)) + else Error (Format.asprintf "Cannot open file: %s" file) + +let get_info map name = + match DefMap.find_opt name map with + | Some info -> Ok info + | None -> Error (Format.asprintf "definition %s not found in glob table" name) diff --git a/coq/glob.mli b/coq/glob.mli new file mode 100644 index 00000000..83376443 --- /dev/null +++ b/coq/glob.mli @@ -0,0 +1,30 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* (t, string) Result.t + +module Info : sig + type t = + { kind : string + ; offset : int * int + } +end + +val get_info : t -> string -> (Info.t, string) Result.t diff --git a/coq/goals.ml b/coq/goals.ml index f0855ad8..9b6b7b4e 100644 --- a/coq/goals.ml +++ b/coq/goals.ml @@ -50,9 +50,10 @@ type ('a, 'pp) goals = ; given_up : 'a list } -let map_goals ~f { goals; stack; bullet; shelf; given_up } = +let map_goals ~f ~g { goals; stack; bullet; shelf; given_up } = let goals = List.map f goals in let stack = List.map (fun (s, r) -> (List.map f s, List.map f r)) stack in + let bullet = Option.map g bullet in let shelf = List.map f shelf in let given_up = List.map f given_up in { goals; stack; bullet; shelf; given_up } diff --git a/coq/goals.mli b/coq/goals.mli index 8614594c..5dc5e616 100644 --- a/coq/goals.mli +++ b/coq/goals.mli @@ -42,7 +42,8 @@ type ('a, 'pp) goals = ; given_up : 'a list } -val map_goals : f:('a -> 'b) -> ('a, 'pp) goals -> ('b, 'pp) goals +val map_goals : + f:('a -> 'b) -> g:('pp -> 'pp') -> ('a, 'pp) goals -> ('b, 'pp') goals type 'pp reified_pp = ('pp reified_goal, 'pp) goals diff --git a/coq/library_file.ml b/coq/library_file.ml new file mode 100644 index 00000000..b0c8c347 --- /dev/null +++ b/coq/library_file.ml @@ -0,0 +1,139 @@ +type t = Names.DirPath.t + +let name n = n +let loaded ~token ~st = State.in_state ~token ~st ~f:Library.loaded_libraries () + +(* Function to extract definitions and lemmas from the environment *) +module DynHandle = Libobject.Dyn.Map (struct + type 'a t = 'a -> unit +end) + +(* Prefix is the module / section things are defined *) +let const_handler + (fn : Names.Constant.t -> Decls.logical_kind -> Constr.t -> unit) prefix + (id, obj) = + let open Names in + let kn = KerName.make prefix.Nametab.obj_mp (Label.of_id id) in + let cst = Global.constant_of_delta_kn kn in + let gr = GlobRef.ConstRef cst in + let env = Global.env () in + let typ, _ = Typeops.type_of_global_in_context env gr in + let kind = Declare.Internal.Constant.kind obj in + fn cst kind typ + +let iter_constructors indsp u fn env nconstr = + for i = 1 to nconstr do + let typ = + Inductive.type_of_constructor + ((indsp, i), u) + (Inductive.lookup_mind_specif env indsp) + in + fn (Names.GlobRef.ConstructRef (indsp, i)) typ + done + +let ind_handler fn prefix (id, (_obj : DeclareInd.Internal.inductive_obj)) = + let open Names in + let kn = KerName.make prefix.Nametab.obj_mp (Label.of_id id) in + let mind = Global.mind_of_delta_kn kn in + let mib = Global.lookup_mind mind in + let env = Global.env () in + let iter_packet i mip = + let ind = (mind, i) in + let u = + Univ.make_abstract_instance (Declareops.inductive_polymorphic_context mib) + in + let typ = + Inductive.type_of_inductive (Inductive.lookup_mind_specif env ind, u) + in + let () = fn (GlobRef.IndRef ind) typ in + let len = Array.length mip.Declarations.mind_user_lc in + iter_constructors ind u fn env len + in + Array.iteri iter_packet mib.mind_packets + +let handler fn_c fn_i prefix = + DynHandle.add Declare.Internal.Constant.tag (const_handler fn_c prefix) + @@ DynHandle.add DeclareInd.Internal.objInductive (ind_handler fn_i prefix) + @@ DynHandle.empty + +let handle h (Libobject.Dyn.Dyn (tag, o)) = + match DynHandle.find tag h with + | f -> f o + | exception Stdlib.Not_found -> () + +let obj_action fn_c fn_i prefix lobj = + match lobj with + | Libobject.AtomicObject o -> handle (handler fn_c fn_i prefix) o + | _ -> () + +let constructor_name c idx = + let cname = + Nametab.shortest_qualid_of_global Names.Id.Set.empty + (Names.GlobRef.ConstructRef (c, idx)) + in + Libnames.string_of_qualid cname + +let constructor_info (gref : Names.GlobRef.t) = + match gref with + | ConstructRef (ind, idx) -> + let ind_dp = Names.(MutInd.modpath (fst ind) |> ModPath.dp) in + Some (ind_dp, constructor_name ind idx) + | VarRef _ | ConstRef _ | IndRef _ -> None + +let belongs_to_lib dps dp = + List.exists (fun p -> Libnames.is_dirpath_prefix_of p dp) dps + +module Entry = struct + type t = + { name : string + ; typ : Constr.t + ; file : string + } +end + +let to_result ~f x = + try Ok (f x) + with exn when CErrors.noncritical exn -> + let iexn = Exninfo.capture exn in + Error iexn + +let try_locate_absolute_library dir = + let f = Loadpath.try_locate_absolute_library in + to_result ~f dir + +let find_v_file dir = + match try_locate_absolute_library dir with + (* EJGA: we want to improve this as to pass the error to the client *) + | Error _ -> "error when trying to locate the .v file" + | Ok file -> file + +let toc dps : Entry.t list = + let res : Entry.t list ref = ref [] in + let obj_action = + let fn_c (cst : Names.Constant.t) (_ : Decls.logical_kind) (typ : Constr.t) + = + let cst_dp = Names.(Constant.modpath cst |> ModPath.dp) in + if belongs_to_lib dps cst_dp then + (* let () = F.eprintf "cst found: %s@\n%!" (Names.Constant.to_string + cst) in *) + let name = Names.Constant.to_string cst in + let file = find_v_file cst_dp in + res := { name; typ; file } :: !res + else () + in + (* We do nothing for inductives, note this is called both on constructors + and inductives, with the name and type *) + let fn_i (gref : Names.GlobRef.t) (typ : Constr.t) = + match constructor_info gref with + | None -> () + | Some (ind_dp, name) -> + if belongs_to_lib dps ind_dp then + let file = find_v_file ind_dp in + res := { name; typ; file } :: !res + in + obj_action fn_c fn_i + in + let () = Declaremods.iter_all_segments obj_action in + List.rev !res + +let toc ~token ~st dps = State.in_state ~token ~st ~f:toc dps diff --git a/coq/library_file.mli b/coq/library_file.mli new file mode 100644 index 00000000..a93fd482 --- /dev/null +++ b/coq/library_file.mli @@ -0,0 +1,38 @@ +(* API to handle vo libraries, we cannot use Library as module name due to Coq's + libs not being wrapped... *) + +(* Library stored in a .vo file, it can contain several modules *) +type t + +(** Logical path of the library *) +val name : t -> Names.DirPath.t + +module Entry : sig + type t = + { name : string + ; typ : Constr.t + ; file : string + } +end + +(** [toc libs] Returns the list of constants and inductives found on .vo + libraries [libs], as pairs of [name, typ]. Note that the constants are + returned in the order they appear on the file. + + NOTE that (unfortunately) this is a very expensive process, similary to + Coq's Search, as this routine will have to traverse all the library objects + in scope. + + Hence, we provide a slightly more efficient version that can do multiple + libraries but with the same complexity. + + There have been several upstream Coq PRs trying to improve this situation, + but so far they didn't make enough progress. *) +val toc : + token:Limits.Token.t + -> st:State.t + -> t list + -> (Entry.t list, Loc.t) Protect.E.t + +(** Recovers the list of loaded libraries for state [st] *) +val loaded : token:Limits.Token.t -> st:State.t -> (t list, Loc.t) Protect.E.t diff --git a/coq/limits.ml b/coq/limits.ml index a6855c6d..847962ba 100644 --- a/coq/limits.ml +++ b/coq/limits.ml @@ -10,7 +10,7 @@ module type Intf = sig val start : unit -> unit val limit : token:Token.t -> f:('a -> 'b) -> 'a -> ('b, exn) Result.t - val name : string + val name : unit -> string val available : bool end @@ -41,7 +41,7 @@ module Coq : Intf = struct let () = Control.interrupt := false in try Ok (f x) with Sys.Break -> Error Sys.Break - let name = "Control.interrupt" + let name () = "Control.interrupt" let available = true end @@ -57,6 +57,18 @@ let select = function | Coq -> backend := (module Coq) | Mp -> backend := (module Mp) +(* Set this to false for 8.19 and lower *) +let sane_coq_base_version = true + +let sane_coq_branch = + CString.string_contains ~where:Coq_config.version ~what:"+lsp" + +let safe_coq = sane_coq_base_version || sane_coq_branch + +let select_best = function + | None -> if Mp.available && safe_coq then select Mp else select Coq + | Some backend -> select backend + module Token = struct type t = | C of Coq.Token.t @@ -65,7 +77,7 @@ module Token = struct let create () = let module M = (val !backend) in - match M.name with + match M.name () with | "memprof-limits" -> M (Mp.Token.create ()) | "Control.interrupt" | _ -> C (Coq.Token.create ()) @@ -95,5 +107,8 @@ let limit ~token ~f x = let () = Control.interrupt := false in Ok (f x) -let name = "select backend" +let name () = + let module M = (val !backend) in + M.name () + let available = true diff --git a/coq/limits.mli b/coq/limits.mli index 631b4c3a..b5886c4c 100644 --- a/coq/limits.mli +++ b/coq/limits.mli @@ -10,7 +10,7 @@ module type Intf = sig val start : unit -> unit val limit : token:Token.t -> f:('a -> 'b) -> 'a -> ('b, exn) Result.t - val name : string + val name : unit -> string val available : bool end @@ -25,4 +25,7 @@ type backend = (** *Must* be called *only* once *) val select : backend -> unit +(** If [None] will pick the best backend, must be called only once *) +val select_best : backend option -> unit + val create_atomic : unit -> Token.t diff --git a/coq/limits_mp_impl.fake.ml b/coq/limits_mp_impl.fake.ml index 7baeca46..386991fb 100644 --- a/coq/limits_mp_impl.fake.ml +++ b/coq/limits_mp_impl.fake.ml @@ -9,5 +9,5 @@ end let start () = () let limit ~token:_ ~f x = Result.Ok (f x) -let name = "memprof-limits" +let name () = "memprof-limits (fake)" let available = false diff --git a/coq/limits_mp_impl.real.ml b/coq/limits_mp_impl.real.ml index d5c4801f..a3a162ea 100644 --- a/coq/limits_mp_impl.real.ml +++ b/coq/limits_mp_impl.real.ml @@ -7,5 +7,5 @@ let limit ~token ~f x = let f () = f x in Memprof_limits.limit_with_token ~token f -let name = "memprof-limits" +let name () = "memprof-limits" let available = true diff --git a/coq/loader.ml b/coq/loader.ml index e9af4464..9dc1503e 100644 --- a/coq/loader.ml +++ b/coq/loader.ml @@ -38,6 +38,7 @@ let check_package_exists fl_pkg = let map_serlib fl_pkg = let supported = match fl_pkg with (* Supported by serlib *) (* directory *) + | "coq-core.plugins.btauto" (* btauto *) | "coq-core.plugins.cc" (* cc *) | "coq-core.plugins.extraction" (* extraction *) | "coq-core.plugins.firstorder" (* firstorder *) @@ -45,6 +46,7 @@ let map_serlib fl_pkg = | "coq-core.plugins.ltac" (* ltac *) | "coq-core.plugins.ltac2" (* ltac2 *) | "coq-core.plugins.micromega" (* micromega *) + | "coq-core.plugins.micromega_core" (* micromega_core *) | "coq-core.plugins.ring" (* ring *) | "coq-core.plugins.ssreflect" (* ssreflect *) | "coq-core.plugins.ssrmatching" (* ssrmatching *) diff --git a/coq/protect.ml b/coq/protect.ml index 284ce801..75313251 100644 --- a/coq/protect.ml +++ b/coq/protect.ml @@ -82,6 +82,7 @@ module E = struct { r; feedback = feedback @ fb2 } let ok v = { r = Completed (Ok v); feedback = [] } + let error err = { r = R.error err; feedback = [] } module O = struct let ( let+ ) x f = map ~f x diff --git a/coq/protect.mli b/coq/protect.mli index ee262dfe..c0c2fe73 100644 --- a/coq/protect.mli +++ b/coq/protect.mli @@ -39,6 +39,7 @@ module E : sig val map_loc : f:('l -> 'm) -> ('a, 'l) t -> ('a, 'm) t val bind : f:('a -> ('b, 'l) t) -> ('a, 'l) t -> ('b, 'l) t val ok : 'a -> ('a, 'l) t + val error : Pp.t -> ('a, 'l) t module O : sig val ( let+ ) : ('a, 'l) t -> ('a -> 'b) -> ('b, 'l) t diff --git a/coq/utf8.mli b/coq/utf8.mli deleted file mode 100644 index 2c66e66e..00000000 --- a/coq/utf8.mli +++ /dev/null @@ -1,52 +0,0 @@ -(* Copyright (C) 2002, 2003 Yamagata Yoriyuki. *) - -(* This library is free software; you can redistribute it and/or *) -(* modify it under the terms of the GNU Lesser General Public License *) -(* as published by the Free Software Foundation; either version 2 of *) -(* the License, or (at your option) any later version. *) - -(* As a special exception to the GNU Library General Public License, you *) -(* may link, statically or dynamically, a "work that uses this library" *) -(* with a publicly distributed version of this library to produce an *) -(* executable file containing portions of this library, and distribute *) -(* that executable file under terms of your choice, without any of the *) -(* additional requirements listed in clause 6 of the GNU Library General *) -(* Public License. By "a publicly distributed version of this library", *) -(* we mean either the unmodified Library as distributed by the authors, *) -(* or a modified version of this library that is distributed under the *) -(* conditions defined in clause 3 of the GNU Library General Public *) -(* License. This exception does not however invalidate any other reasons *) -(* why the executable file might be covered by the GNU Library General *) -(* Public License . *) - -(* This library is distributed in the hope that it will be useful, *) -(* but WITHOUT ANY WARRANTY; without even the implied warranty of *) -(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU *) -(* Lesser General Public License for more details. *) - -(* You should have received a copy of the GNU Lesser General Public *) -(* License along with this library; if not, write to the Free Software *) -(* Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 *) -(* USA *) - -(* Taken from camomille *) - -(* utf8 utils, both Coq and Camomile have similar implementations, at some point - we should remove this but for now we keep it internal. For now we use the - Camomille functions *) - -type char = int -type index = int - -(** Byte index to UTF-8 character position *) -val char_of_index : line:string -> byte:index -> char option - -(** UTF-8 Char to byte index position *) -val index_of_char : line:string -> char:char -> index option - -(** Lenght in utf-8 chars *) -val length : string -> char - -(** Get the byte potition of a code point indexed in UTF-16 code units in a - UTF-8 encoded string. *) -val get_byte_offset_from_utf16_pos : string -> int -> int option diff --git a/coq/utils.ml b/coq/utils.ml index 53331257..12caf7c3 100644 --- a/coq/utils.ml +++ b/coq/utils.ml @@ -16,12 +16,10 @@ (* We convert in case of failure to some default values *) -let char_of_index ~lines ~line ~byte = +let utf16_offset_of_utf8_offset ~lines ~line ~byte = if line < Array.length lines then let line = Array.get lines line in - match Utf8.char_of_index ~line ~byte with - | Some char -> char - | None -> Utf8.length line + Lang.Utf.utf16_offset_of_utf8_offset ~line ~offset:byte else 0 let to_range ~lines (p : Loc.t) : Lang.Range.t = @@ -34,8 +32,12 @@ let to_range ~lines (p : Loc.t) : Lang.Range.t = let start_col = bp - bol_pos in let end_col = ep - bol_pos_last in - let start_col = char_of_index ~lines ~line:start_line ~byte:start_col in - let end_col = char_of_index ~lines ~line:end_line ~byte:end_col in + let start_col = + utf16_offset_of_utf8_offset ~lines ~line:start_line ~byte:start_col + in + let end_col = + utf16_offset_of_utf8_offset ~lines ~line:end_line ~byte:end_col + in Lang.Range. { start = { line = start_line; character = start_col; offset = bp } ; end_ = { line = end_line; character = end_col; offset = ep } diff --git a/coq/workspace.ml b/coq/workspace.ml index e9aca9f4..649f8502 100644 --- a/coq/workspace.ml +++ b/coq/workspace.ml @@ -272,6 +272,11 @@ let load_objs libs = in List.(iter rq_file (rev libs)) +let fleche_chop_extension basename = + match Filename.chop_suffix_opt ~suffix:".v.tex" basename with + | Some file -> file + | None -> Filename.chop_extension basename + (* We need to compute this with the right load path *) let dirpath_of_uri ~uri = let f = Lang.LUri.File.to_string_file uri in @@ -282,7 +287,7 @@ let dirpath_of_uri ~uri = with Not_found -> Libnames.default_root_prefix in let f = - try Filename.chop_extension (Filename.basename f) + try fleche_chop_extension (Filename.basename f) with Invalid_argument _ -> f in let id = Names.Id.of_string f in diff --git a/editor/code/CHANGELOG.md b/editor/code/CHANGELOG.md index b5eee4a5..1396f16b 100644 --- a/editor/code/CHANGELOG.md +++ b/editor/code/CHANGELOG.md @@ -1,3 +1,87 @@ +# coq-lsp 0.1.9: Hasta el 40 de Mayo... +--------------------------------------- + + - new configuration value `check_only_on_request` which will delay + checking the document until a request has been made. This means + users can now switch between continuous and on-demand modes. (#629, + cc: #24, @ejgallego) + - display the continous/on-request checking mode in the status bar, + allow to change it by clicking on it (@ejgallego, #721) + - new Coq Language Status Item that display server status, version, + and memory use. We recommend the users to pin it. + - new heatmap feature allowing timing data to be seen in the + editor. use the `Coq LSP: Toggle heatmap` command. Colors and + granularity are configurable, see settings (@Alizter, #686) + - new VSCode commands to allow to move one sentence backwards / + forward, this is particularly useful when combined with lazy + checking mode (@ejgallego, #671, fixes #263, fixes #580) + - VSCode commands `coq-lsp.sentenceNext` / `coq-lsp.sentencePrevious` + are now bound by default to `Alt + N` / `Alt + P` keybindings + (@ejgallego, #718) + - new option `show_loc_info_on_hover` that will display parsing debug + information on hover + - fix activation bug that prevented extension activation for `.mv` + files (@ejgallego @r3m0t, #598, cc #596, reported by Théo Zimmerman) + - require VSCode >= 1.82 in package.json. (@ejgallego, #599, + thanks to Théo Zimmerman for the report) + - update progress indicator correctly on End Of File (@ejgallego, + #605, fixes #445) + - switch default of `goal_after_tactic` to `true` (@Alizter, + @ejgallego, cc: #614) + - error recovery: Recognize `Defined` and `Admitted` in lex recovery + (@ejgallego, #616) + - don't trigger the goals window in general markdown buffer + (@ejgallego, #625, reported by Théo Zimmerman) + - fix typo on package.json configuration section (@ejgallego, #645) + - support for Coq 8.16 has been abandoned due to lack of dev + resources (@ejgallego, #649) + - new "Coq LSP: Free Memory" command to liberate space used in the + cache (@ejgallego, #662, fixes #367 cc: #253 #236 #348) + - fix Coq performance view display panel (@ejgallego, #663, + regression in #513) + - new public VSCode extension API so other extensions can perform + actions when the user request the goals (@ejgallego, @bhaktishh, + #672, fixes #538) + - Support Visual Studio Live Share URIs better (`vsls://`), in + particular don't try to display goals if the URI is VSLS one + (@ejgallego, #676) + - Send performance performance data for the full document + (@ejgallego, @Alizter, #689, #693) + - New client option to enable / disable `coq/perfData` (@ejgallego, #717) + - The `coq-lsp.document` VSCode command will now display the returned + JSON data in a new editor (@ejgallego, #701) + - Update server settings on the fly when tweaking them in VSCode. + Implement `workspace/didChangeConfiguration` (@ejgallego, #702) + - Always dispose UI elements. This should improve some strange + behaviors on extension restart (@ejgallego, #708) + - Support Coq meta-commands (Reset, Reset Initial, Back) They are + actually pretty useful to hint the incremental engine to ignore + changes in some part of the document (@ejgallego, #709) + - New `coq/viewRange` notification, from client to server, than hints + the scheduler for the visible area of the document; combined with + the new lazy checking mode, this provides checking on scroll, a + feature inspired from Isabelle IDE (@ejgallego, #717) + - Have VSCode wait for full LSP client shutdown on server + restart. This fixes some bugs on extension restart (finally!) + (@ejgallego, #719) + - Center the view if cursor goes out of scope in + `sentenceNext/sentencePrevious` (@ejgallego, #718) + - Switch Flèche range encoding to protocol native, this means UTF-16 + code points for now (Léo Stefanesco, @ejgallego, #624, fixes #620, + #621) + - Give `Goals` panel focus back if it has lost it (in case of + multiple panels in the second viewColumn of Vscode) whenever + user navigates proofs (@Alidra @ejgallego, #722, #725) + - Add an example of multiple workspaces (@ejgallego, @Blaisorblade, + #611) + - Don't show types of un-expanded goals. We should add an option for + this, but we don't have the cycles (@ejgallego, #730, workarounds + #525 #652) + - Support for `.lv / .v.tex` TeX files with embedded Coq code + (@ejgallego, #727) + - Don't expand bullet goals at previous levels by default + (@ejgallego, @Alizter, #731 cc #525) + # coq-lsp 0.1.8: Trick-or-treat ------------------------------- diff --git a/editor/code/lib/types.ts b/editor/code/lib/types.ts index 2de1f115..1e196f07 100644 --- a/editor/code/lib/types.ts +++ b/editor/code/lib/types.ts @@ -31,6 +31,7 @@ export interface Message { export type Id = ["Id", string]; +// XXX: Only used in obligations, move them to Range export interface Loc { fname: any; line_nb: number; @@ -113,16 +114,26 @@ export interface FlecheSaveParams { textDocument: VersionedTextDocumentIdentifier; } -export interface SentencePerfParams { - loc: Loc; +export interface PerfInfo { + // Original Execution Time (when not cached) time: number; - mem: number; + // Difference in words allocated in the heap using `Gc.quick_stat` + memory: number; + // Whether the execution was cached + cache_hit: boolean; + // Caching overhead + time_hash: number; } -export interface DocumentPerfParams { +export interface SentencePerfParams { + range: R; + info: PerfInfo; +} + +export interface DocumentPerfParams { textDocument: VersionedTextDocumentIdentifier; summary: string; - timings: SentencePerfParams[]; + timings: SentencePerfParams[]; } // View messaging interfaces; should go on their own file @@ -152,3 +163,48 @@ export type CoqMessagePayload = RenderGoals | WaitingForInfo | InfoError; export interface CoqMessageEvent extends MessageEvent { data: CoqMessagePayload; } + +// For perf panel data +export interface PerfUpdate { + method: "update"; + params: DocumentPerfParams; +} + +export interface PerfReset { + method: "reset"; +} + +export type PerfMessagePayload = PerfUpdate | PerfReset; + +export interface PerfMessageEvent extends MessageEvent { + data: PerfMessagePayload; +} + +export interface ViewRangeParams { + textDocument: VersionedTextDocumentIdentifier; + range: Range; +} + +// Server version and status notifications + +export interface CoqServerVersion { + coq: string; + ocaml: string; + coq_lsp: string; +} + +export interface CoqBusyStatus { + status: "Busy"; + modname: string; +} + +export interface CoqIdleStatus { + status: "Idle"; + mem: string; +} + +export interface CoqStoppedStatus { + status: "Stopped"; +} + +export type CoqServerStatus = CoqBusyStatus | CoqIdleStatus | CoqStoppedStatus; diff --git a/editor/code/package-lock.json b/editor/code/package-lock.json index 6a382f61..3fb54af4 100644 --- a/editor/code/package-lock.json +++ b/editor/code/package-lock.json @@ -1,12 +1,12 @@ { "name": "coq-lsp", - "version": "0.1.9-dev", + "version": "0.1.9", "lockfileVersion": 3, "requires": true, "packages": { "": { "name": "coq-lsp", - "version": "0.1.9-dev", + "version": "0.1.9", "dependencies": { "@vscode/webview-ui-toolkit": "^1.2.2", "jquery": "^3.7.1", diff --git a/editor/code/package.json b/editor/code/package.json index bca67a6b..c1bb58a6 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.9-dev", + "version": "0.1.9", "contributors": [ "Emilio Jesús Gallego Arias ", "Ali Caglayan ", @@ -29,7 +29,8 @@ "url": "https://github.com/ejgallego/coq-lsp" }, "activationEvents": [ - "onLanguage:markdown" + "onLanguage:markdown", + "onLanguage:latex" ], "contributes": { "languages": [ @@ -54,6 +55,15 @@ "extensions": [ ".mv" ] + }, + { + "id": "latex", + "aliases": [ + "LaTeX" + ], + "extensions": [ + ".lv" + ] } ], "grammars": [ @@ -90,13 +100,17 @@ "command": "coq-lsp.toggle", "title": "Coq LSP: Toggle the running status of Coq Language Server" }, + { + "command": "coq-lsp.toggle_mode", + "title": "Coq LSP: Toggle checking mode between continous / on-demand" + }, { "command": "coq-lsp.goals", - "title": "Coq LSP: Show Goals at Point" + "title": "Coq LSP: Show Goals at point" }, { "command": "coq-lsp.document", - "title": "Coq LSP: Get document in serialized format, print in console" + "title": "Coq LSP: Serialize document to JSON" }, { "command": "coq-lsp.save", @@ -104,15 +118,19 @@ }, { "command": "coq-lsp.trim", - "title": "Coq LSP: Request the server to trim caches and compact memory (useful to try reduce memory comsumption)" + "title": "Coq LSP: Free memory" }, { "command": "coq-lsp.sentenceNext", - "title": "Coq LSP: try to jump to next Coq sentence" + "title": "Coq LSP: Try to jump to next Coq sentence" + }, + { + "command": "coq-lsp.sentencePrevious", + "title": "Coq LSP: Try to jump to previous Coq sentence" }, { - "command": "coq-lsp.sentenceBack", - "title": "Coq LSP: try to jump to previous Coq sentence" + "command": "coq-lsp.heatmap.toggle", + "title": "Coq LSP: Toggle heatmap" } ], "keybindings": [ @@ -121,6 +139,18 @@ "key": "alt+enter", "mac": "meta+enter", "when": "editorTextFocus && (editorLangId == coq || editorTextFocus && editorLangId == markdown)" + }, + { + "command": "coq-lsp.sentenceNext", + "key": "Alt+N", + "mac": "cmd+N", + "when": "editorTextFocus && (editorLangId == coq || editorTextFocus && editorLangId == markdown)" + }, + { + "command": "coq-lsp.sentencePrevious", + "key": "Alt+P", + "mac": "cmd+P", + "when": "editorTextFocus && (editorLangId == coq || editorTextFocus && editorLangId == markdown)" } ], "viewsContainers": { @@ -278,8 +308,13 @@ }, "coq-lsp.check_only_on_request": { "type": "boolean", - "default": false, - "description": "Check files lazily, that is to say, goal state for a point will only be computed when the data is actually demanded. Note that this option is experimental and not recommended for use yet; we expose it only for testing and further development." + "default": true, + "description": "(Experimental) Check files lazily, that is to say, goal state for a point will only be computed when the data is actually demanded." + }, + "coq-lsp.check_on_scroll": { + "type": "boolean", + "default": true, + "description": "(Experimental) When in lazy mode, check files on scroll." } } }, @@ -309,6 +344,41 @@ "description": "Automatically ignore Coq object files in the workspace (.vo, .vos, ...)" } } + }, + { + "title": "Heatmap", + "type": "object", + "properties": { + "coq-lsp.heatmap.enabled": { + "type": "boolean", + "default": false, + "description": "Enable heatmap for Coq files." + }, + "coq-lsp.heatmap.warmColor": { + "type": "string", + "default": "#ff0000", + "description": "Defines the warm color for the heatmap." + }, + "coq-lsp.heatmap.coldColor": { + "type": "string", + "default": "#000000", + "description": "Defines the cold color for the heatmap." + }, + "coq-lsp.heatmap.heatLevels": { + "type": "number", + "default": 100, + "description": "Defines the number of heat levels in the heatmap." + }, + "coq-lsp.heatmap.mode": { + "type": "string", + "default": "time", + "enum": [ + "time", + "memory" + ], + "description": "Defines the heatmap mode." + } + } } ] }, diff --git a/editor/code/src/client.ts b/editor/code/src/client.ts index 302c3842..c600a556 100644 --- a/editor/code/src/client.ts +++ b/editor/code/src/client.ts @@ -13,10 +13,17 @@ import { WorkspaceConfiguration, Disposable, languages, + Uri, + TextEditorVisibleRangesChangeEvent, } from "vscode"; +import * as vscode from "vscode"; +import * as lsp from "vscode-languageserver-types"; + import { BaseLanguageClient, + DidChangeConfigurationNotification, + DidChangeConfigurationParams, LanguageClientOptions, NotificationType, RequestType, @@ -30,14 +37,43 @@ import { GoalRequest, GoalAnswer, PpString, + DocumentPerfParams, + ViewRangeParams, } from "../lib/types"; + +import { + CoqLanguageStatus, + defaultVersion, + defaultStatus, + coqServerVersion, + coqServerStatus, +} from "./status"; import { CoqLspClientConfig, CoqLspServerConfig, CoqSelector } from "./config"; import { InfoPanel, goalReq } from "./goals"; import { FileProgressManager } from "./progress"; import { coqPerfData, PerfDataView } from "./perf"; -import { sentenceNext, sentenceBack } from "./edit"; +import { sentenceNext, sentencePrevious } from "./edit"; +import { HeatMap, HeatMapConfig } from "./heatmap"; +import { debounce, throttle } from "throttle-debounce"; + +// Convert perf data to VSCode format +function toVsCodePerf( + p: DocumentPerfParams +): DocumentPerfParams { + let textDocument = p.textDocument; + let summary = p.summary; + let timings = p.timings.map((t) => { + return { + range: client.protocol2CodeConverter.asRange(t.range), + info: t.info, + }; + }); + return { textDocument, summary, timings }; +} let config: CoqLspClientConfig; +let serverConfig: CoqLspServerConfig; + let client: BaseLanguageClient; // Lifetime of the info panel == extension lifetime. @@ -49,10 +85,17 @@ let fileProgress: FileProgressManager; // Status Bar Button let lspStatusItem: StatusBarItem; +// Language Status Indicators +let languageStatus: CoqLanguageStatus; +let languageVersionHook: Disposable; +let languageStatusHook: Disposable; + // Lifetime of the perf data setup == client lifetime for the hook, extension for the webview let perfDataView: PerfDataView; let perfDataHook: Disposable; +let heatMap: HeatMap; + // Client Factory types export type ClientFactoryType = ( context: ExtensionContext, @@ -79,19 +122,32 @@ export function activateCoqLSP( ): CoqLspAPI { window.showInformationMessage("Coq LSP Extension: Going to activate!"); - workspace.onDidChangeConfiguration((cfgChange) => { - if (cfgChange.affectsConfiguration("coq-lsp")) { - // Refactor to remove the duplicate call below - const wsConfig = workspace.getConfiguration("coq-lsp"); - config = CoqLspClientConfig.create(wsConfig); + // Update config on client and server + function configDidChange(wsConfig: any): CoqLspServerConfig { + config = CoqLspClientConfig.create(wsConfig); + let client_version = context.extension.packageJSON.version; + let settings = CoqLspServerConfig.create(client_version, wsConfig); + let params: DidChangeConfigurationParams = { settings }; + + if (client && client.isRunning()) { + let type = DidChangeConfigurationNotification.type; + client.sendNotification(type, params); } - }); - function coqCommand(command: string, fn: () => void) { + // Store setting on the server for local use + serverConfig = settings; + return settings; + } + + function coqCommand( + command: string, + fn: (...args: any[]) => void | Promise + ) { let disposable = commands.registerCommand("coq-lsp." + command, fn); context.subscriptions.push(disposable); } function coqEditorCommand(command: string, fn: (editor: TextEditor) => void) { + // EJGA: we should check for document selector here. let disposable = commands.registerTextEditorCommand( "coq-lsp." + command, fn @@ -125,30 +181,30 @@ export function activateCoqLSP( ...fexc, }); } + const stop = () => { if (client && client.isRunning()) { - client + return client .dispose(2000) - .then(updateStatusBar) - .then(() => { + .finally(updateStatusBar) + .finally(() => { infoPanel.dispose(); fileProgress.dispose(); perfDataHook.dispose(); + heatMap.dispose(); + languageVersionHook.dispose(); + languageStatusHook.dispose(); }); - } + } else return Promise.resolve(); }; const start = () => { if (client && client.isRunning()) return; const wsConfig = workspace.getConfiguration("coq-lsp"); - config = CoqLspClientConfig.create(wsConfig); - let client_version = context.extension.packageJSON.version; - const initializationOptions = CoqLspServerConfig.create( - client_version, - wsConfig - ); + // This also sets `config` variable + const initializationOptions: CoqLspServerConfig = configDidChange(wsConfig); const clientOptions: LanguageClientOptions = { documentSelector: CoqSelector.local, @@ -163,39 +219,63 @@ export function activateCoqLSP( fileProgress = new FileProgressManager(client); perfDataHook = client.onNotification(coqPerfData, (data) => { perfDataView.update(data); + heatMap.update(toVsCodePerf(data)); + }); + + languageVersionHook = client.onNotification(coqServerVersion, (data) => { + languageStatus.updateVersion(data); }); + + languageStatusHook = client.onNotification(coqServerStatus, (data) => { + languageStatus.updateStatus(data, serverConfig.check_only_on_request); + }); + resolve(client); }); - cP.then((client) => - client - .start() - .then(updateStatusBar) - .then(() => { - if (window.activeTextEditor) { - goalsCall( - window.activeTextEditor, - TextEditorSelectionChangeKind.Command - ); - } - }) - ).catch((error) => { - let emsg = error.toString(); - console.log(`Error in coq-lsp start: ${emsg}`); - setFailedStatuBar(emsg); - }); + return cP + .then((client) => + client + .start() + .then(updateStatusBar) + .then(() => { + if (window.activeTextEditor) { + goalsCall( + window.activeTextEditor, + TextEditorSelectionChangeKind.Command + ); + } + }) + ) + .catch((error) => { + let emsg = error.toString(); + console.log(`Error in coq-lsp start: ${emsg}`); + setFailedStatusBar(emsg); + }); }; - const restart = () => { - stop(); - start(); + const restart = async () => { + await stop().finally(start); }; - const toggle = () => { - if (client && client.isRunning()) { - stop(); + const toggle_lazy_checking = async () => { + let wsConfig = workspace.getConfiguration(); + let newValue = !wsConfig.get("coq-lsp.check_only_on_request"); + await wsConfig.update("coq-lsp.check_only_on_request", newValue); + languageStatus.updateStatus({ status: "Idle", mem: "" }, newValue); + }; + + // switches between the different status of the server + const toggle = async () => { + if (client && client.isRunning() && !serverConfig.check_only_on_request) { + // Server on, and in continous mode, set lazy + await toggle_lazy_checking().then(updateStatusBar); + } else if (client && client.isRunning()) { + // Server on, and in lazy mode, stop + await stop(); } else { - start(); + // Server is off, set continous mode and start + await toggle_lazy_checking().then(start); } }; @@ -204,15 +284,31 @@ export function activateCoqLSP( // Check VSCoq is not installed checkForVSCoq(); + // Config change events setup + let onDidChange = workspace.onDidChangeConfiguration((cfgChange) => { + if (cfgChange.affectsConfiguration("coq-lsp")) { + // Refactor to remove the duplicate call below + const wsConfig = workspace.getConfiguration("coq-lsp"); + configDidChange(wsConfig); + } + }); + + context.subscriptions.push(onDidChange); + // InfoPanel setup. infoPanel = new InfoPanel(context.extensionUri); context.subscriptions.push(infoPanel); const goals = (editor: TextEditor) => { if (!client.isRunning()) return; - let uri = editor.document.uri; + let uri = editor.document.uri.toString(); let version = editor.document.version; - let position = editor.selection.active; + + // XXX: EJGA: For some reason TS doesn't catch the typing error here, + // beware, because this creates many problems once out of the standard + // Node-base Language client and object are serialized! + let cursor = editor.selection.active; + let position = client.code2ProtocolConverter.asPosition(cursor); infoPanel.updateFromServer( client, uri, @@ -264,6 +360,40 @@ export function activateCoqLSP( context.subscriptions.push(goalsHook); + const viewRangeNotification = new NotificationType( + "coq/viewRange" + ); + + let viewRangeHook = window.onDidChangeTextEditorVisibleRanges( + throttle(400, (evt: TextEditorVisibleRangesChangeEvent) => { + if ( + config.check_on_scroll && + serverConfig.check_only_on_request && + languages.match(CoqSelector.local, evt.textEditor.document) > 0 && + evt.visibleRanges[0] + ) { + let uri = evt.textEditor.document.uri.toString(); + let version = evt.textEditor.document.version; + let textDocument = { uri, version }; + let range = client.code2ProtocolConverter.asRange(evt.visibleRanges[0]); + let params: ViewRangeParams = { textDocument, range }; + client.sendNotification(viewRangeNotification, params); + } + }) + ); + + context.subscriptions.push(viewRangeHook); + + // Heatmap setup + heatMap = new HeatMap( + workspace.getConfiguration("coq-lsp").get("heatmap") as HeatMapConfig + ); + + const heatMapToggle = () => { + heatMap.toggle(); + }; + + // Document request setup const docReq = new RequestType( "coq/getDocument" ); @@ -276,15 +406,31 @@ export function activateCoqLSP( version ); let params: FlecheDocumentParams = { textDocument }; - client.sendRequest(docReq, params).then((fd) => console.log(fd)); + client.sendRequest(docReq, params).then((fd) => { + // EJGA: uri_result could be used to set the suggested save path + // for the new editor, however we need to see how to do that + // and set `content` too for the new editor. + let path = `${uri.fsPath}-${version}.json`; + let uri_result = Uri.file(path).with({ scheme: "untitled" }); + + let open_options = { + language: "json", + content: JSON.stringify(fd, null, 2), + }; + workspace.openTextDocument(open_options).then((document) => { + window.showTextDocument(document); + }); + }); }; + // Trim notification setup const trimNot = new NotificationType<{}>("coq/trimCaches"); const cacheTrim = () => { client.sendNotification(trimNot, {}); }; + // Save request setup const saveReq = new RequestType( "coq/saveVo" ); @@ -319,13 +465,22 @@ export function activateCoqLSP( context.subscriptions.push(lspStatusItem); }; + // This stuff should likely go in the CoqLSP client class + languageStatus = new CoqLanguageStatus(defaultVersion, defaultStatus, false); + // Ali notes about the status item text: we should keep it short // We violate this on the error case, but only because it is exceptional. const updateStatusBar = () => { if (client && client.isRunning()) { - lspStatusItem.text = "$(check) coq-lsp (running)"; - lspStatusItem.backgroundColor = undefined; - lspStatusItem.tooltip = "coq-lsp is running. Click to disable."; + if (serverConfig.check_only_on_request) { + lspStatusItem.text = "$(check) coq-lsp (on-demand checking)"; + lspStatusItem.backgroundColor = undefined; + lspStatusItem.tooltip = "coq-lsp is running. Click to disable."; + } else { + lspStatusItem.text = "$(check) coq-lsp (continous checking)"; + lspStatusItem.backgroundColor = undefined; + lspStatusItem.tooltip = "coq-lsp is running. Click to disable."; + } } else { lspStatusItem.text = "$(circle-slash) coq-lsp (stopped)"; lspStatusItem.backgroundColor = new ThemeColor( @@ -335,7 +490,7 @@ export function activateCoqLSP( } }; - const setFailedStatuBar = (emsg: string) => { + const setFailedStatusBar = (emsg: string) => { lspStatusItem.text = "$(circle-slash) coq-lsp (failed to start)"; lspStatusItem.backgroundColor = new ThemeColor( "statusBarItem.errorBackground" @@ -353,12 +508,16 @@ export function activateCoqLSP( coqCommand("toggle", toggle); coqCommand("trim", cacheTrim); + coqCommand("toggle_mode", toggle_lazy_checking); + coqEditorCommand("goals", goals); coqEditorCommand("document", getDocument); coqEditorCommand("save", saveDocument); coqEditorCommand("sentenceNext", sentenceNext); - coqEditorCommand("sentenceBack", sentenceBack); + coqEditorCommand("sentencePrevious", sentencePrevious); + + coqEditorCommand("heatmap.toggle", heatMapToggle); createEnableButton(); diff --git a/editor/code/src/config.ts b/editor/code/src/config.ts index 68614e57..21f4821f 100644 --- a/editor/code/src/config.ts +++ b/editor/code/src/config.ts @@ -14,6 +14,7 @@ export interface CoqLspServerConfig { show_stats_on_hover: boolean; show_loc_info_on_hover: boolean; check_only_on_request: boolean; + send_perf_data: boolean; } export namespace CoqLspServerConfig { @@ -35,6 +36,7 @@ export namespace CoqLspServerConfig { show_stats_on_hover: wsConfig.show_stats_on_hover, show_loc_info_on_hover: wsConfig.show_loc_info_on_hover, check_only_on_request: wsConfig.check_only_on_request, + send_perf_data: wsConfig.send_perf_data, }; } } @@ -49,6 +51,7 @@ export enum ShowGoalsOnCursorChange { export interface CoqLspClientConfig { show_goals_on: ShowGoalsOnCursorChange; pp_format: "Pp" | "Str"; + check_on_scroll: boolean; } function pp_type_to_pp_format(pp_type: 0 | 1 | 2): "Pp" | "Str" { @@ -67,6 +70,7 @@ export namespace CoqLspClientConfig { let obj: CoqLspClientConfig = { show_goals_on: wsConfig.show_goals_on, pp_format: pp_type_to_pp_format(wsConfig.pp_type), + check_on_scroll: wsConfig.check_on_scroll, }; return obj; } @@ -77,6 +81,8 @@ export namespace CoqSelector { export const all: TextDocumentFilter[] = [ { language: "coq" }, { language: "markdown", pattern: "**/*.mv" }, + { language: "latex", pattern: "**/*.lv" }, + { language: "latex", pattern: "**/*.v.tex" }, ]; // Local Coq files, suitable for interaction with a local server diff --git a/editor/code/src/edit.ts b/editor/code/src/edit.ts index e01c64a2..c537a6ec 100644 --- a/editor/code/src/edit.ts +++ b/editor/code/src/edit.ts @@ -1,7 +1,23 @@ // Edition facilities for Coq files -import { TextEditor, Position, Range, Selection } from "vscode"; +import { + TextEditor, + Position, + Range, + Selection, + TextEditorRevealType, +} from "vscode"; -export function sentenceBack(editor: TextEditor) { +function setSelection(editor: TextEditor, newCursor: Position) { + editor.selection = new Selection(newCursor, newCursor); + + // Is there not a better way? + editor.revealRange( + new Range(newCursor, newCursor), + TextEditorRevealType.InCenterIfOutsideViewport + ); +} + +export function sentencePrevious(editor: TextEditor) { // Slice from the beginning of the document let cursor = editor.selection.active; let range = new Range(editor.document.positionAt(0), cursor); @@ -19,7 +35,7 @@ export function sentenceBack(editor: TextEditor) { index = text.lastIndexOf(match) + match.length; } let newCursor = editor.document.positionAt(index); - editor.selection = new Selection(newCursor, newCursor); + setSelection(editor, newCursor); } } @@ -40,6 +56,6 @@ export function sentenceNext(editor: TextEditor) { let newCursor = editor.document.positionAt( editor.document.offsetAt(cursor) + index ); - editor.selection = new Selection(newCursor, newCursor); + setSelection(editor, newCursor); } } diff --git a/editor/code/src/goals.ts b/editor/code/src/goals.ts index c5c81184..7a085b1b 100644 --- a/editor/code/src/goals.ts +++ b/editor/code/src/goals.ts @@ -1,5 +1,4 @@ import { - Position, Uri, WebviewPanel, window, @@ -11,6 +10,7 @@ import { import { BaseLanguageClient, RequestType, + ResponseError, VersionedTextDocumentIdentifier, } from "vscode-languageclient"; import { @@ -21,6 +21,12 @@ import { ErrorData, } from "../lib/types"; +import { + URI, + Position, + TextDocumentIdentifier, +} from "vscode-languageserver-types"; + export const goalReq = new RequestType, void>( "proof/goals" ); @@ -91,6 +97,10 @@ export class InfoPanel { ensurePanel() { if (!this.panel) { this.panelFactory(); + } else { + if (!this.panel.visible) { + this.panel.reveal(2, true); + } } } postMessage({ method, params }: CoqMessagePayload) { @@ -127,7 +137,12 @@ export class InfoPanel { this.requestSent(params); client.sendRequest(goalReq, params).then( (goals) => this.requestDisplay(goals), - (reason) => this.requestError(reason) + (error: ResponseError) => { + let textDocument = params.textDocument; + let position = params.position; + let message = error.message; + this.requestError({ textDocument, position, message }); + } ); } @@ -139,22 +154,27 @@ export class InfoPanel { let goals_fn = goals as GoalAnswer; this.listeners.forEach((fn) => fn(goals_fn)); }, - // We should actually provide a better setup so we can pass the rejection of the promise to our clients, YMMV tho. - (reason) => this.requestError(reason) + // We should actually provide a better setup so we can pass + // the rejection of the promise to our clients, YMMV tho. + (error: ResponseError) => { + let textDocument = params.textDocument; + let position = params.position; + let message = error.message; + this.requestError({ textDocument, position, message }); + } ); } } + + // Protocol-level data updateFromServer( client: BaseLanguageClient, - uri: Uri, + uri: URI, version: number, position: Position, pp_format: "Pp" | "Str" ) { - let textDocument = VersionedTextDocumentIdentifier.create( - uri.toString(), - version - ); + let textDocument = VersionedTextDocumentIdentifier.create(uri, version); // Example to test the `command` parameter // let command = "idtac."; diff --git a/editor/code/src/heatmap.ts b/editor/code/src/heatmap.ts new file mode 100644 index 00000000..49746746 --- /dev/null +++ b/editor/code/src/heatmap.ts @@ -0,0 +1,178 @@ +import { + window, + TextEditorDecorationType, + Range, + Disposable, + TextEditor, + languages, + workspace, + ConfigurationChangeEvent, +} from "vscode"; + +import { CoqSelector } from "./config"; +import { DocumentPerfParams, SentencePerfParams } from "../lib/types"; + +export interface HeatMapConfig { + enabled: boolean; + heatLevels: number; + warmColor: string; + coldColor: string; + perfDataType: "time" | "memory"; +} + +export class HeatMap { + private enabled: boolean = false; + private subscriptions: Disposable[] = []; + private heatStyles: TextEditorDecorationType[] = []; + private perfData: DocumentPerfParams | undefined = undefined; + private perfDataType: "time" | "memory" = "time"; + + constructor(config: HeatMapConfig) { + this.enabled = config.enabled; + this.apply_config(config); + this.subscriptions.push(this.listenToConfigChanges()); + } + + dispose() { + this.subscriptions.forEach((subscription) => subscription.dispose()); + this.heatStyles.forEach((style) => style.dispose()); + } + + toggle() { + this.enabled = !this.enabled; + if (this.enabled) { + this.draw(window.activeTextEditor); + } else { + this.clearHeatMap(); + } + } + + draw(editor?: TextEditor) { + if ( + !editor || + !this.enabled || + languages.match(CoqSelector.local, editor.document) === 0 || + this.perfData === undefined + ) { + return; + } + + const perfData = this.perfData; + + const getData = (perf: SentencePerfParams) => { + if (this.perfDataType === "time") { + return perf.info.time; + } else if (this.perfDataType === "memory") { + return perf.info.memory; + } else { + throw new Error("Unknown perfDataType"); + } + }; + + const dataPoints = perfData.timings.map(getData); + const minData = Math.min(...dataPoints); + const maxData = Math.max(...dataPoints); + const dataRange = maxData - minData; + + if (dataRange === 0) { + return; + } + + const dataPerLevel = dataRange / this.heatStyles.length; + const ranges: Range[][] = new Array(this.heatStyles.length) + .fill(null) + .map(() => []); + + this.perfData.timings.forEach((perf) => { + const dataPoint = getData(perf); + const bucket = Math.min( + this.heatStyles.length - 1, + Math.floor((dataPoint - minData) / dataPerLevel) + ); + ranges[bucket].push(perf.range); + }); + + this.heatStyles.forEach((style, i) => + editor.setDecorations(style, ranges[i]) + ); + } + + private clearHeatMap() { + const editor = window.activeTextEditor; + if (editor) { + this.heatStyles.forEach((style) => editor.setDecorations(style, [])); + } + } + + private listenToConfigChanges() { + return workspace.onDidChangeConfiguration( + (event: ConfigurationChangeEvent) => { + if (event.affectsConfiguration("coq-lsp.heatmap")) { + let config = workspace + .getConfiguration("coq-lsp") + .get("heatmap") as HeatMapConfig; + this.apply_config(config); + this.draw(window.activeTextEditor); + } + } + ); + } + + private apply_config(config: HeatMapConfig) { + // Read settings + const heatLevels = config.heatLevels || 100; + const warmColor = config.warmColor || "#ff0000"; + const coldColor = config.coldColor || "#000000"; + this.perfDataType = config.perfDataType || "time"; + + // Use the settings + this.updateHeatMapStyles(heatLevels, warmColor, coldColor); + } + + private updateHeatMapStyles( + heatLevels: number, + warmColour: string, + coldColour: string + ) { + this.heatStyles.forEach((style) => style.dispose()); // Clear existing styles + this.heatStyles = []; + + const [r1, g1, b1] = this.parseColor(coldColour); + const [r2, g2, b2] = this.parseColor(warmColour); + + for (let i = 0; i < heatLevels; i++) { + const alphaValue = i / (heatLevels - 1); + const r = Math.round(r1 + (r2 - r1) * alphaValue); + const g = Math.round(g1 + (g2 - g1) * alphaValue); + const b = Math.round(b1 + (b2 - b1) * alphaValue); + + this.heatStyles.push( + window.createTextEditorDecorationType({ + backgroundColor: `rgba(${r}, ${g}, ${b}, ${alphaValue})`, + }) + ); + } + } + + // Parse hexadecimal color + private parseColor(color: string): number[] { + const hexRegex = /^#?([a-f\d]{2})([a-f\d]{2})([a-f\d]{2})$/i; + const matches = color.match(hexRegex); + if (!matches) { + console.warn( + `Invalid color format: ${color}. Using default color "#ff0000."` + ); + return [0xff, 0, 0]; // Default to red + } + return [ + parseInt(matches[1], 16), + parseInt(matches[2], 16), + parseInt(matches[3], 16), + ]; + } + + update(data: DocumentPerfParams) { + this.perfData = data; + this.draw(window.activeTextEditor); + } +} diff --git a/editor/code/src/perf.ts b/editor/code/src/perf.ts index 34c73f40..c42aa915 100644 --- a/editor/code/src/perf.ts +++ b/editor/code/src/perf.ts @@ -6,16 +6,17 @@ import { WebviewViewResolveContext, window, } from "vscode"; +import { Range } from "vscode-languageserver-types"; import { NotificationType } from "vscode-languageclient"; -import { DocumentPerfParams } from "../lib/types"; +import { DocumentPerfParams, PerfMessagePayload } from "../lib/types"; -export const coqPerfData = new NotificationType( +export const coqPerfData = new NotificationType>( "$/coq/filePerfData" ); export class PerfDataView implements Disposable { private panel: Disposable; - private updateWebView: (data: DocumentPerfParams) => void = () => {}; + private updateWebView: (data: DocumentPerfParams) => void = () => {}; constructor(extensionUri: Uri) { let resolveWebviewView = ( @@ -50,12 +51,14 @@ export class PerfDataView implements Disposable { `; - this.updateWebView = (params: DocumentPerfParams) => { - webview.webview.postMessage({ method: "update", params }); + this.updateWebView = (params: DocumentPerfParams) => { + let message: PerfMessagePayload = { method: "update", params }; + webview.webview.postMessage(message); }; // We reset spurious old-sessions data - webview.webview.postMessage({ method: "reset" }); + let message: PerfMessagePayload = { method: "reset" }; + webview.webview.postMessage(message); }; let perfProvider: WebviewViewProvider = { resolveWebviewView }; this.panel = window.registerWebviewViewProvider( @@ -66,7 +69,7 @@ export class PerfDataView implements Disposable { dispose() { this.panel.dispose(); } - update(data: DocumentPerfParams) { + update(data: DocumentPerfParams) { this.updateWebView(data); } } diff --git a/editor/code/src/status.ts b/editor/code/src/status.ts new file mode 100644 index 00000000..f9a5f406 --- /dev/null +++ b/editor/code/src/status.ts @@ -0,0 +1,104 @@ +import { LanguageStatusItem, LanguageStatusSeverity, languages } from "vscode"; +import { NotificationType } from "vscode-languageclient"; + +import { CoqSelector } from "./config"; + +import { CoqServerVersion, CoqServerStatus } from "../lib/types"; + +export const coqServerVersion = new NotificationType( + "$/coq/serverVersion" +); + +export const coqServerStatus = new NotificationType( + "$/coq/serverStatus" +); + +// We should likely have one class per item, but not a big deal yet +export class CoqLanguageStatus { + // Checking and what + status: LanguageStatusItem; + // Version info + version: LanguageStatusItem; + // Root: one or multiple, to be done soon + // root : LanguageStatusItem; + + constructor( + version: CoqServerVersion, + status: CoqServerStatus, + lazy_mode: boolean + ) { + // Version info + this.version = languages.createLanguageStatusItem( + "coq.version", + CoqSelector.all + ); + this.version.name = "Version"; + + // Server status + this.status = languages.createLanguageStatusItem( + "coq.status", + CoqSelector.all + ); + this.status.name = "Running Status"; + + // this.status.command = "start continous toogle continous"; + // root = languages.createLanguageStatusItem("coq.root", CoqSelector.all); + + this.updateVersion(version); + this.updateStatus(status, lazy_mode); + } + + updateVersion(version: CoqServerVersion) { + this.version.text = `coq-lsp ${version.coq_lsp}`; + this.version.detail = `Coq ${version.coq}, OCaml ${version.ocaml}`; + } + + updateStatus(status: CoqServerStatus, lazy_mode: boolean) { + let command = lazy_mode + ? { + title: "Enable Continous Mode", + command: "coq-lsp.toggle_mode", + } + : { + title: "Enable On-Demand Mode", + command: "coq-lsp.toggle_mode", + args: true, + }; + + let status_name = lazy_mode ? "On-demand" : "Continous"; + + if (status.status == "Busy") { + this.status.busy = true; + this.status.text = `coq-lsp: Checking ${status.modname}`; + this.status.detail = `set mode`; + this.status.command = command; + this.status.severity = LanguageStatusSeverity.Information; + } else if (status.status == "Idle") { + // Idle + this.status.busy = false; + this.status.text = `coq-lsp: Idle (${status_name} |${status.mem})`; + this.status.detail = ""; + this.status.command = command; + this.status.severity = LanguageStatusSeverity.Information; + } else if (status.status == "Stopped") { + this.status.busy = false; + this.status.text = `Stopped`; + this.status.detail = ""; + this.status.command = { title: "Start Server", command: "coq-lsp.start" }; + this.status.severity = LanguageStatusSeverity.Error; + } + } + + dispose() { + this.status.dispose(); + this.version.dispose(); + // root.dispose(); + } +} + +export const defaultVersion: CoqServerVersion = { + coq: "N/A", + ocaml: "N/A", + coq_lsp: "N/A", +}; +export const defaultStatus: CoqServerStatus = { status: "Idle", mem: "" }; diff --git a/editor/code/syntaxes/coq.json b/editor/code/syntaxes/coq.json index ab9b086c..be74f453 100644 --- a/editor/code/syntaxes/coq.json +++ b/editor/code/syntaxes/coq.json @@ -100,7 +100,7 @@ } }, { - "match": "\\b(Hint|Constructors|Resolve|Rewrite|Ltac|Implicit(\\s+Types)?|Set|Unset|Remove\\s+Printing|Arguments|Tactic\\s+Notation|Notation|Infix|Reserved\\s+Notation|Section|Module\\s+Type|Module|End|Check|Print|Eval|Search|Universe|Coercions?|Generalizable\\s+All|Generalizable\\s+Variable?|Existing\\s+Instance|Existing\\s+Class|Canonical|About|Locate|Collection|Typeclasses\\s+(Opaque|Transparent))\\b", + "match": "\\b(Hint|Constructors|Resolve|Rewrite|Ltac|Implicit(\\s+Types)?|Set|Unset|Remove\\s+Printing|Arguments|Tactic\\s+Notation|Notation|Infix|Reserved\\s+Notation|Section|Module\\s+Type|Module|End|Check|Print|Eval|Search|Universe|Coercions?|Generalizable\\s+All|Generalizable\\s+Variable?|Existing\\s+Instance|Existing\\s+Class|Canonical|About|Locate|Collection|Typeclasses\\s+(Opaque|Transparent)|Reset(\\s+Initial)?|Back)\\b", "comment": "Vernacular keywords", "name": "keyword.source.coq" }, diff --git a/editor/code/views/info/Goals.tsx b/editor/code/views/info/Goals.tsx index 531b77da..1b479e69 100644 --- a/editor/code/views/info/Goals.tsx +++ b/editor/code/views/info/Goals.tsx @@ -61,16 +61,24 @@ function Goal({ goal, idx, open }: GoalP) { } }); + // XXX: We want to add an option for this that can be set interactively + let show_goal_on_header = false; + + let gtyp = ( +
+ +
+ ); + return (
+ {show_goal_on_header ? "" : gtyp}
-
- -
+ {show_goal_on_header ? gtyp : ""}
); } @@ -141,7 +149,7 @@ function StackGoals({ idx, stack }: StackSummaryP) {
diff --git a/editor/code/views/info/Loc.tsx b/editor/code/views/info/Loc.tsx index a7d7142a..56faf477 100644 --- a/editor/code/views/info/Loc.tsx +++ b/editor/code/views/info/Loc.tsx @@ -1,12 +1,15 @@ import { Loc } from "../../lib/types"; export type LocP = { loc?: Loc }; + +// Note, this is for display, so we need to adjust for both lines and +// columns to start at 1, hence the + 1 export function Loc({ loc }: LocP) { if (!loc) return null; - let l1 = loc.line_nb + 1; - let c1 = loc.bp - loc.bol_pos; - let l2 = loc.line_nb_last + 1; - let c2 = loc.ep - loc.bol_pos_last; + let l1 = loc.line_nb; + let c1 = loc.bp - loc.bol_pos + 1; + let l2 = loc.line_nb_last; + let c2 = loc.ep - loc.bol_pos_last + 1; return {`l:${l1},c:${c1}--l:${l2},c:${c2}`}; } diff --git a/editor/code/views/perf/App.tsx b/editor/code/views/perf/App.tsx index 17f59a44..c7004767 100644 --- a/editor/code/views/perf/App.tsx +++ b/editor/code/views/perf/App.tsx @@ -1,5 +1,5 @@ import { WebviewApi } from "vscode-webview"; -import React, { ReactElement, useEffect, useState } from "react"; +import { ReactElement, useEffect, useState } from "react"; import { VSCodeDataGrid, VSCodeDataGridRow, @@ -7,19 +7,42 @@ import { } from "@vscode/webview-ui-toolkit/react"; import "./media/App.css"; import { Range } from "vscode-languageserver-types"; -import { DocumentPerfParams } from "../../lib/types"; +import { + DocumentPerfParams, + PerfMessageEvent, + SentencePerfParams, +} from "../../lib/types"; -const vscode: WebviewApi = acquireVsCodeApi(); +const vscode: WebviewApi> = acquireVsCodeApi(); -let empty: DocumentPerfParams = { +let empty: DocumentPerfParams = { textDocument: { uri: "", version: 0 }, summary: "No Data Yet", timings: [], }; -let init = vscode.getState() || empty; +function validateViewState(p: DocumentPerfParams) { + return ( + p.textDocument && + p.summary && + p.timings && + p.timings[0] && + p.timings[0].range && + p.timings[0].info + ); +} -interface CoqMessageEvent extends MessageEvent {} +function validOrEmpty( + p: DocumentPerfParams | undefined +): DocumentPerfParams { + // XXX We need to be careful here, when we update the + // DocumentPerfParams data type, the saved data here will make the + // view crash + if (p && validateViewState(p)) return p; + else return empty; +} + +let init = validOrEmpty(vscode.getState()); function printWords(w: number) { if (w < 1024) { @@ -31,29 +54,55 @@ function printWords(w: number) { } } -function SentencePerfCell({ field, value }) { +// XXX: Would be nice to have typing here, but... +interface PerfCellP { + field: keyof SentencePerfParams | string; + value: any; +} + +function SentencePerfCell({ field, value }: PerfCellP) { switch (field) { - case "loc": + case "range": let r = value as Range; return ( {`l: ${r.start.line} c: ${r.start.character} -- l: ${r.end.line} c: ${r.end.character}`} ); + case "time_hash": case "time": return {`${value.toFixed(4).toString()} secs`}; - case "mem": + case "memory": return {printWords(value)}; + case "cache_hit": + return {value ? "True" : "False"}; default: return null; } } -function SentencePerfRow({ idx, value }) { + +interface PerfParamsP { + idx: number; + value: SentencePerfParams; +} + +function perfFlatten(v: SentencePerfParams) { + return { + range: v.range, + time: v.info.time, + memory: v.info.memory, + cache_hit: v.info.cache_hit, + time_hash: v.info.time_hash, + }; +} + +function SentencePerfRow({ idx, value }: PerfParamsP) { + console.log(value); return ( <> - {Object.entries(value).map(([field, _value], idx) => { + {Object.entries(perfFlatten(value)).map(([field, value], idx) => { return ( - + ); })} @@ -62,13 +111,29 @@ function SentencePerfRow({ idx, value }) { ); } +function timeCmp(t1: SentencePerfParams, t2: SentencePerfParams) { + return t2.info.time - t1.info.time; +} + +function viewSort(p: DocumentPerfParams) { + let textDocument = p.textDocument; + let summary = p.summary; + let tlength = p.timings.length; + let timings = Array.from(p.timings) + .sort(timeCmp) + .slice(0, Math.min(30, tlength)); + return { textDocument, summary, timings }; +} + function App() { let [perfData, setPerfData] = useState(init); - function viewDispatch(event: CoqMessageEvent) { + function viewDispatch(event: PerfMessageEvent) { switch (event.data.method) { case "update": - vscode.setState(event.data.params); + if (!validateViewState(event.data.params)) break; + let data = viewSort(event.data.params); + vscode.setState(data); setPerfData(event.data.params); break; case "reset": @@ -92,19 +157,19 @@ function App() { <> - {Object.entries(perfData.timings[0] ?? []).map( - ([field, _value], idx) => { - return ( - - {field} - - ); - } - )} + {Object.entries( + perfData.timings[0] ? perfFlatten(perfData.timings[0]) : {} + ).map(([field, _value], idx) => { + return ( + + {field} + + ); + })} <> diff --git a/editor/code/views/perf/index.tsx b/editor/code/views/perf/index.tsx index d111c6fc..24fdd75f 100644 --- a/editor/code/views/perf/index.tsx +++ b/editor/code/views/perf/index.tsx @@ -1,5 +1,5 @@ // This is the script that is loaded by Coq's webview -import React from "react"; +import * as React from "react"; import { createRoot } from "react-dom/client"; import App from "./App"; diff --git a/editor/code/views/perf/tsconfig.json b/editor/code/views/perf/tsconfig.json index de553660..22e48b33 100644 --- a/editor/code/views/perf/tsconfig.json +++ b/editor/code/views/perf/tsconfig.json @@ -5,5 +5,5 @@ "target": "ESNext", "jsx": "react-jsx" }, - "include": ["**/*.ts", "../../lib/**/*"] + "include": ["**/*.ts", "**/*.tsx", "../../lib/**/*"] } diff --git a/etc/doc/PROTOCOL.md b/etc/doc/PROTOCOL.md index cc512143..8da3b04c 100644 --- a/etc/doc/PROTOCOL.md +++ b/etc/doc/PROTOCOL.md @@ -52,6 +52,7 @@ If a feature doesn't appear here it usually means it is not planned in the short |---------------------------------------|---------|------------------------------------------------------------| | `workspace/workspaceFolders` | Yes | Each folder should have a `_CoqProject` file at the root. | | `workspace/didChangeWorkspaceFolders` | Yes | | +| `workspace/didChangeConfiguration` | Yes (*) | We still do a client -> server push, instead of pull | |---------------------------------------|---------|------------------------------------------------------------| ### URIs accepted by coq-lsp @@ -138,6 +139,8 @@ interface GoalAnswer { error?: Pp; program?: ProgramInfo; } + +const goalReq : RequestType, void> ``` which can be then rendered by the client in way that is desired. @@ -268,6 +271,8 @@ interface FlecheDocument { spans: RangedSpan[]; completed : CompletionStatus }; + +const docReq : RequestType ``` #### Changelog @@ -298,28 +303,142 @@ The request will return `null`, or fail if not successful. ### Performance Data Notification The `$/coq/filePerfData` notification is sent from server to client -when the checking completes, and includes information about execution -hotspots and memory use by sentences. +when the checking completes (if the server-side `send_perf_data` +option is enabled); it includes information about execution hotspots, +caching, and memory use by sentences: ```typescript -export interface SentencePerfParams { - loc: Loc, - time: number, - mem, number +interface PerfInfo { + // Original Execution Time (when not cached) + time: number; + // Difference in words allocated in the heap using `Gc.quick_stat` + memory: number; + // Whether the execution was cached + cache_hit: boolean; + // Caching overhead + time_hash: number; } -export interface DocumentPerfParams { - summary: string; - timings: SentencePerfParams[]; +interface SentencePerfParams { + range: R; + info: PerfInfo; } + +interface DocumentPerfParams { + textDocument: VersionedTextDocumentIdentifier; + summary: string; + timings: SentencePerfParams[]; } + +const coqPerfData : NotificationType> ``` #### Changelog +- v0.1.9: + + new server-side option to control whether the notification is sent + + Fields renamed: `loc -> range`, `mem -> memory` + + Fixed type for `range`, it was always `Range` + + `time` and `memory` are now into a better `PerfInfo` data, which + correctly provides info for memoized sentences + + We now send the real time, even if the command was cached + + `memory` now means difference in memory from `GC.quick_stat` + + `filePerfData` will send the full document, ordered linearly, in + 0.1.7 we only sent the top 10 hotspots + + generalized typed over `R` parameter for range +- v0.1.8: Spec was accidentally broken, types were invalid - v0.1.7: Initial version ### Trim cache notification The `coq/trimCaches` notification from client to server tells the server to free memory. It has no parameters. + +### Viewport notification + +The `coq/viewRange` notification from client to server tells the +server the visible range of the user. + +```typescript +interface ViewRangeParams { + textDocument: VersionedTextDocumentIdentifier; + range: Range; +} +``` + +### Did Change Configuration and Server Configuration parameters + +The server will listen to the `workspace/didChangeConfiguration` +parameters and try to update them without a full server restart. + +The `settings` field corresponds to the data structure also passed in +the `initializationOptions` parameter for the LSP `init` method. + +As of today, the server exposes the following parameters: + +```typescript +export interface CoqLspServerConfig { + client_version: string; + eager_diagnostics: boolean; + goal_after_tactic: boolean; + show_coq_info_messages: boolean; + show_notices_as_diagnostics: boolean; + admit_on_bad_qed: boolean; + debug: boolean; + unicode_completion: "off" | "normal" | "extended"; + max_errors: number; + pp_type: 0 | 1 | 2; + show_stats_on_hover: boolean; + show_loc_info_on_hover: boolean; + check_only_on_request: boolean; +} +``` + +The settings are documented in the `package.json` file for the VSCode +client. + +#### Changelog + +- v0.1.9: First public documentation. + +### Server Version Notification + +The server will send the `$/coq/serverVersion` notification to inform +the client about `coq-lsp` version specific info. + +The parameters are: +```typescript +export interface CoqServerVersion { + coq: string; + ocaml: string; + coq_lsp: string; +} +``` + +#### Changelog + +- v0.1.9: First public documentation. + +### Server Status Notification + +The server will send the `$/coq/serverStatus` notification to inform +the client of checking status (start / end checking file) + +The parameters are: +```typescript + +export interface CoqBusyStatus { + status: "Busy"; + modname: string; +} + +export interface CoqIdleStatus { + status: "Idle" | "Stopped"; +} + +export type CoqServerStatus = CoqBusyStatus | CoqIdleStatus; +``` + +#### Changelog + +- v0.1.9: First public documentation. diff --git a/etc/doc/USER_MANUAL.md b/etc/doc/USER_MANUAL.md index 053dd4e7..bed0f86d 100644 --- a/etc/doc/USER_MANUAL.md +++ b/etc/doc/USER_MANUAL.md @@ -15,35 +15,175 @@ Given a project root `dir`, `coq-lsp` will try to read there. Other tools included in the `coq-lsp` suite usually take a -`--root=dir` command line parameter to set this information. +`--root=dir` command line parameter to set this information up. `coq-lsp` will display information about the project root and setting auto-detection using the standard language server protocol messaging facilities. In VSCode, these settings can be usually displayed in the "Output > Coq-lsp server" window. -## Selecting the interruption backend +## Key features: + +### Continuous vs on-demand mode + +`coq-lsp` offers two checking modes: + +- continuous checking [default]: `coq-lsp` will check all your open + documents eagerly. This is best when working with powerful machines + to minimize latency. When using OCaml 4.x, `coq-lsp` uses the + `memprof-limits` library to interrupt Coq and stay responsive. + +- on-demand checking [set the `check_only_on_request` option]: In this + mode, `coq-lsp` will stay idle and only compute information that is + demanded, for example, when the user asks for goals. This mode + disables some useful features such as `documentSymbol` as they can + only be implemented by checking the full file. + + This mode can use the `check_on_scroll` option, which improves + latency by telling `coq-lsp` to check eagerly what is on view on + user's screen. + +Users can change between on-demand/continuous mode by clicking on the +"Coq language status" item in the bottom right corner for VSCode. We +recommend pinning the language status item to see server status in +real-time. + +### Goal display + +By default, `coq-lsp` will follow cursor and show goals at cursor +position. This can be tweaked in options. + +The `coq-lsp.sentenceNext` and `coq-lsp.sentencePrevious` commands will +try to move the cursor one Coq sentence forward / backwards. These +commands are bound by default to `Alt + N` / `Alt + P` (`Cmd` on +MacOS). + +### Incremental proof edition + +Once you have setup your basic proof style, you may want to work with +`coq-lsp` in a way that is friendly to incremental checking. + +For example, `coq-lsp` will recognize blocks of the form: +```coq +Lemma foo : T. +Proof. + ... +Qed. +``` + +and will allow you to edit inside the `Proof.` `Qed.` block without +re-checking what is outside. + +### Error recovery + +`coq-lsp` can recover many errors automatically and allow you to +continue document edition later on. + +For example, it is not necessary to put `Admitted` in proofs that are +not fully completed. Also, you can work with bullets and `coq-lsp` +will automatically admit unfinished ones, so you can follow the +natural proof structure. + +### Server Status + + + +### Embedded Markdown and LaTeX documents + +`coq-lsp` supports checking of TeX and Markdown document with embedded +Coq inside. As of today, to enable this feature you must: + +- **markdown**: open a file with `.mv` extension, `coq-lsp` will + recognize code blocks starting with ````coq`. +- **TeX**: open a file with `.lv` extension, `coq-lsp` will recognize + code blocks delimited by `\begin{coq} ... \end{coq}` + +As of today, delimiters are expected at the beginning of the line, +don't hesitate to request for further changes based on this feature. + +## Coq LSP Settings + +### Goal display + +Several settings for goal display exist. + +### Continuous vs on-demand mode: + +A setting to have `coq-lsp` check documents continuously exists. + +## Memory management + +You can tell the server to free up memory with the "Coq LSP: Free +memory" command. + +## Advanced: Multiple Workspaces + +`coq-lsp` does support projects that combine multiple Coq project +roots in a single workspace. That way, one can develop on several +distinct Coq developments seamlessly. + +To enable this, use the "Add Folder" option in VSCode, where each root +must be a folder containing a `_CoqProject` file. + +Check the example at +[../../examples/multiple_workspaces/](../../examples/multiple_workspaces/) +to see it in action! + +## Interrupting coq-lsp When a Coq document is being checked, it is often necessary to _interrupt_ the checking process, for example, to check a new version, -or to retrieve some user-facing information. +or to retrieve some user-facing information, such as goals. -`coq-lsp` supports two interruption methods, selectable at start time -via the `--int_backend` command-line parameter: +`coq-lsp` supports two different interruption methods, selectable at +start time via the `--int_backend` command-line parameter: -- Coq-side polling (`--int_backend=Coq`, default): in this mode, Coq - polls for a flag every once in a while, and will raise an - interruption when the flag is set. This method has the downside that - some paths in Coq don't check the flag often enough, for example, - `Qed.`, so users may face unresponsiveness, as our server can only - run one thread at a time. +- Coq-side polling (`--int_backend=Coq`, default for OCaml 5.x): in + this mode, Coq polls for a flag every once in a while, and will + raise an interruption when the flag is set. This method has the + downside that some paths in Coq don't check the flag often enough, + for example, `Qed.`, so users may face unresponsiveness, as our + server can only run one thread at a time. - `memprof-limits` token-based interruption (`--int_backend=Mp`, - experimental): in this mode, Coq will use the `memprof-limits` - library to interrupt Coq. + experimental, default for OCaml 4.x): in this mode, Coq will use the + `memprof-limits` library to interrupt Coq. Coq has some bugs w.r.t. handling of asynchronous interruptions coming from `memprof-limits`. The situation is better in Coq 8.20, but users on Coq <= 8.19 do need to install a version of Coq with the backported fixes. See the information about Coq upstream bugs in the README for more information about available branches. + +`coq-lsp` will reject to enable the new interruption mode by default +on Coq < 8.20 unless the `lsp` Coq branch version is detected. + +## Advanced incremental tricks + +You can use the `Reset $id` and `Back $steps` commands to isolate +parts of the document from each other in terms of rechecking. + +For example, the command `Reset $id` will make the parts of the +document after it use the state before the node `id` was found. Thus, +any change between `$id` and the `Reset $id` command will not trigger +a recheck of the rest of the document. + +```coq +(* Coq code 1 *) + +Lemma foo : T. +Proof. ... Qed. + +(* Coq code 2 *) + +Reset foo. + +(* Coq code 3 *) +``` + +In the above code, any change in the "`Coq code 2`" section will not +trigger a recheck of the "`Coq code 3`" Section, by virtue of the +incremental engine. + +Using `Reset Initial`, you can effectively partition the document on +`N` parts! This is pretty cool for some use cases! diff --git a/etc/img/on_demand.gif b/etc/img/on_demand.gif new file mode 100644 index 00000000..8ed14f48 Binary files /dev/null and b/etc/img/on_demand.gif differ diff --git a/etc/release_notes/0.1.9.md b/etc/release_notes/0.1.9.md new file mode 100644 index 00000000..694d7776 --- /dev/null +++ b/etc/release_notes/0.1.9.md @@ -0,0 +1,255 @@ +Dear all, + +We are happy to announce the 0.1.9 release of `coq-lsp`. + +This release brings many new features and fixes, in particular: + +- New on-demand checking mode: `coq-lsp` can now check files on + demand, either by following the goals requested, or by following the + current viewport of your editor. Combined with the new keybinding + `M-n/M-p` for moving between Coq sentences, this provides a mode + similar to the usual one in Proof General. Additionally, we now show + real-time server status and checking information in the VSCode + language status area. + +- New interruption support using `memprofs-limits` (only in OCaml + 4). This solves all known cases of the server hanging. + (By E. J. Gallego Arias, thanks to Guillaume Munch-Maccagnoni and + Alex Sanchez-Stern). + +- `petanque`: a new server built on top of Flèche specifically + targeted at high-throughput low-latency reinforcement learning + applications. A subset of `petanque` has been experimentally + embedded into LSP for profit of extensions. (By E. J. Gallego + Arias, Guillaume Baudart, and Laetitia Teodorescu; thanks to Alex + Sanchez-Stern). + +- New heatmap feature to detect execution time hotspots in your Coq + documents, by Ali Caglayan; plus many more improvements and fixes + w.r.t. performance monitoring. + +- Coq meta commands `Reset` / `Reset Inital` and `Back` are supported, + together with the incremental checking engine they do provide some + interesting document splitting and isolation features. + +- New user manual with some information on how to start with `coq-lsp` + +- `coq-lsp` will now recognize literate LaTeX Coq files that end in + `.v.tex` or `.lv` and allow interacting with the Coq code inside + `\begin{coq}/\end{coq}` blocks. + +- Improved support for VSCode Live Share; full support requires + approval from Microsoft, please see below if you are interested in + helping with this. + +- New `Free Memory` server command. + +- Server settings are now updated on the fly when edited in VSCode. + +- Locations are now stored in the server in protocol format, this + should solve some Unicode issues present in previous versions + (by E. J. Gallego Arias and Leo Stefanesco). + +- Many improvements to both client and server plugin API, including a + new client extension API by E. J. Gallego Arias and Bhakti Shah. + +This version should be quite usable for a large majority of users, we +encourage you to test it! + +Please see the detailed Changelog below. We have added to the README a +list of tools using `coq-lsp` that may be of your interest. + +We'd like to thank to all the contributors and bug reporters for their +work. Contributions, bug reports, and feedback over `coq-lsp` are much +welcome, get in touch with us at GitHub or Zulip if you have questions +or comments. + +`coq-lsp` is compatible with Coq 8.17-8.20. The `fcc` compiler has +been ported back to 8.11, for the benefit of some SerAPI users. + +## Live Share support + +If you are interesting in seeing VSCode Live Share support, please go +to this issue and click the "Thumbs Up" icon at end of the first +comment: + +https://github.com/microsoft/live-share/issues/5046 + +This will help MS developers prioritizing support based on number of +demands. Please, _don't comment_ on the issue as this would create +load for MS developers, unless you have some feedback about the +technical implementation points + +Full Changelog +============== + + - Added new heatmap feature allowing timing data to be seen in the + editor. Can be enabled with the `Coq LSP: Toggle heatmap` + comamnd. Can be configured to show memory usage. Colors and + granularity are configurable. (@Alizter and @ejgallego, #686, + grants #681). + - new option `show_loc_info_on_hover` that will display parsing debug + information on hover; previous flag was fixed in code, which is way + less flexible. This also fixes the option being on in 0.1.8 by + mistake (@ejgallego, #588) + - hover plugins can now access the full document, this is convenient + for many use cases (@ejgallego, #591) + - fix hover position computation on the presence of Utf characters + (@ejgallego, #597, thanks to Pierre Courtieu for the report and + example, closes #594) + - fix activation bug that prevented extension activation for `.mv` + files, see discussion in the issues about the upstream policy + (@ejgallego @r3m0t, #598, cc #596, reported by Théo Zimmerman) + - require VSCode >= 1.82 in package.json . Our VSCode extension uses + `vscode-languageclient` 9 which imposes this. (@ejgallego, #599, + thanks to Théo Zimmerman for the report) + - `proof/goals` request: new `mode` parameter, to specify goals + after/before sentence display; renamed `pretac` to `command`, as to + provide official support for speculative execution (@ejgallego, #600) + - fix some cases where interrupted computations where memoized + (@ejgallego, #603) + - [internal] Flèche [Doc.t] API will now absorb errors on document + update and creation into the document itself. Thus, a document that + failed to create or update is still valid, but in the right failed + state. This is a much needed API change for a lot of use cases + (@ejgallego, #604) + - support OCaml 5.1.x (@ejgallego, #606) + - update progress indicator correctly on End Of File (@ejgallego, + #605, fixes #445) + - [plugins] New `astdump` plugin to dump AST of files into JSON and + SEXP (@ejgallego, #607) + - errors on save where not properly caught (@ejgallego, #608) + - switch default of `goal_after_tactic` to `true` (@Alizter, + @ejgallego, cc: #614) + - error recovery: Recognize `Defined` and `Admitted` in lex recovery + (@ejgallego, #616) + - completion: correctly understand UTF-16 code points on completion + request (Léo Stefanesco, #613, fixes #531) + - don't trigger the goals window in general markdown buffer + (@ejgallego, #625, reported by Théo Zimmerman) + - allow not to postpone full document requests (#626, @ejgallego) + - new configuration value `check_only_on_request` which will delay + checking the document until a request has been made (#629, cc: #24, + @ejgallego) + - fix typo on package.json configuration section (@ejgallego, #645) + - be more resilient with invalid _CoqProject files (@ejgallego, #646) + - support for Coq 8.16 has been abandoned due to lack of dev + resources (@ejgallego, #649) + - new option `--no_vo` for `fcc`, which will skip the `.vo` saving + step. `.vo` saving is now an `fcc` plugins, but for now, it is + enabled by default (@ejgallego, #650) + - depend on `memprof-limits` on OCaml 4.x (@ejgallego, #660) + - bump minimal OCaml version to 4.12 due to `memprof-limits` + (@ejgallego, #660) + - monitor all Coq-level calls under an interruption token + (@ejgallego, #661) + - interpret require thru our own custom execution env-aware path + (@bhaktishh, @ejgallego, #642, #643, #644) + - new `coq-lsp.plugin.goaldump` plugin, as an example on how to dump + goals from a document (@ejgallego @gbdrt, #619) + - new trim command (both in the server and in VSCode) to liberate + space used in the cache (@ejgallego, #662, fixes #367 cc: #253 #236 + #348) + - fix Coq performance view display (@ejgallego, #663, regression in + #513) + - allow more than one input position in `selectionRange` LSP call + (@ejgallego, #667, fixes #663) + - new VSCode commands to allow to move one sentence backwards / + forward, this is particularly useful when combined with lazy + checking mode (@ejgallego, #671, fixes #263, fixes #580) + - VSCode commands `coq-lsp.sentenceNext` / `coq-lsp.sentencePrevious` + are now bound by default to `Alt + N` / `Alt + P` keybindings + (@ejgallego, #718) + - change diagnostic `extra` field to `data`, so we now conform to the + LSP spec, include the data only when the `send_diags_extra_data` + server-side option is enabled (@ejgallego, #670) + - include range of full sentence in error diagnostic extra data + (@ejgallego, #670 , thanks to @driverag22 for the idea, cc: #663). + - The `coq-lsp.pp_type` VSCode client option now takes effect + immediately, no more need to restart the server to get different + goal display formats (@ejgallego, #675) + - new public VSCode extension API so other extensions can perform + actions when the user request the goals (@ejgallego, @bhaktishh, + #672, fixes #538) + - Support Visual Studio Live Share URIs better (`vsls://`), in + particular don't try to display goals if the URI is VSLS one + (@ejgallego, #676) + - New `InjectRequire` plugin API for plugins to be able to instrument + the default import list of files (@ejgallego @corwin-of-amber, + #679) + - Add `--max_errors=n` option to `fcc`, this way users can set + `--max_errors=0` to imitate `coqc` behavior (@ejgallego, #680) + - Fix `fcc` exit status when checking terminates with fatal errors + (@ejgallego, @Alizter, #680) + - Fix install to OPAM switches from `main` branch (@ejgallego, #683, + fixes #682, cc #479 #488, thanks to @Hazardouspeach for the report) + - New `--int_backend={Coq,Mp}` command line parameter to select the + interruption method for Coq (@ejgallego, #684) + - Update `package-lock.json` for latest bugfixes (@ejgallego, #687) + - Update Nix flake enviroment (@Alizter, #684 #688) + - Update `prettier` (@Alizter @ejgallego, #684 #688) + - Store original performance data in the cache, so we now display the + original timing and memory data even for cached commands (@ejgallego, #693) + - Fix type errors in the Performance Data Notifications (@ejgallego, + @Alizter, #689, #693) + - Send performance performance data for the full document + (@ejgallego, @Alizter, #689, #693) + - Better types `coq/perfData` call (@ejgallego @Alizter, #689) + - New server option to enable / disable `coq/perfData` (@ejgallego, #689) + - New client option to enable / disable `coq/perfData` (@ejgallego, #717) + - The `coq-lsp.document` VSCode command will now display the returned + JSON data in a new editor (@ejgallego, #701) + - Update server settings on the fly when tweaking them in VSCode. + Implement `workspace/didChangeConfiguration` (@ejgallego, #702) + - [Coq API] Add functions to retrieve list of declarations done in + .vo files (@ejallego, @eytans, #704) + - New `petanque` API to interact directly with Coq's proof + engine. (@ejgallego, @gbdrt, Laetitia Teodorescu #703, thanks to + Alex Sanchez-Stern for many insightful feedback and testing) + - New `petanque` JSON-RPC `pet.exe`, which can be used à la SerAPI + to perform proof search and more (@ejgallego, @gbdrt, #705) + - New `pet-server.exe` TCP server for keep-alive sessions (@gbdrt, + #697) + - Always dispose UI elements. This should improve some strange + behaviors on extension restart (@ejgallego, #708) + - Support Coq meta-commands (Reset, Reset Initial, Back) They are + actually pretty useful to hint the incremental engine to ignore + changes in some part of the document (@ejgallego, #709) + - JSON-RPC library now supports all kind of incoming messages + (@ejgallego, #713) + - New `coq/viewRange` notification, from client to server, than hints + the scheduler for the visible area of the document; combined with + the new lazy checking mode, this provides checking on scroll, a + feature inspired from Isabelle IDE (@ejgallego, #717) + - Have VSCode wait for full LSP client shutdown on server + restart. This fixes some bugs on extension restart (finally!) + (@ejgallego, #719) + - Center the view if cursor goes out of scope in + `sentenceNext/sentencePrevious` (@ejgallego, #718) + - Switch Flèche range encoding to protocol native, this means UTF-16 + code points for now (Léo Stefanesco, @ejgallego, #624, fixes #620, + #621) + - Give `Goals` panel focus back if it has lost it (in case of + multiple panels in the second viewColumn of Vscode) whenever + user navigates proofs (@Alidra @ejgallego, #722, #725) + - `fcc`: new option `--diags_level` to control whether Coq's notice + and info messages appear as diagnostics + - Display the continous/on-request checking mode in the status bar, + allow to change it by clicking on it (@ejgallego, #721) + - Add an example of multiple workspaces (@ejgallego, @Blaisorblade, + #611) + - Don't show types of un-expanded goals. We should add an option for + this, but we don't have the cycles (@ejgallego, #730, workarounds + #525 #652) + - Support for `.lv / .v.tex` TeX files with embedded Coq code + (@ejgallego, #727) + - Don't expand bullet goals at previous levels by default + (@ejgallego, @Alizter, #731 cc #525) + - [petanque] Return basic goal information after `run_tac`, so we + avoid a `goals` round-trip for each tactic (@gbdrt, @ejgallego, + #733) + - [coq] Add support for reading glob files metadata (@ejgallego, + #735) + - [petanque] Return extra premise information: file name, position, + raw_text, using the above support for reading .glob files + (@ejgallego, #735) diff --git a/examples/MetaCommands.v b/examples/MetaCommands.v new file mode 100644 index 00000000..8b54b52d --- /dev/null +++ b/examples/MetaCommands.v @@ -0,0 +1,38 @@ +Lemma foo : 3 = 3. +Proof. now reflexivity. Qed. + +About foo. + +Reset Initial. + +About foo. + +Lemma foo : 2 = 2. +Proof. now reflexivity. Qed. + +Lemma bar : 4 = 4. +Proof. now reflexivity. Qed. + +About bar. +About foo. + +Reset foo. + +About foo. +About bar. + +Lemma muu : 4 = 4. +Proof. +now reflexivity. +Back 2. +now reflexivity. +Qed. + +Reset Initial. + +About muu. +About foo. +About bar. + + + diff --git a/examples/Rtrigo1.v b/examples/Rtrigo1.v index d85678d1..709c177d 100644 --- a/examples/Rtrigo1.v +++ b/examples/Rtrigo1.v @@ -116,7 +116,7 @@ Proof. 2:{ apply pow_nonzero; assumption. } unfold Rsqr; ring. Qed. -Definition muuu := 3. + (**********) Lemma continuity_cos : continuity cos. Proof. diff --git a/examples/chicken.jpg b/examples/chicken.jpg index 0028a92e..7488cd2f 100644 Binary files a/examples/chicken.jpg and b/examples/chicken.jpg differ diff --git a/examples/goals.v b/examples/goals.v index edc3834e..7ebb2d43 100644 --- a/examples/goals.v +++ b/examples/goals.v @@ -52,4 +52,16 @@ About baaar. Lemma err_bullet: Type. _. _ -Qed. \ No newline at end of file +Qed. + +(* Case from https://github.com/ejgallego/coq-lsp/issues/525 *) +Reset Initial. + +Inductive foo := a | b | c | d | e. + +Goal forall x y z w v : foo, Type. +intros []. +- intros []. + + intros []. + * intros []. + -- intros []. \ No newline at end of file diff --git a/examples/int_tc_loop.v b/examples/int_tc_loop.v new file mode 100644 index 00000000..46556b89 --- /dev/null +++ b/examples/int_tc_loop.v @@ -0,0 +1,20 @@ +(* From https://github.com/ejgallego/coq-lsp/issues/484, thanks ! *) +From Coq Require Import Prelude. + +Axiom Loop : Type. +Existing Class Loop. + +Axiom loop : Loop -> Loop. +#[export] Existing Instance loop. + +Global Instance foo : Loop. +Proof. Admitted. + +Goal Loop. +exact _. + +(* Some extra content as to test goals here *) +Lemma foo : True. +Proof. + +Qed. diff --git a/examples/lists.lv b/examples/lists.lv new file mode 100644 index 00000000..53b7d956 --- /dev/null +++ b/examples/lists.lv @@ -0,0 +1,82 @@ +\documentclass{article} + +\usepackage{listings} + +\lstdefinelanguage{Coq} + {morekeywords={Theorem, Definition}} + +\lstnewenvironment{coq} + { + \lstset{ + language=Coq, + basicstyle=\ttfamily, + breaklines=true, + columns=fullflexible} + } + { + } + +\begin{document} + +\section{Welcome to Coq LSP} + +\begin{itemize} +\item You can edit this document as you please +\item Coq will recognize the code snippets as Coq +\item You will be able to save the document and link to other documents soon +\end{itemize} + +\begin{coq} +From Coq Require Import List. +Import ListNotations. +\end{coq} + +\subsection{Here is a simple Proof about Lists} + +$$ + \forall~x~l, + \mathsf{rev}(l \mathrel{++} [x]) = x \mathrel{::} (\mathsf{rev}~l) +$$ + +\begin{coq} +Lemma rev_snoc_cons A : + forall (x : A) (l : list A), rev (l ++ [x]) = x :: rev l. +Proof. + induction l. + - reflexivity. + - simpl. rewrite IHl. simpl. reflexivity. +Qed. +\end{coq} + +\subsection{Here is another proof depending on it} + +Try to update \emph{above} and \textbf{below}: + +\begin{coq} +Theorem rev_rev A : forall (l : list A), rev (rev l) = l. +Proof. + induction l. + - reflexivity. + - simpl. rewrite rev_snoc_cons. rewrite IHl. + reflexivity. +Qed. +\end{coq} + +Please edit your code here! + +\section{Here we do some lambda terms, because we can!} + +\begin{coq} +Inductive term := + | Var : nat -> term + | Abs : term -> term + | Lam : term -> term -> term. +\end{coq} + +\end{document} + + +%%% Local Variables: +%%% mode: LaTeX +%%% TeX-master: "lists" +%%% End: diff --git a/examples/lists.v.tex b/examples/lists.v.tex new file mode 100644 index 00000000..53b7d956 --- /dev/null +++ b/examples/lists.v.tex @@ -0,0 +1,82 @@ +\documentclass{article} + +\usepackage{listings} + +\lstdefinelanguage{Coq} + {morekeywords={Theorem, Definition}} + +\lstnewenvironment{coq} + { + \lstset{ + language=Coq, + basicstyle=\ttfamily, + breaklines=true, + columns=fullflexible} + } + { + } + +\begin{document} + +\section{Welcome to Coq LSP} + +\begin{itemize} +\item You can edit this document as you please +\item Coq will recognize the code snippets as Coq +\item You will be able to save the document and link to other documents soon +\end{itemize} + +\begin{coq} +From Coq Require Import List. +Import ListNotations. +\end{coq} + +\subsection{Here is a simple Proof about Lists} + +$$ + \forall~x~l, + \mathsf{rev}(l \mathrel{++} [x]) = x \mathrel{::} (\mathsf{rev}~l) +$$ + +\begin{coq} +Lemma rev_snoc_cons A : + forall (x : A) (l : list A), rev (l ++ [x]) = x :: rev l. +Proof. + induction l. + - reflexivity. + - simpl. rewrite IHl. simpl. reflexivity. +Qed. +\end{coq} + +\subsection{Here is another proof depending on it} + +Try to update \emph{above} and \textbf{below}: + +\begin{coq} +Theorem rev_rev A : forall (l : list A), rev (rev l) = l. +Proof. + induction l. + - reflexivity. + - simpl. rewrite rev_snoc_cons. rewrite IHl. + reflexivity. +Qed. +\end{coq} + +Please edit your code here! + +\section{Here we do some lambda terms, because we can!} + +\begin{coq} +Inductive term := + | Var : nat -> term + | Abs : term -> term + | Lam : term -> term -> term. +\end{coq} + +\end{document} + + +%%% Local Variables: +%%% mode: LaTeX +%%% TeX-master: "lists" +%%% End: diff --git a/examples/ltac2_simple.v b/examples/ltac2_simple.v new file mode 100644 index 00000000..d8937f45 --- /dev/null +++ b/examples/ltac2_simple.v @@ -0,0 +1,6 @@ +From Ltac2 Require Import Ltac2. + +Goal True /\ True. + split; exact I. +Qed. + diff --git a/examples/multiple_workspaces/README.md b/examples/multiple_workspaces/README.md new file mode 100644 index 00000000..58ebebfc --- /dev/null +++ b/examples/multiple_workspaces/README.md @@ -0,0 +1,42 @@ +# Multiple workspaces setup + +## How to run it: + +Try to load the `example.code-workspace` file in VSCode. + +You may need to compile the right `.vo` files for the imports to +work. You can do that with the `Save VO command`; as of now, `coq-lsp` +will require you do this before opening the depending files. + +`coq-lsp` will take care of this automatically in the next version, +including the auto-update. You can also do: + +```sh +$ coqc -R bar bar bar/barx.y +$ coqc -R foo foo foo/foox.y +``` + +## `coq-lsp` workspace documentation + +One can add multiple folders or roots to a workspace — for instance +via the "Add Folder to Workspace" command (or +[alternatives](https://code.visualstudio.com/docs/editor/multi-root-workspaces#_adding-folders)). + +For each workspace added to a project, `coq-lsp` will try to configure +it by searching for a `_CoqProject` file, then it will apply the +options found there. In the near future, we will also detect +`dune-project` files at the root too. + +`coq-lsp` does determine the workspace roots using the standard +methods provided by the LSP protocol, in particular `wsFolders`, +`rootURI`, and `rootPath` at initialiation, in this order; and by +listening to the `workspace/didChangeWorkspaceFolders` notification +after initialization. + +## Known problems + +When projects are using Coq plugins, `findlib` doesn't properly +support having multiple roots in the same process. We are using a hack +that seems to work (we reinitialize `findlib`), however the hack is +very fragile; we should improve `findlib` upstream to support our use +case. diff --git a/examples/multiple_workspaces/bar/_CoqProject b/examples/multiple_workspaces/bar/_CoqProject new file mode 100644 index 00000000..475f78d8 --- /dev/null +++ b/examples/multiple_workspaces/bar/_CoqProject @@ -0,0 +1 @@ +-R . bar diff --git a/examples/multiple_workspaces/bar/barx.v b/examples/multiple_workspaces/bar/barx.v new file mode 100644 index 00000000..5fcaa519 --- /dev/null +++ b/examples/multiple_workspaces/bar/barx.v @@ -0,0 +1,3 @@ +Definition x := 3. + +Print x. diff --git a/examples/multiple_workspaces/bar/bary.v b/examples/multiple_workspaces/bar/bary.v new file mode 100644 index 00000000..d2fabedf --- /dev/null +++ b/examples/multiple_workspaces/bar/bary.v @@ -0,0 +1,3 @@ +From bar Require Import barx. + +Print x. diff --git a/examples/multiple_workspaces/example.code-workspace b/examples/multiple_workspaces/example.code-workspace new file mode 100644 index 00000000..e72e6f59 --- /dev/null +++ b/examples/multiple_workspaces/example.code-workspace @@ -0,0 +1,27 @@ +{ + "folders": [ + { + "path": "bar" + }, + { + "path": "foo" + } + ], + "settings": { + "files.exclude": { + "**/*.vo": true, + "**/*.vok": true, + "**/*.vos": true, + "**/*.aux": true, + "**/*.glob": true, + "**/.git": true, + "**/.svn": true, + "**/.hg": true, + "**/CVS": true, + "**/.DS_Store": true, + "**/Thumbs.db": true, + "**/*.olean": true, + "out": false + } + } +} \ No newline at end of file diff --git a/examples/multiple_workspaces/foo/_CoqProject b/examples/multiple_workspaces/foo/_CoqProject new file mode 100644 index 00000000..35a0741d --- /dev/null +++ b/examples/multiple_workspaces/foo/_CoqProject @@ -0,0 +1 @@ +-R . foo diff --git a/examples/multiple_workspaces/foo/foox.v b/examples/multiple_workspaces/foo/foox.v new file mode 100644 index 00000000..82ae5066 --- /dev/null +++ b/examples/multiple_workspaces/foo/foox.v @@ -0,0 +1,3 @@ +Definition x := 3. + +Print x. \ No newline at end of file diff --git a/examples/multiple_workspaces/foo/fooy.v b/examples/multiple_workspaces/foo/fooy.v new file mode 100644 index 00000000..c80500f5 --- /dev/null +++ b/examples/multiple_workspaces/foo/fooy.v @@ -0,0 +1,3 @@ +From foo Require Import foox. + +Print x. diff --git a/examples/unicode1.v b/examples/unicode1.v index 27613197..cb0753b9 100644 --- a/examples/unicode1.v +++ b/examples/unicode1.v @@ -7,3 +7,8 @@ Goal forall Γ Δ, Γ ⊆ Δ -> P Γ. (* check goal is updated after the intros here properly *) intros Γ Δ s. foo. +Abort. + +Goal forall Γ Δ, Γ ⊆ Δ -> P Γ. +(* check goal is updated after the intros here properly *) +intros Γ Δ 𝒞. foo. diff --git a/fleche/config.ml b/fleche/config.ml index e8ee723e..2ad0b302 100644 --- a/fleche/config.ml +++ b/fleche/config.ml @@ -52,6 +52,8 @@ type t = (** Experimental setting to check document lazily *) ; send_diags_extra_data : bool [@default false] (** Send extra diagnostic data on the `data` diagnostic field. *) + ; send_serverStatus : bool [@default true] + (** Send server status client notification to the client *) } let default = @@ -75,6 +77,7 @@ let default = ; send_diags = true ; check_only_on_request = false ; send_diags_extra_data = false + ; send_serverStatus = true } let v = ref default diff --git a/fleche/contents.ml b/fleche/contents.ml index 83db8510..bbd73b59 100644 --- a/fleche/contents.ml +++ b/fleche/contents.ml @@ -25,6 +25,18 @@ module Util = struct let nl = l_c - l_p in let nc, padding = if l_p = l_c then (c_c - c_p, 0) else (c_c, o_c - o_p) in String.make padding ' ' ^ String.make nl '\n' ^ String.make nc ' ' + + let extract_raw ~raw ~(range : Lang.Range.t) = + let start = range.start.offset in + let length = range.end_.offset - start in + (* We need to be careful here as Doc.t always adds a last empty node on EOF, + but somehow the offset of this node seems suspicious, it seems like the + Coq parser increases the offset by one, we need to investigate. *) + let length = + if String.length raw < start + length then String.length raw - start + else length + in + String.sub raw start length end module Markdown = struct @@ -45,6 +57,24 @@ module Markdown = struct String.concat "\n" lines end +module LaTeX = struct + let gen l = String.make (String.length l) ' ' + + let rec tex_map_lines coq l = + match l with + | [] -> [] + | l :: ls -> + (* opening vs closing a markdown block *) + let code_marker = if coq then "\\end{coq}" else "\\begin{coq}" in + if String.equal code_marker l then gen l :: tex_map_lines (not coq) ls + else (if coq then l else gen l) :: tex_map_lines coq ls + + let process text = + let lines = String.split_on_char '\n' text in + let lines = tex_map_lines false lines in + String.concat "\n" lines +end + module WaterProof = struct open Fleche_waterproof.Json @@ -112,6 +142,7 @@ let process_contents ~uri ~raw = let ext = Lang.LUri.File.extension uri in match ext with | ".v" -> R.Ok raw + | ".lv" | ".tex" -> R.Ok (LaTeX.process raw) | ".mv" -> R.Ok (Markdown.process raw) | ".wpn" -> WaterProof.process raw | _ -> R.Error "unknown file format" @@ -130,7 +161,7 @@ let get_last_text text = let lines = CString.split_on_char '\n' text |> Array.of_list in let n_lines = Array.length lines in let last_line = if n_lines < 1 then "" else Array.get lines (n_lines - 1) in - let character = Coq.Utf8.length last_line in + let character = Lang.Utf.length_utf16 last_line in (Lang.Point.{ line = n_lines - 1; character; offset }, lines) let make ~uri ~raw = @@ -144,3 +175,5 @@ let make_raw ~raw = let text = raw in let last, lines = get_last_text text in { raw; text; last; lines } + +let extract_raw ~contents:{ raw; _ } ~range = Util.extract_raw ~raw ~range diff --git a/fleche/contents.mli b/fleche/contents.mli index 453ab986..ce6b1fda 100644 --- a/fleche/contents.mli +++ b/fleche/contents.mli @@ -31,3 +31,7 @@ val make : uri:Lang.LUri.File.t -> raw:string -> t R.t (** Make an object of type [t] but don't process the text, this is only used internally to still provide some contents when [make] fails. *) val make_raw : raw:string -> t + +(** [extract_raw contents ~range] Returns the sub-string of the [raw] part of + the document *) +val extract_raw : contents:t -> range:Lang.Range.t -> string diff --git a/fleche/doc.ml b/fleche/doc.ml index 8fdb89dc..657f5c6a 100644 --- a/fleche/doc.ml +++ b/fleche/doc.ml @@ -30,13 +30,13 @@ module Util = struct (if !Config.v.mem_stats then let size = Memo.all_size () in Io.Log.trace "stats" (string_of_int size)); - let stats = Stats.dump () in - Io.Log.trace "cache" (Stats.to_string stats); - Io.Log.trace "cache" (Memo.CacheStats.stats ()); + let stats = Stats.Global.dump () in + Io.Log.trace "cache" (Stats.Global.to_string stats); + Io.Log.trace "cache" (Memo.GlobalCacheStats.stats ()); (* this requires patches to Coq *) (* Io.Log.error "coq parsing" (CoqParsingStats.dump ()); *) (* CoqParsingStats.reset (); *) - Memo.CacheStats.reset (); + Memo.GlobalCacheStats.reset (); Stats.reset () let safe_sub s pos len = @@ -76,29 +76,44 @@ module Node = struct module Info = struct type t = - { cache_hit : bool - ; parsing_time : float - ; time : float option - ; mw_prev : float - ; mw_after : float - ; stats : Stats.t (** Info about cumulative stats *) + { parsing_time : float + ; stats : Memo.Stats.t option + ; global_stats : Stats.Global.t (** Info about cumulative stats *) } - let make ?(cache_hit = false) ~parsing_time ?time ~mw_prev ~mw_after ~stats - () = - { cache_hit; parsing_time; time; mw_prev; mw_after; stats } + let make ~parsing_time ?stats ~global_stats () = + { parsing_time; stats; global_stats } + + let pp_cache_hit fmt = function + | None -> Format.fprintf fmt "N/A" + | Some hit -> Format.fprintf fmt "%b" hit let pp_time fmt = function | None -> Format.fprintf fmt "N/A" | Some time -> Format.fprintf fmt "%.3f" time - let print { cache_hit; parsing_time; time; mw_prev; mw_after; stats } = - let cptime = Stats.get_f stats ~kind:Stats.Kind.Parsing in - let cetime = Stats.get_f stats ~kind:Stats.Kind.Exec in + let pp_words fmt = function + | None -> Format.fprintf fmt "N/A" + | Some memory -> Stats.pp_words fmt memory + + let osplit = function + | None -> (None, None, None) + | Some (x, y, z) -> (Some x, Some y, Some z) + + let print { parsing_time; stats; global_stats } = + let cptime = Stats.Global.get_f global_stats ~kind:Stats.Kind.Parsing in + let cetime = Stats.Global.get_f global_stats ~kind:Stats.Kind.Exec in + let cache_hit, time, memory = + Option.map + (fun (s : Memo.Stats.t) -> + (s.cache_hit, s.stats.time, s.stats.memory)) + stats + |> osplit + in Format.asprintf - "Cached: %b | P: %.3f / %.2f | E: %a / %.2f | M: %a | Diff: %a" - cache_hit parsing_time cptime pp_time time cetime Stats.pp_words - mw_after Stats.pp_words (mw_after -. mw_prev) + "Cached: %a | P: %.3f / %.2f | E: %a / %.2f | Mem-Diff: %a" pp_cache_hit + cache_hit parsing_time cptime.time pp_time time cetime.time pp_words + memory end module Message = struct @@ -110,6 +125,7 @@ module Node = struct type t = { range : Lang.Range.t + ; prev : t option ; ast : Ast.t option (** Ast of node *) ; state : Coq.State.t (** (Full) State of node *) ; diags : Lang.Diagnostic.t list @@ -266,7 +282,7 @@ type t = ; completed : Completion.t (** Status of the document, usually either completed, suspended, or waiting for some IO / external event *) - ; toc : Lang.Range.t CString.Map.t (** table of contents *) + ; toc : Node.t CString.Map.t (** table of contents *) ; env : Env.t (** External document enviroment *) ; root : Coq.State.t (** [root] contains the first state document state, obtained by applying @@ -279,22 +295,23 @@ let asts doc = List.filter_map Node.ast doc.nodes let diags doc = List.concat_map (fun node -> node.Node.diags) doc.nodes (* TOC handling *) -let rec add_toc_info toc { Lang.Ast.Info.name; range; children; _ } = +let rec add_toc_info node toc { Lang.Ast.Info.name; children; _ } = let toc = match name.v with | None -> toc - | Some id -> CString.Map.add id range toc + | Some id -> CString.Map.add id node toc in - Option.cata (List.fold_left add_toc_info toc) toc children + Option.cata (List.fold_left (add_toc_info node) toc) toc children -let update_toc_info toc ast_info = List.fold_left add_toc_info toc ast_info +let update_toc_info toc ast_info node = + List.fold_left (add_toc_info node) toc ast_info let update_toc_node toc node = match Node.ast node with | None -> toc | Some { Node.Ast.ast_info = None; _ } -> toc | Some { Node.Ast.ast_info = Some ast_info; _ } -> - update_toc_info toc ast_info + update_toc_info toc ast_info node let rebuild_toc nodes = List.fold_left update_toc_node CString.Map.empty nodes @@ -311,22 +328,20 @@ let drange = let end_ = Point.{ line = 0; character = 1; offset = 1 } in Range.{ start; end_ } -let process_init_feedback ~lines ~stats state feedback = +let process_init_feedback ~lines ~stats ~global_stats state feedback = let messages = List.map (Node.Message.feedback_to_message ~lines) feedback in if not (CList.is_empty messages) then let diags, messages = Diags.of_messages ~drange messages in let parsing_time = 0.0 in - let { Gc.major_words = mw_prev; _ } = Gc.quick_stat () in - let info = - Node.Info.make ~parsing_time ~mw_prev ~mw_after:mw_prev ~stats () - in + let info = Node.Info.make ~parsing_time ?stats ~global_stats () in let range = drange in - [ { Node.range; ast = None; state; diags; messages; info } ] + let prev = None in + [ { Node.range; prev; ast = None; state; diags; messages; info } ] else [] (* Memoized call to [Coq.Init.doc_init] *) let mk_doc ~token ~env ~uri = - Memo.Init.eval ~token (env.Env.init, env.workspace, uri) + Memo.Init.evalS ~token (env.Env.init, env.workspace, uri) (* Create empty doc, in state [~completed] *) let empty_doc ~uri ~contents ~version ~env ~root ~nodes ~completed = @@ -350,17 +365,20 @@ let conv_error_doc ~raw ~uri ~version ~env ~root ~completed err = let err = (None, Diags.err, Pp.(str "Error in document conversion: " ++ str err)) in - let stats = Stats.dump () in - let nodes = process_init_feedback ~lines ~stats root [ err ] in + (* No execution to add *) + let stats = None in + let global_stats = Stats.Global.dump () in + let nodes = process_init_feedback ~lines ~stats ~global_stats root [ err ] in empty_doc ~uri ~version ~env ~root ~nodes ~completed ~contents let create ~token ~env ~uri ~version ~contents = let () = Stats.reset () in - let root = mk_doc ~token ~env ~uri in - Coq.Protect.E.map root ~f:(fun root -> - let nodes = [] in - let completed range = Completion.Stopped range in - empty_doc ~uri ~contents ~version ~env ~root ~nodes ~completed) + let root, stats = mk_doc ~token ~env ~uri in + ( Coq.Protect.E.map root ~f:(fun root -> + let nodes = [] in + let completed range = Completion.Stopped range in + empty_doc ~uri ~contents ~version ~env ~root ~nodes ~completed) + , stats ) (** Create a permanently failed doc, to be removed when we drop 8.16 support *) let handle_failed_permanent ~env ~uri ~version ~contents = @@ -369,10 +387,12 @@ let handle_failed_permanent ~env ~uri ~version ~contents = let doc, feedback = error_doc ~loc ~message ~uri ~contents ~version ~env ~completed in - let stats = Stats.dump () in + let stats = None in + let global_stats = Stats.Global.dump () in let nodes = let lines = contents.Contents.lines in - process_init_feedback ~lines ~stats env.Env.init feedback @ doc.nodes + process_init_feedback ~lines ~stats ~global_stats env.Env.init feedback + @ doc.nodes in let diags_dirty = not (CList.is_empty nodes) in { doc with nodes; diags_dirty } @@ -382,7 +402,7 @@ let handle_failed_permanent ~env ~uri ~version ~contents = the initial document. *) let handle_doc_creation_exec ~token ~env ~uri ~version ~contents = let completed range = Completion.Failed range in - let { Coq.Protect.E.r; feedback } = + let { Coq.Protect.E.r; feedback }, stats = create ~token ~env ~uri ~version ~contents in let doc, extra_feedback = @@ -400,10 +420,12 @@ let handle_doc_creation_exec ~token ~env ~uri ~version ~contents = | Completed (Ok doc) -> (doc, []) in let state = doc.root in - let stats = Stats.dump () in + let stats = Some stats in + let global_stats = Stats.Global.dump () in let nodes = let lines = contents.Contents.lines in - process_init_feedback ~lines ~stats state (feedback @ extra_feedback) + process_init_feedback ~lines ~stats ~global_stats state + (feedback @ extra_feedback) @ doc.nodes in let diags_dirty = not (CList.is_empty nodes) in @@ -651,22 +673,56 @@ end = struct | Completed (Error _) -> st end -let interp_and_info ~st ~files ast = +let interp_and_info ~token ~st ~files ast = match Coq.Ast.Require.extract ast with - | None -> Memo.Interp.evalS (st, ast) - | Some ast -> Memo.Require.evalS (st, files, ast) - -let interp_and_info ~token ~parsing_time ~st ~files 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 } = - interp_and_info ~token ~st ~files ast - in - let { Gc.major_words = mw_after; _ } = Gc.quick_stat () in - let stats = Stats.dump () in - let info = - Node.Info.make ~cache_hit ~parsing_time ~time ~mw_prev ~mw_after ~stats () + | None -> Memo.Interp.evalS ~token (st, ast) + | Some ast -> Memo.Require.evalS ~token (st, files, ast) + +(* Support for meta-commands, a bit messy, but cool in itself *) +let search_node ~command ~doc = + let nstats (node : Node.t option) = + Option.cata + (fun (node : Node.t) -> Option.default Memo.Stats.zero node.info.stats) + Memo.Stats.zero node in + match command with + | Coq.Ast.Meta.Command.Back num -> ( + match Base.List.nth doc.nodes num with + | None -> + let ll = List.length doc.nodes in + let message = + Pp.( + str "not enough nodes: [" ++ int num ++ str " > " ++ int ll + ++ str "] available document nodes") + in + (Coq.Protect.E.error message, nstats None) + | Some node -> (Coq.Protect.E.ok node.state, nstats (Some node))) + | ResetName id -> ( + let toc = doc.toc in + let id = Names.Id.to_string id.v in + match CString.Map.find_opt id toc with + | None -> + ( Coq.Protect.E.error Pp.(str "identifier " ++ str id ++ str " not found") + , Memo.Stats.zero ) + | Some node -> + let node = Option.default node node.prev in + (Coq.Protect.E.ok node.state, nstats (Some node))) + | ResetInitial -> (Coq.Protect.E.ok doc.root, nstats None) + +let interp_and_info ~token ~st ~files ~doc ast = + match Coq.Ast.Meta.extract ast with + | None -> interp_and_info ~token ~st ~files ast + | Some { command; loc = _; attrs = _; control = _ } -> + (* That's an interesting point, for now we don't measure time Flèche is + spending on error recovery and meta stuff, we should record that time + actually at some point too. In this case, maybe we could recover the + cache hit from the original node? *) + search_node ~command ~doc + +let interp_and_info ~token ~parsing_time ~st ~files ~doc ast = + let res, stats = interp_and_info ~token ~st ~files ~doc ast in + let global_stats = Stats.Global.dump () in + let info = Node.Info.make ~parsing_time ~stats ~global_stats () in (res, info) type parse_action = @@ -679,9 +735,10 @@ type parse_action = (* Returns parse_action, diags, parsing_time *) let parse_action ~token ~lines ~st last_tok doc_handle = let start_loc = Coq.Parsing.Parsable.loc doc_handle |> CLexer.after in - let parse_res, time = parse_stm ~token ~st doc_handle in + let parse_res, stats = parse_stm ~token ~st doc_handle in let f = Coq.Utils.to_range ~lines in let { Coq.Protect.E.r; feedback } = Coq.Protect.E.map_loc ~f parse_res in + let { Stats.time; memory = _ } = stats in match r with | Coq.Protect.R.Interrupted -> (EOF (Stopped last_tok), [], feedback, time) | Coq.Protect.R.Completed res -> ( @@ -721,16 +778,14 @@ type document_action = } | Interrupted of Lang.Range.t -let unparseable_node ~range ~parsing_diags ~parsing_feedback ~state +let unparseable_node ~range ~prev ~parsing_diags ~parsing_feedback ~state ~parsing_time = let fb_diags, messages = Diags.of_messages ~drange:range parsing_feedback in let diags = fb_diags @ parsing_diags in - let stats = Stats.dump () in - let { Gc.major_words = mw_prev; _ } = Gc.quick_stat () in - let info = - Node.Info.make ~parsing_time ~mw_prev ~mw_after:mw_prev ~stats () - in - { Node.range; ast = None; diags; messages; state; info } + let stats = None in + let global_stats = Stats.Global.dump () in + let info = Node.Info.make ~parsing_time ?stats ~global_stats () in + { Node.range; prev; ast = None; diags; messages; state; info } let assemble_diags ~range ~parsing_diags ~parsing_feedback ~diags ~feedback = let parsing_fb_diags, parsing_messages = @@ -741,24 +796,24 @@ let assemble_diags ~range ~parsing_diags ~parsing_feedback ~diags ~feedback = let messages = parsing_messages @ fb_messages in (diags, messages) -let parsed_node ~range ~ast ~state ~parsing_diags ~parsing_feedback ~diags +let parsed_node ~range ~prev ~ast ~state ~parsing_diags ~parsing_feedback ~diags ~feedback ~info = let diags, messages = assemble_diags ~range ~parsing_diags ~parsing_feedback ~diags ~feedback in - { Node.range; ast = Some ast; diags; messages; state; info } + { Node.range; prev; ast = Some ast; diags; messages; state; info } 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 ~lines ~token ~doc ~range ~ast ~st ~parsing_diags +let node_of_coq_result ~lines ~token ~doc ~range ~prev ~ast ~st ~parsing_diags ~parsing_feedback ~feedback ~info last_tok res = match res with | Ok state -> let node = - parsed_node ~range ~ast ~state ~parsing_diags ~parsing_feedback ~diags:[] - ~feedback ~info + parsed_node ~range ~prev ~ast ~state ~parsing_diags ~parsing_feedback + ~diags:[] ~feedback ~info in Continue { state; last_tok; node } | Error (Coq.Protect.Error.Anomaly (err_range, msg) as coq_err) @@ -771,20 +826,20 @@ let node_of_coq_result ~lines ~token ~doc ~range ~ast ~st ~parsing_diags in let recovery_st = Recovery.handle ~token ~context ~st in let node = - parsed_node ~range ~ast ~state:recovery_st ~parsing_diags + parsed_node ~range ~prev ~ast ~state:recovery_st ~parsing_diags ~parsing_feedback ~diags:err_diags ~feedback ~info in strategy_of_coq_err ~node ~state:recovery_st ~last_tok coq_err (* Build a document node, possibly executing *) let document_action ~token ~st ~parsing_diags ~parsing_feedback ~parsing_time - ~doc last_tok doc_handle action = + ~prev ~doc last_tok doc_handle action = match action with (* End of file *) | EOF completed -> let range = Completion.range completed in let node = - unparseable_node ~range ~parsing_diags ~parsing_feedback ~state:st + unparseable_node ~range ~prev ~parsing_diags ~parsing_feedback ~state:st ~parsing_time in Stop (completed, node) @@ -795,7 +850,7 @@ let document_action ~token ~st ~parsing_diags ~parsing_feedback ~parsing_time in let st = Recovery.handle ~token ~context ~st in let node = - unparseable_node ~range:span_range ~parsing_diags ~parsing_feedback + unparseable_node ~range:span_range ~prev ~parsing_diags ~parsing_feedback ~state:st ~parsing_time in Continue { state = st; last_tok; node } @@ -803,7 +858,7 @@ let document_action ~token ~st ~parsing_diags ~parsing_feedback ~parsing_time | Process ast -> ( let lines, files = (doc.contents.lines, doc.env.files) in let process_res, info = - interp_and_info ~token ~parsing_time ~st ~files ast + interp_and_info ~token ~parsing_time ~st ~files ~doc ast in let f = Coq.Utils.to_range ~lines in let { Coq.Protect.E.r; feedback } = Coq.Protect.E.map_loc ~f process_res in @@ -821,7 +876,7 @@ let document_action ~token ~st ~parsing_diags ~parsing_feedback ~parsing_time this point then, hence the new last valid token last_tok_new *) let last_tok_new = Coq.Parsing.Parsable.loc doc_handle in let last_tok_new = Coq.Utils.to_range ~lines last_tok_new in - node_of_coq_result ~lines ~token ~doc ~range:ast_range ~ast ~st + node_of_coq_result ~lines ~token ~doc ~range:ast_range ~prev ~ast ~st ~parsing_diags ~parsing_feedback ~feedback ~info last_tok_new res) module Target = struct @@ -849,10 +904,10 @@ let log_beyond_target last_tok target = ("target reached " ^ Lang.Range.to_string last_tok); Io.Log.trace "beyond_target" ("target is " ^ pr_target target) -let max_errors_node ~state ~range = +let max_errors_node ~state ~range ~prev = let msg = Pp.str "Maximum number of errors reached" in let parsing_diags = [ Diags.make range Diags.err msg ] in - unparseable_node ~range ~parsing_diags ~parsing_feedback:[] ~state + unparseable_node ~range ~prev ~parsing_diags ~parsing_feedback:[] ~state ~parsing_time:0.0 module Stop_cond = struct @@ -869,7 +924,7 @@ end (* main interpretation loop *) let process_and_parse ~io ~token ~target ~uri ~version doc last_tok doc_handle = - let rec stm doc st (last_tok : Lang.Range.t) acc_errors = + let rec stm doc st (last_tok : Lang.Range.t) prev acc_errors = (* Reporting of progress and diagnostics (if dirty) *) let doc = send_eager_diagnostics ~io ~uri ~version ~doc in report_progress ~io ~doc last_tok; @@ -877,7 +932,7 @@ let process_and_parse ~io ~token ~target ~uri ~version doc last_tok doc_handle = match Stop_cond.should_stop acc_errors last_tok target with | Max_errors -> let completed = Completion.Failed last_tok in - let node = max_errors_node ~state:st ~range:last_tok in + let node = max_errors_node ~state:st ~range:last_tok ~prev in let doc = add_node ~node doc in set_completion ~completed doc | Target -> @@ -898,7 +953,7 @@ let process_and_parse ~io ~token ~target ~uri ~version doc last_tok doc_handle = (* Execution *) let action = document_action ~token ~st ~parsing_diags ~parsing_feedback - ~parsing_time ~doc last_tok doc_handle action + ~parsing_time ~prev ~doc last_tok doc_handle action in match action with | Interrupted last_tok -> set_completion ~completed:(Stopped last_tok) doc @@ -910,7 +965,7 @@ let process_and_parse ~io ~token ~target ~uri ~version doc last_tok doc_handle = | Continue { state; last_tok; node } -> let n_errors = CList.count Lang.Diagnostic.is_error node.Node.diags in let doc = add_node ~node doc in - stm doc state last_tok (acc_errors + n_errors)) + stm doc state last_tok (Some node) (acc_errors + n_errors)) in (* Reporting of progress and diagnostics (if stopped or failed, if completed the doc manager will take care of it) *) @@ -931,12 +986,13 @@ let process_and_parse ~io ~token ~target ~uri ~version doc last_tok doc_handle = let last_node = Util.hd_opt doc.nodes in let st, stats = Option.cata - (fun { Node.state; info = { stats; _ }; _ } -> (state, stats)) - (doc.root, Stats.zero ()) + (fun { Node.state; info = { global_stats; _ }; _ } -> + (state, global_stats)) + (doc.root, Stats.Global.zero ()) last_node in - Stats.restore stats; - let doc = stm doc st last_tok 0 in + Stats.Global.restore stats; + let doc = stm doc st last_tok last_node 0 in (* Set the document to "finished" mode: reverse the node list *) let doc = { doc with nodes = List.rev doc.nodes } in doc @@ -962,9 +1018,7 @@ let loc_after ~lines ~uri (r : Lang.Range.t) = let end_index = let line = Array.get lines r.end_.line in debug_loc_after line r; - match Coq.Utf8.index_of_char ~line ~char:r.end_.character with - | None -> String.length line - | Some index -> index + Lang.Utf.utf8_offset_of_utf16_offset ~line ~offset:r.end_.character in let bol_pos_last = r.end_.offset - end_index in { Loc.fname = init_fname ~uri @@ -1024,5 +1078,4 @@ let save ~token ~doc = () | _ -> let error = Pp.(str "Can't save document that failed to check") in - let r = Coq.Protect.R.error error in - Coq.Protect.E.{ r; feedback = [] } + Coq.Protect.E.error error diff --git a/fleche/doc.mli b/fleche/doc.mli index 9eeb7c50..2d1d206c 100644 --- a/fleche/doc.mli +++ b/fleche/doc.mli @@ -14,13 +14,10 @@ module Node : sig end module Info : sig - type t = private - { cache_hit : bool - ; parsing_time : float - ; time : float option - ; mw_prev : float - ; mw_after : float - ; stats : Stats.t (** Info about cumulative stats *) + type t = + { parsing_time : float + ; stats : Memo.Stats.t option + ; global_stats : Stats.Global.t (** Info about cumulative stats *) } val print : t -> string @@ -32,6 +29,7 @@ module Node : sig type t = private { range : Lang.Range.t + ; prev : t option ; ast : Ast.t option (** Ast of node *) ; state : Coq.State.t (** (Full) State of node *) ; diags : Lang.Diagnostic.t list (** Diagnostics associated to the node *) @@ -85,7 +83,7 @@ type t = private ; completed : Completion.t (** Status of the document, usually either completed, suspended, or waiting for some IO / external event *) - ; toc : Lang.Range.t CString.Map.t (** table of contents *) + ; toc : Node.t CString.Map.t (** table of contents *) ; env : Env.t (** External document enviroment *) ; root : Coq.State.t (** [root] contains the first state document state, obtained by applying diff --git a/fleche/io.ml b/fleche/io.ml index 0a4c34f1..1f376f2b 100644 --- a/fleche/io.ml +++ b/fleche/io.ml @@ -19,6 +19,8 @@ module CallBack = struct ; fileProgress : uri:Lang.LUri.File.t -> version:int -> Progress.Info.t list -> unit ; perfData : uri:Lang.LUri.File.t -> version:int -> Perf.t -> unit + ; serverVersion : ServerInfo.Version.t -> unit + ; serverStatus : ServerInfo.Status.t -> unit } let default = @@ -27,6 +29,8 @@ module CallBack = struct ; diagnostics = (fun ~uri:_ ~version:_ _ -> ()) ; fileProgress = (fun ~uri:_ ~version:_ _ -> ()) ; perfData = (fun ~uri:_ ~version:_ _ -> ()) + ; serverVersion = (fun _ -> ()) + ; serverStatus = (fun _ -> ()) } let cb = ref default @@ -52,4 +56,6 @@ module Report = struct io.CallBack.fileProgress ~uri ~version d let perfData ~io ~uri ~version pd = io.CallBack.perfData ~uri ~version pd + let serverVersion ~io vi = io.CallBack.serverVersion vi + let serverStatus ~io st = io.CallBack.serverStatus st end diff --git a/fleche/io.mli b/fleche/io.mli index fefc30ee..822c3710 100644 --- a/fleche/io.mli +++ b/fleche/io.mli @@ -23,6 +23,8 @@ module CallBack : sig ; fileProgress : uri:Lang.LUri.File.t -> version:int -> Progress.Info.t list -> unit ; perfData : uri:Lang.LUri.File.t -> version:int -> Perf.t -> unit + ; serverVersion : ServerInfo.Version.t -> unit + ; serverStatus : ServerInfo.Status.t -> unit } val set : t -> unit @@ -56,4 +58,7 @@ module Report : sig val perfData : io:CallBack.t -> uri:Lang.LUri.File.t -> version:int -> Perf.t -> unit + + val serverVersion : io:CallBack.t -> ServerInfo.Version.t -> unit + val serverStatus : io:CallBack.t -> ServerInfo.Status.t -> unit end diff --git a/fleche/memo.ml b/fleche/memo.ml index 11c84c76..a288f8aa 100644 --- a/fleche/memo.ml +++ b/fleche/memo.ml @@ -1,21 +1,27 @@ module CS = Stats module Stats = struct - type 'a t = - { res : 'a - ; cache_hit : bool - ; memory : int - ; time : float + type t = + { stats : Stats.t + ; time_hash : float + (** Time in hashing consumed in the original execution *) + ; cache_hit : bool (** Whether we had a cache hit *) } - let make ?(cache_hit = false) ~time res = - (* This is quite slow! *) + let make ~stats ?(cache_hit = false) ~time_hash () = + (* This is quite slow, to the point it is not really usable, but a more + precise option *) (* let memory = Obj.magic res |> Obj.reachable_words in *) - let memory = 0 in - { res; cache_hit; memory; time } + { stats; time_hash; cache_hit } + + let zero = + { stats = { Stats.time = 0.0; memory = 0.0 } + ; time_hash = 0.0 + ; cache_hit = false + } end -module CacheStats = struct +module GlobalCacheStats = struct let nhit, ntotal = (ref 0, ref 0) let reset () = @@ -50,12 +56,15 @@ module MemoTable = struct val clear : 'a t -> unit val add_execution : - ('a, 'l) Coq.Protect.E.t t -> key -> ('a, 'l) Coq.Protect.E.t -> unit + (('a, 'l) Coq.Protect.E.t * 'b) t + -> key + -> ('a, 'l) Coq.Protect.E.t * 'b + -> unit val add_execution_loc : - ('v * ('a, 'l) Coq.Protect.E.t) t + ('v * ('a, 'l) Coq.Protect.E.t * 'b) t -> key - -> 'v * ('a, 'l) Coq.Protect.E.t + -> 'v * ('a, 'l) Coq.Protect.E.t * 'b -> unit (** sorted *) @@ -87,12 +96,12 @@ module MemoTable = struct to_seq_values count |> List.of_seq |> List.sort (fun x y -> -Int.compare x y) - let add_execution t k ({ Coq.Protect.E.r; _ } as v) = + let add_execution t k (({ Coq.Protect.E.r; _ }, _) as v) = match r with | Coq.Protect.R.Interrupted -> () | _ -> add t k v - let add_execution_loc t k ((_, { Coq.Protect.E.r; _ }) as v) = + let add_execution_loc t k ((_, { Coq.Protect.E.r; _ }, _) as v) = match r with | Coq.Protect.R.Interrupted -> () | _ -> add t k v @@ -163,7 +172,9 @@ module type S = sig (** [eval i] Eval an input [i] and produce stats *) val evalS : - token:Coq.Limits.Token.t -> input -> (output, Loc.t) Coq.Protect.E.t Stats.t + token:Coq.Limits.Token.t + -> input + -> (output, Loc.t) Coq.Protect.E.t * Stats.t (** [size ()] Return the cache size in words, expensive *) val size : unit -> int @@ -191,28 +202,22 @@ module SEval (E : EvalType) : let all_freqs = HC.all_freqs let clear () = HC.clear cache - let eval ~token v = - match HC.find_opt cache v with - | None -> - let res = E.eval ~token v in - HC.add_execution cache v res; - res - | Some cached_res -> cached_res - let in_cache i = let kind = CS.Kind.Hashing in CS.record ~kind ~f:(HC.find_opt cache) i let evalS ~token i = match in_cache i with - | Some cached_res, time -> Stats.make ~cache_hit:true ~time cached_res - | None, time_hash -> + | Some (cached_res, stats), { time = time_hash; memory = _ } -> + (cached_res, Stats.make ~stats ~cache_hit:true ~time_hash ()) + | None, { time = time_hash; memory = _ } -> let kind = CS.Kind.Exec in let f i = E.eval ~token i in - let res, time_interp = CS.record ~kind ~f i in - let () = HC.add_execution cache i res in - let time = time_hash +. time_interp in - Stats.make ~cache_hit:false ~time res + let res, stats = CS.record ~kind ~f i in + let () = HC.add_execution cache i (res, stats) in + (res, Stats.make ~stats ~cache_hit:false ~time_hash ()) + + let eval ~token i = evalS ~token i |> fst end module type LocEvalType = sig @@ -229,7 +234,7 @@ module CEval (E : LocEvalType) = struct module Result = struct (* We store the location as to compute an offset for cached results *) - type t = Loc.t * (E.output, Loc.t) Coq.Protect.E.t + type t = Loc.t * (E.output, Loc.t) Coq.Protect.E.t * CS.t end type cache = Result.t HC.t @@ -246,24 +251,23 @@ module CEval (E : LocEvalType) = struct let kind = CS.Kind.Hashing in CS.record ~kind ~f:(HC.find_opt cache) i - let evalS ~token i : _ Stats.t = + let evalS ~token i = let stm_loc = E.loc_of_input i in match in_cache i with - | Some (cached_loc, res), time -> + | Some (cached_loc, res, stats), { time = time_hash; memory = _ } -> if Debug.cache then Io.Log.trace "memo" "cache hit"; - CacheStats.hit (); + GlobalCacheStats.hit (); let res = Loc_utils.adjust_offset ~stm_loc ~cached_loc res in - Stats.make ~cache_hit:true ~time res - | None, time_hash -> + (res, Stats.make ~stats ~cache_hit:true ~time_hash ()) + | None, { time = time_hash; memory = _ } -> if Debug.cache then Io.Log.trace "memo" "cache miss"; - CacheStats.miss (); + GlobalCacheStats.miss (); let kind = CS.Kind.Exec in - let res, time_interp = CS.record ~kind ~f:(E.eval ~token) i in - let () = HC.add_execution_loc cache i (stm_loc, res) in - let time = time_hash +. time_interp in - Stats.make ~time res + let res, stats = CS.record ~kind ~f:(E.eval ~token) i in + let () = HC.add_execution_loc cache i (stm_loc, res, stats) in + (res, Stats.make ~stats ~cache_hit:false ~time_hash ()) - let eval ~token i = (evalS ~token i).res + let eval ~token i = evalS ~token i |> fst end module VernacEval = struct diff --git a/fleche/memo.mli b/fleche/memo.mli index 22b167cc..205385c5 100644 --- a/fleche/memo.mli +++ b/fleche/memo.mli @@ -1,10 +1,12 @@ module Stats : sig - type 'a t = - { res : 'a - ; cache_hit : bool - ; memory : int - ; time : float + type t = + { stats : Stats.t + ; time_hash : float + (** Time in hashing consumed in the original execution *) + ; cache_hit : bool (** Whether we had a cache hit *) } + + val zero : t end (** Flèche memo / cache tables, with some advanced features *) @@ -20,7 +22,9 @@ module type S = sig (** [eval i] Eval an input [i] and produce stats *) val evalS : - token:Coq.Limits.Token.t -> input -> (output, Loc.t) Coq.Protect.E.t Stats.t + token:Coq.Limits.Token.t + -> input + -> (output, Loc.t) Coq.Protect.E.t * Stats.t (** [size ()] Return the cache size in words, expensive *) val size : unit -> int @@ -56,7 +60,7 @@ module Require : (** Admit evaluation cache *) module Admit : S with type input = Coq.State.t and type output = Coq.State.t -module CacheStats : sig +module GlobalCacheStats : sig val reset : unit -> unit (** Returns the hit ratio of the cache, etc... *) diff --git a/fleche/perf.ml b/fleche/perf.ml index 346829ac..7f434a2c 100644 --- a/fleche/perf.ml +++ b/fleche/perf.ml @@ -5,11 +5,20 @@ (* Written by: Emilio J. Gallego Arias *) (************************************************************************) +module Info = struct + type t = + { time : float (** Original Execution Time (when not cached) *) + ; memory : float + (** Difference in words allocated in the heap using `Gc.quick_stat` *) + ; cache_hit : bool (** was the sentence cached? *) + ; time_hash : float (** Memo timing overhead *) + } +end + module Sentence = struct type t = - { loc : Lang.Range.t - ; time : float - ; mem : float + { range : Lang.Range.t + ; info : Info.t } end diff --git a/fleche/perf.mli b/fleche/perf.mli index 5e8bb57a..b743f30f 100644 --- a/fleche/perf.mli +++ b/fleche/perf.mli @@ -5,11 +5,20 @@ (* Written by: Emilio J. Gallego Arias *) (************************************************************************) +module Info : sig + type t = + { time : float (** Original Execution Time (when not cached) *) + ; memory : float + (** Difference in words allocated in the heap using `Gc.quick_stat` *) + ; cache_hit : bool (** was the sentence cached? *) + ; time_hash : float (** Memo timing overhead *) + } +end + module Sentence : sig type t = - { loc : Lang.Range.t - ; time : float - ; mem : float + { range : Lang.Range.t + ; info : Info.t } end diff --git a/fleche/perf_analysis.ml b/fleche/perf_analysis.ml index 158c97b0..bc82cfda 100644 --- a/fleche/perf_analysis.ml +++ b/fleche/perf_analysis.ml @@ -4,20 +4,38 @@ let rec list_take n = function | [] -> [] | x :: xs -> if n = 0 then [] else x :: list_take (n - 1) xs -let mk_loc_time (n : Doc.Node.t) = - let time = Option.default 0.0 n.info.time in - let mem = n.info.mw_after -. n.info.mw_prev in - let loc = n.Doc.Node.range in - Sentence.{ loc; time; mem } +let mk_info (n : Doc.Node.t) = + let time, memory, cache_hit, time_hash = + Option.cata + (fun (stats : Memo.Stats.t) -> + (stats.stats.time, stats.stats.memory, stats.cache_hit, stats.time_hash)) + (0.0, 0.0, false, 0.0) n.info.stats + in + Info.{ time; memory; cache_hit; time_hash } + +let mk_sentence (n : Doc.Node.t) = + let range = n.range in + let info = mk_info n in + Sentence.{ range; info } let get_stats ~(doc : Doc.t) = match List.rev doc.nodes with - | [] -> "no stats" - | n :: _ -> Stats.to_string n.info.stats + | [] -> "no global stats" + | n :: _ -> Stats.Global.to_string n.info.global_stats (** Turn into a config option at some point? This is very expensive *) let display_cache_size = false +let node_time_compare (n1 : Doc.Node.t) (n2 : Doc.Node.t) = + match (n1.info.stats, n2.info.stats) with + | Some s1, Some s2 -> -compare s1.stats.time s2.stats.time + | None, Some _ -> 1 + | Some _, None -> -1 + | None, None -> 0 + +(* Old mode of sending only the 10 hotspots *) +let hotspot = false + let make (doc : Doc.t) = let n_stm = List.length doc.nodes in let stats = get_stats ~doc in @@ -28,11 +46,9 @@ let make (doc : Doc.t) = Format.asprintf "{ num sentences: %d@\n; stats: %s; cache: %a@\n}" n_stm stats Stats.pp_words cache_size in - let top = - List.stable_sort - (fun (n1 : Doc.Node.t) n2 -> compare n2.info.time n1.info.time) - doc.nodes + let timings = + if hotspot then List.stable_sort node_time_compare doc.nodes |> list_take 10 + else doc.nodes in - let top = list_take 10 top in - let timings = List.map mk_loc_time top in + let timings = List.map mk_sentence timings in { summary; timings } diff --git a/fleche/serverInfo.ml b/fleche/serverInfo.ml new file mode 100644 index 00000000..85c8b8c4 --- /dev/null +++ b/fleche/serverInfo.ml @@ -0,0 +1,21 @@ +(************************************************************************) +(* Coq Language Server Protocol *) +(* Copyright 2019 MINES ParisTech -- Dual License LGPL 2.1 / GPL3+ *) +(* Copyright 2019-202r Inria -- Dual License LGPL 2.1 / GPL3+ *) +(* Written by: Emilio J. Gallego Arias *) +(************************************************************************) + +module Version = struct + type t = + { coq : string + ; ocaml : string + ; coq_lsp : string + } +end + +module Status = struct + type t = + | Stopped + | Idle of string (* memory use *) + | Running of string (* modname *) +end diff --git a/fleche/stats.ml b/fleche/stats.ml index 2ef7e5c8..ce37eeb9 100644 --- a/fleche/stats.ml +++ b/fleche/stats.ml @@ -14,44 +14,59 @@ module Kind = struct | Exec end -let stats = Hashtbl.create 1000 -let find kind = Hashtbl.find_opt stats kind |> Option.default 0.0 +type t = + { time : float + ; memory : float + } -type t = float * float * float +let stats : (Kind.t, t) Hashtbl.t = Hashtbl.create 1000 +let z = { time = 0.0; memory = 0.0 } +let find kind = Hashtbl.find_opt stats kind |> Option.default z -let zero () = (0.0, 0.0, 0.0) -let dump () = (find Kind.Hashing, find Kind.Parsing, find Kind.Exec) +module Global = struct + type nonrec 'a stats = t + type nonrec t = t * t * t -let restore (h, p, e) = - Hashtbl.replace stats Kind.Hashing h; - Hashtbl.replace stats Kind.Parsing p; - Hashtbl.replace stats Kind.Exec e + let zero () = (z, z, z) + let dump () = (find Kind.Hashing, find Kind.Parsing, find Kind.Exec) -let get_f (h, p, e) ~kind = - match kind with - | Kind.Hashing -> h - | Parsing -> p - | Exec -> e + 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 get_f (h, p, e) ~kind = + match kind with + | Kind.Hashing -> h + | Parsing -> p + | Exec -> e + + let to_string (h, p, e) = + Format.asprintf "hashing: %f | parsing: %f | exec: %f" h.time p.time e.time +end + +let bump kind { time; memory } = let acc = find kind in - Hashtbl.replace stats kind (acc +. time) + let time = acc.time +. time in + let memory = acc.memory +. memory in + Hashtbl.replace stats kind { time; memory } -let time f x = +let time_and_mem f x = + let { Gc.major_words = mw_prev; _ } = Gc.quick_stat () in let before = Unix.gettimeofday () in - let res = f x in + let v = f x in let after = Unix.gettimeofday () in - (res, after -. before) + let { Gc.major_words = mw_after; _ } = Gc.quick_stat () in + let time = after -. before in + let memory = mw_after -. mw_prev in + (v, { time; memory }) let record ~kind ~f x = - let res, time = time f x in - bump kind time; - (res, time) - -let get ~kind = find kind + let res, stats = time_and_mem f x in + bump kind stats; + (res, stats) -let to_string (h, p, e) = - Format.asprintf "hashing: %f | parsing: %f | exec: %f" h p e +let get_accumulated ~kind = find kind let reset () = Hashtbl.remove stats Kind.Hashing; diff --git a/fleche/stats.mli b/fleche/stats.mli index 4a0bf9c9..e7fa3216 100644 --- a/fleche/stats.mli +++ b/fleche/stats.mli @@ -1,4 +1,4 @@ -(** time-based stats *) +(** time and memory-based stats *) module Kind : sig type t = | Hashing @@ -6,17 +6,36 @@ module Kind : sig | Exec end -val get : kind:Kind.t -> float -val record : kind:Kind.t -> f:('a -> 'b) -> 'a -> 'b * float +type t = + { time : float + ; memory : float + } + +(** [record ~kind ~f x] returns [f x] with timing and memory use data attached + to it; it will also update the global table for [kind] *) +val record : kind:Kind.t -> f:('a -> 'b) -> 'a -> 'b * t + +(** [get_accumulated ~kind] returns global accumulated stats for [kind] *) +val get_accumulated : kind:Kind.t -> t + +(** [reset ()] Reset global accumulated stats *) val reset : unit -> unit -type t +module Global : sig + (** Operations to save/restore global accumulated state *) + type nonrec 'a stats = t + + type t -val zero : unit -> t -val to_string : t -> string -val dump : unit -> t -val restore : t -> unit -val get_f : t -> kind:Kind.t -> float + val zero : unit -> t + val dump : unit -> t + val restore : t -> unit + + (** Get a particular field *) + val get_f : t -> kind:Kind.t -> unit stats + + val to_string : t -> string +end (** Pretty-print memory info as words *) val pp_words : Format.formatter -> float -> unit diff --git a/fleche/theory.ml b/fleche/theory.ml index 29f4f827..1c79e714 100644 --- a/fleche/theory.ml +++ b/fleche/theory.ml @@ -194,6 +194,8 @@ module Check : sig val maybe_check : io:Io.CallBack.t -> token:Coq.Limits.Token.t -> (Int.Set.t * Doc.t) option + + val set_scheduler_hint : uri:Lang.LUri.File.t -> point:int * int -> unit end = struct let pending = ref [] @@ -214,9 +216,18 @@ end = struct | None -> pend_try f tt | Some r -> Some r) + let hint : (int * int) option ref = ref None + let get_check_target pt_requests = let target_of_pt_handle (_, (l, c)) = Doc.Target.Position (l, c) in - Option.map target_of_pt_handle (List.nth_opt pt_requests 0) + match Option.map target_of_pt_handle (List.nth_opt pt_requests 0) with + | None -> + Option.map + (fun (l, c) -> + hint := None; + Doc.Target.Position (l, c)) + !hint + | Some t -> Some t (* Notification handling; reply is optional / asynchronous *) let check ~io ~token ~uri = @@ -233,8 +244,17 @@ end = struct pending := pend_pop !pending; None | (None | Some _) as tgt -> + let uri_short = + Lang.LUri.File.to_string_file uri |> Filename.basename + in let target = Option.default Doc.Target.End tgt in + Io.Report.serverStatus ~io (ServerInfo.Status.Running uri_short); let doc = Doc.check ~io ~token ~target ~doc:handle.doc () in + let mem = + Format.asprintf "%a" Stats.pp_words + (Gc.((quick_stat ()).heap_words) |> Float.of_int) + in + Io.Report.serverStatus ~io (ServerInfo.Status.Idle mem); let requests = Handle.update_doc_info ~handle ~doc in if Doc.Completion.is_completed doc.completed then Register.Completed.fire ~io ~token ~doc; @@ -255,6 +275,12 @@ end = struct let deschedule ~uri = pending := CList.remove Lang.LUri.File.equal uri !pending + + let set_scheduler_hint ~uri ~point = + if CList.is_empty !pending then + let () = hint := Some point in + schedule ~uri (* if the hint is set we wanna override it *) + else if not (Option.is_empty !hint) then hint := Some point end let create ~io ~token ~env ~uri ~raw ~version = diff --git a/fleche/theory.mli b/fleche/theory.mli index 33bbb896..e20c2cf7 100644 --- a/fleche/theory.mli +++ b/fleche/theory.mli @@ -21,6 +21,8 @@ module Check : sig progress and diagnostics notifications using output function [ofn]. *) val maybe_check : io:Io.CallBack.t -> token:Coq.Limits.Token.t -> (Int.Set.t * Doc.t) option + + val set_scheduler_hint : uri:Lang.LUri.File.t -> point:int * int -> unit end (** Create a document inside a theory *) diff --git a/fleche/version.ml b/fleche/version.ml index d9c0dd8d..ece862fa 100644 --- a/fleche/version.ml +++ b/fleche/version.ml @@ -12,6 +12,6 @@ type t = string (************************************************************************) (* UPDATE VERSION HERE *) -let server = "0.1.9-dev" +let server = "0.1.9" (* UPDATE VERSION HERE *) (************************************************************************) diff --git a/lang/diagnostic.ml b/lang/diagnostic.ml index 582cbd7e..393b1168 100644 --- a/lang/diagnostic.ml +++ b/lang/diagnostic.ml @@ -1,6 +1,6 @@ (************************************************************************) (* Flèche => document manager: Language Support *) -(* Copyright 2019-2023 Inria -- Dual License LGPL 2.1 / GPL3+ *) +(* Copyright 2019-2024 Inria -- Dual License LGPL 2.1 / GPL3+ *) (* Written by: Emilio J. Gallego Arias *) (************************************************************************) diff --git a/lang/diagnostic.mli b/lang/diagnostic.mli index 273b766b..220d8547 100644 --- a/lang/diagnostic.mli +++ b/lang/diagnostic.mli @@ -1,6 +1,6 @@ (************************************************************************) (* Flèche => document manager: Language Support *) -(* Copyright 2019-2023 Inria -- Dual License LGPL 2.1 / GPL3+ *) +(* Copyright 2019-2024 Inria -- Dual License LGPL 2.1 / GPL3+ *) (* Written by: Emilio J. Gallego Arias *) (************************************************************************) diff --git a/lang/dune b/lang/dune index a16cede5..dfca2321 100644 --- a/lang/dune +++ b/lang/dune @@ -1,4 +1,15 @@ (library (name lang) (public_name coq-lsp.lang) + (modules :standard \ utf_tests) (libraries uri coq-core.library)) + +; We had to do this due to ppx_inline_test enabling backtraces + +(library + (name lang_tests) + (inline_tests) + (modules utf_tests) + (preprocess + (pps ppx_inline_test)) + (libraries lang)) diff --git a/coq/utf8.ml b/lang/utf.ml similarity index 53% rename from coq/utf8.ml rename to lang/utf.ml index 9051e717..a4e78049 100644 --- a/coq/utf8.ml +++ b/lang/utf.ml @@ -1,9 +1,75 @@ +(************************************************************************) +(* Flèche => document manager: Language Support *) +(* Copyright 2019-2024 Inria -- Dual License LGPL 2.1 / GPL3+ *) +(* Written by: Emilio J. Gallego Arias *) +(************************************************************************) + +(* LICENSE NOTE: this file includes code from camomille and OCaml stdlib (for + compatibilty). This is just out of convenience, the included functions are + quite trivial, and eventually we should be able to use OCaml's stdlib and + remove most of this code. *) + +(* Camomille Copyright: *) +(* Copyright (C) 2002, 2003 Yamagata Yoriyuki. *) + +(* This library is free software; you can redistribute it and/or *) +(* modify it under the terms of the GNU Lesser General Public License *) +(* as published by the Free Software Foundation; either version 2 of *) +(* the License, or (at your option) any later version. *) + +(* As a special exception to the GNU Library General Public License, you *) +(* may link, statically or dynamically, a "work that uses this library" *) +(* with a publicly distributed version of this library to produce an *) +(* executable file containing portions of this library, and distribute *) +(* that executable file under terms of your choice, without any of the *) +(* additional requirements listed in clause 6 of the GNU Library General *) +(* Public License. By "a publicly distributed version of this library", *) +(* we mean either the unmodified Library as distributed by the authors, *) +(* or a modified version of this library that is distributed under the *) +(* conditions defined in clause 3 of the GNU Library General Public *) +(* License. This exception does not however invalidate any other reasons *) +(* why the executable file might be covered by the GNU Library General *) +(* Public License . *) + +(* This library is distributed in the hope that it will be useful, *) +(* but WITHOUT ANY WARRANTY; without even the implied warranty of *) +(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU *) +(* Lesser General Public License for more details. *) + +(* You should have received a copy of the GNU Lesser General Public *) +(* License along with this library; if not, write to the Free Software *) +(* Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 *) +(* USA *) + +(** This module provides facilities for translating language-based locations to + protocol-based locations. + + After a long discussion (thanks Léo !), we have decided that the best is to + have `Lang.Point` to store columns offset in the values that are native to + the protocol under consideration, set by the upper layers. + + This scheme kind of follows what we have done since the start with coq-lsp. *) +module Encoding = struct + (* Used for char offsets *) + type t = + | Utf8 + | Utf16 + | Utf32 +end + +(* Future work: support multiple encondings *) +(* val set_protocol_encoding : *) + +(* EJGA: Taken from Camomille, but note what I wrote below *) + (* utf8 utils, both Coq and Camomile have similar implementations, at some point we should remove this but for now we keep it internal. For now we use the Camomille functions *) +type utf8_string = string type char = int -type index = int +type utf8_index = int +type utf16_index = int (* Taken from camomille *) (* Copyright (C) 2002, 2003 Yamagata Yoriyuki. *) @@ -46,30 +112,6 @@ let nth s n = nth_aux s 0 n (* end of camomille *) -(* That's a tricky one, if the char we are requesting is out of bounds, then we - return the last index, 0 in the case line is empty. *) -let index_of_char ~line ~char = - if char < length line then Some (nth line char) else None - -let find_char line byte = - let rec f index n_chars = - let next_index = next line index in - if next_index > byte then n_chars else f next_index (n_chars + 1) - in - if byte < String.length line then Some (f 0 0) else None - -let char_of_index ~line ~byte = - (* if Debug.unicode then *) - (* Io.Log.trace "char_of_index" *) - (* (Format.asprintf "str: '%s' | byte: %d" line byte); *) - let char = find_char line byte in - (* (if Debug.unicode then *) - (* match char with *) - (* | None -> Io.Log.trace "get_last_text" "failed" *) - (* | Some char -> Io.Log.trace "get_last_text" (Format.asprintf "char: %d" - char)); *) - char - (* We disabled auto-formatting in copied code *) [@@@ocamlformat "disable=true"] @@ -176,44 +218,115 @@ let string_get_utf_8_uchar s i = (* End of copy from Stdlib *) [@@@ocamlformat "disable=false"] -let get_byte_offset_from_utf16_pos line (char : int) = +let length_utf16 line = let byte_idx = ref 0 in - let utf16_char_count = ref 0 in - while !byte_idx < String.length line && !utf16_char_count < char do + let utf16_len = ref 0 in + let len = String.length line in + while !byte_idx < len do let ch = string_get_utf_8_uchar line !byte_idx in - byte_idx := next line !byte_idx; - let code_unit_count = - uchar_utf_16_byte_length (uchar_utf_decode_uchar ch) / 2 - in - utf16_char_count := !utf16_char_count + code_unit_count; - () + let next_idx = next line !byte_idx in + byte_idx := next_idx; + let l = uchar_utf_16_byte_length (uchar_utf_decode_uchar ch) / 2 in + utf16_len := !utf16_len + l done; - if !byte_idx < String.length line then Some !byte_idx else None - -let%test_unit "utf16 offsets" = - let testcases_x = - [ ("aax", 2, true) - ; (" xoo", 2, true) - ; ("0123", 4, false) - ; (" 𝒞x", 4, true) - ; (" 𝒞x𝒞", 4, true) - ; (" 𝒞∫x", 5, true) - ; (" 𝒞", 4, false) - ; ("∫x.dy", 1, true) - ] + !utf16_len + +(* UTF16 <-> UTF8 *) + +let utf8_offset_of_utf16_offset ~line ~(offset : utf16_index) = + let byte_idx = ref 0 in + let utf16_char_count = ref 0 in + let len = String.length line in + (try + while !utf16_char_count < offset do + let ch = string_get_utf_8_uchar line !byte_idx in + let next_idx = next line !byte_idx in + if next_idx >= len then raise Not_found else byte_idx := next_idx; + let code_unit_count = + uchar_utf_16_byte_length (uchar_utf_decode_uchar ch) / 2 + in + utf16_char_count := !utf16_char_count + code_unit_count; + () + done + with _ -> ()); + !byte_idx + +let utf16_offset_of_utf8_offset ~line ~(offset : utf8_index) = + let byte_idx = ref 0 in + let utf16_char_count = ref 0 in + let len = String.length line in + (try + while !byte_idx < offset do + let ch = string_get_utf_8_uchar line !byte_idx in + let next_idx = next line !byte_idx in + if next_idx > len then raise Not_found else byte_idx := next_idx; + let code_unit_count = + uchar_utf_16_byte_length (uchar_utf_decode_uchar ch) / 2 + in + utf16_char_count := !utf16_char_count + code_unit_count; + () + done + with _ -> ()); + !utf16_char_count + +(******************************************************) +(** Not used anywhere, remove? *) +(******************************************************) + +(* UTF16 <-> Char *) +let char_of_utf16_offset ~line ~(offset : utf16_index) = + let byte_idx = ref 0 in + let count = ref 0 in + let utf16_char_count = ref 0 in + let len = String.length line in + (try + while !utf16_char_count < offset do + let ch = string_get_utf_8_uchar line !byte_idx in + let next_idx = next line !byte_idx in + if next_idx >= len then raise Not_found else byte_idx := next_idx; + let code_unit_count = + uchar_utf_16_byte_length (uchar_utf_decode_uchar ch) / 2 + in + utf16_char_count := !utf16_char_count + code_unit_count; + count := !count + 1; + () + done + with _ -> ()); + !count + +let utf16_offset_of_char ~line ~(char : char) = + let offset16 = ref 0 in + let idx = ref 0 in + for _ = 0 to char - 1 do + let ch = string_get_utf_8_uchar line !idx in + let byte_len = uchar_utf_16_byte_length (uchar_utf_decode_uchar ch) in + offset16 := !offset16 + (byte_len / 2); + idx := next line !idx + done; + !offset16 + +(* UTF8 <-> Char *) + +(* That's a tricky one, if the char we are requesting is out of bounds, then we + return the last index, 0 in the case line is empty. *) +let utf8_offset_of_char ~line ~char = + if char < length line then Some (nth line char) else None + +let find_char line byte = + let rec f index n_chars = + let next_index = next line index in + if next_index > byte then n_chars else f next_index (n_chars + 1) in - List.iter - (fun (s, i, b) -> - let res = get_byte_offset_from_utf16_pos s i in - if b then - let res = Option.map (fun i -> s.[i]) res in - match res with - | Some x when x = 'x' -> () - | Some x -> - failwith - (Printf.sprintf "Didn't find x in test %s : %d, instead: %c" s i x) - | None -> - failwith (Printf.sprintf "Didn't not find x in test %s : %d" s i) - else if res != None then - failwith (Printf.sprintf "Shouldn't find x in test %s : %d" s i)) - testcases_x + if byte < String.length line then Some (f 0 0) else None + +let char_of_utf8_offset ~line ~offset = + (* if Debug.unicode then *) + (* Io.Log.trace "char_of_index" *) + (* (Format.asprintf "str: '%s' | byte: %d" line byte); *) + let char = find_char line offset in + (* (if Debug.unicode then *) + (* match char with *) + (* | None -> Io.Log.trace "get_last_text" "failed" *) + (* | Some char -> Io.Log.trace "get_last_text" (Format.asprintf "char: %d" + char)); *) + char diff --git a/lang/utf.mli b/lang/utf.mli new file mode 100644 index 00000000..1bdce61a --- /dev/null +++ b/lang/utf.mli @@ -0,0 +1,83 @@ +(************************************************************************) +(* Flèche => document manager: Language Support *) +(* Copyright 2019-2024 Inria -- Dual License LGPL 2.1 / GPL3+ *) +(* Written by: Emilio J. Gallego Arias *) +(************************************************************************) + +(** This module provides facilities for translating language-based locations to + protocol-based locations. + + After a long discussion (thanks Léo !), we have decided that the best is to + have `Lang.Point` to store columns offset in the values that are native to + the protocol under consideration, set by the upper layers. + + This scheme kind of follows what we have done since the start with coq-lsp. *) + +module Encoding : sig + (* Used for char offsets *) + type t = + | Utf8 + | Utf16 + | Utf32 +end + +(** Future work: support setting protocol enconding *) +(* val set_protocol_encoding : Enconding.t -> unit *) + +(* utf8 utils, both Coq and Camomile have similar implementations, at some point + we should remove this but for now we keep it internal. For now we use the + Camomille functions *) + +(** Unicode terminology refresher: + - character, code point: The real unicode character + - byte or 16bit offset / code unit: The encoded version *) + +type utf8_string = string +type char = int +type utf8_index = int +type utf16_index = int + +(** UTF-16 offset from UTF-8 offset; line is enconded in UTF-8 *) +val utf16_offset_of_utf8_offset : + line:utf8_string -> offset:utf8_index -> utf16_index + +(** Get the byte position of a code point indexed in UTF-16 code units in a + UTF-8 encoded utf8_string. Returns the position of the last character if the + UTF-16 position was out of bounds. *) +val utf8_offset_of_utf16_offset : + line:utf8_string -> offset:utf16_index -> utf8_index + +(** To UTF-16 offsets *) + +(** Length in UTF-16 code points *) +val length_utf16 : utf8_string -> utf16_index + +(******************************************************) +(** Not used anywhere, remove? *) +(******************************************************) + +(** Number of characters in the utf-8-encoded utf8_string. *) +val length : utf8_string -> char + +(** Converstion from char to UTF-8/16 *) + +(** UTF-8 Char to byte index position; line is enconded in UTF-8 *) +val utf8_offset_of_char : line:utf8_string -> char:char -> utf8_index option + +(** Get the utf16 position of a code point indexed in unicode code points in a + UTF-8 encoded utf8_string. The position must be in bounds. *) +val utf16_offset_of_char : line:utf8_string -> char:int -> utf16_index + +(** Converstion to char from UTF-8/16 *) + +(** Byte index to character position [also called a codepoint], line is encoded + in UTF-8 *) +val char_of_utf8_offset : line:utf8_string -> offset:utf8_index -> char option + +(** Get the unicode position of a code point indexed in UTF-16 code units in a + utf-8 encoded utf8_string. Returns the position of the last character if the + utf-16 position was out of bounds. *) +val char_of_utf16_offset : line:utf8_string -> offset:utf16_index -> char + +(** For testing *) +val next : string -> int -> int diff --git a/lang/utf_tests.ml b/lang/utf_tests.ml new file mode 100644 index 00000000..e90017ec --- /dev/null +++ b/lang/utf_tests.ml @@ -0,0 +1,114 @@ +open Lang.Utf + +(* 𝒞 = 2 codepoints in UTF-16 *) +let%test_unit "utf16 length" = + let test_cases = + [ ("aax", 3) + ; (" xoo", 5) + ; ("0123", 4) + ; (" 𝒞x", 5) + ; (" 𝒞x𝒞", 7) + ; (" 𝒞∫x", 6) + ; (" 𝒞", 4) + ; ("∫x.dy", 5) + ; (" 𝒰 ", 4) + ] + in + List.iter + (fun (line, expected) -> + let res = length_utf16 line in + if res != expected then + failwith + (Printf.sprintf "Incorrect utf16_length for %s, got: %d expected: %d" + line res expected)) + test_cases + +let%test_unit "utf16 byte offsets" = + let check_last s i = i < String.length s && next s i == String.length s in + let testcases_x = + [ ("aax", 2, true) + ; (" xoo", 2, true) + ; ("0123", 4, false) + ; (" 𝒞x", 4, true) + ; (" 𝒞x𝒞", 4, true) + ; (" 𝒞∫x", 5, true) + ; (" 𝒞", 4, false) + ; ("∫x.dy", 1, true) + ] + in + List.iter + (fun (s, i, b) -> + let res = utf8_offset_of_utf16_offset ~line:s ~offset:i in + if b then ( + let res = s.[res] in + if res != 'x' then + failwith + (Printf.sprintf "Didn't find x in test %s : %d, instead: %c" s i res)) + else if not (check_last s res) then + failwith + (Printf.sprintf "Shouldn't find x in test %s / %d got %d" s i res)) + testcases_x + +let%test_unit "utf16 unicode offsets" = + (* line, utf8 offset, utf16 offset *) + let testcases = + [ ("aax", 2, 2) + ; (" xoo", 2, 2) + ; ("0123", 4, 4) + ; (" 𝒞x", 4, 4) + ; (" 𝒞x𝒞", 4, 4) + ; (" 𝒞∫x", 5, 4) + ; (" 𝒞", 4, 4) + ; ("∫x.dy", 1, 1) + ; (" 𝒰 ", 4, 3) + ] + in + List.iter + (fun (line, offset, expect) -> + let res = utf16_offset_of_utf8_offset ~line ~offset in + if res != expect then + failwith + (Printf.sprintf "Wrong result: got %d expected %d in test %s" res + expect line)) + testcases + +let%test_unit "utf16 unicode offsets" = + let testcases = + [ ("aax", 2, 2) + ; (" xoo", 2, 2) + ; ("0123", 4, 3) + ; (" 𝒞x", 4, 3) + ; (" 𝒞x𝒞", 4, 3) + ; (" 𝒞∫x", 5, 4) + ; (" 𝒞", 4, 2) + ; ("∫x.dy", 1, 1) + ] + in + List.iter + (fun (s, i, e) -> + let res = char_of_utf16_offset ~line:s ~offset:i in + if res != e then + failwith + (Printf.sprintf "Wrong result: got %d expected %d in test %s" res e s)) + testcases + +let%test_unit "unicode utf16 offsets" = + let testcases = + [ ("aax", 2, 2) + ; (" xoo", 2, 2) + ; ("0123", 3, 3) + ; (" 𝒞x", 3, 4) + ; (" 𝒞x𝒞", 3, 4) + ; (" 𝒞∫x", 4, 5) + ; (" 𝒞", 2, 2) + ; ("∫x.dy", 1, 1) + ] + in + List.iter + (fun (line, char, e) -> + let res = utf16_offset_of_char ~line ~char in + if res != e then + failwith + (Printf.sprintf "Wrong result: got %d expected %d in test %s" res e + line)) + testcases diff --git a/lsp/base.ml b/lsp/base.ml index 988e0eca..4a84481e 100644 --- a/lsp/base.ml +++ b/lsp/base.ml @@ -22,63 +22,126 @@ module J = Yojson.Safe module U = Yojson.Safe.Util +let int_field name dict = U.to_int List.(assoc name dict) let string_field name dict = U.to_string List.(assoc name dict) -let odict_field ~default name dict = - Option.cata U.to_assoc default (List.assoc_opt name dict) +module Params = struct + type t = (string * Yojson.Safe.t) list -module Message = struct + let to_yojson dict = `Assoc dict +end + +module Notification = struct + type t = + { method_ : string + ; params : Params.t + } + + let make ~method_ ~params () = { method_; params } + + let to_yojson { method_; params } = + let params = [ ("params", Params.to_yojson params) ] in + `Assoc ([ ("jsonrpc", `String "2.0"); ("method", `String method_) ] @ params) +end + +module Request = struct type t = - | Notification of - { method_ : string [@key "method"] - ; params : (string * Yojson.Safe.t) list + { id : int + ; method_ : string + ; params : Params.t + } + + let make ~method_ ~id ~params () = { id; method_; params } + + let to_yojson { method_; id; params } = + let params = [ ("params", Params.to_yojson params) ] in + `Assoc + ([ ("jsonrpc", `String "2.0") + ; ("id", `Int id) + ; ("method", `String method_) + ] + @ params) +end + +module Response = struct + type t = + | Ok of + { id : int + ; result : Yojson.Safe.t } - | Request of + | Error of { id : int - ; method_ : string [@key "method"] - ; params : (string * Yojson.Safe.t) list + ; code : int + ; message : string + ; data : Yojson.Safe.t option } - (** 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 = odict_field ~default:[] "params" dict in - (match List.assoc_opt "id" dict with - | None -> Notification { method_; params } - | Some id -> - let id = U.to_int id in - Request { id; method_; params }) - |> Result.ok - with - | Not_found -> Error ("missing parameter: " ^ J.to_string msg) - | U.Type_error (msg, obj) -> - Error (Format.asprintf "msg: %s; obj: %s" msg (J.to_string obj)) + let mk_ok ~id ~result = Ok { id; result } + let mk_error ~id ~code ~message = Error { id; code; message; data = None } - let method_ = function - | Notification { method_; _ } | Request { method_; _ } -> method_ + let id = function + | Ok { id; _ } | Error { id; _ } -> id - let params = function - | Notification { params; _ } | Request { params; _ } -> params + let to_yojson = function + | Ok { id; result } -> + `Assoc [ ("jsonrpc", `String "2.0"); ("id", `Int id); ("result", result) ] + | Error { id; code; message; data = _ } -> + `Assoc + [ ("jsonrpc", `String "2.0") + ; ("id", `Int id) + ; ("error", `Assoc [ ("code", `Int code); ("message", `String message) ]) + ] end -let mk_reply ~id ~result = - `Assoc [ ("jsonrpc", `String "2.0"); ("id", `Int id); ("result", result) ] +module Message = struct + type t = + | Notification of Notification.t + | Request of Request.t + | Response of Response.t + + let response_of_yojson dict = + let id = int_field "id" dict in + match List.assoc_opt "error" dict with + | None -> + let result = List.assoc "result" dict in + Response.Ok { id; result } + | Some error -> + let error = U.to_assoc error in + let code = int_field "code" error in + let message = string_field "message" error in + let data = None in + Error { id; code; message; data } + + let request_of_yojson method_ dict = + let params = + List.assoc_opt "params" dict |> Option.map U.to_assoc |> Option.default [] + in + match List.assoc_opt "id" dict with + | None -> Notification { Notification.method_; params } + | Some id -> + let id = U.to_int id in + Request { Request.id; method_; params } + + let of_yojson msg = + let dict = U.to_assoc msg in + match List.assoc_opt "method" dict with + | None -> Response (response_of_yojson dict) + | Some method_ -> request_of_yojson (U.to_string method_) dict + + let of_yojson msg = + try of_yojson msg |> Result.ok with + | Not_found -> Error ("missing parameter: " ^ J.to_string msg) + | U.Type_error (msg, obj) -> + Error (Format.asprintf "msg: %s; obj: %s" msg (J.to_string obj)) -let mk_request_error ~id ~code ~message = - `Assoc - [ ("jsonrpc", `String "2.0") - ; ("id", `Int id) - ; ("error", `Assoc [ ("code", `Int code); ("message", `String message) ]) - ] + let to_yojson = function + | Notification n -> Notification.to_yojson n + | Request r -> Request.to_yojson r + | Response r -> Response.to_yojson r -let mk_notification ~method_ ~params = - `Assoc - [ ("jsonrpc", `String "2.0") - ; ("method", `String method_) - ; ("params", params) - ] + let notification n = Notification n + let response r = Response r +end module ProgressToken : sig type t = @@ -111,7 +174,8 @@ end let mk_progress ~token ~value f = let params = ProgressParams.(to_yojson f { token; value }) in - mk_notification ~method_:"$/progress" ~params + let params = U.to_assoc params in + Notification.(to_yojson { method_ = "$/progress"; params }) module WorkDoneProgressBegin = struct type t = diff --git a/lsp/base.mli b/lsp/base.mli index cee26d2e..3643ac11 100644 --- a/lsp/base.mli +++ b/lsp/base.mli @@ -15,34 +15,69 @@ (* Written by: Emilio J. Gallego Arias *) (************************************************************************) -(** Basic JSON-RPC Incoming Messages *) -module Message : sig +(* XXX: EJGA This should be an structured value (object or array) *) +module Params : sig + type t = (string * Yojson.Safe.t) list +end + +module Notification : sig + type t = + { method_ : string + ; params : Params.t + } + [@@deriving to_yojson] + + val make : method_:string -> params:Params.t -> unit -> t +end + +module Request : sig + type t = + { id : int + ; method_ : string + ; params : Params.t + } + [@@deriving to_yojson] + + val make : method_:string -> id:int -> params:Params.t -> unit -> t +end + +(* Request response *) +module Response : sig type t = - | Notification of - { method_ : string - ; params : (string * Yojson.Safe.t) list + | Ok of + { id : int + ; result : Yojson.Safe.t } - | Request of + | Error of { id : int - ; method_ : string - ; params : (string * Yojson.Safe.t) list + ; code : int + ; message : string + ; data : Yojson.Safe.t option } + [@@deriving to_yojson] - (** Reify an incoming message *) - val from_yojson : Yojson.Safe.t -> (t, string) Result.t + (** Answer to a request *) + val mk_ok : id:int -> result:Yojson.Safe.t -> t - val method_ : t -> string - val params : t -> (string * Yojson.Safe.t) list + (** Fail a request *) + val mk_error : id:int -> code:int -> message:string -> t + + val id : t -> int end -(** Build notification *) -val mk_notification : method_:string -> params:Yojson.Safe.t -> Yojson.Safe.t +(** Basic JSON-RPC Incoming Messages *) +module Message : sig + type t = + | Notification of Notification.t + | Request of Request.t + | Response of Response.t + [@@deriving yojson] -(** Answer to a request *) -val mk_reply : id:int -> result:Yojson.Safe.t -> Yojson.Safe.t + val notification : Notification.t -> t + val response : Response.t -> t +end -(** Fail a request *) -val mk_request_error : id:int -> code:int -> message:string -> Yojson.Safe.t +(** Build request *) (** Progress *) module ProgressToken : sig diff --git a/lsp/io.ml b/lsp/io.ml index f5479275..020de655 100644 --- a/lsp/io.ml +++ b/lsp/io.ml @@ -21,7 +21,7 @@ module J = Yojson.Safe let fn = ref (fun _ -> ()) let set_log_fn f = fn := f -let read_raw_request ic = +let read_raw_message ic = let cl = input_line ic in let sin = Scanf.Scanning.from_string cl in let raw_obj = @@ -41,10 +41,8 @@ let read_raw_request ic = in J.from_string raw_obj -exception ReadError of string - -let read_raw_request ic = - try Some (read_raw_request ic) with +let read_raw_message ic = + try Some (Ok (read_raw_message ic)) with (* if the end of input is encountered while some more characters are needed to read the current conversion specification, or the lsp server closes *) | End_of_file -> None @@ -53,7 +51,7 @@ let read_raw_request ic = (* if a conversion to a number is not possible. *) | Failure msg (* if the format string is invalid. *) - | Invalid_argument msg -> raise (ReadError msg) + | Invalid_argument msg -> Some (Error msg) let mut = Mutex.create () let log = ref (fun _ _ -> ()) @@ -113,14 +111,16 @@ end let logMessage ~lvl ~message = let method_ = "window/logMessage" in let lvl = Lvl.to_int lvl in - let params = `Assoc [ ("type", `Int lvl); ("message", `String message) ] in - let msg = Base.mk_notification ~method_ ~params in + (* Replace with the json serializer in petanque protocol *) + let params = [ ("type", `Int lvl); ("message", `String message) ] in + let msg = Base.Notification.(make ~method_ ~params () |> to_yojson) in !fn msg let logMessageInt ~lvl ~message = let method_ = "window/logMessage" in - let params = `Assoc [ ("type", `Int lvl); ("message", `String message) ] in - let msg = Base.mk_notification ~method_ ~params in + (* Replace with the json serializer in petanque protocol *) + let params = [ ("type", `Int lvl); ("message", `String message) ] in + let msg = Base.Notification.(make ~method_ ~params () |> to_yojson) in !fn msg let logTrace ~message ~extra = @@ -128,10 +128,10 @@ let logTrace ~message ~extra = let params = match (!trace_value, extra) with | Verbose, Some extra -> - `Assoc [ ("message", `String message); ("verbose", `String extra) ] - | _, _ -> `Assoc [ ("message", `String message) ] + [ ("message", `String message); ("verbose", `String extra) ] + | _, _ -> [ ("message", `String message) ] in - Base.mk_notification ~method_ ~params |> !fn + Base.Notification.(make ~method_ ~params () |> to_yojson) |> !fn let trace hdr ?extra msg = let message = Format.asprintf "[%s]: @[%s@]" hdr msg in @@ -147,13 +147,10 @@ let trace_object hdr obj = let () = log := trace_object (** Misc helpers *) -let rec read_request ic = - match read_raw_request ic with +let read_message ic = + match read_raw_message ic with | None -> None (* EOF *) - | Some com -> ( + | Some (Ok com) -> if Fleche.Debug.read then trace_object "read" com; - match Base.Message.from_yojson com with - | Ok msg -> Some msg - | Error msg -> - trace "read_request" ("error: " ^ msg); - read_request ic) + Some (Base.Message.of_yojson com) + | Some (Error err) -> Some (Error err) diff --git a/lsp/io.mli b/lsp/io.mli index 4d3c7a3d..5d8d8856 100644 --- a/lsp/io.mli +++ b/lsp/io.mli @@ -20,13 +20,11 @@ (** Set the log function *) val set_log_fn : (Yojson.Safe.t -> unit) -> unit -(** Read a JSON-RPC request from channel *) -val read_raw_request : in_channel -> Yojson.Safe.t option +(** Read a JSON-RPC message from channel *) +val read_raw_message : in_channel -> (Yojson.Safe.t, string) Result.t option (** [None] signals [EOF] *) -val read_request : in_channel -> Base.Message.t option - -exception ReadError of string +val read_message : in_channel -> (Base.Message.t, string) Result.t option (** Send a JSON-RPC request to channel *) val send_json : Format.formatter -> Yojson.Safe.t -> unit diff --git a/lsp/jCoq.ml b/lsp/jCoq.ml index f828dfaf..d1df2ccf 100644 --- a/lsp/jCoq.ml +++ b/lsp/jCoq.ml @@ -59,13 +59,20 @@ module Goals = struct let to_ { Coq.Goals.goals; stack; bullet; shelf; given_up } = { goals; stack; bullet; shelf; given_up } + + let of_ { goals; stack; bullet; shelf; given_up } = + { Coq.Goals.goals; stack; bullet; shelf; given_up } end type ('a, 'pp) goals = ('a, 'pp) Coq.Goals.goals let goals_to_yojson f pp g = Goals_.to_ g |> Goals_.to_yojson f pp - type 'pp reified_pp = ('pp reified_goal, 'pp) goals [@@deriving to_yojson] + let goals_of_yojson f pp j = + let open Ppx_deriving_yojson_runtime in + Goals_.of_yojson f pp j >|= Goals_.of_ + + type 'pp reified_pp = ('pp reified_goal, 'pp) goals [@@deriving yojson] end module Ast = struct diff --git a/lsp/jFleche.ml b/lsp/jFleche.ml index 130ae1d9..7df22a2f 100644 --- a/lsp/jFleche.ml +++ b/lsp/jFleche.ml @@ -62,8 +62,9 @@ let mk_progress ~uri ~version processing = let textDocument = { Doc.VersionedTextDocumentIdentifier.uri; version } in let params = FileProgress.to_yojson { FileProgress.textDocument; processing } + |> Yojson.Safe.Util.to_assoc in - Base.mk_notification ~method_:"$/coq/fileProgress" ~params + Base.Notification.make ~method_:"$/coq/fileProgress" ~params () module Message = struct type 'a t = @@ -116,6 +117,10 @@ module FlecheDocument = struct [@@deriving yojson] end +module Info = struct + type t = [%import: Fleche.Perf.Info.t] [@@deriving yojson] +end + module SentencePerfData = struct type t = [%import: Fleche.Perf.Sentence.t] [@@deriving yojson] end @@ -133,6 +138,25 @@ let mk_perf ~uri ~version perf = let textDocument = { Doc.VersionedTextDocumentIdentifier.uri; version } in let params = let { Fleche.Perf.summary; timings } = perf in - DocumentPerfData.(to_yojson { textDocument; summary; timings }) + DocumentPerfData.( + to_yojson { textDocument; summary; timings } |> Yojson.Safe.Util.to_assoc) + in + Base.Notification.make ~method_:"$/coq/filePerfData" ~params () + +module ServerVersion = struct + type t = [%import: Fleche.ServerInfo.Version.t] [@@deriving yojson] +end + +let mk_serverVersion vi = + let params = ServerVersion.to_yojson vi |> Yojson.Safe.Util.to_assoc in + Base.Notification.make ~method_:"$/coq/serverVersion" ~params () + +let mk_serverStatus (st : Fleche.ServerInfo.Status.t) = + let params = + match st with + | Stopped -> [ ("status", `String "Stopped") ] + | Idle mem -> [ ("status", `String "Idle"); ("mem", `String mem) ] + | Running modname -> + [ ("status", `String "Busy"); ("modname", `String modname) ] in - Base.mk_notification ~method_:"$/coq/filePerfData" ~params + Base.Notification.make ~method_:"$/coq/serverStatus" ~params () diff --git a/lsp/jFleche.mli b/lsp/jFleche.mli index ba99218a..57a5091b 100644 --- a/lsp/jFleche.mli +++ b/lsp/jFleche.mli @@ -28,7 +28,7 @@ val mk_progress : uri:Lang.LUri.File.t -> version:int -> Fleche.Progress.Info.t list - -> Yojson.Safe.t + -> Base.Notification.t module FileProgress : sig type t = @@ -99,4 +99,8 @@ module DocumentPerfData : sig end val mk_perf : - uri:Lang.LUri.File.t -> version:int -> Fleche.Perf.t -> Yojson.Safe.t + uri:Lang.LUri.File.t -> version:int -> Fleche.Perf.t -> Base.Notification.t + +(* Server status notifications *) +val mk_serverVersion : Fleche.ServerInfo.Version.t -> Base.Notification.t +val mk_serverStatus : Fleche.ServerInfo.Status.t -> Base.Notification.t diff --git a/lsp/jLang.ml b/lsp/jLang.ml index 166db692..304b8c66 100644 --- a/lsp/jLang.ml +++ b/lsp/jLang.ml @@ -89,14 +89,13 @@ module Diagnostic = struct _t_to_yojson { range; severity; message; data } end -let mk_diagnostics ~uri ~version ld : Yojson.Safe.t = +let mk_diagnostics ~uri ~version ld : Base.Notification.t = let diags = List.map Diagnostic.to_yojson ld in let uri = Lang.LUri.File.to_string_uri uri in let params = - `Assoc - [ ("uri", `String uri) - ; ("version", `Int version) - ; ("diagnostics", `List diags) - ] + [ ("uri", `String uri) + ; ("version", `Int version) + ; ("diagnostics", `List diags) + ] in - Base.mk_notification ~method_:"textDocument/publishDiagnostics" ~params + Base.Notification.make ~method_:"textDocument/publishDiagnostics" ~params () diff --git a/lsp/jLang.mli b/lsp/jLang.mli index 0ddf3d1a..9772fea7 100644 --- a/lsp/jLang.mli +++ b/lsp/jLang.mli @@ -21,7 +21,26 @@ end module Diagnostic : sig type t = Lang.Diagnostic.t [@@deriving to_yojson] + + module Point : sig + type t = + { line : int + ; character : int + } + [@@deriving yojson] + end + + module Range : sig + type t = + { start : Point.t + ; end_ : Point.t [@key "end"] + } + [@@deriving yojson] + end end val mk_diagnostics : - uri:Lang.LUri.File.t -> version:int -> Lang.Diagnostic.t list -> Yojson.Safe.t + uri:Lang.LUri.File.t + -> version:int + -> Lang.Diagnostic.t list + -> Base.Notification.t diff --git a/petanque/README.md b/petanque/README.md new file mode 100644 index 00000000..a7a85a6c --- /dev/null +++ b/petanque/README.md @@ -0,0 +1,130 @@ +_Petanque_ (pronounced "petanque") is a +[gymnasium](https://gymnasium.farama.org/)-like environment for the +Coq Proof Assistant. + +_Petanque_ is geared towards use cases where interacting at the +document-level (like Flèche provides) in not enough, usually because +we want to work on purely proof-search level vs the document level +one. + +Petanque follows the methodology developed in SerAPI, thus we specify +an OCaml API (`agent.mli`) which is then exposed via some form of RPC. + +## Authors + +- Guilaume Baudart (Inria) +- Emilio J. Gallego Arias (Inria) +- Laetitia Teodorescu (Inria) + +## Acknowledgments + +- Andrei Kozyrev +- Alex Sánchez-Stern + +## Install instructions + +Please see the regular `coq-lsp` install instructions. In general you +have three options: + +- use a released version from Opam +- use a development version directly from the tree +- install a development version using Opam + +See the contributing guide for instructions on how to perform the last +two. + +## Running `petanque` JSON shell + +You can use `petanque` in 2 different ways: + +- call the API directly from your OCaml program +- use the provided `pet` JSON-RPC shell + +to execute the `pet` JSON-RPC shell do: +``` +make +dune exec -- rlwrap %{bin:pet} +``` + +`rlwrap` is just a convenience, if your dune version is too old and +don't recognize the `%{bin:pet}` form, you can just do `dune exec -- pet`. + +### Petanque options + +Petanque can be initalized from the command line by passing the `--root` parameter to it: +``` +make +dune exec -- rlwrap %{bin:pet} --root=/absolute/path/to/my/project +``` + +NOTE: If you use this option, you should not call `Init`! + +### A first example: + +Please use one line per json input. json input examples are: +```json +["Init",{"debug": false,"root":"file:///home/egallego/research/coq-lsp/examples/"}] +["Init",["Ok",1]] + +["Start",{"env":1,"uri": "file:///home/egallego/research/coq-lsp/examples/ex0.v","thm":"addnC"}] +["Start",["Ok",1]] + +["Run_tac", {"st": 1, "tac": "induction n."}] +["Run_tac", ["Ok", 2]] + +["Run_tac", {"st": 2, "tac": "simpl."}] +["Run_tac", 3] + +["Run_tac", {"st": 3, "tac": "auto."}] +["Run_tac",4] + +["Premises", {"st": 2}] +["Premises", ...] +``` + +Seems to work! (TM) (Famous last words) + +## Running `pet-server` + +After building Petanque, you can launch a TCP server with: +``` +dune exec -- pet-server +``` + +Default address is 127.0.0.1 and default port is 8765. + +``` +❯ dune exec -- pet-server --help +PET(1) Pet Manual PET(1) + +NAME + pet - Petanque Server + +SYNOPSIS + pet [--address=ADDRESS] [--backlog=BACKLOG] [--port=PORT] [OPTION]… + +DESCRIPTION + Launch a petanque server to interact with Coq + +USAGE + See the documentation on the project's webpage for more information + +OPTIONS + -a ADDRESS, --address=ADDRESS (absent=127.0.0.1) + address to listen to + + -b BACKLOG, --backlog=BACKLOG (absent=10) + socket backlog + + -p PORT, --port=PORT (absent=8765) + port to listen to + +COMMON OPTIONS + --help[=FMT] (default=auto) + Show this help in format FMT. The value FMT must be one of auto, + pager, groff or plain. With auto, the format is pager or plain + whenever the TERM env var is dumb or undefined. + + --version + Show version information. +``` diff --git a/petanque/agent.ml b/petanque/agent.ml new file mode 100644 index 00000000..dcb846a8 --- /dev/null +++ b/petanque/agent.ml @@ -0,0 +1,266 @@ +(************************************************************************) +(* Flèche => RL agent: petanque *) +(* Copyright 2019 MINES ParisTech -- Dual License LGPL 2.1 / GPL3+ *) +(* Copyright 2019-2024 Inria -- Dual License LGPL 2.1 / GPL3+ *) +(* Written by: Emilio J. Gallego Arias & coq-lsp contributors *) +(************************************************************************) + +let pet_debug = false + +module State = struct + type t = Coq.State.t + + let hash = Coq.State.hash + let equal = Coq.State.equal +end + +module Env = struct + type t = Fleche.Doc.Env.t +end + +(** Petanque errors *) +module Error = struct + type t = + | Interrupted + | Parsing of string + | Coq of string + | Anomaly of string + | Theorem_not_found of string + + let to_string = function + | Interrupted -> Format.asprintf "Interrupted" + | Parsing msg -> Format.asprintf "Parsing: %s" msg + | Coq msg -> Format.asprintf "Coq: %s" msg + | Anomaly msg -> Format.asprintf "Anomaly: %s" msg + | Theorem_not_found msg -> Format.asprintf "Theorem_not_found: %s" msg + + (* JSON-RPC server reserved codes *) + let to_code = function + | Interrupted -> -32001 + | Parsing _ -> -32002 + | Coq _ -> -32003 + | Anomaly _ -> -32004 + | Theorem_not_found _ -> -32005 +end + +module R = struct + type 'a t = ('a, Error.t) Result.t +end + +module Run_result = struct + type 'a t = + | Proof_finished of 'a + | Current_state of 'a +end + +let init_coq ~debug = + let load_module = Dynlink.loadfile in + let load_plugin = Coq.Loader.plugin_handler None in + Coq.Init.(coq_init { debug; load_module; load_plugin }) + +let cmdline : Coq.Workspace.CmdLine.t = + { coqlib = Coq_config.coqlib + ; coqcorelib = Filename.concat Coq_config.coqlib "../coq-core" + ; ocamlpath = None + ; vo_load_path = [] + ; ml_include_path = [] + ; args = [] + ; require_libraries = [] + } + +let trace_stderr hdr ?extra:_ msg = + Format.eprintf "@[[trace] %s | %s @]@\n%!" hdr msg + +let trace_ref = ref trace_stderr + +let message_stderr ~lvl:_ ~message = + Format.eprintf "@[[message] %s @]@\n%!" message + +let message_ref = ref message_stderr + +let io = + let trace hdr ?extra msg = !trace_ref hdr ?extra msg in + let message ~lvl ~message = !message_ref ~lvl ~message in + let diagnostics ~uri:_ ~version:_ _diags = () in + let fileProgress ~uri:_ ~version:_ _pinfo = () in + let perfData ~uri:_ ~version:_ _perf = () in + let serverVersion _ = () in + let serverStatus _ = () in + { Fleche.Io.CallBack.trace + ; message + ; diagnostics + ; fileProgress + ; perfData + ; serverVersion + ; serverStatus + } + +let read_raw ~uri = + let file = Lang.LUri.File.to_string_file uri in + try Ok Coq.Compat.Ocaml_414.In_channel.(with_open_text file input_all) + with Sys_error err -> Error err + +let find_thm ~(doc : Fleche.Doc.t) ~thm = + let { Fleche.Doc.toc; _ } = doc in + match CString.Map.find_opt thm toc with + | None -> + let msg = Format.asprintf "@[[find_thm] Theorem not found!@]" in + Error (Error.Theorem_not_found msg) + | Some node -> + if pet_debug then Format.eprintf "@[[find_thm] Theorem found!@\n@]%!"; + (* let point = (range.start.line, range.start.character) in *) + Ok (Fleche.Doc.Node.state node) + +let pp_diag fmt { Lang.Diagnostic.message; _ } = + Format.fprintf fmt "%a" Pp.pp_with message + +let print_diags (doc : Fleche.Doc.t) = + let d = Fleche.Doc.diags doc in + Format.(eprintf "@[%a@]" (pp_print_list pp_diag) d) + +let init ~token ~debug ~root = + let init = init_coq ~debug in + Fleche.Io.CallBack.set io; + let dir = Lang.LUri.File.to_string_file root in + (let open Coq.Compat.Result.O in + let+ workspace = Coq.Workspace.guess ~token ~debug ~cmdline ~dir in + let files = Coq.Files.make () in + Fleche.Doc.Env.make ~init ~workspace ~files) + |> Result.map_error (fun msg -> Error.Coq msg) + +let start ~token ~env ~uri ~thm = + match read_raw ~uri with + | Ok raw -> + (* Format.eprintf "raw: @[%s@]%!" raw; *) + let doc = Fleche.Doc.create ~token ~env ~uri ~version:0 ~raw in + print_diags doc; + let target = Fleche.Doc.Target.End in + let doc = Fleche.Doc.check ~io ~token ~target ~doc () in + find_thm ~doc ~thm + | Error err -> + let msg = Format.asprintf "@[[read_raw] File not found %s@]" err in + Error (Error.Theorem_not_found msg) + +let parse ~loc tac st = + let str = Gramlib.Stream.of_string tac in + let str = Coq.Parsing.Parsable.make ?loc str in + Coq.Parsing.parse ~st str + +let proof_finished { Coq.Goals.goals; stack; shelf; given_up; _ } = + List.for_all CList.is_empty [ goals; shelf; given_up ] && CList.is_empty stack + +let parse_and_execute_in ~token ~loc tac st = + let open Coq.Protect.E.O in + let* ast = parse ~token ~loc tac st in + match ast with + | Some ast -> ( + let open Coq.Protect.E.O in + let* st = Fleche.Memo.Interp.eval ~token (st, ast) in + let+ goals = Fleche.Info.Goals.goals ~token ~st in + match goals with + | None -> Run_result.Proof_finished st + | Some goals when proof_finished goals -> Run_result.Proof_finished st + | _ -> Run_result.Current_state st) + | None -> Coq.Protect.E.ok (Run_result.Current_state st) + +let protect_to_result (r : _ Coq.Protect.E.t) : (_, _) Result.t = + match r with + | { r = Interrupted; feedback = _ } -> Error Error.Interrupted + | { r = Completed (Error (User (_loc, msg))); feedback = _ } -> + Error (Error.Coq (Pp.string_of_ppcmds msg)) + | { r = Completed (Error (Anomaly (_loc, msg))); feedback = _ } -> + Error (Error.Anomaly (Pp.string_of_ppcmds msg)) + | { r = Completed (Ok r); feedback = _ } -> Ok r + +let run_tac ~token ~st ~tac : (_ Run_result.t, Error.t) Result.t = + (* Improve with thm? *) + let loc = None in + Coq.State.in_stateM ~token ~st ~f:(parse_and_execute_in ~token ~loc tac) st + |> protect_to_result + +let goals ~token ~st = + let f goals = + let f = Coq.Goals.map_reified_goal ~f:Pp.string_of_ppcmds in + let g = Pp.string_of_ppcmds in + Option.map (Coq.Goals.map_goals ~f ~g) goals + in + Coq.Protect.E.map ~f (Fleche.Info.Goals.goals ~token ~st) |> protect_to_result + +module Premise = struct + type t = + { full_name : string + (* should be a Coq DirPath, but let's go step by step *) + ; file : string (* file (in FS format) where the premise is found *) + ; kind : (string, string) Result.t (* type of object *) + ; range : (Lang.Range.t, string) Result.t (* a range if known *) + ; offset : (int * int, string) Result.t + (* a offset in the file if known (from .glob files) *) + ; raw_text : (string, string) Result.t (* raw text of the premise *) + } +end + +(* We need some caching here otherwise it is very expensive to re-parse the glob + files all the time. + + XXX move this caching to Flèche. *) +module Memo = struct + module H = Hashtbl.Make (CString) + + let table_glob = H.create 1000 + + let open_file glob = + match H.find_opt table_glob glob with + | Some g -> g + | None -> + let g = Coq.Glob.open_file glob in + H.add table_glob glob g; + g + + let table_source = H.create 1000 + + let input_source file = + match H.find_opt table_source file with + | Some res -> res + | None -> + if Sys.file_exists file then ( + let res = + Ok Coq.Compat.Ocaml_414.In_channel.(with_open_text file input_all) + in + H.add table_source file res; + res) + else + let res = Error "source file is not available" in + H.add table_source file res; + res +end + +let info_of ~glob ~name = + let open Coq.Compat.Result.O in + let* g = Memo.open_file glob in + let+ { Coq.Glob.Info.kind; offset } = Coq.Glob.get_info g name in + (kind, offset) + +let raw_of ~file ~offset = + match offset with + | Ok (bp, ep) -> + let open Coq.Compat.Result.O in + let* c = Memo.input_source file in + if String.length c < ep then Error "offset out of bounds" + else Ok (String.sub c bp (ep - bp + 1)) + | Error err -> Error ("offset information is not available: " ^ err) + +let to_premise (p : Coq.Library_file.Entry.t) : Premise.t = + let { Coq.Library_file.Entry.name; typ = _; file } = p in + let file = Filename.(remove_extension file ^ ".v") in + let glob = Filename.(remove_extension file ^ ".glob") in + let range = Error "not implemented yet" in + let kind, offset = info_of ~glob ~name |> Coq.Compat.Result.split in + let raw_text = raw_of ~file ~offset in + { full_name = name; file; kind; range; offset; raw_text } + +let premises ~token ~st = + (let open Coq.Protect.E.O in + let* all_libs = Coq.Library_file.loaded ~token ~st in + let+ all_premises = Coq.Library_file.toc ~token ~st all_libs in + List.map to_premise all_premises) + |> protect_to_result diff --git a/petanque/agent.mli b/petanque/agent.mli new file mode 100644 index 00000000..18a3152d --- /dev/null +++ b/petanque/agent.mli @@ -0,0 +1,97 @@ +(************************************************************************) +(* Flèche => RL agent: petanque *) +(* Copyright 2019 MINES ParisTech -- Dual License LGPL 2.1 / GPL3+ *) +(* Copyright 2019-2024 Inria -- Dual License LGPL 2.1 / GPL3+ *) +(* Written by: Emilio J. Gallego Arias & coq-lsp contributors *) +(************************************************************************) + +(** Petanque.Agent *) + +module State : sig + type t + + val hash : t -> int + val equal : t -> t -> bool +end + +module Env : sig + (** Coq Workspaces / project enviroments *) + type t +end + +(** Petanque errors *) +module Error : sig + type t = + | Interrupted + | Parsing of string + | Coq of string + | Anomaly of string + | Theorem_not_found of string + + val to_string : t -> string + val to_code : t -> int +end + +(** Petanque results *) +module R : sig + type 'a t = ('a, Error.t) Result.t +end + +module Run_result : sig + type 'a t = + | Proof_finished of 'a + | Current_state of 'a +end + +(** I/O handling, by default, print to stderr *) + +(** [trace header extra message] *) +val trace_ref : (string -> ?extra:string -> string -> unit) ref + +(** [message level message] *) +val message_ref : (lvl:Fleche.Io.Level.t -> message:string -> unit) ref + +(** [init ~debug ~root] Initializes Coq, with project and workspace settings + from [root]. [root] needs to be in URI format. This function needs to be + called _once_ before all others. *) +val init : + token:Coq.Limits.Token.t -> debug:bool -> root:Lang.LUri.File.t -> Env.t R.t + +(** [start uri thm] start a new proof for theorem [thm] in file [uri]. *) +val start : + token:Coq.Limits.Token.t + -> env:Env.t + -> uri:Lang.LUri.File.t + -> thm:string + -> State.t R.t + +(** [run_tac ~token ~st ~tac] tries to run [tac] over state [st] *) +val run_tac : + token:Coq.Limits.Token.t + -> st:State.t + -> tac:string + -> State.t Run_result.t R.t + +(** [goals ~token ~st] return the list of goals for a given [st] *) +val goals : + token:Coq.Limits.Token.t + -> st:State.t + -> string Coq.Goals.reified_pp option R.t + +module Premise : sig + type t = + { full_name : string + (* should be a Coq DirPath, but let's go step by step *) + ; file : string (* file (in FS format) where the premise is found *) + ; kind : (string, string) Result.t (* type of object *) + ; range : (Lang.Range.t, string) Result.t (* a range if known *) + ; offset : (int * int, string) Result.t + (* a offset in the file if known (from .glob files) *) + ; raw_text : (string, string) Result.t (* raw text of the premise *) + } +end + +(** Return the list of defined constants and inductives for a given state. For + now we just return their fully qualified name, but more options are of + course possible. *) +val premises : token:Coq.Limits.Token.t -> st:State.t -> Premise.t list R.t diff --git a/petanque/dune b/petanque/dune new file mode 100644 index 00000000..8da9d20f --- /dev/null +++ b/petanque/dune @@ -0,0 +1,4 @@ +(library + (public_name coq-lsp.petanque) + (name petanque) + (libraries fleche)) diff --git a/petanque/json_shell/client.ml b/petanque/json_shell/client.ml new file mode 100644 index 00000000..4535775d --- /dev/null +++ b/petanque/json_shell/client.ml @@ -0,0 +1,90 @@ +(* Client wrap *) +module type Chans = sig + val ic : in_channel + val oc : Format.formatter + val trace : ?verbose:string -> string -> unit + val message : lvl:int -> message:string -> unit +end + +(* Display incoming requests *) +let display_requests = false + +let maybe_display_request method_ = + if display_requests then Format.eprintf "received request: %s@\n%!" method_ + +let do_trace ~trace params = + match Protocol.Trace.Params.of_yojson (`Assoc params) with + | Ok { message; verbose } -> trace ?verbose message + | Error _ -> () + +let do_message ~message params = + match Protocol.Message.Params.of_yojson (`Assoc params) with + | Ok { type_; message = msg } -> message ~lvl:type_ ~message:msg + | Error _ -> () + +(* Read until we find a response *) +let rec read_response ~trace ~message ic = + match Lsp.Io.read_message ic with + | Some (Ok (Lsp.Base.Message.Response r)) -> Ok r + | Some (Ok (Notification { method_; params })) + when String.equal method_ Protocol.Trace.method_ -> + do_trace ~trace params; + read_response ~trace ~message ic + | Some (Ok (Notification { method_; params })) + when String.equal method_ Protocol.Message.method_ -> + do_message ~message params; + read_response ~trace ~message ic + | Some (Ok (Request { method_; _ })) | Some (Ok (Notification { method_; _ })) + -> + maybe_display_request method_; + read_response ~trace ~message ic + | Some (Error err) -> Error err + | None -> assert false (* not in our testing setup *) + +let id_counter = ref 0 + +let get_id () = + incr id_counter; + !id_counter + +module Wrap (R : Protocol.Request.S) (C : Chans) : sig + val call : R.Params.t -> (R.Response.t, string) Result.t +end = struct + let trace = C.trace + let message = C.message + + let call params = + let id = get_id () in + let method_ = R.method_ in + let params = Yojson.Safe.Util.to_assoc (R.Params.to_yojson params) in + let request = + Lsp.Base.Request.(make ~id ~method_ ~params () |> to_yojson) + in + let () = Lsp.Io.send_json C.oc request in + read_response ~trace ~message C.ic |> fun r -> + Result.bind r (function + | Ok { id = _; result } -> R.Response.of_yojson result + | Error { id = _; code = _; message; data = _ } -> Error message) +end + +module S (C : Chans) = struct + let init = + let module M = Wrap (Protocol.Init) (C) in + M.call + + let start = + let module M = Wrap (Protocol.Start) (C) in + M.call + + let run_tac = + let module M = Wrap (Protocol.RunTac) (C) in + M.call + + let goals = + let module M = Wrap (Protocol.Goals) (C) in + M.call + + let premises = + let module M = Wrap (Protocol.Premises) (C) in + M.call +end diff --git a/petanque/json_shell/client.mli b/petanque/json_shell/client.mli new file mode 100644 index 00000000..83dcbefa --- /dev/null +++ b/petanque/json_shell/client.mli @@ -0,0 +1,16 @@ +module type Chans = sig + val ic : in_channel + val oc : Format.formatter + val trace : ?verbose:string -> string -> unit + val message : lvl:int -> message:string -> unit +end + +open Protocol + +module S (C : Chans) : sig + val init : Init.Params.t -> (Init.Response.t, string) result + val start : Start.Params.t -> (Start.Response.t, string) result + val run_tac : RunTac.Params.t -> (RunTac.Response.t, string) result + val goals : Goals.Params.t -> (Goals.Response.t, string) result + val premises : Premises.Params.t -> (Premises.Response.t, string) result +end diff --git a/petanque/json_shell/dune b/petanque/json_shell/dune new file mode 100644 index 00000000..bd19ff96 --- /dev/null +++ b/petanque/json_shell/dune @@ -0,0 +1,20 @@ +(library + (name petanque_json) + (public_name coq-lsp.petanque.json) + (modules :standard \ pet server) + (preprocess + (staged_pps ppx_import ppx_deriving_yojson)) + (libraries cmdliner lsp petanque)) + +(executable + (name pet) + (public_name pet) + (modules pet) + (libraries petanque_json)) + +(executable + (name server) + (public_name pet-server) + (modules server) + (optional) + (libraries logs.lwt lwt.unix petanque_json)) diff --git a/petanque/json_shell/interp.ml b/petanque/json_shell/interp.ml new file mode 100644 index 00000000..38735748 --- /dev/null +++ b/petanque/json_shell/interp.ml @@ -0,0 +1,47 @@ +open Protocol +module A = Petanque.Agent + +let do_request ~token (module R : Request.S) ~id ~params = + match R.Handler.Params.of_yojson (`Assoc params) with + | Ok params -> ( + match R.Handler.handler ~token params with + | Ok result -> + let result = R.Handler.Response.to_yojson result in + Lsp.Base.Response.mk_ok ~id ~result + | Error err -> + let message = A.Error.to_string err in + let code = A.Error.to_code err in + Lsp.Base.Response.mk_error ~id ~code ~message) + | Error message -> + (* JSON-RPC Parse error *) + let code = -32700 in + Lsp.Base.Response.mk_error ~id ~code ~message + +let handle_request ~token ~id ~method_ ~params = + match method_ with + | s when String.equal Init.method_ s -> + do_request ~token (module Init) ~id ~params + | s when String.equal Start.method_ s -> + do_request ~token (module Start) ~id ~params + | s when String.equal RunTac.method_ s -> + do_request ~token (module RunTac) ~id ~params + | s when String.equal Goals.method_ s -> + do_request ~token (module Goals) ~id ~params + | s when String.equal Premises.method_ s -> + do_request ~token (module Premises) ~id ~params + | _ -> + (* JSON-RPC method not found *) + let code = -32601 in + let message = "method not found" in + Lsp.Base.Response.mk_error ~id ~code ~message + +let interp ~token (r : Lsp.Base.Message.t) : Yojson.Safe.t option = + match r with + | Request { id; method_; params } -> + let response = handle_request ~token ~id ~method_ ~params in + let response = Lsp.Base.Response.to_yojson response in + Some response + | Notification { method_ = _; params = _ } -> None + | Response _ -> + (* XXX: to implement *) + None diff --git a/petanque/json_shell/jAgent.ml b/petanque/json_shell/jAgent.ml new file mode 100644 index 00000000..d69ecb82 --- /dev/null +++ b/petanque/json_shell/jAgent.ml @@ -0,0 +1,45 @@ +(* Serialization for agent types *) + +(* Implement State.t and Env.t serialization methods *) +module State = Obj_map.Make (Petanque.Agent.State) +module Env = Obj_map.Make (Petanque.Agent.Env) + +(* The typical protocol dance *) + +module Stdlib = struct + module Result = struct + include Stdlib.Result + + type ('a, 'e) t = [%import: ('a, 'e) Stdlib.Result.t] [@@deriving yojson] + end +end + +(* What a mess result stuff is, we need this in case result is installed, as + then the types below will be referenced as plain result ... *) +module Result = Stdlib.Result + +module Error = struct + type t = [%import: Petanque.Agent.Error.t] [@@deriving yojson] +end + +module Run_result = struct + type 'a t = [%import: 'a Petanque.Agent.Run_result.t] [@@deriving yojson] +end + +module R = struct + type 'a t = [%import: 'a Petanque.Agent.R.t] [@@deriving yojson] +end + +module Goals = struct + type t = string Lsp.JCoq.Goals.reified_pp option [@@deriving yojson] +end + +module Lang = struct + module Range = struct + type t = Lsp.JLang.Range.t [@@deriving yojson] + end +end + +module Premise = struct + type t = [%import: Petanque.Agent.Premise.t] [@@deriving yojson] +end diff --git a/petanque/json_shell/obj_map.ml b/petanque/json_shell/obj_map.ml new file mode 100644 index 00000000..70f1707b --- /dev/null +++ b/petanque/json_shell/obj_map.ml @@ -0,0 +1,43 @@ +module type Obj = sig + type t + (* Not yet *) + (* val equal : t -> t -> bool *) +end + +module type S = sig + type t [@@deriving yojson] +end + +module Make (O : Obj) : S with type t = O.t = struct + type t = O.t + type _t = int [@@deriving yojson] + + module Memo = Hashtbl.Make (Int) + + let memo = Memo.create 1000 + + let dump_memo () = + let keys = Memo.to_seq_keys memo |> List.of_seq in + Format.(eprintf "@[size: %d@]@\n%!" (List.length keys)); + Format.(eprintf "@[%a@]@\n%!" (pp_print_list pp_print_int) keys) + + let last_id = ref 0 + + let mk_id _ = + incr last_id; + !last_id + + let of_obj (s : O.t) : int = + let id = mk_id s in + let () = Memo.add memo id s in + id + + let to_obj (id : int) : O.t = + try Memo.find memo id + with Not_found -> + dump_memo (); + raise Not_found + + let of_yojson json = _t_of_yojson json |> Result.map to_obj + let to_yojson st : Yojson.Safe.t = of_obj st |> _t_to_yojson +end diff --git a/petanque/json_shell/pet.ml b/petanque/json_shell/pet.ml new file mode 100644 index 00000000..2b390fe4 --- /dev/null +++ b/petanque/json_shell/pet.ml @@ -0,0 +1,78 @@ +(* json rpc server *) +open Petanque_json + +let interp ~token request = + match Interp.interp ~token request with + | None -> () + | Some response -> + Lsp.Io.send_json Format.std_formatter response; + Format.pp_print_flush Format.std_formatter () + +let rec loop ~token : unit = + match Lsp.Io.read_message stdin with + | None -> () (* EOF *) + | Some (Ok request) -> + interp ~token request; + loop ~token + | Some (Error err) -> + Format.eprintf "@[error: %s@\n@]%!" err; + loop ~token + +let trace_notification hdr ?extra msg = + let module M = Protocol.Trace in + let method_ = M.method_ in + let message = Format.asprintf "[%s] %s" hdr msg in + let params = { M.Params.message; verbose = extra } in + let params = M.Params.to_yojson params |> Yojson.Safe.Util.to_assoc in + let notification = + Lsp.Base.Notification.(make ~method_ ~params () |> to_yojson) + in + Lsp.Io.send_json Format.std_formatter notification + +let message_notification ~lvl ~message = + let module M = Protocol.Message in + let method_ = M.method_ in + let type_ = Fleche.Io.Level.to_int lvl in + let params = M.Params.({ type_; message } |> to_yojson) in + let params = Yojson.Safe.Util.to_assoc params in + let notification = + Lsp.Base.Notification.(make ~method_ ~params () |> to_yojson) + in + Lsp.Io.send_json Format.std_formatter notification + +let trace_enabled = true + +let pet_main debug roots = + Coq.Limits.start (); + (* Don't trace for now *) + if trace_enabled then ( + Petanque.Agent.trace_ref := trace_notification; + Petanque.Agent.message_ref := message_notification); + let token = Coq.Limits.Token.create () in + let () = Utils.set_roots ~token ~debug ~roots in + loop ~token + +open Cmdliner + +let pet_cmd : unit Cmd.t = + let doc = "Petanque Coq Environment" in + let man = + [ `S "DESCRIPTION" + ; `P "Petanque Coq Environment" + ; `S "USAGE" + ; `P "See the documentation on the project's webpage for more information" + ] + in + let version = Fleche.Version.server in + let pet_term = + Term.(const pet_main $ Coq.Args.debug $ Coq.Args.roots) + (* const pet_main $ roots $ display $ debug $ plugins $ file $ coqlib *) + (* $ coqcorelib $ ocamlpath $ rload_path $ load_path $ rifrom) *) + in + Cmd.(v (Cmd.info "pet" ~version ~doc ~man) pet_term) + +let main () = + let ecode = Cmd.eval pet_cmd in + exit ecode + +let () = main () diff --git a/petanque/json_shell/protocol.ml b/petanque/json_shell/protocol.ml new file mode 100644 index 00000000..a3c0defb --- /dev/null +++ b/petanque/json_shell/protocol.ml @@ -0,0 +1,220 @@ +open Petanque + +(* Serialization for agent types *) +open JAgent + +(* RPC-side server mappings, internal; we could split this in a different module + eventually as to make this clearer. *) +module type Handler = sig + (* Server-side RPC specification *) + module Params : sig + type t [@@deriving of_yojson] + end + + (* Server-side RPC specification *) + module Response : sig + type t [@@deriving to_yojson] + end + + val handler : token:Coq.Limits.Token.t -> Params.t -> Response.t R.t +end + +(* Note that here we follow JSON-RPC / LSP capitalization conventions *) +module Request = struct + module type S = sig + val method_ : string + + (* Protocol params specification *) + module Params : sig + type t [@@deriving yojson] + end + + (* Protocol response specification *) + module Response : sig + type t [@@deriving yojson] + end + + module Handler : Handler + end +end + +(* init RPC *) +module Init = struct + let method_ = "petanque/init" + + module Params = struct + type t = + { debug : bool + ; root : Lsp.JLang.LUri.File.t + } + [@@deriving yojson] + end + + module Response = struct + type t = int [@@deriving yojson] + end + + module Handler = struct + module Params = Params + + module Response = struct + type t = Env.t [@@deriving yojson] + end + + let handler ~token { Params.debug; root } = Agent.init ~token ~debug ~root + end +end + +(* start RPC *) +module Start = struct + let method_ = "petanque/start" + + module Params = struct + type t = + { env : int + ; uri : Lsp.JLang.LUri.File.t + ; thm : string + } + [@@deriving yojson] + end + + module Response = struct + type t = int [@@deriving yojson] + end + + module Handler = struct + module Params = struct + type t = + { env : Env.t + ; uri : Lsp.JLang.LUri.File.t + ; thm : string + } + [@@deriving yojson] + end + + module Response = struct + type t = State.t [@@deriving yojson] + end + + let handler ~token { Params.env; uri; thm } = + Agent.start ~token ~env ~uri ~thm + end +end + +(* run_tac RPC *) +module RunTac = struct + let method_ = "petanque/run" + + module Params = struct + type t = + { st : int + ; tac : string + } + [@@deriving yojson] + end + + module Response = struct + type t = int Run_result.t [@@deriving yojson] + end + + module Handler = struct + module Params = struct + type t = + { st : State.t + ; tac : string + } + [@@deriving yojson] + end + + module Response = struct + type t = State.t Run_result.t [@@deriving yojson] + end + + let handler ~token { Params.st; tac } = Agent.run_tac ~token ~st ~tac + end +end + +(* goals RPC *) +module Goals = struct + let method_ = "petanque/goals" + + module Params = struct + type t = { st : int } [@@deriving yojson] + end + + module Response = struct + type t = Goals.t [@@deriving yojson] + end + + module Handler = struct + module Params = struct + type t = { st : State.t } [@@deriving yojson] + end + + module Response = Response + + let handler ~token { Params.st } = Agent.goals ~token ~st + end +end + +(* premises RPC *) +module Premises = struct + let method_ = "petanque/premises" + + module Params = struct + type t = { st : int } [@@deriving yojson] + end + + module Response = struct + type t = Premise.t list [@@deriving yojson] + end + + module Handler = struct + module Params = struct + type t = { st : State.t } [@@deriving yojson] + end + + module Response = Response + + let handler ~token { Params.st } = Agent.premises ~token ~st + end +end + +(* Notifications don't get a reply *) +module Notification = struct + module type S = sig + val method_ : string + + module Params : sig + type t [@@deriving yojson] + end + end +end + +(* These two are identical from LSP *) + +(* Trace notification *) +module Trace = struct + let method_ = "$/logTrace" + + module Params = struct + type t = + { message : string + ; verbose : string option [@default None] + } + [@@deriving yojson] + end +end + +(* Message notification *) +module Message = struct + let method_ = "window/logMessage" + + module Params = struct + type t = + { type_ : int [@key "type"] + ; message : string + } + [@@deriving yojson] + end +end diff --git a/petanque/json_shell/server.ml b/petanque/json_shell/server.ml new file mode 100644 index 00000000..1e536945 --- /dev/null +++ b/petanque/json_shell/server.ml @@ -0,0 +1,109 @@ +open Lwt +open Lwt.Syntax +open Petanque_json + +let rq_info (r : Lsp.Base.Message.t) = + match r with + | Notification { method_; _ } -> Format.asprintf "notification: %s" method_ + | Request { method_; _ } -> Format.asprintf "request: %s" method_ + | Response (Ok { id; _ } | Error { id; _ }) -> + Format.asprintf "response for: %d" id + +let rec handle_connection ~token ic oc () = + try + let* request = Lwt_io.read_line ic in + let request = Yojson.Safe.from_string request in + match Lsp.Base.Message.of_yojson request with + | Error err -> + (* error in Json message *) + let* () = Logs_lwt.info (fun m -> m "Error: %s" err) in + handle_connection ~token ic oc () + | Ok request -> ( + (* everything is fine up to JSON-RPC level *) + let* () = Logs_lwt.info (fun m -> m "Received: %s" (rq_info request)) in + (* request could be a notification, so maybe we don't have to do a + reply! *) + match Interp.interp ~token request with + | None -> handle_connection ~token ic oc () + | Some reply -> + let* () = Logs_lwt.info (fun m -> m "Sent reply") in + let* () = Lwt_io.fprintl oc (Yojson.Safe.to_string reply) in + handle_connection ~token ic oc ()) + with End_of_file -> return () + +let accept_connection ~token conn = + let fd, _ = conn in + let ic = Lwt_io.of_fd ~mode:Lwt_io.Input fd in + let oc = Lwt_io.of_fd ~mode:Lwt_io.Output fd in + let* () = Logs_lwt.info (fun m -> m "New connection") in + Lwt.on_failure (handle_connection ~token ic oc ()) (fun e -> + Logs.err (fun m -> m "%s" (Printexc.to_string e))); + return () + +let create_socket ~address ~port ~backlog = + let open Lwt_unix in + let sock = socket PF_INET SOCK_STREAM 0 in + ( bind sock @@ ADDR_INET (Unix.inet_addr_of_string address, port) |> fun x -> + ignore x ); + listen sock backlog; + sock + +let create_server ~token sock = + let rec serve () = + let* conn = Lwt_unix.accept sock in + let* () = accept_connection ~token conn in + serve () + in + serve + +let pet_main debug roots address port backlog = + Coq.Limits.start (); + let token = Coq.Limits.Token.create () in + let () = Logs.set_reporter (Logs.format_reporter ()) in + let () = Logs.set_level (Some Logs.Info) in + let sock = create_socket ~address ~port ~backlog in + let serve = create_server ~token sock in + let () = Utils.set_roots ~token ~debug ~roots in + Lwt_main.run @@ serve () + +open Cmdliner + +let address = + let doc = "address to listen to" in + Arg.( + value & opt string "127.0.0.1" + & info [ "a"; "address" ] ~docv:"ADDRESS" ~doc) + +let port = + let doc = "port to listen to" in + Arg.(value & opt int 8765 & info [ "p"; "port" ] ~docv:"PORT" ~doc) + +let backlog = + let doc = "socket backlog" in + Arg.(value & opt int 10 & info [ "b"; "backlog" ] ~docv:"BACKLOG" ~doc) + +let pet_cmd : unit Cmd.t = + let doc = "Petanque Server" in + let man = + [ `S "DESCRIPTION" + ; `P "Launch a petanque server to interact with Coq" + ; `S "USAGE" + ; `P + "See\n\ + \ the\n\ + \ documentation on the project's webpage for more information" + ] + in + let version = Fleche.Version.server in + let pet_term = + Term.( + const pet_main $ Coq.Args.debug $ Coq.Args.roots $ address $ port + $ backlog) + in + Cmd.(v (Cmd.info "pet" ~version ~doc ~man) pet_term) + +let main () = + let ecode = Cmd.eval pet_cmd in + exit ecode + +let () = main () diff --git a/petanque/json_shell/utils.ml b/petanque/json_shell/utils.ml new file mode 100644 index 00000000..84ebf089 --- /dev/null +++ b/petanque/json_shell/utils.ml @@ -0,0 +1,17 @@ +(* XXX: Flèche LSP backend already handles the conversion at the protocol + level *) +let uri_of_string_exn uri = + Lang.LUri.of_string uri |> Lang.LUri.File.of_uri |> Result.get_ok + +let set_roots ~token ~debug ~roots = + match roots with + | [] -> () + | [ root ] | root :: _ -> ( + let root = uri_of_string_exn root in + match Petanque.Agent.init ~token ~debug ~root with + | Ok env -> + (* hack until we fix the stuff *) + let _ : Yojson.Safe.t = JAgent.Env.to_yojson env in + () + | Error err -> + Format.eprintf "Error: %s@\n%!" (Petanque.Agent.Error.to_string err)) diff --git a/petanque/test/basic_api.ml b/petanque/test/basic_api.ml new file mode 100644 index 00000000..19219ada --- /dev/null +++ b/petanque/test/basic_api.ml @@ -0,0 +1,61 @@ +open Petanque + +let prepare_paths () = + let to_uri file = + Lang.LUri.of_string file |> Lang.LUri.File.of_uri |> Result.get_ok + in + let cwd = Sys.getcwd () in + let file = Filename.concat cwd "test.v" in + (to_uri cwd, to_uri file) + +let msgs = ref [] + +let trace hdr ?extra:_ msg = + msgs := Format.asprintf "[trace] %s | %s" hdr msg :: !msgs + +let message ~lvl:_ ~message = msgs := message :: !msgs +let dump_msgs () = List.iter (Format.eprintf "%s@\n") (List.rev !msgs) + +let start ~token = + let debug = false in + Petanque.Agent.trace_ref := trace; + Petanque.Agent.message_ref := message; + (* Will this work on Windows? *) + let open Coq.Compat.Result.O in + let root, uri = prepare_paths () in + let* env = Agent.init ~token ~debug ~root in + Agent.start ~token ~env ~uri ~thm:"rev_snoc_cons" + +let extract_st (st : _ Agent.Run_result.t) = + match st with + | Proof_finished st | Current_state st -> st + +let main () = + let open Coq.Compat.Result.O in + let token = Coq.Limits.create_atomic () in + let r ~st ~tac = + let st = extract_st st in + Agent.run_tac ~token ~st ~tac + in + let* st = start ~token in + let* _premises = Agent.premises ~token ~st in + let* st = Agent.run_tac ~token ~st ~tac:"induction l." in + let* st = r ~st ~tac:"-" in + let* st = r ~st ~tac:"reflexivity." in + let* st = r ~st ~tac:"-" in + let* st = r ~st ~tac:"now simpl; rewrite IHl." in + let* st = r ~st ~tac:"Qed." in + Agent.goals ~token ~st:(extract_st st) + +let check_no_goals = function + | Error err -> + Format.eprintf "error: in execution: %s@\n%!" (Agent.Error.to_string err); + dump_msgs (); + 129 + | Ok None -> 0 + | Ok (Some _goals) -> + dump_msgs (); + Format.eprintf "error: goals remaining@\n%!"; + 1 + +let () = main () |> check_no_goals |> exit diff --git a/petanque/test/dune b/petanque/test/dune new file mode 100644 index 00000000..fe4c7a8e --- /dev/null +++ b/petanque/test/dune @@ -0,0 +1,21 @@ +(test + (name basic_api) + (modules basic_api) + (deps test.v) + (libraries petanque)) + +(test + (name json_api) + (modules json_api) + (deps test.v %{bin:pet}) + (enabled_if + (<> %{os_type} "Win32")) + (libraries petanque petanque_json lsp)) + +(test + (name json_api_failure) + (modules json_api_failure) + (deps test.v %{bin:pet}) + (enabled_if + (<> %{os_type} "Win32")) + (libraries petanque petanque_json lsp)) diff --git a/petanque/test/json_api.ml b/petanque/test/json_api.ml new file mode 100644 index 00000000..bbd5a53a --- /dev/null +++ b/petanque/test/json_api.ml @@ -0,0 +1,86 @@ +open Petanque_json + +let prepare_paths () = + let to_uri file = + Lang.LUri.of_string file |> Lang.LUri.File.of_uri |> Result.get_ok + in + let cwd = Sys.getcwd () in + let file = Filename.concat cwd "test.v" in + (to_uri cwd, to_uri file) + +let msgs = ref [] +let trace ?verbose:_ msg = msgs := Format.asprintf "[trace] %s" msg :: !msgs +let message ~lvl:_ ~message = msgs := message :: !msgs +let dump_msgs () = List.iter (Format.eprintf "%s@\n") (List.rev !msgs) + +let extract_st (st : Protocol.RunTac.Response.t) = + match st with + | Proof_finished st | Current_state st -> st + +let pp_offset fmt (bp, ep) = Format.fprintf fmt "(%d,%d)" bp ep + +let pp_res_str = + Coq.Compat.Result.pp Format.pp_print_string Format.pp_print_string + +let pp_premise fmt + { Petanque.Agent.Premise.full_name + ; kind + ; file + ; range = _ + ; offset + ; raw_text + } = + Format.( + fprintf fmt + "@[{ name = %s;@ file = %s;@ kind = %a;@ offset = %a;@ raw_text = %a}@]@\n" + full_name file pp_res_str kind + (Coq.Compat.Result.pp pp_offset pp_print_string) + offset pp_res_str raw_text) + +let run (ic, oc) = + let open Coq.Compat.Result.O in + let debug = false in + let module S = Client.S (struct + let ic = ic + let oc = oc + let trace = trace + let message = message + end) in + let r ~st ~tac = + let st = extract_st st in + S.run_tac { st; tac } + in + (* Will this work on Windows? *) + let root, uri = prepare_paths () in + let* env = S.init { debug; root } in + let* st = S.start { env; uri; thm = "rev_snoc_cons" } in + let* _premises = S.premises { st } in + (* Format.(eprintf "@[%a@]@\n%!" (pp_print_list pp_premise) premises); *) + let* st = S.run_tac { st; tac = "induction l." } in + let* st = r ~st ~tac:"-" in + let* st = r ~st ~tac:"reflexivity." in + let* st = r ~st ~tac:"-" in + let* st = r ~st ~tac:"now simpl; rewrite IHl." in + let* st = r ~st ~tac:"Qed." in + S.goals { st = extract_st st } + +let main () = + let server_out, server_in = Unix.open_process "pet" in + run (server_out, Format.formatter_of_out_channel server_in) + +let check_no_goals = function + | Error err -> + Format.eprintf "error: in execution: %s@\n%!" err; + dump_msgs (); + 129 + | Ok None -> 0 + | Ok (Some _goals) -> + dump_msgs (); + Format.eprintf "error: goals remaining@\n%!"; + 1 + +let () = + let result = main () in + (* Need to kill the sever... *) + (* let () = Unix.kill server 9 in *) + check_no_goals result |> exit diff --git a/petanque/test/json_api_failure.ml b/petanque/test/json_api_failure.ml new file mode 100644 index 00000000..71bce482 --- /dev/null +++ b/petanque/test/json_api_failure.ml @@ -0,0 +1,68 @@ +open Petanque_json + +let prepare_paths () = + let to_uri file = + Lang.LUri.of_string file |> Lang.LUri.File.of_uri |> Result.get_ok + in + let cwd = Sys.getcwd () in + let file = Filename.concat cwd "test.v" in + (to_uri cwd, to_uri file) + +let msgs = ref [] +let trace ?verbose:_ msg = msgs := Format.asprintf "[trace] %s" msg :: !msgs +let message ~lvl:_ ~message = msgs := message :: !msgs +let dump_msgs () = List.iter (Format.eprintf "%s@\n") (List.rev !msgs) + +let extract_st (st : Protocol.RunTac.Response.t) = + match st with + | Proof_finished st | Current_state st -> st + +let run (ic, oc) = + let open Coq.Compat.Result.O in + let debug = false in + let module S = Client.S (struct + let ic = ic + let oc = oc + let trace = trace + let message = message + end) in + let r ~st ~tac = + let st = extract_st st in + S.run_tac { st; tac } + in + (* Will this work on Windows? *) + let root, uri = prepare_paths () in + let* env = S.init { debug; root } in + let* st = S.start { env; uri; thm = "rev_snoc_cons" } in + let* _premises = S.premises { st } in + let* st = S.run_tac { st; tac = "induction l." } in + let* st = r ~st ~tac:"-" in + (* Introduce an error *) + (* let* st = r ~st ~tac:"reflexivity." in *) + let* st = r ~st ~tac:"-" in + let* st = r ~st ~tac:"now simpl; rewrite IHl." in + let* st = r ~st ~tac:"Qed." in + S.goals { st = extract_st st } + +let main () = + let server_out, server_in = Unix.open_process "pet" in + run (server_out, Format.formatter_of_out_channel server_in) + +let check_no_goals = function + | Error _err -> + (* errored as expected! *) + 0 + | Ok None -> + dump_msgs (); + Format.eprintf "error: we did succeded when we should not@\n%!"; + 1 + | Ok (Some _goals) -> + dump_msgs (); + Format.eprintf "error: goals remaining@\n%!"; + 1 + +let () = + let result = main () in + (* Need to kill the sever... *) + (* let () = Unix.kill server 9 in *) + check_no_goals result |> exit diff --git a/petanque/test/test.v b/petanque/test/test.v new file mode 100644 index 00000000..cf5ed828 --- /dev/null +++ b/petanque/test/test.v @@ -0,0 +1,10 @@ +From Coq Require Import List. +Import ListNotations. + +Lemma rev_snoc_cons A : + forall (x : A) (l : list A), rev (l ++ [x]) = x :: rev l. +Proof. + induction l. + - reflexivity. + - simpl. rewrite IHl. simpl. reflexivity. +Qed. diff --git a/plugins/goaldump/main.ml b/plugins/goaldump/main.ml index 2da72d3e..980e969e 100644 --- a/plugins/goaldump/main.ml +++ b/plugins/goaldump/main.ml @@ -15,19 +15,6 @@ let of_execution ~io ~what (v : (_, _) Coq.Protect.E.t) = None | Coq.Protect.R.Interrupted -> None) -let extract_raw ~(contents : Contents.t) ~(range : Lang.Range.t) = - let start = range.start.offset in - let length = range.end_.offset - start in - (* We need to be careful here as Doc.t always adds a last empty node on EOF, - but somehow the offset of this node seems suspicious, it seems like the Coq - parser increases the offset by one, we need to investigate. *) - let length = - if String.length contents.raw < start + length then - String.length contents.raw - start - else length - in - String.sub contents.raw start length - (* We output a record for each sentence in the document, linear order. Note that for unparseable nodes, we don't have an AST. *) module AstGoals = struct @@ -45,7 +32,7 @@ module AstGoals = struct let of_node ~io ~token ~(contents : Contents.t) (node : Doc.Node.t) = let range = node.range in - let raw = extract_raw ~contents ~range in + let raw = Fleche.Contents.extract_raw ~contents ~range in let ast = Option.map (fun n -> n.Doc.Node.Ast.v) node.ast in let st = node.state in let goals = of_execution ~io ~what:"goals" (Info.Goals.goals ~token ~st) in diff --git a/test/compiler/basic/run.t b/test/compiler/basic/run.t index 7a63f22c..ac7db57b 100644 --- a/test/compiler/basic/run.t +++ b/test/compiler/basic/run.t @@ -113,38 +113,63 @@ Compile a dependent file without the dep being built b.v b.vo $ cat proj1/a.diags + $ cat proj1/b.diags { "range": { "start": { "line": 0, "character": 0 }, - "end": { "line": 0, "character": 19 } + "end": { "line": 0, "character": 10 } }, - "severity": 4, - "message": "aa is defined" + "severity": 1, + "message": "Cannot find a physical path bound to logical path a." } { "range": { - "start": { "line": 6, "character": 0 }, - "end": { "line": 6, "character": 4 } + "start": { "line": 1, "character": 17 }, + "end": { "line": 1, "character": 21 } }, - "severity": 4, - "message": "foo is defined" + "severity": 1, + "message": "The reference a.aa was not found in the current environment." } - $ cat proj1/b.diags + +Compile a file with all messages: + $ rm -f proj1/a.{diags,vo} + $ fcc --root proj1 --diags_level=1 proj1/a.v + [message] Configuration loaded from Command-line arguments + - coqlib is at: [TEST_PATH] + + coqcorelib is at: [TEST_PATH] + - Modules [Coq.Init.Prelude] will be loaded by default + - 2 Coq path directory bindings in scope; 22 Coq plugin directory bindings in scope + - ocamlpath wasn't overriden + + findlib config: [TEST_PATH] + + findlib default location: [TEST_PATH] + [message] compiling file proj1/a.v + $ cat proj1/a.diags + $ fcc --root proj1 --diags_level=2 proj1/a.v + [message] Configuration loaded from Command-line arguments + - coqlib is at: [TEST_PATH] + + coqcorelib is at: [TEST_PATH] + - Modules [Coq.Init.Prelude] will be loaded by default + - 2 Coq path directory bindings in scope; 22 Coq plugin directory bindings in scope + - ocamlpath wasn't overriden + + findlib config: [TEST_PATH] + + findlib default location: [TEST_PATH] + [message] compiling file proj1/a.v + $ cat proj1/a.diags { "range": { "start": { "line": 0, "character": 0 }, - "end": { "line": 0, "character": 10 } + "end": { "line": 0, "character": 19 } }, - "severity": 1, - "message": "Cannot find a physical path bound to logical path a." + "severity": 4, + "message": "aa is defined" } { "range": { - "start": { "line": 1, "character": 17 }, - "end": { "line": 1, "character": 21 } + "start": { "line": 6, "character": 0 }, + "end": { "line": 6, "character": 4 } }, - "severity": 1, - "message": "The reference a.aa was not found in the current environment." + "severity": 4, + "message": "foo is defined" } Use two workspaces diff --git a/test/compiler/exit_code/run.t b/test/compiler/exit_code/run.t index 5d38e9a2..3d2af0e4 100644 --- a/test/compiler/exit_code/run.t +++ b/test/compiler/exit_code/run.t @@ -18,14 +18,6 @@ Compile normally, even with errors, we exit 0: $ echo $? 0 $ cat Demo.diags - { - "range": { - "start": { "line": 8, "character": 0 }, - "end": { "line": 8, "character": 4 } - }, - "severity": 4, - "message": "add_0_r is defined" - } { "range": { "start": { "line": 11, "character": 8 },