diff --git a/.envrc b/.envrc new file mode 100644 index 000000000..3550a30f2 --- /dev/null +++ b/.envrc @@ -0,0 +1 @@ +use flake diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml index 726d37237..9d3078293 100644 --- a/.github/workflows/build.yml +++ b/.github/workflows/build.yml @@ -90,8 +90,8 @@ jobs: - run: npm ci - run: npx --yes vsce ls - fmt-ocamlfmt: - name: Format with ocamlfmt + treefmt: + name: Format runs-on: ubuntu-latest steps: - name: πŸ”­ Checkout code @@ -100,21 +100,5 @@ jobs: submodules: recursive - name: ❄️ Setup Nix uses: cachix/install-nix-action@v18 - - name: πŸ“ Format with ocamlfmt - run: nix develop .#fmt -c make fmt - - fmt-prettier: - name: Format with prettier - runs-on: ubuntu-latest - defaults: - run: - working-directory: ./editor/code - steps: - - name: πŸ”­ Checkout code - uses: actions/checkout@v3 - - name: πŸš€ Setup node - uses: actions/setup-node@v3 - with: - node-version: 16 - - run: npm ci - - run: npx prettier -c . + - name: πŸ“ Format with alejandra, ocamlformat, prettier + run: nix fmt diff --git a/.gitignore b/.gitignore index b767639e5..eb2c98392 100644 --- a/.gitignore +++ b/.gitignore @@ -5,3 +5,8 @@ _opam .git-ps *.cache + +.direnv +# Nix build will produce this +result + diff --git a/CHANGES.md b/CHANGES.md index cdf86abcf..3d95daae7 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -16,7 +16,7 @@ - Server is now more strict w.r.t. what URIs it will accept for documents, see protocol documentation (@ejgallego, #286, reported by Alex Sanchez-Stern) - - Hypothesis with bodies are now correctly displayed (@ejgallego, + - Hypotheses with bodies are now correctly displayed (@ejgallego, #296, fixes #293, report by Ali Caglayan) - `coq-lsp` incorrectly required the optional `rootPath` initialization parameter, moreover it ignored `rootUri` if present @@ -43,7 +43,29 @@ #314, fixes #308) - Goal display handles background goals better, showing preview, goals stack, and focusing information (@ejgallego, #290, fixes - #288, based on jsCoq code by Shachar Itzhaky) + #288, fixes #304, based on jsCoq code by Shachar Itzhaky) + - Warnings are now printed in the info view messages panel + (@ejgallego, #315, fixes #195) + - Info protocol messages now have location and level + (@ejgallego, #315) + - Warnings are not printed in the info view messages panel + (@ejgallego, #, fixes #195) + - Improved `documentSymbol` return type for newer `DocumentSymbol[]` + hierarchical symbol support. This means that sections and modules + will now be properly represented, as well as constructors for + inductive types, projections for records, etc... (@ejgallego, + #174, fixes #121, #122) + - [internal] Error recovery can now execute full Coq commands as to + amend states, required for #319 (@ejallego, #320) + - Auto-admit the previous bullet goal when a new bullet cannot be + opened due to an unsolved previous bullet. This also works for {} + focusing operators. This is very useful when navigating bulleted + proofs (@ejgallego, @Alizter, #319, fixes #300) + - Store Ast.Info.t incrementally (@ejgallego, #337, fixes #316) + - Basic jump to definition support; due to lack of workspace + metadata, this only works inside the same file (@ejgallego, #318) + - Show type of identifiers at point on hover (@ejgallego, #321, cc: + #164) # coq-lsp 0.1.4: View --------------------- diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md index d779c6db8..76eb68eb5 100644 --- a/CONTRIBUTING.md +++ b/CONTRIBUTING.md @@ -78,9 +78,13 @@ You can also use the regular `dune build @check` etc... targets. #### Nix -We have a Nix flake that you can use. For development, simply run `nix develop`. +We have a Nix flake that you can use. For development, in the case of the server, simply run `nix develop`. +In the case of the client, we expose separate shells, e.g client-vscode, would be `nix develop .#client-vscode` (this can be done on top of the original `nix develop`) -If you wish to do `nix build` or compose this flake from another project, you +You can view the list of packages and devShells that are exposed +by running `nix flake show`. + +If you wish to do `nix build`, you will need to use the .?submodules=1` trick, since we use submodules here for vendoring. For example, building requires: @@ -88,7 +92,8 @@ vendoring. For example, building requires: nix build .?submodules=1 ``` -You can use this flake in other flakes or Nix derivations. +This currently only applies to building the default package (coq-lsp), which is the server. +Clients don't have specific submodules as of yet. #### Releasing diff --git a/README.md b/README.md index 5a9bce913..ad868215a 100644 --- a/README.md +++ b/README.md @@ -1,4 +1,6 @@ -## Coq LSP +# Coq LSP + +[![Github CI][ci-badge]][ci-link] `coq-lsp` is a [Language Server](https://microsoft.github.io/language-server-protocol/) and [Visual @@ -13,73 +15,37 @@ information panel, performance data, and more. experience, as well as to serve as a platform for research and UI integration with other projects. -### Installation - -In order to use `coq-lsp` you'll need to install [**both**](etc/FAQ.md) the -`coq-lsp` server, and the Visual Studio Code extension: - -#### Server - -- **opam**: `opam install coq-lsp` -- **Nix** (coming soon) -- **Coq Platform** (coming soon) -- [Do it yourself!](#server-1) - -#### **Visual Studio Code**: -- Official Marketplace: https://marketplace.visualstudio.com/items?itemName=ejgallego.coq-lsp -- Open VSX: https://open-vsx.org/extension/ejgallego/coq-lsp - -### FAQ - -See our [list of frequently-asked questions](./etc/FAQ.md). - -### Contributing - -Contributions are very welcome! Feel free to chat with the dev team in -[Zulip](https://coq.zulipchat.com/#narrow/stream/329642-coq-lsp) for any -question, or just go ahead and hack. - -We have a [contributing guide](CONTRIBUTING.md), which includes a description of -the organization of the codebase, developer workflow, and more. - -Here is a [list of project ideas](etc/ContributionIdeas.md) that could be of -help in case you are looking for contribution ideas, tho we are convinced that -the best ideas will arise from using `coq-lsp` in your own Coq projects. - -### Discussion Channel - -`coq-lsp` discussion channel it at [Coq's -Zulip](https://coq.zulipchat.com/#narrow/stream/329642-coq-lsp), don't hesitate -to stop by; both users and developers are welcome. - -### Troubleshooting and Known Problems - -- Some problems can be resolved by restarting `coq-lsp`, in Visual Studio Code, - `Ctrl+Shift+P` will give you access to the `coq-lsp.restart` command. -- In VSCode, the "Output" window will have a "Coq LSP Server Events" channel - which should contain some important information; the content of this channel - is controlled by the `Coq LSP > Trace: Server` option. -- If you install `coq-lsp` simultaneously with VSCoq, VSCode gets confused and - neither of them may work. `coq-lsp` will warn about that. If you know how to - improve this, don't hesitate to get in touch with us. -- VS Code may send request completions with a stale document, this will be fixed - in a new upstream release, c.f. https://github.com/ejgallego/coq-lsp/issues/273 - -#### Working with multiple files - -`coq-lsp` can't work with more than one file at the same time, due to problems -with parsing state management upstream. This was fixed in Coq `master` branch -(to become **Coq 8.18**). - -As this is very inconvenient, we do provide a fixed Coq branch that you can -install using `opam pin`: - -- For Coq 8.17: `opam pin add coq-lsp https://github.com/ejgallego/coq.git#v8.17+lsp` -- For Coq 8.16: `opam pin add coq-lsp https://github.com/ejgallego/coq.git#v8.16+lsp` - -## Features - -### Incremental compilation and continuous document checking: +## Table of Contents + +- [🎁 Features](#-features) + - [⏩ Incremental Compilation and Continuous Document Checking](#-incremental-compilation-and-continuous-document-checking) + - [🧠 Smart, Cache-Aware Error Recovery](#-smart-cache-aware-error-recovery) + - [πŸ₯… Whole-Document Goal Display](#-whole-document-goal-display) + - [πŸ—’οΈ Markdown Support](#️-markdown-support) + - [πŸ‘₯ Document Outline](#-document-outline) + - [⏱️ Detailed Timing and Memory Statistics](#️-detailed-timing-and-memory-statistics) + - [πŸ”§ Client-Side Configuration Options](#-client-side-configuration-options) + - [♻️ Reusability, Standards, Modularity](#️-reusability-standards-modularity) + - [πŸ”Ž A Platform for Research!](#-a-platform-for-research) +- [πŸ› οΈ Installation](#️-installation) + - [Server](#server) + - [Visual Studio Code](#visual-studio-code) + - [Neovim](#neovim) +- [πŸ—£οΈ Discussion Channel](#️-discussion-channel) +- [❓FAQ](#faq) +- [⁉️ Troubleshooting and Known Problems](#️-troubleshooting-and-known-problems) + - [Working With Multiple Files](#working-with-multiple-files) +- [πŸ“” Planned Features](#-planned-features) +- [πŸ“• Protocol Documentation](#-protocol-documentation) +- [🀸 Contributing](#-contributing) +- [🌐 Team](#-team) + - [Past Contributors](#past-contributors) +- [©️ Licensing Information](#️-licensing-information) +- [πŸ‘ Acknowledgments](#-acknowledgments) + +## 🎁 Features + +### ⏩ Incremental Compilation and Continuous Document Checking Edit your file, and `coq-lsp` will try to re-check only what is necessary, continuously. No more dreaded `Ctrl-C Ctrl-N`! Rechecking tries to be smart, @@ -93,7 +59,7 @@ 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! -### Smart, Cache-aware Error recovery +### 🧠 Smart, Cache-Aware Error Recovery `coq-lsp` won't stop checking on errors, but supports (and encourages) working with proof documents that are only partially working. Moreover, error recovery @@ -102,14 +68,22 @@ integrates with the incremental cache, and will recognize proof structure. You can edit without fear inside a `Proof. ... Qed.`, the rest of the document won't be rechecked, unless the proof is completed. -### Whole-Document Goal Display +Smart error recovery + +Furthermore, you can leave bullets and focused goals unfinished, and `coq-lsp` +will automatically admit them for you. + +### πŸ₯… Whole-Document Goal Display Press `Alt+Enter` (or `Cmd+Enter` in Mac) to show goals at point in a side panel. Whole-Document Goal Display -### Markdown support +The panel will also include goals that you have given up or shelved. This panel +will also show the current info about open bullets and their goals. + +### πŸ—’οΈ Markdown Support Open a markdown file with a `.mv` extension, `coq-lsp` will check the code parts that are enclosed into `coq` language blocks! `coq-lsp` places human-friendly @@ -117,21 +91,24 @@ documents at the core of its design ideas. Coq + Markdown Editing -### Document outline: +### πŸ‘₯ Document Outline `coq-lsp` supports document outline and code folding, allowing you to jump -directly to definitions in the document. +directly to definitions in the document. Many of the Coq vernacular commands +like `Definition`, `Theorem`, `Lemma`, etc. will be recognized as document +symbols which you can navigate to or see the outline of. + -Document Outline Demo +Document Outline Demo Document Symbols -### Detailed timing and memory stats +### ⏱️ Detailed Timing and Memory Statistics Hover over any Coq sentence, `coq-lsp` will display detailed memory and timing statistics. Stats on Hover -### Client-side configuration options +### πŸ”§ Client-Side Configuration Options `coq-lsp` is configurable, and tries to adapt to your own workflow. What to do when a proof doesn't check, admit or ignore? You decide! @@ -140,7 +117,7 @@ See the `coq-lsp` extension configuration in VSCode for options available. Configuration screen -### Reusability, standards, modularity +### ♻️ Reusability, Standards, Modularity The incremental document checking library of `coq-lsp` has been designed to be reusable by other projects written in OCaml and with needs for document @@ -149,7 +126,7 @@ validation UI, as well as by other Coq projects such as jsCoq. Moreover, we are strongly based on standards, aiming for the least possible extensions. -### A Platform for Research ! +### πŸ”Ž A Platform for Research! A key `coq-lsp` goal is to serve as central platform for researchers in Human-Computer-Interaction, Machine Learning, and Software Engineering willing @@ -158,12 +135,95 @@ to interact with Coq. Towards this goal, `coq-lsp` extends and will eventually replace `coq-serapi`, which has been used by many to that purpose. -### Planned features +## πŸ› οΈ Installation + +In order to use `coq-lsp` you'll need to install [**both**](etc/FAQ.md) +`coq-lsp` and a suitable client. We recommend the Visual Studio Code Extension. + +### Server + +- **opam**: + ``` + opam install coq-lsp + ``` +- **Nix**: + - In nixpkgs: [#213397](https://github.com/NixOS/nixpkgs/pull/213397) + - In your flake: + ```nix + inputs.coq-lsp = { type = "git"; url = "https://github.com/ejgallego/coq-lsp.git"; submodules = true; }; + ... + coq-lsp.packages.${system}.default + ``` +- **Coq Platform** (coming soon) +- [Do it yourself!](#server-1) + +### Visual Studio Code +- Official Marketplace: https://marketplace.visualstudio.com/items?itemName=ejgallego.coq-lsp +- Open VSX: https://open-vsx.org/extension/ejgallego/coq-lsp +- Nix: +```nix +inputs.coq-lsp = { type = "git"; url = "https://github.com/ejgallego/coq-lsp.git"; submodules = true; }; +... +programs.vscode = { + enable = true; + extensions = with pkgs.vscode-extensions; [ + ... + inputs.coq-lsp.packages.${pkgs.system}.vscode-extension + ... + ]; +}; +``` + +### Neovim +- Experimental client by Jaehwang Jung: https://github.com/tomtomjhj/coq-lsp.nvim + +## πŸ—£οΈ Discussion Channel + +`coq-lsp` discussion channel it at [Coq's +Zulip](https://coq.zulipchat.com/#narrow/stream/329642-coq-lsp), don't hesitate +to stop by; both users and developers are welcome. + +## ❓FAQ + +See our [list of frequently-asked questions](./etc/FAQ.md). + +## ⁉️ Troubleshooting and Known Problems + +- Some problems can be resolved by restarting `coq-lsp`, in Visual Studio Code, + `Ctrl+Shift+P` will give you access to the `coq-lsp.restart` command. +- In VSCode, the "Output" window will have a "Coq LSP Server Events" channel + which should contain some important information; the content of this channel + is controlled by the `Coq LSP > Trace: Server` option. +- If you install `coq-lsp` simultaneously with VSCoq, VSCode gets confused and + neither of them may work. `coq-lsp` will warn about that. If you know how to + improve this, don't hesitate to get in touch with us. +- VS Code may send request completions with a stale document, this will be fixed + in a new upstream release, c.f. https://github.com/ejgallego/coq-lsp/issues/273 + +### Working With Multiple Files + +`coq-lsp` can't work with more than one file at the same time, due to problems +with parsing state management upstream. This was fixed in Coq `master` branch +(to become **Coq 8.18**). + +As this is very inconvenient, we do provide a fixed Coq branch that you can +install using `opam pin`: + +- For Coq 8.17: + ``` + opam pin add coq-lsp https://github.com/ejgallego/coq.git#v8.17+lsp + ``` +- For Coq 8.16: + ``` + opam pin add coq-lsp https://github.com/ejgallego/coq.git#v8.16+lsp + ``` + +## πŸ“” Planned Features See [planned features and contribution ideas](etc/ContributionIdeas.md) for a list of things we'd like to happen. -## Protocol Documentation +## πŸ“• Protocol Documentation `coq-lsp` mostly implements the [LSP Standard](https://microsoft.github.io/language-server-protocol/specifications/lsp/3.17/specification/), @@ -171,18 +231,31 @@ plus some extensions specific to Coq. Check [the `coq-lsp` protocol documentation](etc/doc/PROTOCOL.md) for more details. -## Team +## 🀸 Contributing + +Contributions are very welcome! Feel free to chat with the dev team in +[Zulip](https://coq.zulipchat.com/#narrow/stream/329642-coq-lsp) for any +question, or just go ahead and hack. + +We have a [contributing guide](CONTRIBUTING.md), which includes a description of +the organization of the codebase, developer workflow, and more. + +Here is a [list of project ideas](etc/ContributionIdeas.md) that could be of +help in case you are looking for contribution ideas, tho we are convinced that +the best ideas will arise from using `coq-lsp` in your own Coq projects. + +## 🌐 Team - Ali Caglayan (co-coordinator) - Emilio J. Gallego Arias (Inria Paris, co-coordinator) - Shachar Itzhaky (Technion) - Ramkumar Ramachandra (Inria Paris) -### Past contributors +### Past Contributors - Vincent Laporte (Inria) -## Licensing information +## ©️ Licensing Information The license for this project is LGPL 2.1 (or GPL 3+ as stated in the LGPL 2.1). @@ -195,16 +268,19 @@ The license for this project is LGPL 2.1 (or GPL 3+ as stated in the LGPL 2.1). [VSCoq](https://github.com/siegebell/vscoq) by Christian J. Bell, distributed under the terms of the MIT license (see ./editor/code/License-vscoq.text). -## Acknowledgments +## πŸ‘ Acknowledgments Work on this server has been made possible thanks to many discussions, inspirations, and sharing of ideas from colleagues. In particular, we'd like to -thank Rudi Grinberg, Andrey Mokhov, ClΓ©ment Pit-Claudel, and Makarius Wenzel -for their help and advice. +thank Rudi Grinberg, Andrey Mokhov, ClΓ©ment Pit-Claudel, and Makarius Wenzel for +their help and advice. As noted above, the original implementation was based on the Lambdapi LSP server, thanks to all the collaborators in that project! +[ci-badge]: https://github.com/ejgallego/coq-lsp/actions/workflows/build.yml/badge.svg +[ci-link]: https://github.com/ejgallego/coq-lsp/actions/workflows/build.yml + diff --git a/controller/lsp_core.ml b/controller/lsp_core.ml index 90a153888..e59fa1f83 100644 --- a/controller/lsp_core.ml +++ b/controller/lsp_core.ml @@ -75,8 +75,7 @@ module PendingRequest = struct match pr with | DocRequest { uri; handler } -> let doc = Doc_manager.find_doc ~uri in - let lines = doc.contents.lines in - handler ~lines ~doc + handler ~doc | PosRequest { uri; point; handler } -> let doc = Doc_manager.find_doc ~uri in handler ~point ~doc @@ -239,19 +238,21 @@ let do_position_request ~postpone ~params ~handler = let do_hover = do_position_request ~postpone:false ~handler:Rq_hover.hover let do_goals = do_position_request ~postpone:true ~handler:Rq_goals.goals +let do_definition = + do_position_request ~postpone:true ~handler:Rq_definition.request + let do_completion = do_position_request ~postpone:true ~handler:Rq_completion.completion (* Requires the full document to be processed *) let do_document_request ~params ~handler = let uri, doc = get_textDocument params in - let lines = doc.contents.lines in match doc.completed with - | Yes _ -> RAction.ok (handler ~lines ~doc) + | Yes _ -> RAction.ok (handler ~doc) | Stopped _ | Failed _ | FailedPermanent _ -> Postpone (PendingRequest.DocRequest { uri; handler }) -let do_symbols = do_document_request ~handler:Requests.symbols +let do_symbols = do_document_request ~handler:Rq_symbols.symbols let do_trace params = let trace = string_field "value" params in @@ -325,6 +326,7 @@ let dispatch_request ~method_ ~params : RAction.t = | "shutdown" -> do_shutdown ~params (* Symbols and info about the document *) | "textDocument/completion" -> do_completion ~params + | "textDocument/definition" -> do_definition ~params | "textDocument/documentSymbol" -> do_symbols ~params | "textDocument/hover" -> do_hover ~params (* Proof-specific stuff *) diff --git a/controller/requests.ml b/controller/requests.ml index 63cd91594..fad2394ec 100644 --- a/controller/requests.ml +++ b/controller/requests.ml @@ -15,24 +15,5 @@ (* Written by: Emilio J. Gallego Arias *) (************************************************************************) -type document_request = - lines:string Array.t -> doc:Fleche.Doc.t -> Yojson.Safe.t - +type document_request = doc:Fleche.Doc.t -> Yojson.Safe.t type position_request = doc:Fleche.Doc.t -> point:int * int -> Yojson.Safe.t - -open Lsp.JFleche - -let symbols ~lines ~(doc : Fleche.Doc.t) = - let uri = doc.uri in - let f loc id = - let name = Names.Id.to_string id in - let kind = 12 in - let location = - let range = Fleche.Coq_utils.to_range ~lines loc in - { Location.uri; range } - in - SymInfo.(to_yojson { name; kind; location }) - in - let ast = Fleche.Doc.asts doc in - let slist = Coq.Ast.grab_definitions f ast in - `List slist diff --git a/controller/requests.mli b/controller/requests.mli index 82f5b7e7a..9cdda9c0e 100644 --- a/controller/requests.mli +++ b/controller/requests.mli @@ -15,9 +15,5 @@ (* Written by: Emilio J. Gallego Arias *) (************************************************************************) -type document_request = - lines:string Array.t -> doc:Fleche.Doc.t -> Yojson.Safe.t - +type document_request = doc:Fleche.Doc.t -> Yojson.Safe.t type position_request = doc:Fleche.Doc.t -> point:int * int -> Yojson.Safe.t - -val symbols : document_request diff --git a/controller/rq_common.ml b/controller/rq_common.ml new file mode 100644 index 000000000..727c0fab6 --- /dev/null +++ b/controller/rq_common.ml @@ -0,0 +1,46 @@ +(************************************************************************) +(* Coq Language Server Protocol -- Common requests routines *) +(* Copyright 2019 MINES ParisTech -- Dual License LGPL 2.1 / GPL3+ *) +(* Copyright 2019-2023 Inria -- Dual License LGPL 2.1 / GPL3+ *) +(* Written by: Emilio J. Gallego Arias *) +(************************************************************************) + +(* Common with completion... refactor and make proper *) +let is_id_char x = + ('a' <= x && x <= 'z') + || ('A' <= x && x <= 'Z') + || ('0' <= x && x <= '9') + || x = '_' + +let rec find_start s c = + if c <= 0 then 0 + else if not (is_id_char s.[c - 1]) then c + else find_start s (c - 1) + +let id_from_start s start = + let l = String.length s in + let rec end_of_id s c = + if c >= l then c else if is_id_char s.[c] then end_of_id s (c + 1) else c + in + let end_ = end_of_id s start in + if start < end_ then ( + let id = String.sub s start (end_ - start) in + Lsp.Io.trace "find_id" ("found: " ^ id); + Some id) + else None + +let find_id s c = + let start = find_start s c in + Lsp.Io.trace "find_id" ("start: " ^ string_of_int start); + Option.map Coq.Ast.Id.of_string (id_from_start s start) + +let get_id_at_point ~doc ~point = + let line, character = point in + Lsp.Io.trace "get_id_at_point" + ("l: " ^ string_of_int line ^ " c: " ^ string_of_int character); + let { Fleche.Doc.contents; _ } = doc in + let { Fleche.Contents.lines; _ } = contents in + if line <= Array.length lines then + let line = Array.get lines line in + if character <= String.length line then find_id line character else None + else None diff --git a/controller/rq_common.mli b/controller/rq_common.mli new file mode 100644 index 000000000..f892f1b2d --- /dev/null +++ b/controller/rq_common.mli @@ -0,0 +1,8 @@ +(************************************************************************) +(* Coq Language Server Protocol -- Common requests routines *) +(* Copyright 2019 MINES ParisTech -- Dual License LGPL 2.1 / GPL3+ *) +(* Copyright 2019-2023 Inria -- Dual License LGPL 2.1 / GPL3+ *) +(* Written by: Emilio J. Gallego Arias *) +(************************************************************************) + +val get_id_at_point : doc:Fleche.Doc.t -> point:int * int -> Coq.Ast.Id.t option diff --git a/controller/rq_completion.ml b/controller/rq_completion.ml index eb066e45b..1a4343e7f 100644 --- a/controller/rq_completion.ml +++ b/controller/rq_completion.ml @@ -22,11 +22,18 @@ let mk_completion ~label ?insertText ?labelDetails ?textEdit ?commitCharacters CompletionData.( to_yojson { label; insertText; labelDetails; textEdit; commitCharacters }) +let grab_definitions ~doc ~f = + let asts = Fleche.Doc.asts doc in + let df { Fleche.Doc.Node.Ast.ast_info; _ } = ast_info in + List.filter_map df asts |> List.concat |> List.filter_map f + let build_doc_idents ~doc : Yojson.Safe.t list = - let f _loc id = mk_completion ~label:Names.Id.(to_string id) () in - let ast = Fleche.Doc.asts doc in - let clist = Coq.Ast.grab_definitions f ast in - clist + let f { Coq.Ast.Info.name; _ } = + match name.v with + | Anonymous -> None + | Name id -> Some (mk_completion ~label:Names.Id.(to_string id) ()) + in + grab_definitions ~doc ~f let mk_completion_list ~incomplete ~items : Yojson.Safe.t = `Assoc [ ("isIncomplete", `Bool incomplete); ("items", `List items) ] @@ -72,7 +79,7 @@ let validate_line ~(doc : Fleche.Doc.t) ~line = let validate_position ~doc ~point = let line, char = point in Option.bind (validate_line ~doc ~line) (fun line -> - Option.bind (Fleche.Utf8.index_of_char ~line ~char) (fun index -> + Option.bind (Coq.Utf8.index_of_char ~line ~char) (fun index -> Some (String.get line index))) let get_char_at_point ~(doc : Fleche.Doc.t) ~point = diff --git a/controller/rq_definition.ml b/controller/rq_definition.ml new file mode 100644 index 000000000..6c71e3219 --- /dev/null +++ b/controller/rq_definition.ml @@ -0,0 +1,18 @@ +(************************************************************************) +(* Coq Language Server Protocol -- Jump to definition *) +(* Copyright 2019 MINES ParisTech -- Dual License LGPL 2.1 / GPL3+ *) +(* Copyright 2019-2023 Inria -- Dual License LGPL 2.1 / GPL3+ *) +(* Written by: Emilio J. Gallego Arias *) +(************************************************************************) + +let request ~(doc : Fleche.Doc.t) ~point = + Option.cata + (fun id_at_point -> + let { Fleche.Doc.toc; _ } = doc in + match Coq.Ast.Id.Map.find_opt id_at_point toc with + | Some range -> + let uri = doc.uri in + Lsp.JFleche.Location.({ uri; range } |> to_yojson) + | None -> `Null) + `Null + (Rq_common.get_id_at_point ~doc ~point) diff --git a/controller/rq_definition.mli b/controller/rq_definition.mli new file mode 100644 index 000000000..ba18fdbf1 --- /dev/null +++ b/controller/rq_definition.mli @@ -0,0 +1,8 @@ +(************************************************************************) +(* Coq Language Server Protocol -- Jump to definition *) +(* Copyright 2019 MINES ParisTech -- Dual License LGPL 2.1 / GPL3+ *) +(* Copyright 2019-2023 Inria -- Dual License LGPL 2.1 / GPL3+ *) +(* Written by: Emilio J. Gallego Arias *) +(************************************************************************) + +val request : Requests.position_request diff --git a/controller/rq_goals.ml b/controller/rq_goals.ml index 2acc8efc8..37e845145 100644 --- a/controller/rq_goals.ml +++ b/controller/rq_goals.ml @@ -6,13 +6,7 @@ (************************************************************************) (* Replace by ppx when we can print goals properly in the client *) -let mk_message (_loc, lvl, msg) = - let hdr = - if lvl = 4 then Pp.str "[info ] " - else if lvl = 5 then Pp.str "[debug] " - else Pp.mt () - in - Pp.(hdr ++ msg) +let mk_message (range, level, text) = Lsp.JFleche.Message.{ range; level; text } let mk_messages node = Option.map Fleche.Doc.Node.messages node diff --git a/controller/rq_hover.ml b/controller/rq_hover.ml index b65ad1f31..b23c9ccb8 100644 --- a/controller/rq_hover.ml +++ b/controller/rq_hover.ml @@ -7,8 +7,95 @@ open Lsp.JFleche +(* Debug parameters *) +let show_loc_info = false + +(* Taken from printmod.ml, funny stuff! *) +let build_ind_type mip = Inductive.type_of_inductive mip + +let info_of_ind env sigma ((sp, i) : Names.Ind.t) = + let mib = Environ.lookup_mind sp env in + let u = + Univ.make_abstract_instance (Declareops.inductive_polymorphic_context mib) + in + let mip = mib.Declarations.mind_packets.(i) in + let paramdecls = Inductive.inductive_paramdecls (mib, u) in + let env_params, params = + Namegen.make_all_rel_context_name_different env (Evd.from_env env) + (EConstr.of_rel_context paramdecls) + in + let nparamdecls = Context.Rel.length params in + let args = Context.Rel.instance_list Constr.mkRel 0 params in + let arity = + Reduction.hnf_prod_applist_assum env nparamdecls + (build_ind_type ((mib, mip), u)) + args + in + Printer.pr_lconstr_env env_params sigma arity + +let type_of_constant cb = cb.Declarations.const_type + +let info_of_const env cr = + let cdef = Environ.lookup_constant cr env in + (* This prints the definition *) + (* let cb = Environ.lookup_constant cr env in *) + (* Option.cata (fun (cb,_univs,_uctx) -> Some cb ) None *) + (* (Global.body_of_constant_body Library.indirect_accessor cb), *) + type_of_constant cdef + +let info_of_var env vr = + let vdef = Environ.lookup_named vr env in + (* This prints the value if some *) + (* Option.cata (fun cb -> Some cb) None (Context.Named.Declaration.get_value + vdef) *) + Context.Named.Declaration.get_type vdef + +(* XXX: Some work to do wrt Global.type_of_global_unsafe *) +let info_of_constructor env cr = + (* let cdef = Global.lookup_pinductive (cn, cu) in *) + let ctype, _uctx = + Typeops.type_of_global_in_context env (Names.GlobRef.ConstructRef cr) + in + ctype + +let info_of_id env sigma id = + let qid = Libnames.qualid_of_ident id in + (* try locate the kind of object the name refers to *) + try + let lid = Nametab.locate qid in + (* dispatch based on type *) + let open Names.GlobRef in + (match lid with + | VarRef vr -> info_of_var env vr |> Printer.pr_type_env env sigma + | ConstRef cr -> info_of_const env cr |> Printer.pr_type_env env sigma + | IndRef ir -> info_of_ind env sigma ir + | ConstructRef cr -> + info_of_constructor env cr |> Printer.pr_type_env env sigma) + |> fun x -> Some x + with _ -> ( + try Some (info_of_var env id |> Printer.pr_type_env env sigma) + with _ -> None) + +let info_of_id ~st id = + let st = Coq.State.to_coq st in + let sigma, env = + match st with + | { Vernacstate.lemmas = Some pstate; _ } -> + Vernacstate.LemmaStack.with_top pstate + ~f:Declare.Proof.get_current_context + | _ -> + let env = Global.env () in + (Evd.from_env env, env) + in + info_of_id env sigma id + +let info_of_id_at_point ~doc ~point id = + let st = Fleche.Info.LC.node ~doc ~point Exact in + Option.bind st (fun node -> + let st = node.Fleche.Doc.Node.state in + Fleche.Info.LC.in_state ~st ~f:(info_of_id ~st) id) + let hover ~doc ~point = - let show_loc_info = true in let range_span = Fleche.Info.LC.range ~doc ~point Exact in let range_string = let none fmt () = Format.fprintf fmt "no ast" in @@ -23,6 +110,18 @@ let hover ~doc ~point = if show_loc_info then range_string ^ "\n___\n" ^ info_string else info_string in + let hover_string = + match Rq_common.get_id_at_point ~doc ~point with + | Some id -> ( + let id = Coq.Ast.Id.to_coq id in + match info_of_id_at_point ~doc ~point id with + | None -> hover_string + | Some typ -> + let id = Names.Id.to_string id in + let typ = Pp.string_of_ppcmds typ in + Format.asprintf "```coq\n%s : %s\n```\n___\n%s" id typ hover_string) + | None -> hover_string + in let contents = { HoverContents.kind = "markdown"; value = hover_string } in let range = range_span in HoverInfo.(to_yojson { contents; range }) diff --git a/controller/rq_init.ml b/controller/rq_init.ml index 51940c921..3565631c7 100644 --- a/controller/rq_init.ml +++ b/controller/rq_init.ml @@ -78,6 +78,7 @@ let do_initialize ~params = [ ("triggerCharacters", `List [ `String "\\" ]) ; ("resolveProvider", `Bool false) ] ) + ; ("definitionProvider", `Bool true) ] in ( `Assoc diff --git a/controller/rq_symbols.ml b/controller/rq_symbols.ml new file mode 100644 index 000000000..26e1f399e --- /dev/null +++ b/controller/rq_symbols.ml @@ -0,0 +1,35 @@ +(************************************************************************) +(* Coq Language Server Protocol -- Requests *) +(* Copyright 2019 MINES ParisTech -- Dual License LGPL 2.1 / GPL3+ *) +(* Copyright 2019-2023 Inria -- Dual License LGPL 2.1 / GPL3+ *) +(* Written by: Emilio J. Gallego Arias *) +(************************************************************************) + +let rec mk_syminfo info = + let Coq.Ast.Info.{ range; name; kind; detail; children } = info in + let { CAst.loc = _name_loc; v = name } = name in + let name = Names.Name.print name |> Pp.string_of_ppcmds in + let children = Option.map (List.map mk_syminfo) children in + let selectionRange = range in + (* Need to fix this at coq.ast level *) + (* let selectionRange = Option.get name_loc in *) + Lsp.JFleche.DocumentSymbol. + { name + ; kind + ; detail + ; tags = None + ; deprecated = None + ; range + ; selectionRange + ; children + } + +let mk_syminfo info = mk_syminfo info |> Lsp.JFleche.DocumentSymbol.to_yojson +let definition_info { Fleche.Doc.Node.Ast.ast_info; _ } = ast_info + +let symbols ~(doc : Fleche.Doc.t) = + let definfo = + Fleche.Doc.asts doc |> List.filter_map definition_info |> List.concat + in + let result = List.map mk_syminfo definfo in + `List result diff --git a/controller/rq_symbols.mli b/controller/rq_symbols.mli new file mode 100644 index 000000000..fcac4d349 --- /dev/null +++ b/controller/rq_symbols.mli @@ -0,0 +1,8 @@ +(************************************************************************) +(* Coq Language Server Protocol -- Requests *) +(* Copyright 2019 MINES ParisTech -- Dual License LGPL 2.1 / GPL3+ *) +(* Copyright 2019-2023 Inria -- Dual License LGPL 2.1 / GPL3+ *) +(* Written by: Emilio J. Gallego Arias *) +(************************************************************************) + +val symbols : Requests.document_request diff --git a/coq-lsp.opam b/coq-lsp.opam index 3d28a7979..dc0f7c806 100644 --- a/coq-lsp.opam +++ b/coq-lsp.opam @@ -24,7 +24,7 @@ depends: [ # lsp dependencies "cmdliner" { >= "1.1.0" } "yojson" { >= "1.7.0" } - "uri" { >= "4.2.0" } + "uri" { >= "4.2.0" } # waterproof parser "menhir" { >= "20220210" } diff --git a/coq/ast.ml b/coq/ast.ml index 056110f2e..4c59b4d2d 100644 --- a/coq/ast.ml +++ b/coq/ast.ml @@ -1,4 +1,4 @@ -module Vernacexpr = Serlib.Ser_vernacexpr +(* module Vernacexpr = Serlib.Ser_vernacexpr *) type t = Vernacexpr.vernac_control @@ -13,65 +13,59 @@ let loc { CAst.loc; _ } = loc let print x = try Ppvernac.pr_vernac x with _ -> Pp.str "XXX Coq printer crashed" -let match_coq_def f v : _ list = - let open Vernacexpr in - let ndecls = - (* TODO: (co)fixpoint, instance, assumption *) - match v.CAst.v.expr with - | VernacDefinition (_, (CAst.{ loc = Some loc; v = name }, _), _) -> - Nameops.Name.fold_left (fun _ id -> [ (loc, id) ]) [] name - | VernacStartTheoremProof (_, ndecls) -> - let f_id = function - | (CAst.{ loc = None; _ }, _), _ -> None - | (CAst.{ loc = Some loc; v }, _), _ -> Some (loc, v) - in - CList.map_filter f_id ndecls - | _ -> [] - in - CList.map (fun (loc, id) -> f loc id) ndecls - -(* | VernacLoad (_, _) -> (??) | VernacSyntaxExtension (_, _) -> (??) | - VernacOpenCloseScope (_, _) -> (??) | VernacDeclareScope _ -> (??) | - VernacDelimiters (_, _) -> (??) | VernacBindScope (_, _) -> (??) | - VernacInfix (_, _, _) -> (??) | VernacNotation (_, _, _) -> (??) | - VernacNotationAddFormat (_, _, _) -> (??) | VernacDeclareCustomEntry _ -> - (??) | VernacEndProof _ -> (??) | VernacExactProof _ -> (??) | - VernacAssumption (_, _, _) -> (??) | VernacInductive (_, _, _, _) -> (??) | - VernacFixpoint (_, _) -> (??) | VernacCoFixpoint (_, _) -> (??) | - VernacScheme _ -> (??) | VernacCombinedScheme (_, _) -> (??) | VernacUniverse - _ -> (??) | VernacConstraint _ -> (??) | VernacBeginSection _ -> (??) | - VernacEndSegment _ -> (??) | VernacRequire (_, _, _) -> (??) | VernacImport - (_, _) -> (??) | VernacCanonical _ -> (??) | VernacCoercion (_, _, _) -> (??) - | VernacIdentityCoercion (_, _, _) -> (??) | VernacNameSectionHypSet (_, _) - -> (??) | VernacInstance (_, _, _, _) -> (??) | VernacDeclareInstance (_, _, - _) -> (??) | VernacContext _ -> (??) | VernacExistingInstance _ -> (??) | - VernacExistingClass _ -> (??) | VernacDeclareModule (_, _, _, _) -> (??) | - VernacDefineModule (_, _, _, _, _) -> (??) | VernacDeclareModuleType (_, _, - _, _) -> (??) | VernacInclude _ -> (??) | VernacSolveExistential (_, _) -> - (??) | VernacAddLoadPath (_, _, _) -> (??) | VernacRemoveLoadPath _ -> (??) | - VernacAddMLPath (_, _) -> (??) | VernacDeclareMLModule _ -> (??) | - VernacChdir _ -> (??) | VernacWriteState _ -> (??) | VernacRestoreState _ -> - (??) | VernacResetName _ -> (??) | VernacResetInitial -> (??) | VernacBack _ - -> (??) | VernacBackTo _ -> (??) | VernacCreateHintDb (_, _) -> (??) | - VernacRemoveHints (_, _) -> (??) | VernacHints (_, _) -> (??) | - VernacSyntacticDefinition (_, _, _) -> (??) | VernacArguments (_, _, _, _, _) - -> (??) | VernacReserve _ -> (??) | VernacGeneralizable _ -> (??) | - VernacSetOpacity _ -> (??) | VernacSetStrategy _ -> (??) | VernacUnsetOption - (_, _) -> (??) | VernacSetOption (_, _, _) -> (??) | VernacAddOption (_, _) - -> (??) | VernacRemoveOption (_, _) -> (??) | VernacMemOption (_, _) -> (??) - | VernacPrintOption _ -> (??) | VernacCheckMayEval (_, _, _) -> (??) | - VernacGlobalCheck _ -> (??) | VernacDeclareReduction (_, _) -> (??) | - VernacPrint _ -> (??) | VernacSearch (_, _, _) -> (??) | VernacLocate _ -> - (??) | VernacRegister (_, _) -> (??) | VernacPrimitive (_, _, _) -> (??) | - VernacComments _ -> (??) | VernacAbort _ -> (??) | VernacAbortAll -> (??) | - VernacRestart -> (??) | VernacUndo _ -> (??) | VernacUndoTo _ -> (??) | - VernacFocus _ -> (??) | VernacUnfocus -> (??) | VernacUnfocused -> (??) | - VernacBullet _ -> (??) | VernacSubproof _ -> (??) | VernacEndSubproof -> (??) - | VernacShow _ -> (??) | VernacCheckGuard -> (??) | VernacProof (_, _) -> - (??) | VernacProofMode _ -> (??) | VernacExtend (_, _) -> (??)) *) - -let grab_definitions f nodes = - List.fold_left (fun acc s -> match_coq_def f s @ acc) [] nodes +module Id = struct + type t = Names.Id.t + + let of_string = Names.Id.of_string + let of_coq x = x + let to_coq x = x + + module Set = Names.Id.Set + module Map = Names.Id.Map +end + +module Kinds = struct + (* LSP kinds *) + let _file = 1 + let _module_ = 2 + let _namespace = 3 + let _package = 4 + let class_ = 5 + let method_ = 6 + let _property = 7 + let field = 8 + let _constructor = 9 + let enum = 10 + let _interface = 11 + let function_ = 12 + let variable = 13 + let _constant = 14 + let _string = 15 + let _number = 16 + let _boolean = 17 + let _array = 18 + let _object = 19 + let _key = 20 + let _null = 21 + let enumMember = 22 + let struct_ = 23 + let _event = 24 + let _operator = 25 + let _typeParameter = 26 +end + +module Info = struct + type 'l t = + { range : 'l + ; name : Names.Name.t CAst.t + ; kind : int + ; detail : string option (* usually the type *) + ; children : 'l t list option + } + + let make ~range ~name ~kind ?detail ?children () = + { range; name; kind; detail; children } +end let marshal_in ic : t = Marshal.from_channel ic let marshal_out oc v = Marshal.to_channel oc v [] @@ -92,3 +86,135 @@ let pp_loc ?(print_file = false) fmt loc = let loc_to_string ?print_file loc = Format.asprintf "%a" (pp_loc ?print_file) loc + +open CAst +open Vernacexpr + +let inductive_detail = function + | Inductive_kw -> (Kinds.enum, "Inductive") + | CoInductive -> (Kinds.enum, "CoInductive") + | Variant -> (Kinds.struct_, "Variant") + | Record -> (Kinds.struct_, "Record") + | Structure -> (Kinds.struct_, "Structure") + | Class _ -> (Kinds.class_, "Class") + +let assumption_detail = function + | Decls.Definitional -> "Variable" + | Logical -> "Axiom" + | Conjectural -> "Parameter" + | Context -> "Context" + +let definition_detail = function + | Decls.Definition -> "Definition" + | Coercion -> "Coercion" + | SubClass -> "SubClass" + | CanonicalStructure -> "CanonicalStructure" + | Example -> "Example" + | Fixpoint -> "Fixpoint" + | CoFixpoint -> "CoFixpoint" + | Scheme -> "Scheme" + | StructureComponent -> "StructureComponent" + | IdentityCoercion -> "IdentityCoercion" + | Instance -> "Instance" + | Method -> "Method" + | Let -> "Let" + +let theorem_detail = function + | Decls.Theorem -> "Theorem" + | Lemma -> "Lemma" + | Fact -> "Fact" + | Remark -> "Remark" + | Property -> "Property" + | Proposition -> "Proposition" + | Corollary -> "Corollary" + +let mk_name = CAst.map (fun id -> Names.Name id) + +let constructor_info ~lines ((_, (id, _typ)) : constructor_expr) = + let range = Option.get id.loc in + let range = Utils.to_range ~lines range in + let name = mk_name id in + let detail = "Constructor" in + let kind = Kinds.enumMember in + Info.make ~range ~name ~detail ~kind () + +let local_decl_expr_info ~lines ~kind ~detail (l : local_decl_expr) = + let name = + match l with + | AssumExpr (ln, _, _) -> ln + | DefExpr (ln, _, _, _) -> ln + in + let range = Option.get name.loc in + let range = Utils.to_range ~lines range in + Info.make ~range ~name ~kind ~detail () + +let projection_info ~lines ((ld, _) : local_decl_expr * record_field_attr) = + let kind = Kinds.field in + let detail = "Field" in + local_decl_expr_info ~lines ~detail ~kind ld + +let inductive_info ~lines ~range ikind (expr, _) = + let (_, (id, _)), _, _, cons = expr in + let name = mk_name id in + match cons with + | Constructors ci -> + let children = List.map (constructor_info ~lines) ci in + let kind, detail = inductive_detail ikind in + Info.make ~range ~name ~kind ~detail ~children () + | RecordDecl (_, pi, _) -> + let children = List.map (projection_info ~lines) pi in + let kind, detail = inductive_detail ikind in + Info.make ~range ~name ~kind ~detail ~children () + +let inductives_info ~lines ~range ikind idecls = + match idecls with + | [] -> None + | inds -> Some (List.map (inductive_info ~lines ~range ikind) inds) + +let ident_decl_info ~lines ~kind ~detail (lident, _) = + let range = Option.get lident.loc in + let range = Utils.to_range ~lines range in + let name = mk_name lident in + Info.make ~range ~name ~detail ~kind () + +let assumption_info ~lines kind (_, (ids, _)) = + let detail = assumption_detail kind in + let kind = Kinds.variable in + List.map (ident_decl_info ~lines ~kind ~detail) ids + +let fixpoint_info ~range { fname; _ } = + let name = mk_name fname in + let detail = "Fixpoint" in + Info.make ~range ~name ~detail ~kind:Kinds.function_ () + +let make_info ~st:_ ~lines CAst.{ loc; v } : _ Info.t list option = + let open Vernacexpr in + match loc with + | None -> None + | Some range -> ( + let range = Utils.to_range ~lines range in + (* TODO: sections *) + match v.expr with + | VernacDefinition ((_, kind), (name, _), _) -> + let detail = definition_detail kind in + let kind = Kinds.function_ in + Some [ Info.make ~range ~name ~detail ~kind () ] + | VernacStartTheoremProof (kind, ndecls) -> ( + let detail = theorem_detail kind in + let kind = Kinds.function_ in + match ndecls with + | ((id, _), _) :: _ -> + let name = mk_name id in + Some [ Info.make ~range ~name ~detail ~kind () ] + | [] -> None) + | VernacInductive (ikind, idecls) -> + inductives_info ~lines ~range ikind idecls + | VernacAssumption ((_, kind), _, ids) -> + Some (List.concat_map (assumption_info ~lines kind) ids) + | VernacFixpoint (_, f_expr) -> + Some (List.map (fixpoint_info ~range) f_expr) + | VernacInstance ((name, _), _, _, _, _) -> + let kind = Kinds.method_ in + let detail = "Instance" in + Some [ Info.make ~range ~name ~kind ~detail () ] + | _ -> None) diff --git a/coq/ast.mli b/coq/ast.mli index c845feefa..4fb08fb96 100644 --- a/coq/ast.mli +++ b/coq/ast.mli @@ -3,7 +3,33 @@ type t val loc : t -> Loc.t option val hash : t -> int val compare : t -> t -> int -val grab_definitions : (Loc.t -> Names.Id.t -> 'a) -> t list -> 'a list + +module Id : sig + type t + + val of_string : string -> t + val of_coq : Names.Id.t -> t + val to_coq : t -> Names.Id.t + + module Set : CSet.S with type elt = t + module Map : CMap.ExtS with type key = t and module Set := Set +end + +(** Information about the Ast, to move to lang *) +module Info : sig + type 'l t = + { range : 'l + ; name : Names.Name.t CAst.t + ; kind : int + ; detail : string option (* usually the type *) + ; children : 'l t list option + } +end + +(** [make_info ~st ast] Compute info about a possible definition in [ast], we + need [~st] to compute the type. *) +val make_info : + st:State.t -> lines:string array -> t -> Lang.Range.t Info.t list option (** Printing *) val print : t -> Pp.t diff --git a/coq/protect.ml b/coq/protect.ml index 647137f59..2aff321fc 100644 --- a/coq/protect.ml +++ b/coq/protect.ml @@ -46,24 +46,42 @@ let eval_exn ~f x = if CErrors.is_anomaly e then R.Completed (Error (Anomaly (loc, msg))) else R.Completed (Error (User (loc, msg))) +let _bind_exn ~f x = + match x with + | R.Interrupted -> R.Interrupted + | R.Completed (Error e) -> R.Completed (Error e) + | R.Completed (Ok r) -> f r + +let fb_queue : Loc.t Message.t list ref = ref [] + module E = struct type ('a, 'l) t = { r : ('a, 'l) R.t ; feedback : 'l Message.t list } + let eval ~f x = + let r = eval_exn ~f x in + let feedback = List.rev !fb_queue in + let () = fb_queue := [] in + { r; feedback } + let map ~f { r; feedback } = { r = R.map ~f r; feedback } let map_message ~f (loc, lvl, msg) = (Option.map f loc, lvl, msg) let map_loc ~f { r; feedback } = { r = R.map_loc ~f r; feedback = List.map (map_message ~f) feedback } -end -let fb_queue : Loc.t Message.t list ref = ref [] + let bind ~f { r; feedback } = + match r with + | R.Interrupted -> { r = R.Interrupted; feedback } + | R.Completed (Error e) -> { r = R.Completed (Error e); feedback } + | R.Completed (Ok r) -> + let { r; feedback = fb2 } = f r in + { r; feedback = feedback @ fb2 } + + let ok v = { r = Completed (Ok v); feedback = [] } +end (* Eval with reified exceptions and feedback *) -let eval ~f x = - let r = eval_exn ~f x in - let feedback = List.rev !fb_queue in - let () = fb_queue := [] in - { E.r; feedback } +let eval ~f x = E.eval ~f x diff --git a/coq/protect.mli b/coq/protect.mli index 00d675d77..faf080eb3 100644 --- a/coq/protect.mli +++ b/coq/protect.mli @@ -35,6 +35,8 @@ module E : sig val map : f:('a -> 'b) -> ('a, 'l) t -> ('b, 'l) t 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 end (** Must be hooked to allow [Protect] to capture the feedback. *) diff --git a/coq/state.ml b/coq/state.ml index 01ea22a36..597324ebd 100644 --- a/coq/state.ml +++ b/coq/state.ml @@ -76,6 +76,8 @@ let mode ~st = let parsing ~st = st.Vernacstate.parsing +module Proof_ = Proof + module Proof = struct type t = Vernacstate.LemmaStack.t @@ -98,7 +100,7 @@ let in_state ~st ~f a = in Protect.eval ~f a -let admit ~st = +let admit ~st () = let () = Vernacstate.unfreeze_interp_state st in match st.Vernacstate.lemmas with | None -> st @@ -110,6 +112,15 @@ let admit ~st = let st = Vernacstate.freeze_interp_state ~marshallable:false in { st with lemmas; program } -(* TODO: implement protect once error recovery supports a failing recovery - execution *) -(* let admit ~st = Protect.eval ~f:(admit ~st) () *) +let admit ~st = Protect.eval ~f:(admit ~st) () + +let admit_goal ~st () = + let () = Vernacstate.unfreeze_interp_state st in + match st.Vernacstate.lemmas with + | None -> st + | Some lemmas -> + let f pf = Declare.Proof.by Proofview.give_up pf |> fst in + let lemmas = Some (Vernacstate.LemmaStack.map_top ~f lemmas) in + { st with lemmas } + +let admit_goal ~st = Protect.eval ~f:(admit_goal ~st) () diff --git a/coq/state.mli b/coq/state.mli index 60ac6426a..b1765a0ce 100644 --- a/coq/state.mli +++ b/coq/state.mli @@ -22,8 +22,11 @@ val in_state : st:t -> f:('a -> 'b) -> 'a -> ('b, Loc.t) Protect.E.t (** Drop the proofs from the state *) val drop_proofs : st:t -> t -(** Admit an ongoing proof *) -val admit : st:t -> t +(** Fully admit an ongoing proof *) +val admit : st:t -> (t, Loc.t) Protect.E.t + +(** Admit the current sub-goal *) +val admit_goal : st:t -> (t, Loc.t) Protect.E.t (** Extra / interanl *) val marshal_in : in_channel -> t diff --git a/fleche/utf8.ml b/coq/utf8.ml similarity index 84% rename from fleche/utf8.ml rename to coq/utf8.ml index b5bfb7d52..889ff8d39 100644 --- a/fleche/utf8.ml +++ b/coq/utf8.ml @@ -59,12 +59,13 @@ let find_char line byte = 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); + (* 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)); + (* (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/fleche/utf8.mli b/coq/utf8.mli similarity index 100% rename from fleche/utf8.mli rename to coq/utf8.mli diff --git a/fleche/coq_utils.ml b/coq/utils.ml similarity index 100% rename from fleche/coq_utils.ml rename to coq/utils.ml diff --git a/fleche/coq_utils.mli b/coq/utils.mli similarity index 100% rename from fleche/coq_utils.mli rename to coq/utils.mli diff --git a/default.nix b/default.nix index 19a8f8134..c7d0c267d 100644 --- a/default.nix +++ b/default.nix @@ -1,25 +1,14 @@ -{ - pkgs ? import (fetchTarball "https://github.com/vbgl/nixpkgs/tarball/2a4e60c330d66638897ec450126eb1e3a9a13148") {} -}: - -with pkgs; - -let oc = ocaml-ng.ocamlPackages_4_07; in - -stdenv.mkDerivation { - name = "coq-lsp-0"; - src = builtins.filterSource (p: _: builtins.baseNameOf p != "_build") ./.; - buildInputs = [ - dune oc.ocaml oc.findlib oc.num oc.yojson oc.cmdliner - oc.lablgtk - ]; - - preBuild = '' - for f in kernel dev/tools - do - patchShebangs coq/$f - done - ''; - - inherit (dune) installPhase; -} +( + import + ( + let + lock = builtins.fromJSON (builtins.readFile ./flake.lock); + in + fetchTarball { + url = "https://github.com/edolstra/flake-compat/archive/${lock.nodes.flake-compat.locked.rev}.tar.gz"; + sha256 = lock.nodes.flake-compat.locked.narHash; + } + ) + {src = ./.;} +) +.defaultNix diff --git a/editor/code/CHANGELOG.md b/editor/code/CHANGELOG.md index 512e23f7c..fbfb4e30a 100644 --- a/editor/code/CHANGELOG.md +++ b/editor/code/CHANGELOG.md @@ -1,7 +1,24 @@ # coq-lsp 0.1.5: Form ---------------------- -- Improved syntax highligting of coq markdown files + - General bugfix and quality-of-life release. + - Markdown Coq code blocks now must specify "coq" as a language + - Improved syntax highlighting of Coq markdown files + - Info panel has been greatly improved + - Bugfix on message display after the port to React + - Hover will display type of identifier at point + - Jump to definition support + - Goal display handles background goals better, showing preview, + goals stack, and focusing information + - The goal display now numbers goals starting with 1 instead of 0 + - Hypotheses with bodies are now correctly displayed + - Support unicode characters in filenames + - Stop checking documents after a maximum number of errors (user configurable) + - Goal view now supports find + - Display Coq warnings, info and debug messages in info panel + - Improved outline view, with more details and types + - Server greatly improved with better error heuristics, see server + changelog for more information # coq-lsp 0.1.4: View ---------------------- diff --git a/editor/code/flakeModule.nix b/editor/code/flakeModule.nix new file mode 100644 index 000000000..3ecea7ced --- /dev/null +++ b/editor/code/flakeModule.nix @@ -0,0 +1,52 @@ +{ + perSystem = { + config, + pkgs, + lib, + inputs', + ... + }: { + packages.vsix = (inputs'.napalm.legacyPackages).buildPackage ./. { + installPhase = '' + mkdir $out + ${lib.getExe pkgs.vsce} package -o $out/$name.zip > /dev/null 2>&1 + ''; + + passthru = let + attrs = builtins.fromJSON (builtins.readFile ./package.json); + in { + extPublisher = attrs.publisher; + extName = attrs.name; + extVersion = attrs.version; + extId = with attrs; "${publisher}.${name}"; + }; + }; + + packages.vscode-extension = let + vsix = config.packages.vsix; + in + pkgs.vscode-utils.buildVscodeExtension + { + inherit (vsix) name; + + version = vsix.extVersion; + + vscodeExtPublisher = vsix.extPublisher; + vscodeExtName = vsix.extName; + vscodeExtUniqueId = vsix.extId; + + src = "${vsix}/${vsix.name}.zip"; + }; + + devShells.client-vscode = pkgs.mkShell { + packages = builtins.attrValues { + inherit (pkgs) nodejs; + inherit (pkgs.nodePackages) typescript typescript-language-server; + + inherit (config.treefmt.build) wrapper; + }; + }; + + treefmt.config.programs.prettier.enable = true; + }; +} diff --git a/editor/code/lib/types.ts b/editor/code/lib/types.ts index 74ba83fde..848019838 100644 --- a/editor/code/lib/types.ts +++ b/editor/code/lib/types.ts @@ -1,6 +1,7 @@ import { VersionedTextDocumentIdentifier, Position, + Range, } from "vscode-languageserver-types"; export interface Hyp { @@ -22,11 +23,17 @@ export interface GoalConfig { given_up: Goal[]; } +export interface Message { + range?: Range; + level: number; + text: Pp; +} + export interface GoalAnswer { textDocument: VersionedTextDocumentIdentifier; position: Position; goals?: GoalConfig; - messages: Pp[]; + messages: Pp[] | Message[]; error?: Pp; } diff --git a/editor/code/views/info/Message.tsx b/editor/code/views/info/Message.tsx index 2bc35b5f9..ce03f8817 100644 --- a/editor/code/views/info/Message.tsx +++ b/editor/code/views/info/Message.tsx @@ -1,11 +1,13 @@ import objectHash from "object-hash"; +import { Message } from "../../lib/types"; import { CoqPp } from "./CoqPp"; -export function Message({ message }: { message: string }) { +export function Message({ message }: { message: string | Message }) { let key = objectHash(message); + let text = typeof message === "string" ? message : message.text; return (
  • - +
    • ); } diff --git a/editor/code/views/info/Messages.tsx b/editor/code/views/info/Messages.tsx index 7913a9b06..dd6156b70 100644 --- a/editor/code/views/info/Messages.tsx +++ b/editor/code/views/info/Messages.tsx @@ -1,10 +1,11 @@ import objectHash from "object-hash"; +import { Message as Msg } from "../../lib/types"; import { Details } from "./Details"; import { Message } from "./Message"; import "./media/messages.css"; -export type MessagesParams = { messages: string[] }; +export type MessagesParams = { messages: string[] | Msg[] }; export function Messages({ messages }: MessagesParams) { let count = messages.length; diff --git a/etc/doc/PROTOCOL.md b/etc/doc/PROTOCOL.md index 16a794e03..c3049f271 100644 --- a/etc/doc/PROTOCOL.md +++ b/etc/doc/PROTOCOL.md @@ -102,11 +102,17 @@ interface GoalConfig { given_up : Goal[]; } +export interface Message { + range?: Range; + level : number; + text : Pp +} + interface GoalAnswer { textDocument: VersionedTextDocumentIdentifier; position: Position; goals?: GoalConfig; - messages: Pp[]; + messages: Pp[] | Message[]; error?: Pp; } ``` @@ -145,6 +151,7 @@ implementation, and we adapted it to `coq-lsp`. #### Changelog +- v0.1.5: message type does now include range and level - v0.1.4: goal type generic, the `stacks` and `def` fields appear, compatible v0.1.3 clients - v0.1.3: send full goal configuration with shelf, given_up, versioned identifier for document - v0.1.2: include messages and optional error in the request response diff --git a/etc/img/lsp-doc-symbols.png b/etc/img/lsp-doc-symbols.png new file mode 100644 index 000000000..b0a751a91 Binary files /dev/null and b/etc/img/lsp-doc-symbols.png differ diff --git a/etc/img/lsp-errors.gif b/etc/img/lsp-errors.gif new file mode 100644 index 000000000..f6961e2c1 Binary files /dev/null and b/etc/img/lsp-errors.gif differ diff --git a/examples/Rtrigo1.v b/examples/Rtrigo1.v index 176c4c2eb..6a5ef5d7f 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. @@ -348,6 +348,9 @@ intros a n lower upper; apply pre_cos_bound. replace ((PI/2) * 2) with PI by field. generalize PI_4; intros; lra. Qed. + + + (**********) Lemma neg_cos : forall x:R, cos (x + PI) = - cos x. Proof. diff --git a/examples/documentSymbol.v b/examples/documentSymbol.v new file mode 100644 index 000000000..06cf6e4ff --- /dev/null +++ b/examples/documentSymbol.v @@ -0,0 +1,45 @@ +Record a := { + proj1 : Type + ; proj2 : Type +}. + +Inductive foo := A | B : a -> foo. + +Inductive eh1 := Ah1 : eh2 -> eh1 +with eh2 := Bh1 : eh1 -> eh2. + +Variable (j : nat). + +Axiom test : False. + +Fixpoint f1 (n : nat) := match n with O => true | S n => f2 n end +with f2 (n : nat) := match n with O => true | S n => f1 n end. + +Class EqBar := { wit : nat }. + +(* Fixme here, Instance is not recognized as a proof opener *) +Instance foobar : EqBar. +Admitted. + +Section Moo. + + Variable (jj : nat). + Hypothesis (umm : Type). + + Definition m1 := 3. + + Theorem m2 : Type. Qed. + +End Moo. + +Module Bar. + + Variable (u : nat). + + Parameter (v : nat). + + Definition k := 3. + + Theorem not : False. Qed. + +End Bar. \ No newline at end of file diff --git a/examples/ex0.v b/examples/ex0.v index b89961bd1..0a675e5a5 100644 --- a/examples/ex0.v +++ b/examples/ex0.v @@ -36,7 +36,7 @@ Definition hola := 3. Inductive event : Type := | R of nat - | S of nat. + | S of nat. Record pair_emilio := { fst : nat; @@ -74,6 +74,8 @@ Record network := ; send : time -> address -> time -> bool }. +Definition ab := 3. + Lemma broken1 : False. Proof. admit. Qed. diff --git a/examples/goals.v b/examples/goals.v index ff54ff012..27066206d 100644 --- a/examples/goals.v +++ b/examples/goals.v @@ -13,4 +13,29 @@ Lemma bar : nat. Proof. pose (a := 3). exact a. +Qed. + +Lemma failingBullet : (1 = 1) /\ (21 = 21 /\ 22 = 22) /\ (3 = 3). +Proof. +split;[|split]. +- +- +- +Qed. + +Lemma failingsubProof : (1 = 1) /\ (21 = 21 /\ 22 = 22) /\ (3 = 3). +Proof. +split;[|split]. +3:{ } +- idtac. +- split. 2:{ } + + now auto. +Qed. + +Lemma anotherFailing : nat * nat * nat. +Proof. + refine (_,_,_). + { apply S. } + { exact 2. } + exact 1. Qed. \ No newline at end of file diff --git a/flake.lock b/flake.lock index 92194a57d..3aff546d0 100644 --- a/flake.lock +++ b/flake.lock @@ -1,58 +1,62 @@ { "nodes": { - "flake-compat": { + "coq-serapi": { "flake": false, "locked": { - "lastModified": 1627913399, - "narHash": "sha256-hY8g6H2KFL8ownSiFeMOjwPC8P0ueXpCVEbxgda3pko=", - "owner": "edolstra", - "repo": "flake-compat", - "rev": "12c64ca55c1014cdc1b16ed5a804aa8576601ff2", + "lastModified": 1673473454, + "narHash": "sha256-ZeKkbEcTfe/5X/pW+Kl4Xjcj3cdZcs06LTg4dZIuHq8=", + "owner": "ejgallego", + "repo": "coq-serapi", + "rev": "79880d37705b6ec08108f5e6044fd7a128923753", "type": "github" }, "original": { - "owner": "edolstra", - "repo": "flake-compat", + "owner": "ejgallego", + "ref": "v8.17", + "repo": "coq-serapi", "type": "github" } }, - "flake-utils": { + "flake-compat": { + "flake": false, "locked": { - "lastModified": 1667395993, - "narHash": "sha256-nuEHfE/LcWyuSWnS8t12N1wc105Qtau+/OdUAjtQ0rA=", - "owner": "numtide", - "repo": "flake-utils", - "rev": "5aed5285a952e0b949eb3ba02c12fa4fcfef535f", + "lastModified": 1673956053, + "narHash": "sha256-4gtG9iQuiKITOjNQQeQIpoIB6b16fm+504Ch3sNKLd8=", + "owner": "edolstra", + "repo": "flake-compat", + "rev": "35bb57c0c8d8b62bbfd284272c928ceb64ddbde9", "type": "github" }, "original": { - "owner": "numtide", - "repo": "flake-utils", + "owner": "edolstra", + "repo": "flake-compat", "type": "github" } }, - "flake-utils_2": { + "flake-parts": { + "inputs": { + "nixpkgs-lib": "nixpkgs-lib" + }, "locked": { - "lastModified": 1667395993, - "narHash": "sha256-nuEHfE/LcWyuSWnS8t12N1wc105Qtau+/OdUAjtQ0rA=", - "owner": "numtide", - "repo": "flake-utils", - "rev": "5aed5285a952e0b949eb3ba02c12fa4fcfef535f", + "lastModified": 1675933616, + "narHash": "sha256-/rczJkJHtx16IFxMmAWu5nNYcSXNg1YYXTHoGjLrLUA=", + "owner": "hercules-ci", + "repo": "flake-parts", + "rev": "47478a4a003e745402acf63be7f9a092d51b83d7", "type": "github" }, "original": { - "owner": "numtide", - "repo": "flake-utils", - "type": "github" + "id": "flake-parts", + "type": "indirect" } }, - "flake-utils_3": { + "flake-utils": { "locked": { - "lastModified": 1638122382, - "narHash": "sha256-sQzZzAbvKEqN9s0bzWuYmRaA03v40gaJ4+iL1LXjaeI=", + "lastModified": 1659877975, + "narHash": "sha256-zllb8aq3YO3h8B/U0/J1WBgAL8EX5yWf5pMj3G0NAmc=", "owner": "numtide", "repo": "flake-utils", - "rev": "74f7e4319258e287b0f9cb95426c9853b282730b", + "rev": "c0e246b9b83f637f4681389ecabcb2681b4f3af0", "type": "github" }, "original": { @@ -61,198 +65,118 @@ "type": "github" } }, - "mirage-opam-overlays": { - "flake": false, + "napalm": { + "inputs": { + "flake-utils": "flake-utils", + "nixpkgs": "nixpkgs" + }, "locked": { - "lastModified": 1661959605, - "narHash": "sha256-CPTuhYML3F4J58flfp3ZbMNhkRkVFKmBEYBZY5tnQwA=", - "owner": "dune-universe", - "repo": "mirage-opam-overlays", - "rev": "05f1c1823d891ce4d8adab91f5db3ac51d86dc0b", + "lastModified": 1672245824, + "narHash": "sha256-i596lbPiA/Rfx3DiJiCluxdgxWY7oGSgYMT7OmM+zik=", + "owner": "nix-community", + "repo": "napalm", + "rev": "7c25a05cef52dc405f4688422ce0046ca94aadcf", "type": "github" }, "original": { - "owner": "dune-universe", - "repo": "mirage-opam-overlays", + "owner": "nix-community", + "repo": "napalm", "type": "github" } }, "nixpkgs": { "locked": { - "lastModified": 1672366314, - "narHash": "sha256-F/LEtdZ90LqFzLaGtUmzsJFtarFsPJzxM9rahkb24FM=", - "owner": "nixos", + "lastModified": 1663087123, + "narHash": "sha256-cNIRkF/J4mRxDtNYw+9/fBNq/NOA2nCuPOa3EdIyeDs=", + "owner": "NixOS", "repo": "nixpkgs", - "rev": "726088a96454587d4a640d28ec442126518e449b", + "rev": "9608ace7009ce5bc3aeb940095e01553e635cbc7", "type": "github" }, "original": { - "owner": "nixos", - "ref": "nixpkgs-unstable", + "owner": "NixOS", + "ref": "nixos-unstable", "repo": "nixpkgs", "type": "github" } }, - "nixpkgs_2": { + "nixpkgs-lib": { "locked": { - "lastModified": 1657802959, - "narHash": "sha256-9+JWARSdlL8KiH3ymnKDXltE1vM+/WEJ78F5B1kjXys=", - "owner": "nixos", + "dir": "lib", + "lastModified": 1675183161, + "narHash": "sha256-Zq8sNgAxDckpn7tJo7V1afRSk2eoVbu3OjI1QklGLNg=", + "owner": "NixOS", "repo": "nixpkgs", - "rev": "4a01ca36d6bfc133bc617e661916a81327c9bbc8", + "rev": "e1e1b192c1a5aab2960bf0a0bd53a2e8124fa18e", "type": "github" }, "original": { - "owner": "nixos", + "dir": "lib", + "owner": "NixOS", "ref": "nixos-unstable", "repo": "nixpkgs", "type": "github" } }, - "ocamllsp": { - "inputs": { - "flake-utils": "flake-utils_2", - "nixpkgs": [ - "nixpkgs" - ], - "opam-nix": [ - "opam-nix" - ], - "opam-repository": "opam-repository" - }, - "locked": { - "lastModified": 1672361134, - "narHash": "sha256-zXvIZfrV0/saOmG/IZbqIfC0KkdCc8kTIkLfR6KbDDc=", - "ref": "refs/heads/master", - "rev": "8367f37bab3fb036e19892e46843d3807e25b3a8", - "revCount": 1927, - "submodules": true, - "type": "git", - "url": "https://www.github.com/ocaml/ocaml-lsp" - }, - "original": { - "submodules": true, - "type": "git", - "url": "https://www.github.com/ocaml/ocaml-lsp" - } - }, - "opam-nix": { - "inputs": { - "flake-compat": "flake-compat", - "flake-utils": "flake-utils_3", - "mirage-opam-overlays": "mirage-opam-overlays", - "nixpkgs": "nixpkgs_2", - "opam-overlays": "opam-overlays", - "opam-repository": "opam-repository_2", - "opam2json": "opam2json" - }, - "locked": { - "lastModified": 1670004517, - "narHash": "sha256-7SffiN2S9pVfOoBCcEdY/iJe28p/eiRqVLXG7/8Jb3I=", - "owner": "tweag", - "repo": "opam-nix", - "rev": "b12b7fcd6f9ea0a8a939c05c68a95525f0d80af6", - "type": "github" - }, - "original": { - "owner": "tweag", - "repo": "opam-nix", - "type": "github" - } - }, - "opam-overlays": { - "flake": false, - "locked": { - "lastModified": 1654162756, - "narHash": "sha256-RV68fUK+O3zTx61iiHIoS0LvIk0E4voMp+0SwRg6G6c=", - "owner": "dune-universe", - "repo": "opam-overlays", - "rev": "c8f6ef0fc5272f254df4a971a47de7848cc1c8a4", - "type": "github" - }, - "original": { - "owner": "dune-universe", - "repo": "opam-overlays", - "type": "github" - } - }, - "opam-repository": { - "flake": false, + "nixpkgs_2": { "locked": { - "lastModified": 1671196811, - "narHash": "sha256-8mYe1yUaKpExjyGUh3ppJ2U0BRbkS1kySMoM619In4I=", - "owner": "ocaml", - "repo": "opam-repository", - "rev": "2b84338837f46d5559e476c3766ebc61ed2849f3", + "lastModified": 1675763311, + "narHash": "sha256-bz0Q2H3mxsF1CUfk26Sl9Uzi8/HFjGFD/moZHz1HebU=", + "owner": "NixOS", + "repo": "nixpkgs", + "rev": "fab09085df1b60d6a0870c8a89ce26d5a4a708c2", "type": "github" }, "original": { - "owner": "ocaml", - "repo": "opam-repository", + "owner": "NixOS", + "ref": "nixos-unstable", + "repo": "nixpkgs", "type": "github" } }, - "opam-repository_2": { - "flake": false, + "nixpkgs_3": { "locked": { - "lastModified": 1661161626, - "narHash": "sha256-J3P+mXLwE2oEKTlMnx8sYRxwD/uNGSKM0AkAB7BNTxA=", - "owner": "ocaml", - "repo": "opam-repository", - "rev": "54e69ff0949a3aaec0d5e3d67898bb7f279ab09f", + "lastModified": 1675545634, + "narHash": "sha256-TbQeQcM5TA/wIho6xtzG+inUfiGzUXi8ewwttiQWYJE=", + "owner": "nixos", + "repo": "nixpkgs", + "rev": "0591d6b57bfeb55dfeec99a671843337bc2c3323", "type": "github" }, "original": { - "owner": "ocaml", - "repo": "opam-repository", + "owner": "nixos", + "ref": "nixos-unstable", + "repo": "nixpkgs", "type": "github" } }, - "opam-repository_3": { - "flake": false, - "locked": { - "lastModified": 1672313305, - "narHash": "sha256-FfmBJNaSgU2VnwHKE0rdWG47qNNjK3TQRhPovPGzRnI=", - "owner": "ocaml", - "repo": "opam-repository", - "rev": "9af04a84c30c4ddd01244cc07d626d8c1837d2c7", - "type": "github" - }, - "original": { - "owner": "ocaml", - "repo": "opam-repository", - "type": "github" + "root": { + "inputs": { + "coq-serapi": "coq-serapi", + "flake-compat": "flake-compat", + "flake-parts": "flake-parts", + "napalm": "napalm", + "nixpkgs": "nixpkgs_2", + "treefmt": "treefmt" } }, - "opam2json": { + "treefmt": { "inputs": { - "nixpkgs": [ - "opam-nix", - "nixpkgs" - ] + "nixpkgs": "nixpkgs_3" }, "locked": { - "lastModified": 1665671715, - "narHash": "sha256-7f75C6fIkiLzfkwLpJxlQIKf+YORGsXGV8Dr2LDDi+A=", - "owner": "tweag", - "repo": "opam2json", - "rev": "32fa2dcd993a27f9e75ee46fb8b78a7cd5d05113", + "lastModified": 1675939481, + "narHash": "sha256-LwwcWeyExA02GGn8QCQfZjft+blg101OXBQWglCqPVA=", + "owner": "numtide", + "repo": "treefmt-nix", + "rev": "e9033eca3d7139fd499f310023ddc3bb5abff515", "type": "github" }, "original": { - "owner": "tweag", - "repo": "opam2json", + "owner": "numtide", + "repo": "treefmt-nix", "type": "github" } - }, - "root": { - "inputs": { - "flake-utils": "flake-utils", - "nixpkgs": "nixpkgs", - "ocamllsp": "ocamllsp", - "opam-nix": "opam-nix", - "opam-repository": "opam-repository_3" - } } }, "root": "root", diff --git a/flake.nix b/flake.nix index ee6bbe625..16d0af51f 100644 --- a/flake.nix +++ b/flake.nix @@ -1,70 +1,98 @@ { - inputs = { - nixpkgs.url = "github:nixos/nixpkgs/nixpkgs-unstable"; - opam-nix.url = "github:tweag/opam-nix"; - flake-utils.url = "github:numtide/flake-utils"; - ocamllsp.url = "git+https://www.github.com/ocaml/ocaml-lsp?submodules=1"; - ocamllsp.inputs.opam-nix.follows = "opam-nix"; - ocamllsp.inputs.nixpkgs.follows = "nixpkgs"; - opam-repository = { - url = "github:ocaml/opam-repository"; - flake = false; - }; - }; - outputs = { self, flake-utils, opam-nix, nixpkgs, ocamllsp, opam-repository }@inputs: - let package = "coq-lsp"; - in flake-utils.lib.eachDefaultSystem (system: - let - devPackages = { - # Extra packages for testing - }; - pkgs = nixpkgs.legacyPackages.${system}; - ocamlformat = - # Detection of ocamlformat version from .ocamlformat file - let - ocamlformat_version = - let - lists = pkgs.lib.lists; - strings = pkgs.lib.strings; - ocamlformat_config = strings.splitString "\n" (builtins.readFile ./.ocamlformat); - prefix = "version="; - ocamlformat_version_pred = line: strings.hasPrefix prefix line; - version_line = lists.findFirst ocamlformat_version_pred "not_found" ocamlformat_config; - version = strings.removePrefix prefix version_line; - in - builtins.replaceStrings [ "." ] [ "_" ] version; - in - builtins.getAttr ("ocamlformat_" + ocamlformat_version) pkgs; - in - { - packages = - let - scope = opam-nix.lib.${system}.buildOpamProject' - { - repos = [ opam-repository ]; - } ./. - (devPackages // { ocaml-base-compiler = "4.14.0"; }); + description = "A language server (LSP) for the Coq theorem prover"; + + outputs = inputs @ { + self, + flake-parts, + treefmt, + ... + }: + flake-parts.lib.mkFlake {inherit inputs;} { + systems = ["x86_64-linux" "aarch64-linux" "x86_64-darwin" "aarch64-darwin"]; + imports = [treefmt.flakeModule ./editor/code/flakeModule.nix]; + + perSystem = { + config, + pkgs, + lib, + ... + }: let + l = lib // builtins; + coq_8_17 = pkgs.coqPackages_8_17; + coqPackages = coq_8_17.coqPackages; + ocamlPackages = coq_8_17.coq.ocamlPackages; + in { + packages.default = config.packages.coq-lsp; + + # NOTE(2023-06-02): Nix does not support top-level self submodules (yet) + packages.coq-lsp = ocamlPackages.buildDunePackage { + duneVersion = "3"; + + pname = "coq-lsp"; + version = "${self.lastModifiedDate}+8.17-rc1"; + + src = self.outPath; + + nativeBuildInputs = l.attrValues { + inherit (ocamlPackages) menhir; + }; + + propagatedBuildInputs = let + serapi = + (coqPackages.lib.overrideCoqDerivation { + defaultVersion = "8.17.0+0.17.0"; + } + coqPackages.serapi) + .overrideAttrs (_: { + src = inputs.coq-serapi; + }); in - scope // { default = self.packages.${system}.${package}; }; + l.attrValues { + inherit serapi; + inherit (ocamlPackages) yojson cmdliner uri; + }; + }; + + treefmt.config = { + projectRootFile = "dune-project"; - devShells.fmt = - pkgs.mkShell { - inputsFrom = [ pkgs.dune_3 ]; - buildInputs = [ pkgs.dune_3 ocamlformat ]; + flakeFormatter = true; + + settings.global.excludes = ["./vendor/**"]; + + programs.alejandra.enable = true; + programs.ocamlformat = { + enable = true; + configFile = ./.ocamlformat; }; + }; + + devShells.default = pkgs.mkShell { + inputsFrom = [config.packages.coq-lsp]; - devShell = - pkgs.mkShell { - nativeBuildInputs = [ pkgs.opam ]; - buildInputs = (with pkgs; - [ - # dev tools - ocamlformat - nodejs - ]) ++ [ ocamllsp.outputs.packages.${system}.ocaml-lsp-server ] - ++ (builtins.map (s: builtins.getAttr s self.packages.${system}) - (builtins.attrNames devPackages)); - inputsFrom = [ self.packages.${system}.default ]; + packages = l.attrValues { + inherit (config.treefmt.build) wrapper; + inherit (pkgs) dune_3; + inherit (ocamlPackages) ocaml ocaml-lsp; }; - }); + }; + }; + }; + + inputs = { + nixpkgs.url = "github:NixOS/nixpkgs/nixos-unstable"; + treefmt.url = "github:numtide/treefmt-nix"; + + napalm.url = "github:nix-community/napalm"; + + flake-compat = { + url = "github:edolstra/flake-compat"; + flake = false; + }; + + coq-serapi = { + url = "github:ejgallego/coq-serapi/v8.17"; + flake = false; + }; + }; } diff --git a/fleche/contents.ml b/fleche/contents.ml index f9d3eb1d1..c5cea88ab 100644 --- a/fleche/contents.ml +++ b/fleche/contents.ml @@ -130,7 +130,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 = Utf8.length last_line in + let character = Coq.Utf8.length last_line in (Lang.Point.{ line = n_lines - 1; character; offset }, lines) let make ~uri ~raw = diff --git a/fleche/doc.ml b/fleche/doc.ml index 92dfb21eb..7fc78142c 100644 --- a/fleche/doc.ml +++ b/fleche/doc.ml @@ -12,37 +12,6 @@ module Util = struct | [] -> None | h :: _ -> Some h - let mk_diag ?extra range severity message = - Lang.Diagnostic.{ range; severity; message; extra } - - (* ast-dependent error diagnostic generation *) - let extra_diagnostics_of_ast ast = - match (Coq.Ast.to_coq ast).v with - | Vernacexpr.{ expr = VernacRequire (prefix, _export, module_refs); _ } -> - let refs = List.map fst module_refs in - Some [ Lang.Diagnostic.Extra.FailedRequire { prefix; refs } ] - | _ -> None - - let mk_error_diagnostic ~range ~msg ~ast = - let extra = extra_diagnostics_of_ast ast in - mk_diag ?extra range 1 msg - - let feed_to_diag ~drange (range, severity, message) = - let range = Option.default drange range in - mk_diag range severity message - - let diags_of_messages ~drange fbs = - (* TODO, replace this by a cutoff level *) - let cutoff = - if !Config.v.show_coq_info_messages then 5 - else if !Config.v.show_notices_as_diagnostics then 4 - else 3 - in - let diags, messages = - List.partition (fun (_, lvl, _) -> lvl < cutoff) fbs - in - (List.map (feed_to_diag ~drange) diags, messages) - let build_span start_loc end_loc = Loc. { start_loc with @@ -95,6 +64,15 @@ end (* [node list] is a very crude form of a meta-data map "loc -> data" , where for now [data] is only the goals. *) module Node = struct + module Ast = struct + type t = + { v : Coq.Ast.t + ; ast_info : Lang.Range.t Coq.Ast.Info.t list option + } + + let to_coq { v; _ } = Coq.Ast.to_coq v + end + module Info = struct type t = { cache_hit : bool @@ -111,33 +89,27 @@ module Node = struct let pp_time fmt = function | None -> Format.fprintf fmt "N/A" - | Some time -> Format.fprintf fmt "%.4f" time + | 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 memo_info = - Format.asprintf - "Cache Hit: %b | Parse (s/c): %.4f / %.2f | Exec (s/c): %a / %.2f" - cache_hit parsing_time cptime pp_time time cetime - in - let mem_info = - Format.asprintf "major words: %a | diff %a" Util.pp_words mw_after - Util.pp_words (mw_after -. mw_prev) - in - memo_info ^ "\n___\n" ^ mem_info + Format.asprintf + "Cached: %b | P: %.3f / %.2f | E: %a / %.2f | M: %a | Diff: %a" + cache_hit parsing_time cptime pp_time time cetime Util.pp_words mw_after + Util.pp_words (mw_after -. mw_prev) end module Message = struct type t = Lang.Range.t option * int * Pp.t let feedback_to_message ~lines (loc, lvl, msg) = - (Coq_utils.to_orange ~lines loc, lvl, msg) + (Coq.Utils.to_orange ~lines loc, lvl, msg) end type t = { range : Lang.Range.t - ; ast : Coq.Ast.t option (** Ast of node *) + ; ast : Ast.t option (** Ast of node *) ; state : Coq.State.t (** (Full) State of node *) ; diags : Lang.Diagnostic.t list ; messages : Message.t list @@ -150,6 +122,57 @@ module Node = struct let diags { diags; _ } = diags let messages { messages; _ } = messages let info { info; _ } = info + (* let with_state f n = Option.map (fun x -> (x, n.state)) (f n) *) +end + +module Diags = struct + let make ?extra range severity message = + Lang.Diagnostic.{ range; severity; message; extra } + + (* ast-dependent error diagnostic generation *) + let extra_diagnostics_of_ast ast = + match (Node.Ast.to_coq ast).v with + | Vernacexpr.{ expr = VernacRequire (prefix, _export, module_refs); _ } -> + let refs = List.map fst module_refs in + Some [ Lang.Diagnostic.Extra.FailedRequire { prefix; refs } ] + | _ -> None + + let error ~range ~msg ~ast = + let extra = extra_diagnostics_of_ast ast in + make ?extra range 1 msg + + let of_feed ~drange (range, severity, message) = + let range = Option.default drange range in + make range severity message + + type partition_kind = + | Left + | Both + | Right + + let partition ~f l = + let rec part l r = function + | [] -> (List.rev l, List.rev r) + | x :: xs -> ( + match f x with + | Left -> part (x :: l) r xs + | Both -> part (x :: l) (x :: l) xs + | Right -> part l (x :: r) xs) + in + part [] [] l + + let of_messages ~drange fbs = + (* TODO, replace this by a cutoff level *) + let cutoff = + if !Config.v.show_coq_info_messages then 5 + else if !Config.v.show_notices_as_diagnostics then 4 + else 3 + in + let f (_, lvl, _) = + if lvl = 2 then Both else if lvl < cutoff then Left else Right + in + let diags, messages = partition ~f fbs in + (List.map (of_feed ~drange) diags, messages) end module Completion = struct @@ -177,6 +200,7 @@ type t = { uri : Lang.LUri.File.t ; version : int ; contents : Contents.t + ; toc : Lang.Range.t Coq.Ast.Id.Map.t ; root : Coq.State.t ; nodes : Node.t list ; diags_dirty : bool (** Used to optimize `eager_diagnostics` *) @@ -188,6 +212,26 @@ let mk_doc root_state workspace uri = let asts doc = List.filter_map Node.ast doc.nodes +(* TOC handling *) + +(* XXX add children *) +let add_toc_info toc { Coq.Ast.Info.name; range; children = _; _ } = + match name.v with + | Names.Anonymous -> toc + | Names.Name id -> Coq.Ast.Id.(Map.add (of_coq id) range toc) + +let update_toc_info toc ast_info = List.fold_left add_toc_info 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 + +let rebuild_toc nodes = + List.fold_left update_toc_node Coq.Ast.Id.Map.empty nodes + let init_fname ~uri = let file = Lang.LUri.File.to_string_file uri in Loc.InFile { dirpath = None; file } @@ -196,7 +240,7 @@ let init_loc ~uri = Loc.initial (init_fname ~uri) let process_init_feedback ~stats range state messages = if not (CList.is_empty messages) then - let diags, messages = Util.diags_of_messages ~drange:range messages in + let diags, messages = Diags.of_messages ~drange:range messages in let parsing_time = 0.0 in let { Gc.major_words = mw_prev; _ } = Gc.quick_stat () in let info = @@ -211,15 +255,17 @@ let create ~state ~workspace ~uri ~version ~contents = Coq.Protect.R.map r ~f:(fun root -> let init_loc = init_loc ~uri in let lines = contents.Contents.lines in - let init_range = Coq_utils.to_range ~lines init_loc in + let init_range = Coq.Utils.to_range ~lines init_loc in let feedback = List.map (Node.Message.feedback_to_message ~lines) feedback in let stats = Stats.dump () in + let toc = Coq.Ast.Id.Map.empty in let nodes = process_init_feedback ~stats init_range root feedback in let diags_dirty = not (CList.is_empty nodes) in { uri ; contents + ; toc ; version ; root ; nodes @@ -237,9 +283,10 @@ let create_failed_permanent ~state ~uri ~version ~raw = |> Contents.R.map ~f:(fun contents -> let lines = contents.Contents.lines in let init_loc = init_loc ~uri in - let range = Coq_utils.to_range ~lines init_loc in + let range = Coq.Utils.to_range ~lines init_loc in { uri ; contents + ; toc = Coq.Ast.Id.Map.empty ; version ; root = state ; nodes = [] @@ -274,13 +321,14 @@ let compute_common_prefix ~init_range ~contents (prev : t) = in let common_idx = match_or_stop 0 in let nodes, range = recover_up_to_offset ~init_range prev common_idx in + let toc = rebuild_toc nodes in Io.Log.trace "prefix" ("resuming from " ^ Lang.Range.to_string range); let completed = Completion.Stopped range in - (nodes, completed) + (nodes, completed, toc) let bump_version ~init_range ~version ~contents doc = (* When a new document, we resume checking from a common prefix *) - let nodes, completed = compute_common_prefix ~init_range ~contents doc in + let nodes, completed, toc = compute_common_prefix ~init_range ~contents doc in (* Important: uri, root remain the same *) let uri = doc.uri in let root = doc.root in @@ -289,13 +337,14 @@ let bump_version ~init_range ~version ~contents doc = ; root ; nodes ; contents + ; toc ; diags_dirty = true (* EJGA: Is it worth to optimize this? *) ; completed } let bump_version ~version ~(contents : Contents.t) doc = let init_loc = init_loc ~uri:doc.uri in - let init_range = Coq_utils.to_range ~lines:contents.lines init_loc in + let init_range = Coq.Utils.to_range ~lines:contents.lines init_loc in match doc.completed with (* We can do better, but we need to handle the case where the anomaly is when restoring / executing the first sentence *) @@ -318,7 +367,8 @@ let bump_version ~version ~raw doc = let add_node ~node doc = let diags_dirty = if node.Node.diags <> [] then true else doc.diags_dirty in - { doc with nodes = node :: doc.nodes; diags_dirty } + let toc = update_toc_node doc.toc node in + { doc with nodes = node :: doc.nodes; toc; diags_dirty } let concat_diags doc = List.concat_map (fun node -> node.Node.diags) doc.nodes @@ -359,30 +409,38 @@ let parse_stm ~st ps = let rec find_recovery_for_failed_qed ~default nodes = match nodes with - | [] -> (default, None) + | [] -> Coq.Protect.E.ok (default, None) | { Node.ast = None; _ } :: ns -> find_recovery_for_failed_qed ~default ns | { ast = Some ast; state; range; _ } :: ns -> ( - match (Coq.Ast.to_coq ast).CAst.v.Vernacexpr.expr with + match (Node.Ast.to_coq ast).CAst.v.Vernacexpr.expr with | Vernacexpr.VernacStartTheoremProof _ -> ( if !Config.v.admit_on_bad_qed then - let state = Memo.interp_admitted ~st:state in - (state, Some range) + Memo.interp_admitted ~st:state + |> Coq.Protect.E.map ~f:(fun state -> (state, Some range)) else match ns with - | [] -> (default, None) - | n :: _ -> (n.state, Some n.range)) + | [] -> Coq.Protect.E.ok (default, None) + | n :: _ -> Coq.Protect.E.ok (n.state, Some n.range)) | _ -> find_recovery_for_failed_qed ~default ns) (* Simple heuristic for Qed. *) let state_recovery_heuristic doc st v = - match (Coq.Ast.to_coq v).CAst.v.Vernacexpr.expr with + match (Node.Ast.to_coq v).CAst.v.Vernacexpr.expr with (* Drop the top proof state if we reach a faulty Qed. *) | Vernacexpr.VernacEndProof _ -> - let st, range = find_recovery_for_failed_qed ~default:st doc.nodes in - let loc_msg = Option.cata Lang.Range.to_string "no loc" range in - Io.Log.trace "recovery" (loc_msg ^ " " ^ Memo.input_info (v, st)); - st - | _ -> st + find_recovery_for_failed_qed ~default:st doc.nodes + |> Coq.Protect.E.map ~f:(fun (st, range) -> + let loc_msg = Option.cata Lang.Range.to_string "no loc" range in + Io.Log.trace "recovery" (loc_msg ^ " " ^ Memo.input_info (v.v, st)); + st) + (* If a new focus (or unfocusing) fails, admit the proof and try again *) + | Vernacexpr.VernacBullet _ | Vernacexpr.VernacEndSubproof -> + Io.Log.trace "recovery" "bullet"; + Coq.State.admit_goal ~st + |> Coq.Protect.E.bind ~f:(fun st -> + Coq.Interp.interp ~st v.v + |> Coq.Protect.E.map ~f:(fun { Coq.Interp.Info.res } -> res)) + | _ -> Coq.Protect.E.ok st let interp_and_info ~parsing_time ~st ast = let { Gc.major_words = mw_prev; _ } = Gc.quick_stat () in @@ -417,7 +475,7 @@ type parse_action = let parse_action ~lines ~st last_tok doc_handle = let start_loc = Coq.Parsing.Parsable.loc doc_handle |> clexer_after in let parse_res, time = parse_stm ~st doc_handle in - let f = Coq_utils.to_range ~lines in + let f = Coq.Utils.to_range ~lines in let { Coq.Protect.E.r; feedback } = Coq.Protect.E.map_loc ~f parse_res in match r with | Coq.Protect.R.Interrupted -> (EOF (Stopped last_tok), [], feedback, time) @@ -428,7 +486,7 @@ let parse_action ~lines ~st last_tok doc_handle = EOF, the below trick doesn't work. That will involved updating the type of `main_entry` *) let last_tok = Coq.Parsing.Parsable.loc doc_handle in - let last_tok = Coq_utils.to_range ~lines last_tok in + let last_tok = Coq.Utils.to_range ~lines last_tok in (EOF (Yes last_tok), [], feedback, time) | Ok (Some ast) -> let () = if Debug.parsing then DDebug.parsed_sentence ~ast in @@ -437,15 +495,15 @@ let parse_action ~lines ~st last_tok doc_handle = (* We don't have a better altenative :(, usually missing error loc here means an anomaly, so we stop *) let err_range = last_tok in - let parse_diags = [ Util.mk_diag err_range 1 msg ] in + let parse_diags = [ Diags.make err_range 1 msg ] in (EOF (Failed last_tok), parse_diags, feedback, time) | Error (User (Some err_range, msg)) -> - let parse_diags = [ Util.mk_diag err_range 1 msg ] in + let parse_diags = [ Diags.make err_range 1 msg ] in Coq.Parsing.discard_to_dot doc_handle; let last_tok = Coq.Parsing.Parsable.loc doc_handle in - let last_tok_range = Coq_utils.to_range ~lines last_tok in + let last_tok_range = Coq.Utils.to_range ~lines last_tok in let span_loc = Util.build_span start_loc last_tok in - let span_range = Coq_utils.to_range ~lines span_loc in + let span_range = Coq.Utils.to_range ~lines span_loc in (Skip (span_range, last_tok_range), parse_diags, feedback, time)) (* Result of node-building action *) @@ -460,9 +518,7 @@ type document_action = let unparseable_node ~range ~parsing_diags ~parsing_feedback ~state ~parsing_time = - let fb_diags, messages = - Util.diags_of_messages ~drange:range parsing_feedback - in + 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 @@ -473,9 +529,9 @@ let unparseable_node ~range ~parsing_diags ~parsing_feedback ~state let assemble_diags ~range ~parsing_diags ~parsing_feedback ~diags ~feedback = let parsing_fb_diags, parsing_messages = - Util.diags_of_messages ~drange:range parsing_feedback + Diags.of_messages ~drange:range parsing_feedback in - let fb_diags, fb_messages = Util.diags_of_messages ~drange:range feedback in + let fb_diags, fb_messages = Diags.of_messages ~drange:range feedback in let diags = parsing_diags @ parsing_fb_diags @ fb_diags @ diags in let messages = parsing_messages @ fb_messages in (diags, messages) @@ -497,7 +553,7 @@ let stream_of_string ~offset text = let maybe_ok_diagnostics ~range = if !Config.v.ok_diagnostics then - let ok_diag = Util.mk_diag range 3 (Pp.str "OK") in + let ok_diag = Diags.make range 3 (Pp.str "OK") in [ ok_diag ] else [] @@ -505,6 +561,14 @@ 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 } +(* XXX: This should be refined. *) +let recovery_interp ~doc ~st ~ast = + let { Coq.Protect.E.r; feedback = _ } = state_recovery_heuristic doc st ast in + match r with + | Interrupted -> st + | Completed (Ok st) -> st + | Completed (Error _) -> st + let node_of_coq_result ~doc ~range ~ast ~st ~parsing_diags ~parsing_feedback ~feedback ~info last_tok res = match res with @@ -518,8 +582,8 @@ let node_of_coq_result ~doc ~range ~ast ~st ~parsing_diags ~parsing_feedback | Error (Coq.Protect.Error.Anomaly (err_range, msg) as coq_err) | Error (User (err_range, msg) as coq_err) -> let err_range = Option.default range err_range in - let err_diags = [ Util.mk_error_diagnostic ~range:err_range ~msg ~ast ] in - let recovery_st = state_recovery_heuristic doc st ast in + let err_diags = [ Diags.error ~range:err_range ~msg ~ast ] in + let recovery_st = recovery_interp ~doc ~st ~ast in let node = parsed_node ~range ~ast ~state:recovery_st ~parsing_diags ~parsing_feedback ~diags:err_diags ~feedback ~info @@ -549,7 +613,7 @@ let document_action ~st ~parsing_diags ~parsing_feedback ~parsing_time ~doc | Process ast -> ( let lines = doc.contents.lines in let process_res, info = interp_and_info ~parsing_time ~st ast in - let f = Coq_utils.to_range ~lines in + let f = Coq.Utils.to_range ~lines in let { Coq.Protect.E.r; feedback } = Coq.Protect.E.map_loc ~f process_res in match r with | Coq.Protect.R.Interrupted -> @@ -557,11 +621,14 @@ let document_action ~st ~parsing_diags ~parsing_feedback ~parsing_time ~doc Interrupted last_tok | Coq.Protect.R.Completed res -> let ast_loc = Coq.Ast.loc ast |> Option.get in - let ast_range = Coq_utils.to_range ~lines ast_loc in + let ast_range = Coq.Utils.to_range ~lines ast_loc in + let ast = + Node.Ast.{ v = ast; ast_info = Coq.Ast.make_info ~lines ~st ast } + in (* The evaluation by Coq fully completed, then we can resume checking from this point then, hence the new last valid token last_tok_new *) let last_tok_new = Coq.Parsing.Parsable.loc doc_handle in - let last_tok_new = Coq_utils.to_range ~lines last_tok_new in + let last_tok_new = Coq.Utils.to_range ~lines last_tok_new in node_of_coq_result ~doc ~range:ast_range ~ast ~st ~parsing_diags ~parsing_feedback ~feedback ~info last_tok_new res) @@ -592,7 +659,7 @@ let log_beyond_target last_tok target = let max_errors_node ~state ~range = let msg = Pp.str "Maximum number of errors reached" in - let parsing_diags = [ Util.mk_diag range 1 msg ] in + let parsing_diags = [ Diags.make range 1 msg ] in unparseable_node ~range ~parsing_diags ~parsing_feedback:[] ~state ~parsing_time:0.0 @@ -680,7 +747,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 Utf8.index_of_char ~line ~char:r.end_.character with + match Coq.Utf8.index_of_char ~line ~char:r.end_.character with | None -> String.length line | Some index -> index in diff --git a/fleche/doc.mli b/fleche/doc.mli index 447f3f5de..a8b4ad24c 100644 --- a/fleche/doc.mli +++ b/fleche/doc.mli @@ -6,6 +6,13 @@ (************************************************************************) module Node : sig + module Ast : sig + type t = + { v : Coq.Ast.t + ; ast_info : Lang.Range.t Coq.Ast.Info.t list option + } + end + module Info : sig type t = private { cache_hit : bool @@ -25,7 +32,7 @@ module Node : sig type t = private { range : Lang.Range.t - ; ast : Coq.Ast.t option (** Ast of node *) + ; 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 *) ; messages : Message.t list @@ -33,7 +40,7 @@ module Node : sig } val range : t -> Lang.Range.t - val ast : t -> Coq.Ast.t option + val ast : t -> Ast.t option val state : t -> Coq.State.t val diags : t -> Lang.Diagnostic.t list val messages : t -> Message.t list @@ -56,6 +63,7 @@ type t = private { uri : Lang.LUri.File.t ; version : int ; contents : Contents.t + ; toc : Lang.Range.t Coq.Ast.Id.Map.t ; root : Coq.State.t ; nodes : Node.t list ; diags_dirty : bool @@ -63,7 +71,7 @@ type t = private } (** Return the list of all asts in the doc *) -val asts : t -> Coq.Ast.t list +val asts : t -> Node.Ast.t list (** Note, [create] calls Coq but it is not cached in the Memo.t table *) val create : diff --git a/fleche/info.ml b/fleche/info.ml index d75d071ea..1375c7b5a 100644 --- a/fleche/info.ml +++ b/fleche/info.ml @@ -115,11 +115,12 @@ module type S = sig val node : (approx, Doc.Node.t) query val range : (approx, Lang.Range.t) query - val ast : (approx, Coq.Ast.t) query + val ast : (approx, Doc.Node.Ast.t) query val goals : (approx, Coq.Goals.reified_pp) query val messages : (approx, Doc.Node.Message.t list) query val info : (approx, Doc.Node.Info.t) query val completion : (string, string list) query + val in_state : st:Coq.State.t -> f:('a -> 'b option) -> 'a -> 'b option end let some x = Some x diff --git a/fleche/info.mli b/fleche/info.mli index 31c90be3b..131678150 100644 --- a/fleche/info.mli +++ b/fleche/info.mli @@ -46,11 +46,12 @@ module type S = sig val node : (approx, Doc.Node.t) query val range : (approx, Lang.Range.t) query - val ast : (approx, Coq.Ast.t) query + val ast : (approx, Doc.Node.Ast.t) query val goals : (approx, Coq.Goals.reified_pp) query val messages : (approx, Doc.Node.Message.t list) query val info : (approx, Doc.Node.Info.t) query val completion : (string, string list) query + val in_state : st:Coq.State.t -> f:('a -> 'b option) -> 'a -> 'b option end module LC : S with module P := LineCol diff --git a/fleche/memo.mli b/fleche/memo.mli index 8e12f5ae0..ad7098a34 100644 --- a/fleche/memo.mli +++ b/fleche/memo.mli @@ -11,7 +11,7 @@ end val interp_command : st:Coq.State.t -> Coq.Ast.t -> Coq.State.t Coq.Interp.interp_result Stats.t -val interp_admitted : st:Coq.State.t -> Coq.State.t +val interp_admitted : st:Coq.State.t -> (Coq.State.t, Loc.t) Coq.Protect.E.t (** Stats *) val mem_stats : unit -> int diff --git a/lsp/jFleche.ml b/lsp/jFleche.ml index 8c7fe36ec..b22f9014b 100644 --- a/lsp/jFleche.ml +++ b/lsp/jFleche.ml @@ -60,13 +60,26 @@ let mk_progress ~uri ~version processing = let params = Progress.to_yojson { Progress.textDocument; processing } in Base.mk_notification ~method_:"$/coq/fileProgress" ~params +module Message = struct + type 'a t = + { range : JLang.Range.t option + ; level : int + ; text : 'a + } + [@@deriving yojson] + + let map ~f { range; level; text } = + let text = f text in + { range; level; text } +end + module GoalsAnswer = struct type t = { textDocument : Doc.VersionedTextDocument.t ; position : Lang.Point.t ; goals : string JCoq.Goals.reified_goal JCoq.Goals.goals option - ; messages : string list - ; error : string option + ; messages : string Message.t list + ; error : string option [@default None] } [@@deriving to_yojson] end @@ -74,11 +87,38 @@ end let mk_goals ~uri ~version ~position ~goals ~messages ~error = let f rg = Coq.Goals.map_reified_goal ~f:Pp.to_string rg in let goals = Option.map (Coq.Goals.map_goals ~f) goals in - let messages = List.map Pp.to_string messages in + let messages = List.map (Message.map ~f:Pp.to_string) messages in let error = Option.map Pp.to_string error in GoalsAnswer.to_yojson { textDocument = { uri; version }; position; goals; messages; error } +(** {1 document/definition} *) +module LocationLink = struct + type t = + { originSelectionRange : Lang.Range.t option [@default None] + ; targetUri : Lang.LUri.File.t + ; targetRange : Lang.Range.t + ; targetSelectionRange : Lang.Range.t + } + [@@deriving yojson] +end +(** {1} DocumentSymbols *) + +module DocumentSymbol = struct + type t = + { name : string + ; detail : string option [@default None] + ; kind : int + ; tags : int list option [@default None] + ; deprecated : bool option [@default None] + ; range : Lang.Range.t + ; selectionRange : Lang.Range.t + ; children : t list option [@default None] + } + [@@deriving yojson] +end + +(** Not used as of today, superseded by DocumentSymbol *) module Location = struct type t = { uri : Lang.LUri.File.t @@ -87,6 +127,7 @@ module Location = struct [@@deriving yojson] end +(** Not used as of today, superseded by DocumentSymbol *) module SymInfo = struct type t = { name : string @@ -96,6 +137,8 @@ module SymInfo = struct [@@deriving yojson] end +(** {1} Hover *) + module HoverContents = struct type t = { kind : string @@ -107,11 +150,13 @@ end module HoverInfo = struct type t = { contents : HoverContents.t - ; range : Lang.Range.t option + ; range : Lang.Range.t option [@default None] } [@@deriving yojson] end +(** {1} Completion *) + module LabelDetails = struct type t = { detail : string } [@@deriving yojson] end @@ -128,10 +173,10 @@ end module CompletionData = struct type t = { label : string - ; insertText : string option - ; labelDetails : LabelDetails.t option - ; textEdit : TextEditReplace.t option - ; commitCharacters : string list option + ; insertText : string option [@default None] + ; labelDetails : LabelDetails.t option [@default None] + ; textEdit : TextEditReplace.t option [@default None] + ; commitCharacters : string list option [@default None] } [@@deriving yojson] end diff --git a/lsp/jFleche.mli b/lsp/jFleche.mli index 48800bef5..4c67d487e 100644 --- a/lsp/jFleche.mli +++ b/lsp/jFleche.mli @@ -25,13 +25,21 @@ val mk_progress : -> Fleche.Progress.Info.t list -> Yojson.Safe.t +module Message : sig + type 'a t = + { range : JLang.Range.t option + ; level : int + ; text : 'a + } +end + module GoalsAnswer : sig type t = { textDocument : Doc.VersionedTextDocument.t ; position : Lang.Point.t ; goals : string JCoq.Goals.reified_goal JCoq.Goals.goals option - ; messages : string list - ; error : string option + ; messages : string Message.t list + ; error : string option [@default None] } [@@deriving to_yojson] end @@ -41,10 +49,11 @@ val mk_goals : -> version:int -> position:Lang.Point.t -> goals:Coq.Goals.reified_pp option - -> messages:Pp.t list + -> messages:Pp.t Message.t list -> error:Pp.t option -> Yojson.Safe.t +(** Generic *) module Location : sig type t = { uri : Lang.LUri.File.t @@ -53,6 +62,34 @@ module Location : sig [@@deriving yojson] end +(** {1 document/definition} *) +module LocationLink : sig + type t = + { originSelectionRange : Lang.Range.t option [@default None] + ; targetUri : Lang.LUri.File.t + ; targetRange : Lang.Range.t + ; targetSelectionRange : Lang.Range.t + } + [@@deriving yojson] +end + +(** {1 DocumentSymbols} *) + +module DocumentSymbol : sig + type t = + { name : string + ; detail : string option [@default None] + ; kind : int + ; tags : int list option [@default None] + ; deprecated : bool option [@default None] + ; range : Lang.Range.t + ; selectionRange : Lang.Range.t + ; children : t list option [@default None] + } + [@@deriving yojson] +end + +(** Not used as of today, superseded by DocumentSymbol *) module SymInfo : sig type t = { name : string @@ -62,6 +99,8 @@ module SymInfo : sig [@@deriving yojson] end +(** {1 Hover} *) + module HoverContents : sig type t = { kind : string @@ -73,11 +112,13 @@ end module HoverInfo : sig type t = { contents : HoverContents.t - ; range : Lang.Range.t option + ; range : Lang.Range.t option [@default None] } [@@deriving yojson] end +(** {1 Completion} *) + module LabelDetails : sig type t = { detail : string } [@@deriving yojson] end @@ -94,10 +135,10 @@ end module CompletionData : sig type t = { label : string - ; insertText : string option - ; labelDetails : LabelDetails.t option - ; textEdit : TextEditReplace.t option - ; commitCharacters : string list option + ; insertText : string option [@default None] + ; labelDetails : LabelDetails.t option [@default None] + ; textEdit : TextEditReplace.t option [@default None] + ; commitCharacters : string list option [@default None] } [@@deriving yojson] end diff --git a/shell.nix b/shell.nix new file mode 100644 index 000000000..e6d917316 --- /dev/null +++ b/shell.nix @@ -0,0 +1,14 @@ +( + import + ( + let + lock = builtins.fromJSON (builtins.readFile ./flake.lock); + in + fetchTarball { + url = "https://github.com/edolstra/flake-compat/archive/${lock.nodes.flake-compat.locked.rev}.tar.gz"; + sha256 = lock.nodes.flake-compat.locked.narHash; + } + ) + {src = ./.;} +) +.shellNix