Merge branch 'v8.18' into v8.17

.github/workflows/build.yml

@@ -40,6 +40,8 @@ jobs:
             ocaml: 5.0.x
           - os: ubuntu-latest
             ocaml: 5.1.x
+          - os: ubuntu-latest
+            ocaml: 5.2.x
           - os: macos-latest
             ocaml: 4.14.x
           - name: Windows Latest
@@ -79,6 +81,39 @@ jobs:
       - name: 🐛 Test fcc
         run: opam exec -- make test-compiler
 
+  build-opam:
+    name: Opam dev install
+    strategy:
+      fail-fast: false
+    runs-on: ubuntu-latest
+    steps:
+      - name: 🔭 Checkout code
+        uses: actions/checkout@v3
+        with:
+          submodules: recursive
+
+      - name: 🐫 Setup OCaml
+        uses: ocaml/setup-ocaml@v2
+        with:
+          ocaml-compiler: 4.14.x
+          dune-cache: true
+
+      - name: Install Coq and SerAPI into OPAM switch
+        run: |
+          opam install lwt logs # Also build pet-server
+          opam install memprof-limits # We need to do this to avoid coq-lsp rebuilding Coq below due to deptops
+          opam install vendor/coq/{coq-core,coq-stdlib,coqide-server,coq}.opam
+          opam install vendor/coq-serapi/coq-serapi.opam
+
+      - name: Install `coq-lsp` into OPAM switch
+        run: opam install .
+
+      - name: Test `coq-lsp` in installed switch
+        run: opam exec -- fcc examples/Demo.v
+
+      - name: Test `pet-server` is built
+        run: opam exec -- which pet-server
+
   client-compile:
     runs-on: ubuntu-latest
     defaults:

.ocamlformat

@@ -1,4 +1,4 @@
-version=0.26.0
+version=0.26.1
 profile=conventional
 ocaml-version=4.08.0
 break-separators=before

CHANGES.md

@@ -1,5 +1,5 @@
-# unreleased
-------------
+# coq-lsp 0.1.9: Hasta el 40 de Mayo...
+---------------------------------------
 
  - new option `show_loc_info_on_hover` that will display parsing debug
    information on hover; previous flag was fixed in code, which is way
@@ -65,11 +65,19 @@
    #348)
  - fix Coq performance view display (@ejgallego, #663, regression in
    #513)
+ - Added new heatmap feature allowing timing data to be seen in the
+   editor. Can be enabled with the `Coq LSP: Toggle heatmap`
+   command. Can be configured to show memory usage. Colors and
+   granularity are configurable. (@Alizter and @ejgallego, #686,
+   grants #681).
  - allow more than one input position in `selectionRange` LSP call
    (@ejgallego, #667, fixes #663)
  - new VSCode commands to allow to move one sentence backwards /
    forward, this is particularly useful when combined with lazy
    checking mode (@ejgallego, #671, fixes #263, fixes #580)
+ - VSCode commands `coq-lsp.sentenceNext` / `coq-lsp.sentencePrevious`
+   are now bound by default to `Alt + N` / `Alt + P` keybindings
+   (@ejgallego, #718)
  - change diagnostic `extra` field to `data`, so we now conform to the
    LSP spec, include the data only when the `send_diags_extra_data`
    server-side option is enabled (@ejgallego, #670)
@@ -98,6 +106,81 @@
  - Update `package-lock.json` for latest bugfixes (@ejgallego, #687)
  - Update Nix flake enviroment (@Alizter, #684 #688)
  - Update `prettier` (@Alizter @ejgallego, #684 #688)
+ - Store original performance data in the cache, so we now display the
+   original timing and memory data even for cached commands (@ejgallego, #693)
+ - Fix type errors in the Performance Data Notifications (@ejgallego,
+   @Alizter, #689, #693)
+ - Send performance performance data for the full document
+   (@ejgallego, @Alizter, #689, #693)
+ - Better types `coq/perfData` call (@ejgallego @Alizter, #689)
+ - New server option to enable / disable `coq/perfData` (@ejgallego, #689)
+ - New client option to enable / disable `coq/perfData` (@ejgallego, #717)
+ - The `coq-lsp.document` VSCode command will now display the returned
+   JSON data in a new editor (@ejgallego, #701)
+ - Update server settings on the fly when tweaking them in VSCode.
+   Implement `workspace/didChangeConfiguration` (@ejgallego, #702)
+ - [Coq API] Add functions to retrieve list of declarations done in
+   .vo files (@ejallego, @eytans, #704)
+ - New `petanque` API to interact directly with Coq's proof
+   engine. (@ejgallego, @gbdrt, Laetitia Teodorescu #703, thanks to
+   Alex Sanchez-Stern for many insightful feedback and testing)
+ - New `petanque` JSON-RPC `pet.exe`, which can be used à la SerAPI
+   to perform proof search and more (@ejgallego, @gbdrt, #705)
+ - New `pet-server.exe` TCP server for keep-alive sessions (@gbdrt,
+   #697)
+ - Always dispose UI elements. This should improve some strange
+   behaviors on extension restart (@ejgallego, #708)
+ - [code] Added new heatmap feature allowing timing data to be seen in
+   the editor. Can be enabled with the `Coq LSP: Toggle heatmap`
+   comamnd. Can be configured to show memory usage. Colors and
+   granularity are configurable. (@Alizter and @ejgallego, #686,
+   grants #681).
+ - [server] Support Coq meta-commands (Reset, Reset Initial, Back)
+   They are actually pretty useful to hint the incremental engine to
+   ignore changes in some part of the document (@ejgallego, #709)
+ - JSON-RPC library now supports all kind of incoming messages
+   (@ejgallego, #713)
+ - [code/server] New `coq/viewRange` notification, from client to
+   server, than hints the scheduler for the visible area of the
+   document; combined with the new lazy checking mode, this provides
+   checking on scroll, a feature inspired from Isabelle IDE
+   (@ejgallego, #717)
+ - [code] Have VSCode wait for full LSP client shutdown on server
+   restart. This fixes some bugs on extension restart (finally!)
+   (@ejgallego, #719)
+ - [code] Center the view if cursor goes out of scope in
+   `sentenceNext/sentencePrevious` (@ejgallego, #718)
+ - Switch Flèche range encoding to protocol native, this means UTF-16
+   code points for now (Léo Stefanesco, @ejgallego, #624, fixes #620,
+   #621)
+ - Give `Goals` panel focus back if it has lost it (in case of
+   multiple panels in the second viewColumn of Vscode) whenever
+   user navigates proofs (@Alidra @ejgallego, #722, #725)
+ - `fcc`: new option `--diags_level` to control whether Coq's notice
+   and info messages appear as diagnostics
+ - [code] Display the continous/on-request checking mode in the status bar,
+   allow to change it by clicking on it (@ejgallego, #721)
+ - Add an example of multiple workspaces (@ejgallego, @Blaisorblade,
+   #611)
+ - Don't show types of un-expanded goals. We should add an option for
+   this, but we don't have the cycles (@ejgallego, #730, workarounds
+   #525 #652)
+ - Support for `.lv / .v.tex` TeX files with embedded Coq code
+   (@ejgallego, #727)
+ - Don't expand bullet goals at previous levels by default
+   (@ejgallego, @Alizter, #731 cc #525)
+ - [petanque] Return basic goal information after `run_tac`, so we
+   avoid a `goals` round-trip for each tactic (@gbdrt, @ejgallego,
+   #733)
+ - [coq] Add support for reading glob files metadata (@ejgallego,
+   #735)
+ - [petanque] Return extra premise information: file name, position,
+   raw_text, using the above support for reading .glob files
+   (@ejgallego, #735)
+ - [code] Display server status using the `LanguageStatusItem`
+   facility, for now we display version and checking status
+   information (moved from #721), and we also allow to toggle the
+   checking mode from there (@ejgallego, #728)
 
 # coq-lsp 0.1.8.1: Spring fix
 -----------------------------

CONTRIBUTING.md

@@ -3,17 +3,23 @@ Contributing to Coq LSP
 
 Thank you very much for willing to contribute to coq-lsp!
 
-`coq-lsp` has two components:
+The `coq-lsp` repository contains several tightly coupled components
+in a single repository, also known as a monorepo, in particular:
 
-- a LSP server for Coq project written in OCaml.
-- a `coq-lsp` VS Code extension written in TypeScript and React, in
-  the `editor/code` directory.
+- Flèche: an incremental document engine for Coq supporting literate
+  programming and programability, written in OCaml
+- `fcc`: an extensible command line compiler built on top of Flèche
+- `petanque`: direct access to Coq's proof engine
+- `coq-lsp`a LSP server for the Coq project, written in OCaml on top of Flèche
+- a `coq-lsp/VSCode` extension written in TypeScript and React, in
+  the `editor/code` directory
 
-Read coq-lsp [FAQ](etc/FAQ.md) for an explanation on what the above mean.
+Read coq-lsp [FAQ](etc/FAQ.md) to learn more about LSP and
+server/client roles.
 
-It is possible to hack only in the server, on the client, or on both at the same
-time. We have thus structured this guide in 3 sections: general guidelines,
-server, and VS Code client.
+It is possible to hack only in the server, on the client, or on both
+at the same time. We have thus structured this guide in 3 sections:
+general guidelines, server, and VS Code client.
 
 ## General guidelines
 
@@ -184,14 +190,17 @@ coq-lsp.packages.${system}.default
 
 The `coq-lsp` server consists of several components, we present them bottom-up
 
+- `vendor/coq`: [vendored] Coq version to build coq-lsp against
 - `vendor/coq-serapi`: [vendored] improved utility functions to handle Coq AST
 - `coq`: Utility library / abstracted Coq API. This is the main entry point for
   communication with Coq, and it reifies Coq calls as to present a purely
   functional interface to Coq.
+- `lang`: base language definitions for Flèche
 - `fleche`: incremental document processing backend. Exposes a generic API, but
   closely modelled to match LSP
 - `lsp`: small generic LSP utilities, at some point to be replaced by a generic
   library
+- `petanque`: low-level access to Coq's API
 - `controller`: LSP controller, a thin layer translating LSP transport layer to
   `flèche` surface API, plus some custom event queues for Coq.
 - `controller-js`: LSP controller for Javascript, used for `vscode.dev` and
@@ -209,6 +218,29 @@ Some tips:
 
 [ocamlformat]: https://github.com/ocaml-ppx/ocamlformat
 
+### Unicode setup
+
+Flèche stores locations in the protocol-native format. This has the
+advantage that conversion is needed only at range creation point
+(where we usually have access to the document to perform the
+conversion).
+
+This way, we can send ranges to the client without conversion.
+
+Request that work on the raw `Contents.t` buffer must do the inverse
+conversion, but we handle this via a proper text API that is aware of
+the conversion.
+
+For now, the setup for Coq is:
+
+- protocol-level (and Flèche) encoding: UTF-16 (due to LSP)
+- `Contents.t`: UTF-8 (sent to Coq)
+
+It would be very easy to set this parameters at initialization time,
+ideal would be for LSP clients to catch up and allow UTF-8 encodings
+(so no conversion is needed, at least for Coq), but it seems that we
+will take a while to get to this point.
+
 ## Client guide (VS Code Extension)
 
 The VS Code extension is setup as a standard `npm` Typescript + React package

README.md

@@ -20,6 +20,8 @@ document checking, advanced error recovery, hybrid Coq/markdown document
 support, multiple workspace support, positional goals and information panel,
 performance data, extensible command-line compiler, plugin system, and more.
 
+See the [coq-lsp User Manual](./etc/doc/USER_MANUAL.md) for more information.
+
 `coq-lsp` aims to provide a seamless, modern interactive theorem proving
 experience, as well as to serve as a maintainable platform for research and UI
 integration with other projects.
@@ -37,6 +39,7 @@ and web native usage, providing quite a few extra features from vanilla Coq.
 
 - [🎁 Features](#-features)
   - [⏩ Incremental Compilation and Continuous Document Checking](#-incremental-compilation-and-continuous-document-checking)
+  - [👁 On-demand, Follow The Viewport Document Checking](#-on-demand-follow-the-viewport-document-checking)
   - [🧠 Smart, Cache-Aware Error Recovery](#-smart-cache-aware-error-recovery)
   - [🥅 Whole-Document Goal Display](#-whole-document-goal-display)
   - [🗒️ Markdown Support](#️-markdown-support)
@@ -58,6 +61,7 @@ and web native usage, providing quite a few extra features from vanilla Coq.
   - [✅ Vim](#-vim)
   - [🩱 Neovim](#-neovim)
   - [🐍 Python](#-python)
+- [⇨ `coq-lsp` users and extensions](#-coq-lsp-users-and-extensions)
 - [🗣️ Discussion Channel](#️-discussion-channel)
 - [☎ Weekly Calls](#-weekly-calls)
 - [❓FAQ](#faq)
@@ -87,6 +91,14 @@ restart your proof session where you left it at the last time.
 Incremental support is undergoing refinement, if `coq-lsp` rechecks when it
 should not, please file a bug!
 
+### 👁 On-demand, Follow The Viewport Document Checking
+
+`coq-lsp` does also support on-demand checking. Two modes are available: follow
+the cursor, or follow the viewport; the modes can be toggled using the Language
+Status Item in Code's bottom right corner:
+
+<img alt="On-demand checking" height="572px" src="etc/img/on_demand.gif"/>
+
 ### 🧠 Smart, Cache-Aware Error Recovery
 
 `coq-lsp` won't stop checking on errors, but supports (and encourages) working
@@ -182,6 +194,12 @@ fully-fledged LSP client.
 add your pre/post processing passes, for example to analyze or serialize parts
 of Coq files.
 
+### 🪄 Advanced APIs for Coq Interaction
+
+Thanks to Flèche, we provide some APIs on top of it that allow advanced use
+cases with Coq. In particular, we provide direct, low-overhead access to Coq's
+proof engine using [petanque](./petanque).
+
 ### ♻️ Reusability, Standards, Modularity
 
 The incremental document checking library of `coq-lsp` has been designed to be
@@ -301,6 +319,17 @@ guide](./CONTRIBUTING.md)
 - Interact programmatically with Coq files by using the [Python `coq-lsp` client](https://github.com/sr-lab/coq-lsp-pyclient)
   by Pedro Carrott and Nuno Saavedra.
 
+## ⇨ `coq-lsp` users and extensions
+
+The below projects are using `coq-lsp`, we recommend you try them!
+
+- [CoqPilot uses Large Language Models to generate multiple potential proofs and then uses coq-lsp to typecheck them](https://github.com/JetBrains-Research/coqpilot).
+- [jsCoq: use Coq from your browser](https://github.com/jscoq/jscoq)
+- [Pytanque: a Python library implementing RL Environments](https://github.com/LLM4Coq/pytanque)
+- [ViZX: A Visualizer for the ZX Calculus](https://github.com/inQWIRE/ViZX).
+- [The Waterproof vscode extension helps students learn how to write mathematical proofs](https://github.com/impermeable/waterproof-vscode).
+- [Yade: Support for the YADE diagram editor in VSCode](https://github.com/amblafont/vscode-yade-example).
+
 ## 🗣️ Discussion Channel
 
 `coq-lsp` discussion channel it at [Coq's
@@ -326,7 +355,7 @@ recommend that if you are installing via opam, you use the following branches
 that have some fixes backported:
 
 - For 8.20: No known problems
-- For 8.19: No known problems
+- For 8.19: `opam pin add coq-core https://github.com/ejgallego/coq.git#v8.19+lsp`
 - For 8.18: `opam pin add coq-core https://github.com/ejgallego/coq.git#v8.18+lsp`
 - For 8.17: `opam pin add coq-core https://github.com/ejgallego/coq.git#v8.17+lsp`
 - For 8.16: `opam pin add coq      https://github.com/ejgallego/coq.git#v8.16+lsp`

compiler/args.ml

@@ -14,6 +14,8 @@ type t =
   ; plugins : string list  (** Flèche plugins to load *)
   ; max_errors : int option
         (** Maximum erros before aborting the compilation *)
+  ; coq_diags_level : int
+        (** Whether to include feedback messages in the diagnostics *)
   }
 
 let compute_default_plugins ~no_vo ~plugins =

compiler/compile.ml

@@ -22,7 +22,7 @@ let save_diags_file ~(doc : Fleche.Doc.t) =
   let file = Lang.LUri.File.to_string_file doc.uri in
   let file = Filename.remove_extension file ^ ".diags" in
   let diags = Fleche.Doc.diags doc in
-  Util.format_to_file ~file ~f:Output.pp_diags diags
+  Coq.Compat.format_to_file ~file ~f:Output.pp_diags diags
 
 (** Return: exit status for file:
 
@@ -47,7 +47,7 @@ let compile_file ~cc file : int =
     let workspace = workspace_of_uri ~io ~workspaces ~uri ~default in
     let files = Coq.Files.make () in
     let env = Doc.Env.make ~init:root_state ~workspace ~files in
-    let raw = Util.input_all file in
+    let raw = Coq.Compat.Ocaml_414.In_channel.(with_open_bin file input_all) in
     let () = Theory.create ~io ~token ~env ~uri ~raw ~version:1 in
     match Theory.Check.maybe_check ~io ~token with
     | None -> 102

compiler/driver.ml

@@ -36,18 +36,26 @@ let apply_config ~max_errors =
     max_errors
 
 let go ~int_backend args =
-  let { Args.cmdline; roots; display; debug; files; plugins; max_errors } =
+  let { Args.cmdline
+      ; roots
+      ; display
+      ; debug
+      ; files
+      ; plugins
+      ; max_errors
+      ; coq_diags_level
+      } =
     args
   in
   (* Initialize event callbacks, in testing don't do perfData *)
   let perfData = Option.is_empty fcc_test in
-  let io = Output.init display ~perfData in
+  let io = Output.init ~display ~perfData ~coq_diags_level in
   (* Initialize Coq *)
   let debug = debug || Fleche.Debug.backtraces || !Fleche.Config.v.debug in
   let root_state = coq_init ~debug in
   let roots = if List.length roots < 1 then [ Sys.getcwd () ] else roots in
   let default = Coq.Workspace.default ~debug ~cmdline in
-  let () = Coq.Limits.select int_backend in
+  let () = Coq.Limits.select_best int_backend in
   let () = Coq.Limits.start () in
   let token = Coq.Limits.Token.create () in
   let workspaces =