Contributing to Coq LSP

Thank you very much for willing to contribute to coq-lsp!

The coq-lsp repository contains several tightly coupled components in a single repository, also known as a monorepo, in particular:

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-lspa 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 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.

General guidelines

coq-lsp is developed in an open-source manner using GitHub.

Zulip chat

Our main development channel is hosted at Zulip . 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

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. This also works on Windows using the Coq Platform Source Install

The default development environment for coq-lsp is a "composed" 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.

This will however install a local Coq version which may not be convenient for all use cases; we thus detail below an alternative install method for those that would like to install a coq-lsp development branch into an OPAM switch.

Default development setup, local Coq / `coq-lsp`

This setup will build Coq and coq-lsp locally; it is the recommended way to develop coq-lsp itself.

Install the dependencies (the complete updated list of dependencies can be found in coq-lsp.opam).
```
opam install --deps-only .
```
Initialize submodules (the main branch uses some submodules, which we plan to get rid of soon. Branches v8.x can already skip this step.)
```
make submodules-init
```
Compile the server (the coq-lsp binary can be found in _build/install/default/bin/coq-lsp).
```
make
```

Alternatively, you can also use the regular dune build @check etc... targets.

Now, binaries for Coq and coq-lsp can be found under _build/install/default and used via dune exec -- fcc or dune exec -- $your_editor.

Global OPAM install

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.

You can just do:

make opam-update-and-reinstall

or alternatively, do it step by step

Be sure submodules and coq-lsp are up to date:a
```
git pull --recurse-submodules
```
alternatively you can use make submodules-init to refresh the submodules.

Install vendored Coq

opam install vendor/coq/coq{-core,-stdlib,ide-server,}.opam

Install coq-lsp:
```
opam install .
```

Then, you should get a working OPAM switch with Coq and coq-lsp from your chosen coq-lsp branch.

Nix

We have a Nix flake that you can use.

Dependencies: for development it suffices to run nix develop to spawn a shell with the corresponding dependencies.

With the following line you can save the configuration in a Nix profile which will prevent the nix store gc from deleting the entries:
```
nix develop --profile nix/profiles/dev
```
You can then use the following line to reuse the previous profile:
```
nix develop nix/profiles/dev
```
Initialize submodules (the main branch uses some submodules, which we plan to get rid of soon. Branches v8.x can already skip this step.)
```
make submodules-init
```
Compile the server (the coq-lsp binary can be found in _build/install/default/bin/coq-lsp).
```
make
```

You can view the list of packages and devShells that are exposed by running nix flake show.

If you wish to do nix build, you will need to use the .?submodules=1 trick, since we use submodules here for vendoring. For example, building requires:

nix build .?submodules=1

This currently only applies to building the default package (coq-lsp), which is the server. Clients don't have specific submodules as of yet.

When the flake is out-of-date, for instance when a new version of ocamlformat is out, you can update the flake inputs with:

nix flake update

You can also add the dev version build to your flake as:

inputs.coq-lsp = { type = "git"; url = "https://github.com/ejgallego/coq-lsp.git"; submodules = true; };
...
coq-lsp.packages.${system}.default

Code organization

The coq-lsp server consists of several components, we present them bottom-up

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.
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 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 to automatically format our codebase. make fmt will take care of it if your editor is not configured to so automatically.

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.

Worker version (and debugging tips)

See ocsigen/js_of_ocaml#410 for debugging tips with js_of_ocaml.

Client guide (VS Code Extension)

The VS Code extension is setup as a standard npm Typescript + React package using esbuild as the bundler.

Setup

Navigate to the editor folder
```
cd editor/code
```
Install dependencies:
```
npm i
```

Then 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.

Let VS Code handle building the project

There is nothing to be done, VS Code will build the project automatically when launching the extension. You can skip to launching the extension.

Manual build

Navigate to the editor folder
```
cd editor/code
```

You can now run package.json scripts the usual way:

Typecheck the project
```
npm run typecheck 
```
Fast dev-transpile (no typecheck)
```
npm run compile
```

Launch the extension

From the toplevel directory 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, 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 develop .#client-vscode

The steps to setup the client are similar to the manual build:

Spawn develop shell
```
nix develop
```
Inside develop, spawn the client-vscode shell
```
nix develop .#client-vscode
```
Navigate to the editor folder
```
cd editor/code
```
Install dependencies:
```
npm i
```
Follow the steps in manual build.

You are now ready to launch the extension.

Code organization

The extension is divided into two main folders:

editor/code/src/: contains the main components,
editor/code/views: contains some webviews components written using React.

Testing the Web Extension

coq-lsp has preliminary support to run as a "Web Extension", to test that, you want to use the web extension profile in the launch setup.

Miscellaneous info

The "Restart Coq LSP server" command will be of great help while developing with the server.
We use prettier 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.

Nix:

Nix can be configured to use the version of the VS Code extension from our git in the following way:

inputs.coq-lsp = { type = "git"; url = "https://github.com/ejgallego/coq-lsp.git"; submodules = true; };
...
programs.vscode = {
  enable = true;
  extensions = with pkgs.vscode-extensions; [
    ...
    inputs.coq-lsp.packages.${pkgs.system}.vscode-extension
    ...
  ];
};

Test-suite

coq-lsp has a test-suite in the test directory, see the README there for more details.

Releasing

coq-lsp is released using dune-release tag + dune-release.

The checklist for the release as of today is the following:

Pre-release

update the version number at editor/code/package.json, do npm i
update the version number at fleche/version.ml

Client:

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

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

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

After release

[important] bump version.ml and editor/code/package.json version string to a -dev suffix

Emacs

You should be able to use coq-lsp with eglot or lsp-mode

Emacs support is a goal of coq-lsp, so if you find any trouble using eglot or lsp-mode with coq-lsp, please don't hesitate to open an issue. See coq-lsp README for more notes on Emacs support.

VIM

You should be able to use coq-lsp with VIM.

VIM support is a goal of coq-lsp, so if you find any trouble using coq-lsp with VIM, please don't hesitate to open an issue.

See coq-lsp README for more notes on VIM support.

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

CONTRIBUTING.md

CONTRIBUTING.md

Contributing to Coq LSP

General guidelines

Zulip chat

Code of conduct

License

Submitting a contribution, opening an issue.

Changelog

Server guide

Compilation

Default development setup, local Coq / `coq-lsp`

Global OPAM install

Nix

Code organization

Unicode setup

Worker version (and debugging tips)

Client guide (VS Code Extension)

Setup

Let VS Code handle building the project

Manual build

Launch the extension

Nix

Code organization

Testing the Web Extension

Miscellaneous info

Debugging

Nix:

Test-suite

Releasing

Pre-release

Client:

Server:

After release

Emacs

VIM

Files

CONTRIBUTING.md

Latest commit

History

CONTRIBUTING.md

File metadata and controls

Contributing to Coq LSP

General guidelines

Zulip chat

Code of conduct

License

Submitting a contribution, opening an issue.

Changelog

Server guide

Compilation

Default development setup, local Coq / coq-lsp

Global OPAM install

Nix

Code organization

Unicode setup

Worker version (and debugging tips)

Client guide (VS Code Extension)

Setup

Let VS Code handle building the project

Manual build

Launch the extension

Nix

Code organization

Testing the Web Extension

Miscellaneous info

Debugging

Nix:

Test-suite

Releasing

Pre-release

Client:

Server:

After release

Emacs

VIM

Default development setup, local Coq / `coq-lsp`