Merge branch 'v8.20' into v8.19

.github/workflows/build.yml

@@ -4,6 +4,7 @@ on:
   push:
     branches:
       - main
+      - v8.21
       - v8.20
       - v8.19
       - v8.18
@@ -13,6 +14,7 @@ on:
   pull_request:
     branches:
       - main
+      - v8.21
       - v8.20
       - v8.19
       - v8.18

CHANGES.md

@@ -1,3 +1,80 @@
+# unreleased
+------------
+
+ - [deps] merge serlib into coq-lsp. This allow us to drop the SerAPI
+   dependency, and will greatly easy the development of tools that
+   require AST manipulation (@ejgallego, #698)
+ - [fleche] Remove 8.16 compatibility layer (@ejgallego, #747)
+ - [fleche] Preserve view hint across document changes. With this
+   change, we get local continuous checking mode when the view-port
+   heuristic is enabled (@ejgallego, #748)
+ - [memo] More precise hashing for Coq states, this improves cache
+   performance quite a bit (@ejgallego, #751)
+ - [fleche] Enable sharing of `.vo` file parsing. This enables better
+   sharing, achieving an almost 50% memory reduction for example when
+   opening all of HoTT .v files (@ejgallego, @SkySkimmer, @bhaktishh,
+   #744)
+ - [memo] Provide API to query Hashtbl stats (@ejgallego, #753)
+ - [nix] Add `pet-server` deps to flake.nix (Léo Stefanesco, #754)
+ - [coq-lsp] Fix crash on `--help` option (Léo Stefanesco, @ejgallego,
+   #754)
+ - [vscode] Fix focus race when a Coq file is in column 2 (@ejgallego,
+   #755, cc: #722, #725)
+ - [hover] Show input howto for unicode characters on hover
+   (@ejgallego, Léo Stefanesco, #756)
+ - [lsp] [definition] Support for jump to definition across workspace
+   files. The location information is obtained from `.glob` files, so
+   it is often not perfect. (@ejgallego, #762, fixes #317)
+ - [lsp] [hover] Show full name and provenance of identifiers
+   (@ejgallego, #762)
+ - [lsp] [definition] Try also to resolve and locate module imports
+   (@ejgallego, #764)
+ - [code] Don't start server on extension activation, unless an editor
+   we own is active. We also auto-start the server if a document that
+   we own is opened later (@ejgallego, #758, fixes #750)
+ - [petanque] Allow `init` to be called multiple times (@ejgallego,
+   @gbdrt, #766)
+ - [petanque] Faster query for goals status after `run_tac`
+   (@ejgallego, #768)
+ - [petanque] New parameter `pre_commands` to `start` which allows
+   instrumenting the goal before starting the proof (@ejgallego, Alex
+   Sanchez-Stern #769)
+ - [petanque] New `http_headers={yes,no}` parameter for `pet` json
+   shell, plus some improvements on protocol handling (@ejgallego,
+   #770)
+ - [petanque] Make agent agnostic of environment, allowing embedding
+   inside LSP (@ejgallego, #771)
+ - [diagnostics] Ensure extra diagnostics info is present in all
+   errors, not only on those sentences that did parse successfully
+   (@ejgallego, Diego Rivera, #772)
+ - [hover] New option `show_universes_on_hover` that will display
+   universe data on hover (@ejgallego, @SkySkimmer, #666)
+ - [hover] New plugin `unidiff` that will elaborate a summary of
+   universe data a file, in particular regarding universes added at
+   `Qed` time (@ejgallego, #773)
+ - [fleche] Support meta-command `Abort All` (@ejgallego, #774, fixes
+   #550)
+ - [petanque] Allow memoization control on `petanque/run` via a new
+   parameter `memo` (@ejgallego, #780)
+ - [lsp] [petanque] Allow acces to `petanque` protocol from the lsp
+   server (@ejgallego, #778)
+ - [petanque] Always initialize a workspace. This made `pet` crash if
+   `--root` was not used and client didn't issue the optimal
+   `setWorkspace` call (#782, @ejgallego, @gbdrt)
+ - [lsp] [petanque] New methods `state/eq` and `state/hash`; this
+   allows clients to implement a client-side hash; equality is
+   configurable with different methods; moreover, `petanque/run` can
+   compute some extra data like state hashing without a round-trip
+   (@ejgallego @gbdrt, #779)
+
+# coq-lsp 0.1.10: Hasta el 40 de Mayo _en effect_...
+----------------------------------------------------
+
+ - [code] Add `.v.tex` file extension to contributed language support
+   (@ejgallego, #740).
+ - [code] Don't show the panel on extension activation (@ejgallego,
+   #741, fix #737)
+
 # coq-lsp 0.1.9: Hasta el 40 de Mayo...
 ---------------------------------------
 

CONTRIBUTING.md

@@ -70,7 +70,7 @@ Source
 Install](https://github.com/coq/platform/blob/main/doc/README_Windows.md#installation-by-compiling-from-sources-using-opam-on-cygwin)
 
 The default development environment for `coq-lsp` is a "composed"
-build that includes git submodules for `coq` and `coq-serapi` in the
+build that includes a git submodules for `coq` in the
 `vendor/` directory. This allows us to easily work with PRs using
 experimental Coq branches, and some other advantages like a better CI
 build cache and easier bisects.
@@ -116,11 +116,26 @@ This setup will build Coq and `coq-lsp` and install them to the
 current OPAM switch. This is a good setup for people looking to try
 out `coq-lsp` development versions with other OPAM packages.
 
-1. Install vendored Coq and SerAPI:
+You can just do:
+```
+make opam-update-and-reinstall
+```
+
+or alternatively, do it step by step
+
+0. Be sure submodules and `coq-lsp` are up to date:a
+
+    ```sh
+    git pull --recurse-submodules
+    ```
+
+   alternatively you can use `make submodules-init` to refresh the
+   submodules.
+
+1. Install vendored Coq
 
     ```sh
-    opam install vendor/coq/coq{-core,-stdlib,}.opam
-    opam install vendor/coq-serapi
+    opam install vendor/coq/coq{-core,-stdlib,ide-server,}.opam
     ```
 
 2. Install `coq-lsp`:
@@ -190,8 +205,7 @@ 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
+- `serlib`: 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.
@@ -386,11 +400,12 @@ The checklist for the release as of today is the following:
 
 The above can be done with:
 ```
-export COQLSPV=0.1.8
+export COQLSPV=0.2.0
 git checkout main  && make                    && dune-release tag ${COQLSPV}
-git checkout v8.18 && git merge main  && make && dune-release tag ${COQLSPV}+8.18 && dune-release
+git checkout v8.20 && git merge main  && make && dune-release tag ${COQLSPV}+8.20 && dune-release
+git checkout v8.19 && git merge v8.20  && make && dune-release tag ${COQLSPV}+8.19 && dune-release
+git checkout v8.18 && git merge v8.19  && make && dune-release tag ${COQLSPV}+8.18 && dune-release
 git checkout v8.17 && git merge v8.18 && make && dune-release tag ${COQLSPV}+8.17 && dune-release
-git checkout v8.16 && git merge v8.17 && make && dune-release tag ${COQLSPV}+8.16 && dune-release
 ```
 
 ## Emacs

Makefile

@@ -113,7 +113,6 @@ submodules-deinit:
 .PHONY: submodules-update
 submodules-update:
 	(cd vendor/coq && git checkout master && git pull upstream master)
-	(cd vendor/coq-serapi && git checkout main && git pull upstream main)
 
 # Build the vscode extension
 .PHONY: extension
@@ -127,3 +126,9 @@ ts-fmt:
 
 .PHONY: make-fmt
 make-fmt: build fmt
+
+# Helper for users that want a global opam install
+.PHONY: opam-update-and-reinstall
+opam-update-and-reinstall:
+	git pull
+	opam install .

README.md

@@ -42,7 +42,7 @@ and web native usage, providing quite a few extra features from vanilla Coq.
   - [👁 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)
+  - [🗒️ Markdown Support](#️-markdown-and-latex-support)
   - [👥 Document Outline](#-document-outline)
   - [🐝 Document Hover](#-document-hover)
   - [📁 Multiple Workspaces](#-multiple-workspaces)
@@ -125,16 +125,17 @@ pending obligations, open bullets and their goals.
 Goal display behavior is configurable in case you'd like to trigger goal display
 more conservatively.
 
-### 🗒️ Markdown Support
+### 🗒️ Markdown and LaTeX 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
-documents at the core of its design ideas.
+Open a markdown file with a `.mv` extension, or a `TeX` file ending in `.lv` or
+`.v.tex`, then `coq-lsp` will check the code parts that are enclosed into `coq`
+language blocks! `coq-lsp` places human-friendly documents at the core of its
+design ideas.
 
 <img alt="Coq + Markdown Editing" height="286px" src="etc/img/lsp-markdown.gif"/>
 
-Moreover, you can use Visual Studio Code Markdown preview to render your
-markdown documents nicely!
+Moreover, you can use the usual Visual Studio Code Markdown or LaTeX preview
+facilities to render your markdown documents nicely!
 
 ### 👥 Document Outline
 
@@ -249,11 +250,6 @@ We recommended using Coq 8.19 or `master` version. For other Coq versions, we
 recommend users to install the custom Coq tree as detailed in [Coq Upstream
 Bugs](#coq-upstream-bugs).
 
-Support for Coq 8.15 and 8.16 has been phased out due to lack of development
-resources, but if you are interested it should possible to bring it back with
-reasonable effort. Support for older Coq versions is also possible, with a bit
-more effort; `coq-lsp` should work with Coq versions back to Coq 8.10/8.9.
-
 Note that this section covers user installs, if you would like to contribute to
 `coq-lsp` and build a development version, please check our [contributing
 guide](./CONTRIBUTING.md)
@@ -278,12 +274,12 @@ guide](./CONTRIBUTING.md)
   This provides a Windows native binary that can be executed from VSCode
   normally. As of today a bit of configuration is still needed:
   - In VSCode, set the `Coq-lsp: Path` to:
-    + `C:\Coq-Platform~8.17-lsp\bin\coq-lsp.exe`
+    + `C:\Coq-Platform~8.20-lsp\bin\coq-lsp.exe`
   - In VSCode, set the `Coq-lsp: Args` to:
-    + `--coqlib=C:\Coq-Platform~8.17-lsp\lib\coq\`
-    + `--coqcorelib=C:\Coq-Platform~8.17-lsp\lib\coq-core\`
-    + `--ocamlpath=C:\Coq-Platform~8.17-lsp\lib\`
-  - Replace `C:\Coq-Platform~8.17-lsp\` by the path you have installed Coq above as needed
+    + `--coqlib=C:\Coq-Platform~8.20-lsp\lib\coq\`
+    + `--coqcorelib=C:\Coq-Platform~8.20-lsp\lib\coq-core\`
+    + `--ocamlpath=C:\Coq-Platform~8.20-lsp\lib\`
+  - Replace `C:\Coq-Platform~8.20-lsp\` by the path you have installed Coq above as needed
   - Note that the installers are unsigned (for now), so you'll have to click on
     "More info" then "Run anyway" inside the "Windows Protected your PC" dialog
   - Also note that the installers are work in progress, and may change often.
@@ -316,13 +312,14 @@ guide](./CONTRIBUTING.md)
 
 ### 🐍 Python
 
-- Interact programmatically with Coq files by using the [Python `coq-lsp` client](https://github.com/sr-lab/coq-lsp-pyclient)
+- Interact programmatically with Coq files by using the [Coqpyt](https://github.com/sr-lab/coqpyt)
   by Pedro Carrott and Nuno Saavedra.
 
 ## ⇨ `coq-lsp` users and extensions
 
 The below projects are using `coq-lsp`, we recommend you try them!
 
+- [Coqpyt, a Python client for coq-lsp](https://github.com/sr-lab/coqpyt)
 - [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)
@@ -358,7 +355,6 @@ that have some fixes backported:
 - 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`
 
 ### Known problems
 
@@ -386,19 +382,6 @@ that have some fixes backported:
   which should contain some important information; the content of this channel
   is controlled by the `Coq LSP > Trace: Server` option.
 
-### 📂 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 8.17.
-
-As this is very inconvenient for users in older Coq versions, we do provide a
-fixed Coq branch that you can install using `opam pin`:
-
-- For Coq 8.16:
-  ```
-  opam pin add coq https://github.com/ejgallego/coq.git#v8.16+lsp
-  ```
-
 ## 📔 Planned Features
 
 See [planned features and contribution ideas](etc/ContributionIdeas.md) for a

compiler/compile.ml

@@ -6,14 +6,10 @@ let workspace_of_uri ~io ~uri ~workspaces ~default =
   let file = Lang.LUri.File.to_string_file uri in
   match List.find_opt (fun (dir, _) -> is_in_dir ~dir ~file) workspaces with
   | None ->
-    let lvl = Io.Level.error in
-    let message = "file not in workspace: " ^ file in
-    Io.Report.message ~io ~lvl ~message;
+    Io.Report.msg ~io ~lvl:Error "file not in workspace: %s" file;
     default
   | Some (_, Error err) ->
-    let lvl = Io.Level.error in
-    let message = "invalid workspace for: " ^ file ^ " " ^ err in
-    Io.Report.message ~io ~lvl ~message;
+    Io.Report.msg ~io ~lvl:Error "invalid workspace for: %s %s" file err;
     default
   | Some (_, Ok workspace) -> workspace
 
@@ -34,13 +30,11 @@ let status_of_doc (doc : Doc.t) =
   match doc.completed with
   | Yes _ -> 0
   | Stopped _ -> 2
-  | Failed _ | FailedPermanent _ -> 1
+  | Failed _ -> 1
 
 let compile_file ~cc file : int =
   let { Cc.io; root_state; workspaces; default; token } = cc in
-  let lvl = Io.Level.info in
-  let message = Format.asprintf "compiling file %s" file in
-  Io.Report.message ~io ~lvl ~message;
+  Io.Report.msg ~io ~lvl:Info "compiling file %s" file;
   match Lang.LUri.(File.of_uri (of_string file)) with
   | Error _ -> 222
   | Ok uri -> (

compiler/driver.ml

@@ -22,10 +22,8 @@ let sanitize_paths message =
 
 let log_workspace ~io (dir, w) =
   let message, extra = Coq.Workspace.describe_guess w in
-  Fleche.Io.Log.trace "workspace" ("initialized " ^ dir) ~extra;
-  let lvl = Fleche.Io.Level.info in
-  let message = sanitize_paths message in
-  Fleche.Io.Report.message ~io ~lvl ~message
+  Fleche.Io.Log.trace "workspace" ~extra "initialized %s" dir;
+  Fleche.Io.Report.msg ~io ~lvl:Info "%s" (sanitize_paths message)
 
 let load_plugin plugin_name = Fl_dynload.load_packages [ plugin_name ]
 let plugin_init = List.iter load_plugin

controller/cache.ml

@@ -15,17 +15,17 @@
 (* Written by: Emilio J. Gallego Arias                                  *)
 (************************************************************************)
 
-module LIO = Lsp.Io
+module L = Fleche.Io.Log
 
 (* Cache stuff *)
 let memo_cache_file = ".coq-lsp.cache"
 
 let memo_save_to_disk () =
   try
     (* Fleche.Memo.save_to_disk ~file:memo_cache_file; *)
-    LIO.trace "memo" "cache saved to disk"
+    L.trace "memo" "cache saved to disk"
   with exn ->
-    LIO.trace "memo" (Printexc.to_string exn);
+    L.trace "memo" "%s" (Printexc.to_string exn);
     Sys.remove memo_cache_file;
     ()
 
@@ -35,12 +35,12 @@ let save_to_disk () = if false then memo_save_to_disk ()
 let memo_read_from_disk () =
   try
     if Sys.file_exists memo_cache_file then (
-      LIO.trace "memo" "trying to load cache file";
+      L.trace "memo" "trying to load cache file";
       (* Fleche.Memo.load_from_disk ~file:memo_cache_file; *)
-      LIO.trace "memo" "cache file loaded")
-    else LIO.trace "memo" "cache file not present"
+      L.trace "memo" "cache file loaded")
+    else L.trace "memo" "cache file not present"
   with exn ->
-    LIO.trace "memo" ("loading cache failed: " ^ Printexc.to_string exn);
+    L.trace "memo" "loading cache failed: %s" (Printexc.to_string exn);
     Sys.remove memo_cache_file;
     ()