### Build, Package, and Debug VsCoq VSCode Client

Source: https://github.com/rocq-prover/vsrocq/blob/main/docs/developers.md

These commands provide a comprehensive guide for developing the VsCoq VSCode client extension. They cover installing dependencies, building the extension and its web apps, compiling, packaging for distribution, installing locally, and launching development servers for debugging UI components.

```bash
yarn run install:all
yarn run build:all
yarn run compile
yarn run package
npm install -g @vscode/vsce
vsce package
code --install-extension vscoq-*.vsix
yarn run start:goal-view-ui
yarn run start:search-ui
yarn run build:goal-view-ui
yarn run build:search-ui
nix develop .#vscoq-client -c code .
```

--------------------------------

### Install Opam on Linux/macOS via curl script

Source: https://github.com/rocq-prover/vsrocq/blob/main/client/media/install.md

This command installs the Opam OCaml package manager on Unix-like systems. It downloads and executes an installation script from GitHub via curl. This is the quickest way to get Opam set up for Coq development.

```bash
bash -c "sh <(curl -fsSL https://raw.githubusercontent.com/ocaml/opam/master/shell/install.sh)"
```

--------------------------------

### Install Opam on Windows via PowerShell script

Source: https://github.com/rocq-prover/vsrocq/blob/main/client/media/install.md

This command installs the Opam OCaml package manager on Windows. It executes a remote PowerShell script to perform the installation. This method provides a quick setup for Windows users.

```powershell
Invoke-Expression "& { $(Invoke-RestMethod https://raw.githubusercontent.com/ocaml/opam/master/shell/install.ps1) }"
```

--------------------------------

### Install vscoq-language-server for VSCode Coq extension

Source: https://github.com/rocq-prover/vsrocq/blob/main/client/media/install.md

This command installs the `vscoq-language-server` package using Opam. This language server is essential for the VSCode Coq extension to provide features like syntax highlighting, error checking, and navigation. Run this within your active Opam switch.

```bash
opam install vscoq-language-server
```

--------------------------------

### Install Coq into the current Opam switch

Source: https://github.com/rocq-prover/vsrocq/blob/main/client/media/install.md

This command installs the latest stable version of Coq within the currently active Opam switch. It leverages Opam's package management capabilities to ensure proper dependency resolution. Ensure an Opam switch is created and active before running this command.

```bash
opam install coq
```

--------------------------------

### Install and Manage VsRocq Language Server with opam

Source: https://github.com/rocq-prover/vsrocq/blob/main/docs/FAQ.md

This snippet provides essential shell commands for installing, verifying, pinning specific pre-release versions, and updating the `vsrocq-language-server` using the opam package manager. It also includes commands for activating the opam environment and linking opam switches to project directories.

```Shell
opam install vsrocq-language-server
```

```Shell
which vsrocqtop
```

```Shell
opam pin add vscoq-language-server.2.1.5  https://github.com/coq/vscoq/releases/download/v2.1.5/vscoq-language-server-2.1.5.tar.gz
```

```Shell
eval $(opam env)
```

```Shell
opam update && opam upgrade vsrocq-language-server
```

```Shell
opam switch link <SWITCH_NAME> .
```

--------------------------------

### Build VsCoq Language Server with Nix

Source: https://github.com/rocq-prover/vsrocq/blob/main/docs/developers.md

This command utilizes Nix to set up a development environment and initiate the build process for the VsCoq language server. It navigates into the 'language-server' directory and executes 'dune build' to compile the OCaml project, assuming Nix is installed and configured.

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

--------------------------------

### Install VsCoq Language Server Pre-release via OPAM

Source: https://github.com/rocq-prover/vsrocq/blob/main/client/README.md

For pre-release versions of the VsCoq language server, this OPAM command allows direct installation from a specific release tarball URL. It pins the `vscoq-language-server` package to a particular version and its corresponding GitHub release.

```shell
$ opam pin add vscoq-language-server.2.1.5  https://github.com/coq/vscoq/releases/download/v2.1.5/vscoq-language-server-2.1.5.tar.gz
```

--------------------------------

### Verify VsCoq Language Server Installation Path

Source: https://github.com/rocq-prover/vsrocq/blob/main/README.md

Use the `which` command to find the installation path of the `vscoqtop` executable after the language server has been installed.

```shell
$ which vscoqtop
```

--------------------------------

### Install VsCoq Language Server on NixOS

Source: https://github.com/rocq-prover/vsrocq/blob/main/client/README.md

This command shows how to install the VsCoq language server and its required Coq version on NixOS using `nix profile install`. It directly fetches the necessary packages from `nixpkgs`.

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

--------------------------------

### Install VsCoq Language Server

Source: https://github.com/rocq-prover/vsrocq/blob/main/README.md

Commands to install the VsCoq language server using either the OPAM package manager or on NixOS. OPAM allows pinning a specific Coq version, while NixOS uses `nix profile install`.

```shell
$ opam pin add coq 8.18.0
$ opam install vscoq-language-server
```

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

--------------------------------

### Install VsCoq Language Server with OPAM

Source: https://github.com/rocq-prover/vsrocq/blob/main/client/README.md

This snippet demonstrates how to install the VsCoq language server using OPAM. It first pins a specific Coq version (8.18.0) to ensure compatibility, then installs the `vscoq-language-server` package.

```shell
$ opam pin add coq 8.18.0
$ opam install vscoq-language-server
```

--------------------------------

### VsCoq CI/CD Pipeline Overview

Source: https://github.com/rocq-prover/vsrocq/blob/main/docs/developers.md

Documentation for the automated and manual CI/CD workflows governing VsCoq releases and publishing to various platforms like opam and VSCode marketplaces.

```APIDOC
ci.yml:
  Description: Handles creating draft releases with a tarball archive when a tag is pushed.
  Job: create-release

cd.yml:
  Description: Automatically publishes the release to opam once the draft is released.
  Note: Requires filling out the changelog appropriately before hitting release.
  Pre-release behavior: If it is a pre-release, the pipeline will publish to `coq/opam` instead of `opam/opam-repository`.

publish-server.yml: (Manual Pipeline)
  Description: Allows manual publishing of a release on opam (e.g., if the automatic pipeline encounters issues).
  Parameters:
    - tag: The Git tag with the correct version semantics.
    - type: Specifies if it is a release or pre-release.

publish-extension.yml: (Manual Pipeline)
  Description: Handles publishing the extension on the VSCode marketplace as well as VSCodium.
  Note: This pipeline is always executed manually because the opam release process might take time. The extensions should only be published once the package is successfully on opam.
```

--------------------------------

### Install VsCoq Language Server Pre-release with OPAM

Source: https://github.com/rocq-prover/vsrocq/blob/main/README.md

Command to install a specific pre-release version of the VsCoq language server by pinning its git repository URL using the OPAM package manager.

```shell
$ opam pin add vscoq-language-server.2.1.5  https://github.com/coq/vscoq/releases/download/v2.1.5/vscoq-language-server-2.1.5.tar.gz
```

--------------------------------

### Create a new Opam switch for Coq development

Source: https://github.com/rocq-prover/vsrocq/blob/main/client/media/install.md

This command creates a new, isolated Opam switch. A switch is an independent environment with its own compiler and pinned packages, allowing seamless switching between different Coq versions and package sets. Replace 'name' with your desired switch identifier.

```bash
opam switch create name
```

--------------------------------

### Locate VsCoqtop Executable Path

Source: https://github.com/rocq-prover/vsrocq/blob/main/client/README.md

After installing the VsCoq language server, it's important to know the full path to the `vscoqtop` executable for extension configuration. This command uses `which` to display its location in the shell's PATH.

```shell
$ which vscoqtop
```

--------------------------------

### Coq Module Import and Type Checking Example

Source: https://github.com/rocq-prover/vsrocq/wiki/The-VsCoq-VsRocq-roadmap-2024-2025

Demonstrates a Coq example where the result of 'Check foo_rect' depends on the type of 'X' and the order of module imports. This illustrates a challenge for static analysis or prediction without full execution, as the meaning of a term can change based on context.

```coq
Definition X := hard to type term.

Module M. Inductive foo : Prop := Foo. End M.
Module N. Inductive foo : Prop := Foo (_:X). End M.
Import M. Import N.

Check foo_rect.
(* N.foo_rect if X : Prop or SProp, otherwise M.foo_rect *)
```

--------------------------------

### VsCoq Language Server Architecture Diagram

Source: https://github.com/rocq-prover/vsrocq/blob/main/docs/developers.md

This Mermaid diagram visually represents the architectural components of the VsCoq language server, illustrating the flow and interactions between key modules such as VsCoqtop, LSPManager, DocumentManager, ExecutionManager, DelegationManager, Queries, Document, and Scheduler.

```mermaid
stateDiagram-v2
        A: Vscoqtop
        B: LSPManager
        C: DocumentManager
        D: ExecutionManager
        note left of D: Coq Vernac
        E: DelegationManager
        F: Queries
        note right of F: Coq API
        G: Document
        note right of G: Coq parser
        H: Scheduler
        A --> B
        B --> C
        B --> D
        D --> E
        C --> F
        C --> G
        C --> H
```

--------------------------------

### Pin a specific Coq version in Opam

Source: https://github.com/rocq-prover/vsrocq/blob/main/client/media/install.md

This command pins a specific version of Coq (e.g., 8.18.0) within the current Opam switch. This is useful for maintaining compatibility with projects requiring a particular Coq release. Replace '8.18.0' with the exact version you need.

```bash
opam pin add coq 8.18.0
```

--------------------------------

### Push Git Tag to Origin

Source: https://github.com/rocq-prover/vsrocq/blob/main/docs/developers.md

This command pushes the newly created Git tag to the remote origin repository. Pushing the tag makes the release tag available to others and typically triggers associated CI/CD pipelines for release automation.

```shell
git push origin #VERSION_NUMBER
```

--------------------------------

### Create Signed Git Tag for Release

Source: https://github.com/rocq-prover/vsrocq/blob/main/docs/developers.md

This command creates a cryptographically signed Git tag for a new release, using the specified version number. This ensures the integrity and authenticity of the release tag, which is crucial for release verification.

```shell
git tag -s #VERSION_NUMBER
```

--------------------------------

### Run E2E Tests with Language Server Arguments

Source: https://github.com/rocq-prover/vsrocq/blob/main/docs/developers.md

This command executes end-to-end tests for the VsCoq client, passing custom arguments to the language server via the `VSCOQARGS` environment variable. This is useful for debugging or enabling verbose logging for the language server.

```shell
VSCOQARGS='-vscoq-d all' yarn test
```

--------------------------------

### LSP Custom Request/Notification: vscoq/updateProofView and MoveCursorNotification

Source: https://github.com/rocq-prover/vsrocq/blob/main/docs/protocol.md

Documents the custom LSP mechanisms for managing the Coq goal view and cursor synchronization in vscoq. This includes the `vscoq/updateProofView` request/notification for displaying detailed goal states and messages, and the `MoveCursorNotification` for guiding the client's cursor, particularly in manual proof mode.

```APIDOC
vscoq/updateProofView
  - Type: Request (client to server) and/or Notification (server to client)
  - Purpose: Updates the client's goal view with current Coq goals, hypotheses, shelved goals, given-up goals, and messages.
  - Response (ProofViewNotification):
    - proof: Nullable<ProofViewGoals> (Current goals, shelved goals, given up goals, see TypeScript 'ProofViewGoals' interface)
    - messages: CoqMessage[] (Messages to display in the goal panel, see TypeScript 'CoqMessage' type)
  - Details: Utilizes PpStrings for syntax-colored goal display.

MoveCursorNotification
  - Type: Notification (server to client)
  - Purpose: Informs the client to move the cursor to a specified range within a document.
  - Parameters (MoveCursorNotification):
    - uri: Uri (Document identifier)
    - range: Range (The target range for the cursor)
  - Usage: Sent after operations like 'stepForward' or 'stepBack' in manual mode to synchronize the client's cursor with the proof state.
```

--------------------------------

### VsRocq VS Code Extension Configuration Settings

Source: https://github.com/rocq-prover/vsrocq/blob/main/docs/FAQ.md

This section details key configuration settings for the VsRocq VS Code extension, primarily focusing on how to specify the path to the `vsrocqtop` executable and pass additional arguments. These settings are typically configured in VS Code's `settings.json` file.

```APIDOC
VS Code Settings:

vsrocq.path: string
  - Description: Explicit full path to the `vsrocqtop` executable.
  - Usage: "vsrocq.path": "/path/to/your/vsrocqtop"

vsrocq.args: string[]
  - Description: Array of arguments to pass directly to the `vsrocqtop` executable, useful for passing `-R` or `-Q` arguments.
  - Usage: "vsrocq.args": ["-R", "MyLib", "/path/to/MyLib"]
```

--------------------------------

### Configure VSCoq Coq Integration Settings

Source: https://github.com/rocq-prover/vsrocq/blob/main/client/README.md

This section details configuration options for integrating the VSCoq extension with Coq, including specifying the `vscoqtop` executable path, additional command-line arguments, and server communication tracing levels.

```APIDOC
"vscoq.path": string
  - Description: Specify the path to `vscoqtop` (e.g., `path/to/vscoq/bin/vscoqtop`).
"vscoq.args": string[]
  - Description: An array of strings specifying additional command line arguments for `vscoqtop` (typically accepts the same flags as `coqtop`).
"vscoq-language-server.trace.server": "off" | "messages" | "verbose"
  - Description: Toggles the tracing of communications between the server and client.
```

--------------------------------

### VsRocq and Rocq/Coq Interactive Commands

Source: https://github.com/rocq-prover/vsrocq/blob/main/docs/FAQ.md

A collection of commands available within the VsRocq VS Code extension and direct Rocq/Coq commands for interacting with proofs, querying definitions, and debugging. Output locations vary depending on the command type.

```APIDOC
VsRocq VS Code Commands:
  Rocq: Step Forward (Keyboard Shortcut: Alt+Down)
    // Description: Advances the proof state by one step.
  Rocq: Step Backward (Keyboard Shortcut: Alt+Up)
    // Description: Reverts the proof state by one step.
  Rocq: Interpret to Point
    // Description: Processes the current Rocq/Coq file up to the cursor's position.
  Rocq: Interpret to End
    // Description: Processes the entire current Rocq/Coq file.
  Rocq: Search selection
    // Description: Initiates a search operation using the currently selected text as the query.

Rocq/Coq Query Commands (Output to Query Panel or Goal Panel):
  Print <term>
    // Description: Displays detailed information about a specified term (e.g., definition, type).
    // Example: Print nat.
  Check <term>
    // Description: Verifies the type of a given term.
  Search <pattern>
    // Description: Finds theorems, definitions, or other entities matching the provided pattern.
  Locate <identifier>
    // Description: Pinpoints the location or definition of a specific identifier.
  About <term>
    // Description: Provides general descriptive information about a term.
  Time <command>
    // Description: Executes a command and reports the time taken for its execution.

Rocq/Coq Proof Display Commands:
  Show Proof.
    // Description: Displays the current proof term. Output appears in the Goal Panel and can be expanded.

Rocq/Coq Debugging Commands (Output to "Rocq Log" channel):
  Set Typeclasses Debug
    // Description: Activates debugging messages specifically for typeclass resolution.
  Feedback.msg_debug <message>
    // Description: Emits a custom debug message.
  debug auto
    // Description: Provides debugging output for the `auto` tactic. (Note: May appear in Goal Panel as "Notice" level).
  debug eauto
    // Description: Provides debugging output for the `eauto` tactic. (Note: Typically appears in "Rocq Log" as "Debug" level).
```

--------------------------------

### VsRocq VS Code Extension Configuration Settings

Source: https://github.com/rocq-prover/vsrocq/blob/main/docs/FAQ.md

These settings control various aspects of the VsRocq extension's behavior, including proof navigation mode, how messages are displayed in the goal panel, and the depth of proof term expansion.

```APIDOC
"vsrocq.proof.mode": <integer> (0 | 1)
  // Default: 0 (Manual Mode)
  // Description: Controls how VsRocq navigates proofs.
  //   - 0 (Manual Mode): Requires explicit commands (e.g., "Rocq: Step Forward").
  //   - 1 (Continuous Mode): VsRocq attempts to check the document as you scroll or edit up to the cursor.

"vsrocq.goals.messages.full": <boolean>
  // Default: true
  // Description: Determines if messages from commands like `Print` or `Check` are displayed directly in the Goal Panel.

"vsrocq.goals.maxDepth": <integer>
  // Default: 17
  // Description: Sets the maximum display depth for proof terms shown in the Goal Panel, particularly for `Show Proof.` output. Higher values expand `[...]` more.

"vsrocq.goals.display": <string> ("List" | "Tabs")
  // Default: "List" (implied by context)
  // Description: Configures how multiple goals are presented in the Goal Panel.
  //   - "List": Goals are listed vertically.
  //   - "Tabs": Goals are displayed in separate tabs.
```

--------------------------------

### VSCoq Coq Language Server Configuration

Source: https://github.com/rocq-prover/vsrocq/blob/main/README.md

These settings configure the integration of the VSCoq extension with the Coq language server. They allow specifying the path to the `vscoqtop` executable, passing additional command-line arguments, and controlling the verbosity of communication tracing between the client and server.

```APIDOC
"vscoq.path": ""
  - Specify the path to `vscoqtop` (e.g. `path/to/vscoq/bin/vscoqtop`)
"vscoq.args": []
  - An array of strings specifying additional command line arguments for `vscoqtop` (typically accepts the same flags as `coqtop`)
"vscoq-language-server.trace.server": off | messages | verbose
  - Toggles the tracing of communications between the server and client
```

--------------------------------

### Compile Coq Projects for VsRocq

Source: https://github.com/rocq-prover/vsrocq/blob/main/docs/FAQ.md

This snippet provides common shell commands used to compile Coq `.v` files into `.vo` files. VsRocq requires these compiled files for resolving `Require Import` statements, as it does not compile projects itself.

```Shell
make
```

```Shell
dune build
```

--------------------------------

### LSP Workspace Configuration Handling in vscoq

Source: https://github.com/rocq-prover/vsrocq/blob/main/docs/protocol.md

Documents how vscoq handles standard LSP `workspace/configuration` and `workspace/didChangeConfiguration` notifications to manage server settings. It outlines the purpose of these notifications and references the associated TypeScript data structures used for proof checking, goal view, completion, and diagnostics configurations.

```APIDOC
workspace/configuration
  - Purpose: Client requests configuration settings from the server.
  - Parameters:
    - items: ConfigurationItem[] (array of scopes and sections)
  - Returns: any[] (array of configuration values)

workspace/didChangeConfiguration
  - Purpose: Client notifies the server about changes in configuration settings.
  - Parameters:
    - settings: Configuration (the new configuration settings, see TypeScript 'Configuration' interface)
  - Details: The server processes these settings to adjust its behavior for proof checking, goal view, completion, and diagnostics.
```

--------------------------------

### VSCoq Code Completion Settings

Source: https://github.com/rocq-prover/vsrocq/blob/main/client/README.md

Configures experimental code completion features within the VSCoq extension, allowing control over enablement, algorithm selection, and unification limits.

```APIDOC
vscoq.completion.enable: bool
  - Description: Toggle code completion
  - Default: false

vscoq.completion.algorithm: StructuredSplitUnification | SplitTypeIntersection
  - Description: Specifies which completion algorithm to use

vscoq.completion.unificationLimit: int
  - Description: Sets the limit for how many theorems unification is attempted
```

--------------------------------

### VSCoq Goal and Info Panel Display Configuration

Source: https://github.com/rocq-prover/vsrocq/blob/main/README.md

These settings customize the appearance and behavior of the goal and info view panels within the VSCoq extension. They allow users to choose between tabbed or list displays for goals, toggle diff mode, include warnings/errors in the proof view, and set the maximum depth for goal ellipsis.

```APIDOC
"vscoq.goals.display": Tabs | List
  - Decide whether to display goals in separate tabs or as a list of collapsibles.
"vscoq.goals.diff.mode": on | off | removed
  - Toggles diff mode. If set to `removed`, only removed characters are shown (defaults to `off`)
"vscoq.goals.messages.full": bool
  - A toggle to include warnings and errors in the proof view (defaults to `false`)
"vscoq.goals.maxDepth": int
  - A setting to determine at which point the goal display starts elliding. Defaults to 17. (since version >= 2.1.7)
```

--------------------------------

### Configure VSCoq Proof Checking Behavior

Source: https://github.com/rocq-prover/vsrocq/blob/main/client/README.md

This section details configuration options for controlling proof checking behavior in VSCoq, such as checking mode, interpretation point, cursor stickiness, delegation strategies, worker allocation, error blocking, and display of navigation buttons.

```APIDOC
"vscoq.proof.mode": "Continuous" | "Manual"
  - Description: Decide whether documents should be checked continuously or using the classic navigation commands (defaults to `Manual`).
"vscoq.proof.pointInterpretationMode": "Cursor" | "NextCommand"
  - Description: Determines the point to which the proof should be checked when using the 'Interpret to point' command.
"vscoq.proof.cursor.sticky": boolean
  - Description: A toggle to specify whether the cursor should move as Coq interactively navigates a document (step forward, backward, etc.).
"vscoq.proof.delegation": "None" | "Skip" | "Delegate"
  - Description: Decides which delegation strategy should be used by the server. `Skip` allows to skip proofs which are out of focus and should be used in manual mode. `Delegate` allocates a settable amount of workers to delegate proofs.
"vscoq.proof.workers": int
  - Description: Determines how many workers should be used for proof checking.
"vscoq.proof.block": boolean
  - Description: Determines if the execution of a document should halt on the first error. Defaults to `true`. (Since version >= 2.1.7)
"vscoq.proof.display-buttons": boolean
  - Description: A toggle to control whether buttons related to Coq (step forward/back, reset, etc.) are displayed in the editor actions menu (defaults to `true`).
```

--------------------------------

### Configure VSCoq Goal and Info View Panel Display

Source: https://github.com/rocq-prover/vsrocq/blob/main/client/README.md

This section outlines settings for customizing the display of the goal and info view panels in VSCoq, including options for display mode (tabs or list), diff toggling, message inclusion, and goal ellipsis depth.

```APIDOC
"vscoq.goals.display": "Tabs" | "List"
  - Description: Decide whether to display goals in separate tabs or as a list of collapsibles.
"vscoq.goals.diff.mode": "on" | "off" | "removed"
  - Description: Toggles diff mode. If set to `removed`, only removed characters are shown (defaults to `off`).
"vscoq.goals.messages.full": boolean
  - Description: A toggle to include warnings and errors in the proof view (defaults to `false`).
"vscoq.goals.maxDepth": int
  - Description: A setting to determine at which point the goal display starts elliding. Defaults to 17. (Since version >= 2.1.7)
```

--------------------------------

### VSCoq Proof Checking Behavior Configuration

Source: https://github.com/rocq-prover/vsrocq/blob/main/README.md

These settings control various aspects of proof checking within the VSCoq extension. They allow users to select continuous or manual checking modes, define how the 'Interpret to point' command behaves, manage cursor movement during navigation, configure proof delegation strategies, set worker counts, enable/disable blocking on errors, and control the visibility of Coq navigation buttons.

```APIDOC
"vscoq.proof.mode": Continuous | Manual
  - Decide whether documents should checked continuously or using the classic navigation commmands (defaults to `Manual`)
"vscoq.proof.pointInterpretationMode": Cursor | NextCommand
  - Determines the point to which the proof should be check to when using the 'Interpret to point' command.
"vscoq.proof.cursor.sticky": bool
  - A toggle to specify whether the cursor should move as Coq interactively navigates a document (step forward, backward, etc...)
"vscoq.proof.delegation": None | Skip | Delegate
  - Decides which delegation strategy should be used by the server. `Skip` allows to skip proofs which are out of focus and should be used in manual mode. `Delegate` allocates a settable amount of workers to delegate proofs.
"vscoq.proof.workers": int
  - Determines how many workers should be used for proof checking
"vscoq.proof.block": bool
  - Determines if the the execution of a document should halt on first error. Defaults to true (since version >= 2.1.7).
"vscoq.proof.display-buttons": bool
  - A toggle to control whether buttons related to Coq (step forward/back, reset, etc.) are displayed in the editor actions menu (defaults to `true`)
```

--------------------------------

### Coq Language Server Synchronous Queries API

Source: https://github.com/rocq-prover/vsrocq/blob/main/docs/protocol.md

Documents the synchronous `vscoq/check`, `vscoq/about`, `vscoq/locate`, and `vscoq/print` queries. These requests return their responses directly without separate notification verbs, simplifying the interaction model.

```APIDOC
Coq Language Server Synchronous Queries
  - Description: A set of synchronous requests for immediate information retrieval about Coq elements. These queries return their responses directly without separate notification verbs.
  - Common Request Parameters:
    - textDocument: VersionedTextDocumentIdentifier - The URI and version of the document.
    - pattern: string - The pattern or identifier relevant to the query.
    - position: Position - The cursor's position in the document.

  vscoq/about (Synchronous Request)
    - Description: Retrieves information about a Coq element or the current Coq environment.
    - Request Signature: vscoq/about
    - Request Parameters: (See Common Request Parameters above)
    - Returns: PpString (AboutCoqResponse) - The textual information about the Coq element.

  vscoq/check (Synchronous Request)
    - Description: Checks the type, validity, or properties of a Coq expression or term.
    - Request Signature: vscoq/check
    - Request Parameters: (See Common Request Parameters above)
    - Returns: PpString (CheckCoqResponse) - The result of the check operation.

  vscoq/locate (Synchronous Request)
    - Description: Locates the definition or declaration of a Coq identifier.
    - Request Signature: vscoq/locate
    - Request Parameters: (See Common Request Parameters above)
    - Returns: PpString (LocateCoqResponse) - The location or definition details.

  vscoq/print (Synchronous Request)
    - Description: Prints the definition, value, or current state of a Coq element.
    - Request Signature: vscoq/print
    - Request Parameters: (See Common Request Parameters above)
    - Returns: PpString (PrintCoqResponse) - The printed representation.
```

--------------------------------

### TypeScript Interfaces for Synchronous Coq Queries

Source: https://github.com/rocq-prover/vsrocq/blob/main/docs/protocol.md

Defines the request and response types for synchronous Coq language server queries including `vscoq/about`, `vscoq/check`, `vscoq/locate`, and `vscoq/print`. Each request includes document, pattern, and position, with responses typically being a `PpString`.

```typescript
interface AboutCoqRequest {
    textDocument: VersionedTextDocumentIdentifier;
    pattern: string; 
    position: Position;
}

type AboutCoqResponse = PpString;

interface CheckCoqRequest {
    textDocument: VersionedTextDocumentIdentifier;
    pattern: string; 
    position: Position;
};

type CheckCoqResponse = PpString; 

interface LocateCoqRequest {
    textDocument: VersionedTextDocumentIdentifier;
    pattern: string; 
    position: Position;
};

type LocateCoqResponse = PpString; 

interface PrintCoqRequest {
    textDocument: VersionedTextDocumentIdentifier;
    pattern: string; 
    position: Position;
};

type PrintCoqResponse = PpString;
```

--------------------------------

### Coq Term Lifecycle Flowchart

Source: https://github.com/rocq-prover/vsrocq/wiki/The-VsCoq-VsRocq-roadmap-2024-2025

Illustrates the full lifecycle of a Coq term, from raw text input through parsing, globalization, type checking, and pretty printing, ending in a displayable DOM representation. This diagram highlights the distinct phases a term undergoes within the Coq system.

```mermaid
flowchart LR;
  subgraph synterp
    A[Raw Text] --parsing--> B[Expr];
  end
  subgraph interp
    B1[Expr] --globalisation--> C[Glob]
    C --type checking--> D[Constr]
  end
  subgraph pp
    D1[Contr] --pretty printing--> E[Pp]
    E --pp-display lib--> F[DOM]
  end
  synterp --> interp;
  interp --> pp;
```

--------------------------------

### VSCoq Code Completion Configuration

Source: https://github.com/rocq-prover/vsrocq/blob/main/README.md

Configuration options for controlling the experimental code completion feature in the VSCoq extension. These settings allow enabling/disabling the feature, selecting the underlying algorithm, and setting limits for unification attempts.

```APIDOC
"vscoq.completion.enable": bool
  - Toggle code completion (defaults to false)
"vscoq.completion.algorithm": StructuredSplitUnification | SplitTypeIntersection
  - Which completion algorithm to use
"vscoq.completion.unificationLimit": int
  - Sets the limit for how many theorems unification is attempted
```

--------------------------------

### Enable Detailed Diagnostics for VsRocq Language Server

Source: https://github.com/rocq-prover/vsrocq/blob/main/docs/FAQ.md

To diagnose frequent crashes or unexpected behavior of the VsRocq language server, you can enable detailed diagnostic output and backtraces. These arguments are added to the 'vsrocq.args' array in your VS Code 'settings.json' file, providing more verbose logging for troubleshooting.

```JSON
{
  "vsrocq.args": [
    "-vsrocq-d", "all", // Enable all diagnostic output
    "-bt" // Include backtraces in crash reports
  ]
}
```

--------------------------------

### LSP Configuration Interfaces for vscoq

Source: https://github.com/rocq-prover/vsrocq/blob/main/docs/protocol.md

Defines the TypeScript interfaces and enums used to structure configuration settings for the vscoq language server. These settings control proof checking delegation, worker count, proof checking mode, goal view display options (diff mode, messages), completion features (enablement, ranking algorithm, limits), and diagnostics behavior.

```typescript
enum DelegationMode {
    none: "None", 
    skip: "Skip",
    delegate: "Delegate"
}

enum Mode {
    Manual: 0, 
    Continuous
}

interface Proof {
    //Delegation mode 
    delegate: DelegationMode
    //Number of workers if relevant
    workers: number
    //Proof checking mode 
    mode: Mode
}

// Should we send errors and diagnostics to the message 
// panel of the goal view ?
interface Messages {
    full: boolean;
}

//diff mode
enum DiffMode {
    On: "on", 
    Off: "off",
    Removed: "removed" 
}

interface Diff {
    mode: DiffMode
}

//Config settings pertaining to the goal view
interface Goals {
    diff: Diff
    messages: Messages
}

enum RankingAlgorithm {
    SplitTypeIntersection = 0, 
    StructuredSplitUnification
}

interface Completion {
    enable: boolean
    algorithm: RankingAlgorithm
    unificationLimit: number
    sizeFactor: number
}

interface Diagnostics {
    enable: boolean
    full: boolean
}

interface Configuration {
    proof: Proof
    goals: Goals
    completion: Completion
    diagnostics: Diagnostics
}
```

--------------------------------

### Coq Language Server Asynchronous Search API (`vscoq/search`)

Source: https://github.com/rocq-prover/vsrocq/blob/main/docs/protocol.md

Documents the asynchronous `vscoq/search` request and `vscoq/searchResult` notification. The server first sends a handshake (OK or error), then streams individual results via `SearchCoqResult` notifications, identified by a unique UUID.

```APIDOC
vscoq/search (Asynchronous Request)
  - Description: Initiates an asynchronous search operation within Coq, returning results incrementally.
  - Request Signature: vscoq/search
  - Request Parameters (SearchCoqRequest):
    - id: string (UUID) - A unique identifier provided by the client for this search request.
    - textDocument: VersionedTextDocumentIdentifier - The URI and version of the document where the search is initiated.
    - pattern: string - The Coq search command pattern to be applied.
    - position: Position - The cursor's position in the document, used to infer the current Coq state.
  - Response Flow:
    1. Handshake (SearchCoqHandshake):
       - Description: The language server's initial response to acknowledge the search request.
       - Parameters:
         - id: string - The UUID provided in the initial request.
       - Status: Indicates success (OK) or an error.
    2. Result Notification (SearchCoqResult):
       - Description: Subsequent notifications sent one by one for each found search result.
       - Parameters:
         - id: string - The UUID of the search request this result belongs to.
         - name: PpString - The name of the relevant search result (e.g., theorem, lemma).
         - statement: PpString - The full statement or definition of the search result.
```

--------------------------------

### TypeScript Interfaces for Asynchronous Coq Search API

Source: https://github.com/rocq-prover/vsrocq/blob/main/docs/protocol.md

Defines the data structures for the asynchronous `vscoq/search` request, its handshake, and the subsequent `vscoq/searchResult` notifications. It includes fields for document identification, search pattern, cursor position, and result details.

```typescript
interface SearchCoqRequest {
    // This should be a uuid provided by the client
    id: string;
    // a document uri as given through the vscode api
    textDocument: VersionedTextDocumentIdentifier;
    // The pattern to use for the coq search command
    pattern: string; 
    // The position the cursor is in the document (this is to infer the current coq state)
    position: Position;
}

interface SearchCoqHandshake {
    //Returns the provided uuid
    id: string;
}

interface SearchCoqResult {
    //The uuid of the search associated to this result
    id: string;
    // The name of the relevant search result (theorem or lemma or etc... in coq)
    name: PpString; 
    // The statement of the relevant search result
    statement: PpString;
}
```

--------------------------------

### Configure VSCoq Memory Management Settings

Source: https://github.com/rocq-prover/vsrocq/blob/main/client/README.md

This section describes the memory management settings for the VSCoq extension, allowing users to define a memory limit over which document states are discarded to free up resources when a tab is closed. This feature is available since version 2.1.7.

```APIDOC
"vscoq.memory.limit": int
  - Description: Specifies the memory limit (in Gb) over which, when a user closes a tab, the corresponding document state is discarded in the server to free up memory. Defaults to 4Gb. (Since version >= 2.1.7)
```

--------------------------------

### LSP Goal View Interfaces and Types for vscoq

Source: https://github.com/rocq-prover/vsrocq/blob/main/docs/protocol.md

Defines the TypeScript interfaces and types essential for rendering the Coq goal view in vscoq. This includes structures for pretty-printed Coq strings (`PpString`), individual goals (`Goal`), aggregated goal states (`ProofViewGoals`), message handling (`MessageSeverity`, `CoqMessage`), the main proof view update notification (`ProofViewNotification`), and cursor movement notifications (`MoveCursorNotification`). These types facilitate rich display of Coq's internal state.

```typescript
type PpTag = string;

type BlockType =
  | ["Pp_hbox"]
  | ["Pp_vbox", number]
  | ["Pp_hvbox", number]
  | ["Pp_hovbox", number];

type PpString =
  | ["Ppcmd_empty"]
  | ["Ppcmd_string", string]
  | ["Ppcmd_glue", PpString[]]
  | ["Ppcmd_box", BlockType, PpString]
  | ["Ppcmd_tag", PpTag, PpString]
  | ["Ppcmd_print_break", number, number]
  | ["Ppcmd_force_newline"]
  | ["Ppcmd_comment", string[]];

//A coq goal and its corresponding hypotheses
interface Goal {
    id: number;
    goal: PpString;
    hypotheses: PpString[];
}

//We also display shelved and given up goals
interface ProofViewGoals {
    goals: Goal[];
    shelvedGoals: Goal[];
    givenUpGoals: Goal[];
}

//We display messages in the goal panel
enum MessageSeverity {
    error = "Error",
    warning = "Warning", 
    info = "Information"
}
type CoqMessage = [MessageSeverity, PpString];


// The proof view notification is sent from the server to the client
interface ProofViewNotification {
    proof: Nullable<ProofViewGoals>;
    messages: CoqMessage[];
}

// Sent from the server to the client after a stepForward or stepBack
interface MoveCursorNotification {
    uri: Uri; 
    range: Range; 
}
```

--------------------------------

### Configure VsRocq Memory Limit and Error Blocking

Source: https://github.com/rocq-prover/vsrocq/blob/main/docs/FAQ.md

These settings control the VsRocq language server's memory consumption and its behavior when encountering parsing errors. The 'vsrocq.memory.limit' setting (in MB) attempts to manage memory by discarding states of closed documents. 'vsrocq.proof.block' ensures the server halts execution on the first parsing error.

```JSON
{
  "vsrocq.memory.limit": 4096, // Default 4GB, attempts to free memory by discarding states
  "vsrocq.proof.block": true // Default since v2.1.7, ensures blocking on first parsing error
}
```

--------------------------------

### LSP Custom Notification Interface: vscoq/updateHighlights

Source: https://github.com/rocq-prover/vsrocq/blob/main/docs/protocol.md

Defines the TypeScript interface for the `vscoq/updateHighlights` custom LSP notification. This notification is sent from the server to the client to convey the ranges of code currently being processed or already processed by the Coq server, enabling UI updates like gutter highlights.

```typescript
interface UpdateHighlightsNotification {
    //Document idefinfier
    uri: Uri;
    // The ranges of lines of code currently being processed by the server
    processingRange: vscode.Range[];
    // The ranges of lines of code that have been processed by the server
    processedRange: vscode.Range[];
}
```

--------------------------------

### VSCoq Diagnostics Configuration

Source: https://github.com/rocq-prover/vsrocq/blob/main/README.md

Configuration option for controlling the verbosity of diagnostic output in the VSCoq extension, specifically for 'Info' level messages.

```APIDOC
"vscoq.diagnostics.full": bool
  - Toggles the printing of Info level diagnostics (defaults to false)
```

--------------------------------

### Coq Globalization and Type Checking Flow

Source: https://github.com/rocq-prover/vsrocq/wiki/The-VsCoq-VsRocq-roadmap-2024-2025

Details the transformation of a Coq term from an expression with location information (Expr) to a globalized term (Glob) and finally to a type-checked construct (Constr). This specific flow highlights the potential loss of precise location data during the type-checking phase.

```mermaid
flowchart LR;
    B1("(nat,loc)") --globalisation--> C("(Coq.Init.Datatypes.nat,loc)")
    C --type checking--> D("Coq.Init.Datatypes.nat")
```

--------------------------------

### LSP Custom Notification: vscoq/updateHighlights

Source: https://github.com/rocq-prover/vsrocq/blob/main/docs/protocol.md

Documents the custom `vscoq/updateHighlights` notification, a server-to-client message used by vscoq to communicate the processing status of code ranges. This enables the client to visually indicate which parts of the document are currently being processed or have been successfully processed by the Coq server.

```APIDOC
vscoq/updateHighlights
  - Type: Notification (server to client)
  - Purpose: Informs the client about the processing state of document ranges.
  - Parameters (UpdateHighlightsNotification):
    - uri: Uri (Document identifier)
    - processingRange: vscode.Range[] (Ranges of lines currently being processed by the server)
    - processedRange: vscode.Range[] (Ranges of lines that have been processed by the server)
  - Usage: By default, processed lines are displayed in the VSCode gutter.
```

--------------------------------

### VSCoq Memory Management Configuration

Source: https://github.com/rocq-prover/vsrocq/blob/main/README.md

This setting controls the memory usage of the VSCoq server. It defines a memory limit (in Gigabytes) beyond which the server will discard the state of corresponding documents when their tabs are closed, helping to free up system memory.

```APIDOC
"vscoq.memory.limit: int
  - Specifies the memory limit (in Gb) over which when a user closes a tab, the corresponding document state is discarded in the server to free up memory. Defaults to 4Gb.
```

--------------------------------

### VSCoq Diagnostics Settings

Source: https://github.com/rocq-prover/vsrocq/blob/main/client/README.md

Controls the verbosity of diagnostic output for the VSCoq extension, specifically for 'Info' level messages.

```APIDOC
vscoq.diagnostics.full: bool
  - Description: Toggles the printing of 'Info' level diagnostics
  - Default: false
```

=== COMPLETE CONTENT === This response contains all available snippets from this library. No additional content exists. Do not make further requests.