Merge branch 'main' into v9.0

Author: ejgallego

CHANGES.md

@@ -1,5 +1,5 @@
-# unreleased
-------------
+# coq-lsp 0.2.3: Barrage
+------------------------
 
  - [fleche] fix quick fixes for errors being lost due to incorrect
    handling of `send_diags_extra_data` (@ejgallego, #850)
@@ -71,6 +71,13 @@
    (@JulesViennotFranca, @ejgallego, #962)
  - [doc] [petanque] Document petanque v1, improve readme (@ejgallego,
    #963)
+ - [plugin] [astdump] Make the JSON and SEXP output into a line per
+   object by default (@blackbird1128, @ejgallego, #874)
+ - [doc] [emacs] [protocol] Improve documentation for `proof/goals`,
+   add link to official emacs mode by Josselin Poiret (@ejgallego,
+   #969, thanks to @jpoiret, cc: #941)
+ - [goals] Include `range` in `proof/goals` answer. This is useful for
+   clients willing to do highlighting (@ejgallego, @jpoiret, #970)
 
 # coq-lsp 0.2.2: To Virtual or not To Virtual
 ---------------------------------------------

CONTRIBUTING.md

@@ -310,8 +310,12 @@ Debug" panel in Visual Studio Code, or the F5 keybinding.
 You can of course install the extension in your `~/.vscode/` folder if so you
 desire, although this is not recommended.
 
-### Nix 
-In the case of the client we expose a separate shell, `client-vscode`, which can be spawned with the following line (this can be done on top of the original `nix develop`).
+### Nix
+
+In the case of the client we expose a separate shell, `client-vscode`,
+which can be spawned with the following line (this can be done on top
+of the original `nix develop`).
+
 ```
 nix develop .#client-vscode
 ```
@@ -388,41 +392,49 @@ README there for more details.
 
 The checklist for the release as of today is the following:
 
-### Pre-release
+### Prepare a release commit
 
 - update the version number at `editor/code/package.json`, do `npm i`
 - update the version number at `fleche/version.ml`
+- update the client changelog at `editor/code/CHANGELOG.md`, commit
+- add release notes in `etc/release_notes/` if needed
+- do `make extension` to update the `package-lock.json` file
 
-### Client:
+### Tag and test release commit
+
+```
+export COQLSPV=0.2.3
+git checkout main  &&                    make && make test test-compiler && dune-release tag ${COQLSPV}
+git checkout v9.0  && git merge main  && make && make test test-compiler && dune-release tag ${COQLSPV}+9.0
+git checkout v8.20 && git merge v9.0  && make && make test test-compiler && dune-release tag ${COQLSPV}+8.20
+git checkout v8.19 && git merge v8.20 && make && make test test-compiler && dune-release tag ${COQLSPV}+8.19
+git checkout v8.18 && git merge v8.19 && make && make test test-compiler && dune-release tag ${COQLSPV}+8.18
+git checkout v8.17 && git merge v8.18 && make && make test test-compiler && dune-release tag ${COQLSPV}+8.17
+```
+
+### Client release:
 
-- update the client changelog at `editor/code/CHANGELOG.md`, commit
-- for the `main` branch: `dune release tag $coq_lsp_version`
 - build the extension with `npm run vscode:prepublish`
 - check with `vsce ls` that the client contents are OK
-- `vsce publish`
-- upload vsix to OpenVSX marketplace
+- upload to official VSCode marketplace: `vsce publish`
+- upload vsix to OpenVSX marketplace:
 
 ### Server:
 
-- sync branches for previous Coq versions, using `git merge`, test and push to CI.
-- `dune release tag` for each `$coq_lsp_version+$coq_version`
-- `dune release` for each version that should to the main opam repos
-- [deprecated] update pre-release packages to coq-opam-archive
+`dune release` for each version that should to the main opam repos:
 
-The above can be done with:
 ```
-export COQLSPV=0.2.1
-git checkout main  && make                    && dune-release tag ${COQLSPV}
-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
+export COQLSPV=0.2.3
+git checkout v9.0  && dune-release
+git checkout v8.20 && dune-release
+git checkout v8.19 && dune-release
+git checkout v8.18 && dune-release
+git checkout v8.17 && dune-release
 ```
 
-### After release
+### [important] After release commit
 
-- [important] bump `version.ml` and `editor/code/package.json` version
-  string to a `-dev` suffix
+- bump `version.ml` and `editor/code/package.json` version string to a `$version+1-dev`
 
 ## Emacs
 

Makefile

@@ -73,8 +73,8 @@ vendor/coq/config/coq_config.ml: vendor/coq
 	        -libdir "$$EPATH/_build/install/default/lib/coq" \
 	        -bytecode-compiler $(COQVM) \
 		-native-compiler no \
-	&& cp theories/dune.disabled theories/dune \
-	&& cp user-contrib/Ltac2/dune.disabled user-contrib/Ltac2/dune
+	&& cp theories/Corelib/dune.disabled theories/Corelib/dune \
+	&& cp theories/Ltac2/dune.disabled theories/Ltac2/dune
 
 # We set windows parameters a bit better, note the need to use forward
 # slashed (cygpath -m) due to escaping :( , a conversion to `-w` is
@@ -86,8 +86,8 @@ winconfig:
 	&& ./configure -no-ask -prefix "$$EPATH\\_build\\install\\default\\" \
 	        -libdir "$$EPATH\\_build\\install\\default\\lib\\coq\\" \
 		-native-compiler no \
-	&& cp theories/dune.disabled theories/dune \
-	&& cp user-contrib/Ltac2/dune.disabled user-contrib/Ltac2/dune
+	&& cp theories/Corelib/dune.disabled theories/Corelib/dune \
+	&& cp theories/Ltac2/dune.disabled theories/Ltac2/dune
 
 .PHONY: wp
 wp:

README.md

@@ -1,53 +1,66 @@
-# Coq LSP <img align="right" height="42" src="./etc/img/inria-logo.png"/>  <!-- omit in toc -->
+# Rocq LSP <img align="right" height="42" src="./etc/img/inria-logo.png"/>  <!-- omit in toc -->
 
 [![Github CI][ci-badge]][ci-link]
 
-`coq-lsp` is a [Language
-Server](https://microsoft.github.io/language-server-protocol/) for the [Rocq
-Prover](https://coq.inria.fr). It implements the
-[LSP](https://microsoft.github.io/language-server-protocol/specifications/lsp/3.17/specification/) protocol, with custom [extensions](./etc/doc/PROTOCOL.md), including the [petanque](./petanque)
-protocol, designed for low-latency interaction with Rocq, particularly suited for AI and
-Software Engineering applications.
+`coq-lsp` is a [Language Server](https://microsoft.github.io/language-server-protocol/) for the [Rocq Prover](https://coq.inria.fr). It provides a single server that implements:
+
+- the [LSP](https://microsoft.github.io/language-server-protocol/specifications/lsp/3.17/specification/)
+  protocol, with custom [extensions](./etc/doc/PROTOCOL.md)
+- the [petanque](./petanque) protocol, designed for low-latency interaction with
+  Rocq, idel for AI and software engineering applications
+- the [MCP](https://modelcontextprotocol.io/) protocol (upcoming), an open
+  protocol that standardizes how applications provide context to LLMs
 
 **Key [features](#Features)** of `coq-lsp` are: continuous, incremental document
 checking, real-time interruptions and limits, programmable error recovery,
-literate Rocq/Markdown/LaTeX document support, multiple workspaces, positional
-goals, information panel, performance data, extensible command-line compiler,
-a plugin system, and more.
+literate Markdown and LaTeX document support, multiple workspaces, positional
+goals, information panel, performance data, completion, jump to definition,
+extensible command-line compiler, a plugin system, and more.
+
+`coq-lsp` is built on **Flèche**, a new document checking engine for formal
+documents based on our previous work on
+[SerAPI](https://github.com/ejgallego/coq-serapi/) and
+[jsCoq](https://github.com/jscoq/jscoq).
+
+Designed for interactive use and web-native environments, Flèche is extensible
+and supports [advanced tooling integration](#-a-platform-for-research) and
+capabilities beyond standard Rocq.
 
-See the [User Manual](./etc/doc/USER_MANUAL.md) and the [General
-Documentation Index](./etc/doc/) for more details.
+See the [User Manual](./etc/doc/USER_MANUAL.md) and the [General Documentation Index](./etc/doc/) for more details.
 
 This repository also includes the `coq-lsp` [Visual Studio
 Code](https://code.visualstudio.com/) editor extension for the [Rocq Proof
-Assistant](https://coq.inria.fr), and a few other components, see our
-[contributing guide](#contributing) for more information. Experimental support
+Assistant](https://coq.inria.fr), and a few other components. See our
+[contributing guide](#contributing) for more information. Support
 for [Emacs](#emacs), [Vim](#vim) and [Neovim](#neovim) is also available in
 their own projects.
 
 **Quick Install**:
 
-  - **🐧 Linux / 🍎 macOs / **🪟 Windows:**:**
+  - **🐧 Linux / 🍎 macOs / 🪟 Windows:**
 ```
 $ opam install coq-lsp && code --install-extension ejgallego.coq-lsp
 ```
 
-  - **🪟 Windows:** (alternative method) Download the [Coq Platform installer](#-server)
+  - **🪟 Windows:** (alternative method)
 
-Try it online ☕☕ (experimental) https://github.dev/ejgallego/hello-rocq
+    Download the [Coq Platform installer](#-server)
 
-`coq-lsp` aims to deliver a modern, seamless experience for interactive theorem
-proving, while serving as a robust platform for research and integration with
-other tools.
+  - **🦄 Emacs**:
 
-`coq-lsp` is built on **Flèche**, a new document checking engine for
-formal documents developed from the lessons of
-[SerAPI](https://github.com/ejgallego/coq-serapi/) and
-[jsCoq](https://github.com/jscoq/jscoq). Flèche is optimized for
-interactive use, [SerAPI-like tooling integration](#-a-platform-for-research),
-and web-native environments, offering capabilities beyond standard Rocq.
+```elisp
+ (use-package rocq-mode
+    :vc (:url "https://codeberg.org/jpoiret/rocq-mode.el.git"
+         :rev :newest)
+    :mode "\\.v\\'"
+    :hook
+    (rocq-mode . rocq-follow-viewport-mode)
+    (rocq-mode . rocq-auto-goals-at-point-mode))
+```
+
+  - **☕ Try it online ☕ (experimental)**:
 
-`coq-lsp` supports 🐧 Linux, 🍎 macOS, 🪟 Windows , and ☕ JavaScript (Node/Browser)
+    https://github.dev/ejgallego/hello-rocq
 
 ## Table of Contents <!-- omit in toc -->
 
@@ -257,10 +270,11 @@ ready.
 
 ### 🏘️ Supported Coq Versions
 
-`coq-lsp` supports Coq 8.20, Coq 8.19, Coq 8.18, Coq 8.17, and Coq's `master`
-branch.  Code for each Coq version can be found in the corresponding branch.
+`coq-lsp` supports Rocq 9.0, Coq 8.20, Coq 8.19, Coq 8.18, Coq 8.17, and Coq's
+`master` branch.  Code for each Coq version can be found in the corresponding
+branch.
 
-We recommended using Coq 8.19 or `master` version. For other Coq versions, we
+We recommended using Rocq 9.0 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).
 
@@ -308,10 +322,8 @@ guide](./CONTRIBUTING.md)
 
 ### 🦄 Emacs
 
-- An experimental configuration for `lsp-mode` has been provided by Arthur
-  Azevedo de Amorim, supporting goal display, see [the Zulip
-  thread](https://coq.zulipchat.com/#narrow/stream/329642-coq-lsp/topic/coq-lsp.20under.20Emacs.2E)
-  for more information.
+The official Rocq Emacs mode is https://codeberg.org/jpoiret/rocq-mode.el ,
+maintained by Josselin Poiret with contributions by Arthur Azevedo de Amorim.
 
 ### ✅ Vim
 

controller-js/jsso.ml

@@ -51,7 +51,5 @@ let rec json_to_obj (cobj : < .. > Js.t) (json : Yojson.Safe.t) : < .. > Js.t =
   | `String s -> coerce @@ Js.string s
   | `Int m -> coerce @@ Js.number_of_float (float_of_int m)
   | `Intlit s -> coerce @@ Js.number_of_float (float_of_string s)
-  | `Tuple t -> coerce @@ Array.(Js.array @@ map ofresh (of_list t))
-  | `Variant (_, _) -> pure_js_expr "undefined"
 
 let json_to_obj json = json_to_obj (Js.Unsafe.obj [||]) json

controller/rq_goals.ml

@@ -60,11 +60,13 @@ let goals ~pp_format ~mode ~pretac () ~token ~doc ~point =
   let open Coq.Protect.E.O in
   let+ goals, program = get_goal_info ~token ~doc ~point ~mode ~pretac () in
   let node = Info.LC.node ~doc ~point Exact in
+  let range = Option.map Fleche.Doc.Node.range node in
   let messages = mk_messages node in
   let error = Option.bind node mk_error in
   let pp = pp ~pp_format in
   Lsp.JFleche.GoalsAnswer.(
-    to_yojson pp { textDocument; position; goals; program; messages; error })
+    to_yojson pp
+      { textDocument; position; range; goals; program; messages; error })
   |> Result.ok
 
 let goals ~pp_format ~mode ~pretac () ~token ~doc ~point =

editor/code/CHANGELOG.md

@@ -1,3 +1,34 @@
+# coq-lsp 0.2.3: Barrage
+------------------------
+
+ Mainly small tweaks and improvements, note the changed keybindings in
+ OSX; summary of user-visible changes:
+
+ - [vscode] [macos] Resolve keybinding conflict with Cmd+N and
+   Cmd+Enter, we now use Alt+N and Alt+Shift+Enter, (Andrei
+   Listochkin, #926)
+ - [fleche] fix quick fixes for errors being lost due to incorrect
+   handling of `send_diags_extra_data` (@ejgallego, #850)
+ - [vscode] Syntax highlighting for Coq 8.17-8.20 (@4ever2, #872)
+ - [vscode] [web] Fix web extension not exporting the coq-lsp
+   extension API (@ejgallego, reported by @amblafont, #911, fixes
+   #877)
+ - [hover] New option `show_state_hash_on_hover` that displays state
+    hash on hover for debug (@ejgallego, #954)
+ - [doc] [faq] Updated FAQ to account for VSCoq 2 release in 2023,
+   thanks to Patrick Nicodemus for pointing out the outdated
+   documentation (@ejgallego, #846, fixes #817)
+ - [rocq] [fleche] Disable memprof-limits interruption backend by
+   default, as released Rocq versions are not safe yet. If you want to
+   enable it, you can still do it with the `--int_backend=Mp` command
+   line option (@ejgallego, #957, fixes #857, reported by @dariusf,
+   cc: rocq-prover/rocq#19177)
+ - [lsp] [controller] Include Rocq feedback on request errors, using
+   the optional `data` field. This is useful to still be able to
+   obtain feedback messages such as debug messages even when a request
+   fails. This also opens the door to better protocol handling and
+   petanque integration (@ejgallego, #959, #961)
+
 # coq-lsp 0.2.2: To Virtual or not To Virtual
 ---------------------------------------------
 

editor/code/lib/types.ts

@@ -60,6 +60,7 @@ export type ProgramInfo = [Id, OblsView][];
 export interface GoalAnswer<Pp> {
   textDocument: VersionedTextDocumentIdentifier;
   position: Position;
+  range: Range;
   goals?: GoalConfig<Pp>;
   program?: ProgramInfo;
   messages: Pp[] | Message<Pp>[];

editor/code/package-lock.json

@@ -2,7 +2,7 @@
   "name": "coq-lsp",
   "displayName": "Coq LSP",
   "description": "Coq LSP provides native vsCode support for checking Coq proof documents",
-  "version": "0.2.3-dev",
+  "version": "0.2.3",
   "contributors": [
     "Emilio Jesús Gallego Arias <[email protected]>",
     "Ali Caglayan <[email protected]>",