This page is intended for software developers who wish to help with the VsRocq2 development effort.

The two main building blocks are the language server and the client (the vscode extension, namely).

Language server

The language server is developed in ocaml and makes it possible to link from the client directly to the Rocq API and exploit LSP.

Architecture

The document data structure holds:

• the text
• the parsed document (AST of each sentence, mapping between text positions and sentences)
• the checked document (each sentence comes with a checking result)
• the feedback (each message by the prover is attached to the corresponding sentence)

The architecture is organized in the following components.

• VsCoqtop: This component handles the main event loop.
• LSPManager: This component handles the JSONRPC encoding, LSP requests, notifications and responses as well as LSP events dispatch.
• DocumentManager: The document manager handles everything that pertains to document representation and parsing, handles feedbacks.
• Document: Raw and parsed document representations.
• Scheduler: Incremental static dependency analysis.
• QueryManager: This handles the Rocq queries (Search, About, etc... hover, completion)
• Checking manager: document checking, exec overview
• Execution manager: Handles execution of the Rocq interpreter
• Delegation manager: Handles worker tasks

flowchart TD
    A[vsrocqtop]
    B[LSPManager]

    C["DocumentManager
       (document)"]
    D["ExecutionManager
       (schedule2task, exec promise)"]
    D1[(Rocq Interpreter)]
    E["DelegationManager
       (spawn, kill)"]
    F[QueryManager]
    F1[(Rocq API)]
    G["Document
       (parser state, outline)"]
    G1[(Rocq Parser)]
    H[Scheduler]
    I["CheckingManager
       (observe_id, checking overview)"]
    J[\"proverThread
        (sequentialize, interrupt)"/]
    K[\proverWorker/]
    A --> B
    B --> C
    I --> D
    D --> E
    C --> F
    C --> G
    C --> H
    C --> I
    D --- J
    J ---|stateful| D1
    F --- J
    J ---|stateful| F1
    G --- J
    J ---|stateful| G1
    E --- K
    K ---|stateful| D1
    H ---|pure| F1
    style D1 fill: #f3ef1d
    style F1 fill: #f3ef1d
    style G1 fill: #f3ef1d
    style J fill: #75e15c
    style K fill: #75e15c

Building

If you have nix installed, you can do a full developer build of the language server by running:

nix develop .#vsrocq-language-server -c bash -c "cd language-server && dune build"

Composing the build with Rocq

To build a VsRocq with a local version of Rocq, from the modified Rocq directory:

1. Build Rocq, e.g. with make world to build Rocq and set up dune
2. Clone the VsRocq repository in rocq/vsrocq/ (next to, say, kernel/).
3. Then dune build vsrocq/language-server will build the server, typically in _build/install/default/bin/vsrocqtop (next to the rocq binaries).
4. Set the (absolute) path to the local build "vsrocq.path": "path/rocq/_build/install/default/bin/vsrocqtop" in user settings.
5. Reload VsCode.
6. Whenever you change the Rocq sources dune build will now also rebuild vsrocqtop. If you specify a more specific dune target, remember that vsrocqtop is linked to Rocq, so if you don't rebuild it it will not work.

Debugging

Client

The client is the VSCode extension in itself. Apart from the usual VSCode lingo, we develop two web apps that are used within separate panels in the extension and are specific to Rocq, namely the goal-view-ui and the search-view-ui.

Design pattern for the web apps

Both of the two Rocq exclusive panels are react apps. We use the atomic design pattern and the VSCode webview UI toolkit.

Building

• Make sure you have up to date npm and node.js. For example, at the time of writing this guide, node.js version 19.0.1
• From the client folder run npm install which will ensure all dependencies are installed for the extension and the web apps.
• Still from the client folder, run npm run build --workspaces to build the extension and all the sub-web apps.
• To package the extension run npm run package
• To make an installable .vsx package, npx vsce package. This package can be installed locally in any code workspace or all (not recommended, as it can overwrite an existing globally installed vsx code --install-extension vsrocq-*.vsix)
• For publishing to VSCode market place use the vsce tool

Debugging

You can debug the web apps independently. From the client folder just run npm run start -w goal-view-ui or npm run start -w search-ui. This will launch the corresponding web app in local development server. You can then access it through your usual browser or the VSCode browser.

Note that both the apps can also be built independently through the npm run build -w goal-view-ui or npm run build -w search-ui commands.

To launch the extension in debug mode, assuming you have built the language-server, you can either use a nix dev shell to run vscode (nix develop .#vsrocq-client -c code .) or handle your own config.

Note that you need to set the path to vsrocqtop in the VSCode user settings (just search for vsrocq).

E2E tests

From the client folder run npm test. To pass arguments to the language server you can use the VSCOQARGS env variable, e.g.

VSCOQARGS='-vsrocq-d all' npm test

Remember that if the language server fails to initialize, the log is not displayed in the output panel as usual, but rather written to a file named like /tmp/vsrocq_init_log.xxx.

To run the tests on a language server not in a standard location (not in the language-server folder nor in PATH), set VSCOQPATH to the binary you want to be run by the test.

Release process

To release a new version of VsRocq:

1. First make sure to bump the version number in the three folowing files:
   • flake.nix (look for vsrocq_version)
   • client/package.json (llok for "version":)
   • language-server/vsrocqtop/lspManager.ml (look for let server_info)

1.a Don't forget to add the version requirements in client/src/utilities/versioning.ts, look for versionRequirements.

2. Create a signed tag for the release with the new version number

    git tag -s #VERSION_NUMBER

3. Push

    git push origin #VERSION_NUMBER

Version semantics are currently as follows: v#NUMBER+coq#COQ_VERSION (ex: v1.9.2+coq.8.18) Since we now use opt comp and support all Rocq versions, version semantics are v2.#.# (ex: v2.2.2)

Once the CI has run, a draft release will be automatically created. Open the draft release and edit the change log to your liking. Finally, light a candle, do a little prayer and click release !

Publishing the release on GH fires the cd.yxml job that in turn opens a PR on the opam repository.

After the opam package has been published (PR merged by opam maintainers), the user should then use publish-extension.yml to publish the extensions on the vscode marketplace as well as vscodium.

CI/CD pipeline for release process

The CI pipeline (ci.yml) handles creating the draft release (with a tarball archive) when a tag is pushed. This is done in the create-release job.

The CD pipeline (cd.yml) automatically publishes the release to opam once the draft is released. Don't forget to fill out the change log appropriately before hitting release. If it is a pre-release, the pipeline will publish to rocq-prover/opam instead of opam/opam-repository.

There are two manual pipelines:

• publish-server.yml allows to publish a release on opam manually (if the automatic pipeline goes wrong). The user only need to give the tag (with the correct version semantics) and specify if it is a release or pre-release.
• publish-extension.yml handles publishing the extension on the vscode market place as well as vscodium. This is always done manually because the opam release process might take some time. The extensions should only be published once the package is on opam.