DOCSEARCHbyAlgolia
Submit Docs

VsRocq Documentation

repository·main·Indexed 19 days ago

https://github.com/rocq-prover/vsrocq

Documentation for VsRocq, a Visual Studio Code and VSCodium extension providing support for the Rocq Interactive Theorem Prover. It includes guides on installing the vsrocq-language-server via opam or NixOS, configuring proof checking modes (Manual and Continuous), and managing the LSP-based language server components such as vsrocqtop, the document manager (DM), and the simple event library (SEL).

Tokens
11.8K
Snippets
43
Records
69
Agent score
58%

What's inside VsRocq

  1. Overview of the VSRocq Language Server

    main

    The VSRocq Language Server implements the Rocq LSP (Language Server Protocol) with additional VSRocq-specific messages. These extensions allow for specialized interactions such as declaring points of interest and printing goals. The server is built using several internal components:

    • SEL: A simple event library used for I/O handling.
    • DM: A document manager for Rocq that supports delegation via SEL.
    • vsrocqtop: A Rocq toplevel speaking LSP built upon the DM and SEL components.

  2. Language Server Architecture

    main

    The VsRocq language server (written in OCaml) manages the connection between the VSCode client and the Rocq API via LSP.

    Core Data Structure: The Document The document structure maintains:

    • Text content
    • Parsed document (AST per sentence and text-to-sentence mapping)
    • Checked document (checking results per sentence)
    • Feedback (prover messages attached to sentences)

    Key Components:

    • VsCoqtop: The main event loop.
    • LSPManager: Handles JSONRPC encoding, LSP requests/notifications/responses, and event dispatch.
    • DocumentManager: Manages document representation, parsing, and feedback.
    • Scheduler: Performs incremental static dependency analysis.
    • QueryManager: Handles Rocq queries (Search, About, hover, completion) via the Rocq API.
    • CheckingManager: Manages document checking and execution overview.
    • ExecutionManager: Handles the execution of the Rocq interpreter.
    • DelegationManager: Manages worker tasks (spawn/kill).
    • ProverThread/Worker: Handles sequentialization and interruption of the prover.

  3. Use goal panel ellipsis and modifiers

    main

    Since version 2.1.7, goals can be ellided to manage large displays. You can control depth via the vsrocq.goals.maxDepth setting.

    Keyboard/Mouse Modifiers:

    • Alt + Click: Open/close an ellipsis (only opens partially).
    • Shift + Alt + Click: Fully open an ellipsis (all children are also opened).

  4. Understand how highlights and goal views work in VsRocq

    main

    VsRocq uses specific LSP verbs to provide visual feedback in the editor:

    Highlights

    The prover/updateHighlights notification provides information about which parts of a document are currently being processed. It returns a uri and two sets of ranges:

    • processingRange: Lines currently being processed by the server.
    • processedRange: Lines that have already been processed. By default, processed lines are displayed in the VSCode gutter.

    Goal View

    The goal view is updated via the prover/updateProofView request. It uses PpString to provide syntactic coloration for goals and hypotheses.

    Key components of the proof view include:

    • Goals: An array of Goal objects (containing id, name, goal, and hypotheses).
    • Shelved/Given Up Goals: Separate lists for goals that have been shelved or given up.
    • Messages: A list of RocqMessage objects, which are pairs of MessageSeverity (error, warning, info) and a PpString message.
    • Cursor Movement: The server may send a MoveCursorNotification to inform the client to move the cursor, which is particularly used in Manual proof mode.

  5. Create an opam switch

    main

    In opam, a "switch" is an independent installation prefix containing its own compiler and pinned packages. This allows you to maintain multiple environments with different Coq versions. Create a new switch using the opam switch create command followed by a name of your choice.

    opam switch create <name>

  6. How VsRocq resolves `_CoqProject` files

    main

    VsRocq uses _CoqProject files to resolve Require Import statements and find .vo files.

    • Resolution Logic: Newer versions of VsRocq look for the _CoqProject file closest to the .v file being edited, allowing for multiple sub-projects in one workspace.
    • Compilation Requirement: VsRocq does not compile your project. You must manually compile your .v files (e.g., using make or dune build) so that the .vo files exist for the language server to find.
    • Updating Imports: If changes to .vo files aren't detected after a rebuild, use the "Developer: Reload Window" command. To reload new Require Import statements, you may need to "Reset" and then "Interpret to point".
    • Custom Arguments: You can pass -R or -Q arguments via the vsrocq.args setting.

  8. Understand the vsrocqtop Language Server implementation

    main
    The vsrocqtop module serves as a Rocq toplevel that initializes the Rocq environment and then enters a SEL (System Event Loop) loop specifically for the lsp event. This allows the language server to handle standard LSP (Language Server Protocol) requests alongside specialized VsRocq messages. The core logic for managing these events is implemented in the lspManager module.

  9. Run extension tests

    main

    To run the test suite:

    1. Open the Debug viewlet (Ctrl+Shift+D or Cmd+Shift+D on Mac).
    2. Select Extension Tests from the launch configuration dropdown.
    3. Press F5 to run the tests in a new window.
    4. Check the Debug Console for test results.

    Test File Requirements:

    • The test runner only executes files matching the pattern **.test.ts.
    • Place new test files inside the test/suite folder.
    # Select 'Extension Tests' in the debug dropdown and press F5

  10. Install the VsRocq language server

    main

    To use VsRocq, you must first install the language server. It is recommended to match the version of the vsrocq-language-server opam package with the version of the VsRocq extension installed in VS Code to avoid LSP initialization failures.

    Using opam

    After creating an opam switch and pinning Rocq, install the package:

    # For Coq 8.x, use coq / coq-core instead of rocq-core
$ opam pin add rocq-core 9.1.0
$ opam install vsrocq-language-server.2.3.4

    Using NixOS

    nix profile install nixpkgs#coq_8_18 nixpkgs#coqPackages_8_18.vscoq-language-server

    Pre-release versions

    To use a pre-release version via opam, pin the specific release tarball:

    $ opam pin add vsrocq-language-server.2.3.1 https://github.com/rocq-prover/vsrocq/releases/download/v2.3.1/vsrocq-language-server-2.3.1.tar.gz

    After installation, verify the path to the executable using:

    $ which vsrocqtop
    $ opam install vsrocq-language-server.2.3.4

  11. Build VsRocq using a local Rocq installation

    main

    To develop VsRocq alongside a modified local version of Rocq, follow these steps:

    1. Build your local Rocq (e.g., using make world).
    2. Clone the VsRocq repository into rocq/vsrocq/ (adjacent to your Rocq directory, e.g., kernel/).
    3. Run dune build vsrocq/language-server. The resulting binary vsrocqtop will typically be located in _build/install/default/bin/vsrocqtop next to your Rocq binaries.
    4. In VSCode user settings, set the absolute path to this binary using the vsrocq.path key: "vsrocq.path": "path/rocq/_build/install/default/bin/vsrocqtop".
    5. Reload VSCode.

    Note: Because vsrocqtop is linked to Rocq, you must rebuild it whenever you change Rocq sources for the changes to take effect.

    "vsrocq.path": "path/rocq/_build/install/default/bin/vsrocqtop"