Merge branch 'v8.17' into v8.16

CHANGES.md

@@ -1,3 +1,50 @@
+# coq-lsp 0.1.5: Form
+---------------------
+
+ - Fix a bug when trying to complete in an empty file (@ejgallego,
+   #270)
+ - Fix a bug with the position reported by the `$/coq/fileProgress`
+   notification
+ - Fix messages panel rendering after the port to React (@ejgallego,
+   #272)
+ - Fix non-compliance with LSP range type due to extra `offset` field
+   (@ejgallego, #271)
+ - The goal display now numbers goals starting with 1 instead of 0
+   (@artagnon, #277, report by Hugo Herbelin)
+ - Markdown Coq code blocks now must specify "coq" as a language
+   (@ejgallego, #280)
+ - 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,
+   #296, fixes #293, report by Ali Caglayan)
+ - `coq-lsp` incorrectly required the optional `rootPath`
+   initialization parameter, moreover it ignored `rootUri` if present
+   which goes against the LSP spec (@ejgallego, #295, report by Alex
+   Sanchez-Stern)
+ - `coq-lsp` will now reject opening multiple files when the
+   underlying Coq version is buggy (@ejgallego, fixes #275, fixes
+   #281)
+ - Fix bug when parsing client option for unicode completion
+   (@ejgallego #301)
+ - Support unicode characters in filenames (@artagnon, #302)
+ - Stop checking documents after a maximum number of errors,
+   user-configurable (by default 150) (@ejgallego, #303)
+ - Coq Markdown files (.mv extension) are now highlighted properly
+   using both Coq and Markdown syntax rules (@4ever2, #307)
+ - Goal view now supports find (@Alizter, #309, closes #305)
+ - coq-lsp now understands a basic version of Coq Waterproof files
+   (.wpn) Note that we don't associate to them by default, as to allow
+   the waterproof extension to take over the files (@ejgallego, #306)
+ - URI validation is now more strict, and some further bugs should be
+   solved; note still this can be an issue on some client settings
+   (@ejgallego, #313, fixes #187)
+ - Display Coq info and debug messages in info panel (@ejgallego,
+   #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)
+
 # coq-lsp 0.1.4: View
 ---------------------
 
@@ -25,7 +72,8 @@
  - Full document stats are now correctly computed on checking
    resumption, still cached sentences will display the cached timing
    tho (@ejgallego, #257)
- - Set Coq library name correctly (@ejgallego, #260)
+ - Set Coq library name correctly from URI, note this makes the server
+   to accept less URIs (@ejgallego, #260)
  - `_CoqProject` file is now detected using LSP client `rootPath`
    (@ejgallego, #261)
  - You can press `\` to trigger Unicode completion by the server. This

CONTRIBUTING.md

@@ -6,38 +6,181 @@ Thank you very much for willing to contribute to coq-lsp!
 `coq-lsp` has two components:
 
 - a LSP server for Coq project written in OCaml.
-- a `coq-lsp` VS Code extension written in TypeScript.
+- a `coq-lsp` VS Code extension written in TypeScript and React, in
+  the `editor/code` directory.
 
-## Compilation
+Read coq-lsp [FAQ](etc/FAQ.md) for an explanation on what the above mean.
 
-### Server
+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.
 
-The server project uses a standard OCaml + dune development setup.
+## General guidelines
 
-You can use the regular `dune build @check` etc... targets; `coq-lsp`
-is released with `dune-release`
+`coq-lsp` is developed in an open-source manner using GitHub.
+
+### Zulip chat
+
+Our main development channel is [hosted at
+Zulip](https://coq.zulipchat.com/#narrow/stream/329642-coq-lsp)
+. Please don't hesitate to stop by if you have any questions.
+
+### Code of conduct
+
+All contributors of `coq-lsp` must agree to our [code of
+conduct](./CODE_OF_CONDUCT.md)
+
+### License
+
+`coq-lsp` uses the LGPL 2.1 license, which is compatible with Coq's
+license.
+
+### Submitting a contribution, opening an issue.
+
+Please use the github standard interfaces to do so. When you submit a
+pull-request, you agree to share your code under `coq-lsp` license.
+
+We have a set of tags to classify pull requests and issues, we try to
+use them as much as possible. As of today, GitHub requires some
+permissions for regular users to be able to manipulate this meta-data,
+let us know if you need access.
+
+### Changelog
+
+We require an entry in `CHANGES.md` for all changes of relevance; note
+that as of today, `CHANGES.md` is the canonical changelog for _both_
+the server and the client.
+
+The client changelog that is used by the VS Code marketplace is at
+`editor/code/CHANGELOG.md`, but you should not modify it, as of today
+we will generate it from the relevant entries in `CHANGES.md` at
+release time.
+
+## Server guide
+
+### Compilation
+
+The server project uses a standard OCaml development setup based on
+Opam and Dune.
+
+To build it, you'll need an environment with the dependencies stated
+in `coq-lsp.opam`.
 
 `make` will compile the server (the `coq-lsp` binary, to be found in
 `_build/install/default/bin/coq-lsp`).
 
 As of today the `main` branch uses some submodules, be sure they are
 properly initialized (`make submodules-init`).
 
-We plan to get rid of the submodules soon.
+(We plan to get rid of the submodules soon)
+
+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`.
+
+If you wish to do `nix build` or compose this flake from another project, you
+will need to use the .?submodules=1` trick, since we use submodules here for
+vendoring. For example, building requires:
+
+```
+nix build .?submodules=1
+```
+
+You can use this flake in other flakes or Nix derivations.
 
-### VS Code Extension
+#### Releasing
 
-The VS Code extension is setup as a standard npm package using
-`esbuild` as the bundler. The extension has a main component and some
-webviews components written using React.
+`coq-lsp` is released using `dune-release tag` + `dune-release`.
 
-For the client, the recommended setup is `dune exec -- code
-editor/code` , that will open the VSCode extension development
-environment, you can run the extension from the Run panel.
+### Code organization
 
-## Miscellaneous events
+The `coq-lsp` server consists of several components, we present them bottom-up
 
-- We use `ocamlformat` to automatically format our codebase.
+- `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.
+- `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
+- `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 jsCoq.
+
+Some tips:
+
+- we much prefer not to address Coq API directly, but always use the
+  `coq` library to do it.
+- `fleche` has carefully controlled dependencies and code structure
+  due to a) having to run in JS, b) targeting other systems in
+  addition to Coq.
+- We use [ocamlformat](https://github.com/ocaml-ppx/ocamlformat) to
+  automatically format our codebase. `make fmt` will take care of it
+  if your editor is not configured to so automatically.
+
+## VS Code Extension guide
+
+The VS Code extension is setup as a standard `npm` type-script + React
+package using `esbuild` as the bundler. The extension has a main
+component in `editor/code/src/` and some webviews components written
+using React under `editor/code/views`.
+
+There are two ways to work with the VS Code extension: you can let VS Code
+itself take care of building it (preferred setup), or you can build it manually.
+
+First, run `npm install` in `editor/code`:
+
+```sh
+(cd editor/code && npm i)
+```
+
+That will setup the required packages as it is usual. You can run `package.json`
+scripts the usual way:
+
+```sh
+(cd editor/code && npm run typecheck) # typecheck the project
+(cd editor/code && npm run compile) # fast dev-transpile (no typecheck)
+```
+
+If you want to work with VS Code, these commands are not necessary, VS
+Code will build the project automatically.
+
+Launch VS Code using `dune exec -- code -n editor/code`, which will setup the
+right environment variables such as `PATH` and `OCAMLPATH`, so the `coq-lsp`
+binary can be found by VS Code. If you have installed `coq-lsp` globally, you
+don't need `dune exec`, and can just run `code -n editor/code`.
+
+Once in VS Code, you can launch the extension normally using the left "Run and
+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, tho this is not recommended.
+
+### Miscellaneous info
+
+- The "Restart Coq LSP server" command will be of great help while
+  developing with the server.
 - We use
   [prettier](https://marketplace.visualstudio.com/items?itemName=esbenp.prettier-vscode)
-  to automatically format files in editor/code.
+  to automatically format files in editor/code. `make ts-fmt` will do
+  this in batch mode.
+
+### Debugging
+
+The default build target will allow you to debug the extension by
+providing the right sourcemaps.
+
+## Emacs
+
+You should be able to use `coq-lsp` with [eglot](https://joaotavora.github.io/eglot/).
+
+If you find any trouble using `eglot` or `lsp-mode` with coq-lsp, please don't
+hesitate to open an issue, Emacs support is a goal of `coq-lsp`.
+
+# VIM
+
+`coq-lsp` should also run on VIM, VIM/NeoVIM support is a goal of `coq-lsp`