Merge branch 'v8.19' into v8.18

.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,35 @@ 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 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
+
   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,6 +1,11 @@
 # unreleased
 ------------
 
+ - Added new heatmap feature allowing timing data to be seen in the
+   editor. Can be enabled with the `Coq LSP: Toggle heatmap`
+   comamnd. Can be configured to show memory usage. Colors and
+   granularity are configurable. (@Alizter and @ejgallego, #686,
+   grants #681).
  - new option `show_loc_info_on_hover` that will display parsing debug
    information on hover; previous flag was fixed in code, which is way
    less flexible. This also fixes the option being on in 0.1.8 by
@@ -70,6 +75,9 @@
  - 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,48 @@
  - 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 cleint 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)
+ - New server option to enable / disable `coq/perfData` (@ejgallego,
+   #689)
+ - 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, #703, thanks to Alex Sanchez-Stern)
+ - New `petanque` JSON-RPC `pet.exe`, which can be used à la SerAPI
+   to perform proof search and more (@ejgallego, @gbdrt, #705)
+ - Always dispose UI elements. This should improve some strange
+   behaviors on extension restart (@ejgallego, #708)
+ - Support Coq meta-commands (Reset, Reset Initial, Back) They are
+   actually pretty useful to hint the incremental engine to ignore
+   changes in some part of the document (@ejgallego, #709)
+ - JSON-RPC library now supports all kind of incoming messages
+   (@ejgallego, #713)
+ - New `coq/viewRange` notification, from client to server, than hints
+   the scheduler for the visible area of the document; combined with
+   the new lazy checking mode, this provides checking on scroll, a
+   feature inspired from Isabelle IDE (@ejgallego, #717)
+ - Have VSCode wait for full LSP client shutdown on server
+   restart. This fixes some bugs on extension restart (finally!)
+   (@ejgallego, #719)
+ - Center the view if cursor goes out of scope in
+   `sentenceNext/sentencePrevious` (@ejgallego, #718)
+ - Switch Flèche range encoding to protocol native, this means UTF-16
+   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)
 
 # 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

@@ -182,6 +182,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

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
+  Fleche.Compat.format_to_file ~file ~f:Output.pp_diags diags
 
 (** Return: exit status for file:
 
@@ -47,7 +47,9 @@ 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 =
+      Fleche.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

@@ -47,7 +47,7 @@ let go ~int_backend args =
   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 =

compiler/fcc.ml

@@ -25,10 +25,6 @@ let fcc_main int_backend roots display debug plugins files coqlib coqcorelib
 
 (****************************************************************************)
 (* Specific to fcc *)
-let roots : string list Term.t =
-  let doc = "Workspace(s) root(s)" in
-  Arg.(value & opt_all string [] & info [ "root" ] ~docv:"ROOTS" ~doc)
-
 let display : Args.Display.t Term.t =
   let doc = "Verbosity display settings" in
   let dparse =

controller/coq_lsp.ml

@@ -91,28 +91,38 @@ let exit_notification =
 let rec lsp_init_loop ~ifn ~ofn ~cmdline ~debug =
   match ifn () with
   | None -> raise Lsp_exit
-  | Some msg -> (
+  | Some (Ok msg) -> (
     match lsp_init_process ~ofn ~cmdline ~debug msg with
     | Init_effect.Exit -> raise Lsp_exit
     | Init_effect.Loop -> lsp_init_loop ~ifn ~ofn ~cmdline ~debug
     | Init_effect.Success w -> w)
+  | Some (Error err) ->
+    Lsp.Io.trace "read_request" ("error: " ^ err);
+    lsp_init_loop ~ifn ~ofn ~cmdline ~debug
 
 let lsp_main bt coqcorelib coqlib ocamlpath vo_load_path ml_include_path
     require_libraries delay int_backend =
-  Coq.Limits.select int_backend;
+  Coq.Limits.select_best int_backend;
   Coq.Limits.start ();
 
   (* Try to be sane w.r.t. \r\n in Windows *)
   Stdlib.set_binary_mode_in stdin true;
   Stdlib.set_binary_mode_out stdout true;
 
   (* We output to stdout *)
-  let ifn () = LIO.read_request stdin in
+  let ifn () = LIO.read_message stdin in
+
   (* Set log channels *)
-  let ofn = LIO.send_json Format.std_formatter in
-  LIO.set_log_fn ofn;
+  let json_fn = LIO.send_json Format.std_formatter in
+
+  let ofn response =
+    let response = Lsp.Base.Response.to_yojson response in
+    LIO.send_json Format.std_formatter response
+  in
 
-  let io = lsp_cb ofn in
+  LIO.set_log_fn json_fn;
+
+  let io = lsp_cb json_fn in
   Fleche.Io.CallBack.set io;
 
   (* IMPORTANT: LSP spec forbids any message from server to client before
@@ -138,9 +148,12 @@ let lsp_main bt coqcorelib coqlib ocamlpath vo_load_path ml_include_path
     | None ->
       (* EOF, push an exit notication to the queue *)
       enqueue_message exit_notification
-    | Some msg ->
+    | Some (Ok msg) ->
       enqueue_message msg;
       read_loop ()
+    | Some (Error err) ->
+      Lsp.Io.trace "read_request" ("error: " ^ err);
+      read_loop ()
   in
 
   (* Input/output will happen now *)
@@ -152,7 +165,7 @@ let lsp_main bt coqcorelib coqlib ocamlpath vo_load_path ml_include_path
         Fleche.Config.(
           v := { !v with send_diags = false; send_perf_data = false });
         LIO.set_log_fn (fun _obj -> ());
-        let io = concise_cb ofn in
+        let io = concise_cb json_fn in
         Fleche.Io.CallBack.set io;
         io)
       else io