rocq-mcp

An MCP server for Rocq (formerly Coq) proof development. It exposes compilation, verification, querying, and interactive tactic stepping as MCP tools, so that LLM agents can write and check Rocq proofs.

• Thirteen MCP tools backed by pet (Rocq’s coq-lsp interactive backend).
• Interactive tools. Inspect proof goals, search the environment, step through tactics.
• Staged verification. Sandboxed audit of admits, axioms, and statement mismatches.
• State is cached across calls for fast iteration.

A note on this README. The sections that follow are detailed reference documentation aimed primarily at AI agents consuming these tools (and the human operators briefing them).

Prerequisites

• Rocq / Coq – coqc must be on your PATH. If the workspace contains a _RocqProject or _CoqProject file, the server parses it for load-path flags (-Q, -R, -I). For dune projects (no _CoqProject but a dune-project file present), the server auto-detects load paths via dune coq top — or dune rocq top for modern (using rocq ...) projects — once per (coq.theory ...) / (rocq.theory ...) stanza, so multi-theory workspaces resolve cross-theory imports correctly, and writes a _RocqProject file in the workspace so that coq-lsp also picks them up. This generated file stays in the workspace and should be added to .gitignore. Otherwise it defaults to -Q Test.
• pet (from coq-lsp) – recommended. Powers the interactive tools (rocq_query, rocq_assumptions, rocq_start, rocq_check, rocq_step_multi, rocq_toc, rocq_notations) and the proof-state enrichment / multi-error walker on rocq_compile_file. Without pet you fall back to coqc-only operation: rocq_compile, rocq_compile_file (first error only, no goals), rocq_verify, rocq_diag — a substantial reduction in what an agent can do.
• Python 3.11+

Installation

Using uv:

# Install (includes pytanque for interactive tools)
uv pip install -e .

For development (includes pytest):

uv pip install -e ".[dev]"

Tools

The server exposes thirteen MCP tools:

Compilation tools (coqc-based, no pytanque needed)

Interactive tools (pytanque-based, require pet)

Diagnostic tools

Switch selection: The server resolves coqc and pet from the PATH / opam environment of the process Claude Code (or your MCP client) launched — not from your interactive shell. So the switch is fixed at server-launch time and can silently differ from opam switch show in your terminal. Pin it explicitly in the MCP client config, e.g. register the server command as opam exec --switch= -- uv run --directory rocq-mcp, or set env: { … } (PATH / OPAM_SWITCH_PREFIX). Call rocq_health to see the switch the server is actually on. To change it: either edit the launch command and reconnect the MCP server (/mcp → reconnect, or restart the client), or call rocq_switch(name=…) to swap in-session — the latter clears all live state_ids and may leave .vo artifacts ABI-incompatible, so prefer the launch-time pin for a stable setup.

Stale file warning: Interactive sessions (rocq_start / rocq_check / rocq_step_multi) read the .v file at session start and do not track subsequent edits. If another process or agent modifies the file while a session is active, the proof state becomes stale and tactics may fail or produce wrong results. In multi-agent setups, work on a copy of the file for interactive proving, or restart the session with rocq_start after edits. A stale_warning field is returned when a file modification is detected. A held state_id also freezes its loaded dependency .vos: if another caller rebuilds one through the server (e.g. rocq_compile_file), the session’s stale_warning fires too — proof_finished can then diverge from a clean compile, so re-verify with rocq_compile_file before trusting it. (Rebuilds from outside the server — e.g. a terminal dune build — are not observed.) See also the Concurrency model section below.

Workspace auto-detection: When a file-accepting tool (rocq_compile_file, rocq_query, rocq_assumptions, rocq_toc, rocq_start) is called without an explicit workspace, the server walks up from the file’s directory looking for _RocqProject, _CoqProject, or dune-project markers and uses the directory of the innermost match. Falls back to ROCQ_WORKSPACE if no marker is found. Pass workspace= explicitly to override (e.g. for monorepos with nested project files).

Workspace warning: When the resolved workspace contains no _RocqProject / _CoqProject / dune-project marker AND the call provided explicit workspace= or a file= hint, the response carries workspace_warning: str advising on the load-path resolution. Source-string tools without workspace= / file= (the legitimate scratch / one-off workflow) stay quiet.

.vo rebuild warning: When rocq_compile_file rewrites .vo artifacts in a workspace that has one or more active interactive sessions (rocq_start / rocq_check / rocq_step_multi), the response carries vo_rebuild_warning: str advising the other agents to call rocq_start again to refresh held dependency state. Quiet when no .vo changed, when no interactive session lives in this workspace, or when the workspace exceeds the internal scan cap. Calling rocq_compile_file with keep_vo=True makes the .vo persist between calls, so subsequent compiles of the same file are more likely to trip this warning.

Multi-error reporting: When rocq_compile_file fails (reason: "compile_error") and pet is available, the response carries errors: list[dict] with per-declaration entries (proof_name, kind, start_line, end_line, code, message) covering errors in named declarations and top-level vernaculars (broken Require, broken Notation, etc.) reached via inter-chunk regions. This surfaces additional errors beyond the first one coqc reports; cascade failures within a single proof body are deduplicated. The walk stops at the first top-level / inter-chunk error (a broken Require/Import/Notation): such a failure poisons the environment for every later declaration, so continuing would emit a flood of downstream “reference/library not found” entries that bury the real cause (coqc’s own first error is still in error_positions). A failed named declaration (Definition/Fixpoint/proof) is its own chunk and does not stop the walk. Collection stops at ROCQ_COMPILE_MULTI_ERROR_CAP (default 20; set to 0 to disable). The field can be present and empty (errors: []) when the walker ran but pet did not reproduce the coqc-reported failure — treat it as “no additional errors found” rather than “no errors at all.” Quiet on successful compiles, when pet is unavailable, and on source-string rocq_compile (this feature is rocq_compile_file only).

Compile-file options: rocq_compile_file accepts three opt-in tuning kwargs. All default off — pure additions, no behavior change to the baseline call.

• keep_vo=True preserves the produced .vo/.vok/.vos artifacts. Useful when a sibling file Requires the result; the default behavior is to clean every artifact except the source .v. Combining keep_vo=True with mode="vos" produces only a .vos — downstream full-mode Require Import will then fail with "Unable to locate library ... (.vos file)". Use keep_vo=True with mode="full" when the sibling consumer expects a .vo. In a dune project this flag is a no-op — see the dune callout below.

Dune projects — artifacts go to _build: When the file lives in a dune project (a dune-project ancestor exists), rocq_compile_file keeps the compiled .vo/.vos out of the source tree: full-mode in-stanza files build via dune build (artifacts under _build/default/…), and everything else (scratch files, mode="vos", timing=True) compiles with coqc -o-redirected into the same _build/default path. This prevents a source-tree .vo from shadowing dune’s pre-built copy. In this mode keep_vo has no effect (the .vo always persists in _build, where sibling Requires resolve it via the dune load path). If dune build cannot build a file because it is not part of a stanza, the response carries a dune_build_warning noting that coqc was used instead. Set ROCQ_DUNE_BUILD=0 to force the legacy coqc-into-source-tree behavior.

• mode="vos" selects a fast statements-only pre-pass (coqc -vos). Skips proof bodies entirely — does NOT execute them — so it catches missing imports, statement type errors, holes, and notation conflicts in seconds, but accepts any proof body (Theorem t : False. Proof. exact I. Qed. passes under "vos"). Use as a cheap pre-pass during iteration, then run mode="full" for the real check.
• timing=True runs coqc with -time and adds a timing: {total_sentences, top_slowest, last_completed} response field carrying per-sentence diagnostics; top_slowest is capped at 5 by descending duration. On timeout, last_completed is woven into the error string: "timed out after 590s. Last completed sentence: line 221 [Theorem.foo] (15.3s)". On a successful compile, last_completed is the file’s literal final sentence (not a failure marker).

Proof-tactics chain status: When a rocq_check call finishes a proof (proof_finished: True), the server walks the LRU state table backward from the leaf to reconstruct proof_tactics. If an ancestor state was LRU-evicted, or (defensively) a cycle is detected, the walk cannot complete; the response then omits proof_tactics and proof_hint and carries proof_tactics_status ("ancestor_evicted" or "cycle"), proof_tactics_broken_at: int (the state id where the walk gave up), and a short proof_tactics_hint instead. Clients that ignore these keys see no half-chain — they never render a partial walk as a finished proof.

Per-call timeout clamp: When any pet-routed tool (rocq_query, rocq_start, rocq_step_multi, rocq_check, rocq_assumptions, rocq_toc, rocq_notations) is invoked with timeout= exceeding ROCQ_QUERY_TIMEOUT_CAP (default 300), the call runs with the cap as the actual budget and the response carries clamped_timeout: . The timeout= parameter is the user’s request; clamped_timeout is the server-side ceiling.

Choosing a tool

The tools table above is reference-style. This subsection is intent → tool: find the row that matches what you want to do, then read its tool’s full entry above for details.

Recommended usage patterns

Multi-tactic exploration: rocq_check then rocq_step_multi

To explore N alternative tactics from a known good state, advance the state with rocq_check first, then branch with rocq_step_multi:

# Step 1: confirm the prefix and advance.
result = rocq_check(from_state=S, body="intros n m H.")
new_state = result["state_id"]

# Step 2: try alternatives from that state.
rocq_step_multi(from_state=new_state, tactics=[
    "by ring.",
    "by lia.",
    "by reflexivity.",
])

This is more efficient than passing the prefix repeatedly inside tactics=[...] (each tactic would re-run the prefix). It also makes the agent’s intent — “I’m confident in the prefix; explore the next step” — explicit.

Imports and scopes in rocq_query

Statements like Require Import, From X Require Y, Open Scope, Set, Unset, Local, and Section must go in the preamble= parameter (a multi-line string), not in body=:

rocq_query(
    preamble="From Coq Require Import Reals.\nOpen Scope R_scope.",
    command="Search (_ + _).",
)

Why: each statement in body= runs in isolation, so Open Scope in body would not propagate to the next statement. For multi-import preambles, prefer file= to a .v file containing the imports — more reliable when the imports include Set / Unset directives that may need a specific ordering.

For mid-proof queries — e.g. Search against the live proof state — use from_state= instead of preamble; the live state already has all imports and scopes set up.

Failure envelope and reason taxonomy

Every failure response carries {success: False, error: str, reason: str} so an agent can dispatch on reason without parsing message text. The same reason is recorded into the recent_errors ring buffer that rocq_diag returns. Values:

• Validation / lookup (set by tools before reaching pet): "validation", "not_found" (typo on rocq_start / rocq_assumptions).
• Pet-side (set by _run_with_pet on subprocess-level failures): "timeout", "crashed", "memory_exhausted", "lock_contended", "unavailable". When pet had to be killed, the response also carries pet_restarted: True.
• rocq_check mid-batch: "tactic_failed" (Coq rejected the tactic — distinct from a transport-level "crashed").
• rocq_compile / rocq_compile_file: "compile_error" (coqc returned non-zero).
• rocq_verify-specific: "compile_error", "axiom_dependency" (proof relies on Admitted/admit/custom axiom), "type_mismatch" (Phase 3 found the proof’s type differs from the problem’s type).

When a tool returns pet_restarted: True, call rocq_diag for memory headroom and recent-error history.

Concurrency model

Background (both audiences): rocq-mcp is single-tenant per process. All agent-facing state — the live state_id table, the import cache, the active workspace, and the single pet subprocess — is process-global. Two correctness floors keep concurrent sessions from clobbering each other:

• LRU-protected state table. A state_id you keep querying via from_state will not be evicted by a peer caller churning through new states (see ROCQ_MAX_STATES).
• No implicit current state. rocq_check and rocq_step_multi require from_state explicitly — there is no global “last touched” state a peer could re-point under you.

The remaining cross-agent costs are pure latency: workspace-swap thrash when peers are on different workspaces, pet RAM growth from accumulated Fleche cache, and the rare case of a peer calling force_restart=True (which kills pet under everyone). A second process-global mutator is rocq_switch, which moves the whole server to a different opam switch — killing pet and clearing the state table for everyone, and potentially invalidating in-flight .vo artifacts. It is a deliberate operator action rather than incidental contention, but in a shared session check rocq_diag’s live_states for peer entries before calling it (see the Switch selection callout).

Agent-side recovery: rocq_start(..., force_restart=True). When a state_id you actively depend on goes missing despite the LRU floor — typically because a peer just force-restarted pet — rocq_start with force_restart=True is the recovery. This kills pet, clears the state table, respawns a fresh pet, and returns a new state_id. Note that “fresh” is point-in-time: a different concurrent caller can force_restart again right after, so this is recovery, not enforced isolation. For non-contention triggers (RAM bloat, indexing corruption) the same call applies.

Orchestrator-side monitoring: rocq_diag. When you cannot deploy a separate rocq-mcp per sub-agent (see the Claude Code escape hatch below for one workaround), rocq_diag is the natural primitive for spotting cross-agent interference. Useful checks between sub-agent dispatches: live_states[*].file shows entries created by peer callers (sharing signal when agents are on disjoint files); memory.pet_rss_mb against max_rss_mb_threshold catches accumulated Fleche bloat before it forces a restart; recent_errors shows whether a peer just hit lock_contended / memory_exhausted / a force_restart; load_average["1m"] against the host CPU count distinguishes CPU saturation from a diverging tactic when a timeout fires (None on platforms without os.getloadavg). Field reports suggest this tool is consistently underused — worth a checklist line in your orchestrator prompt.

Operator-side hardening: the cleanest deployment is one rocq-mcp subprocess per concurrent agent. Over stdio this happens naturally when each MCP client launches its own server; the case that needs care is parallel sub-agents within one client, which inherit the parent’s MCP connections and share one rocq-mcp. If you’re orchestrating parallel Rocq work, prefer separate top-level invocations over one parent with concurrent sub-agents — or, within one client, the named-pool pattern below.

Claude Code sub-agent scoping — and its limit. Sub-agents in .claude/agents/.md accept an inline mcpServers entry in their frontmatter (Claude Code docs). An inline definition scopes a rocq-mcp server to that sub-agent — connected when the sub-agent starts, torn down when it finishes, and hidden from the main thread; a bare string reference shares the parent’s connection instead.

This scopes the server to the definition, not to each instance. Claude Code keys MCP servers by name — one server process per distinct name per session, shared by every sub-agent instance that references that name. So N concurrently-running instances of the same sub-agent definition still share one rocq-mcp pet: the inline entry isolates a sub-agent’s server from the parent’s, not one instance from another. (Name it something unique, too — an inline server literally named rocq-mcp collides with a session-level rocq-mcp server and is silently aliased to it.)

mcpServers:
  - rocqprover:            # a UNIQUE name — not "rocq-mcp"
      type: stdio
      command: rocq-mcp

Isolating concurrent instances — the named pool. Because the only isolation unit the harness exposes is the server name, give parallel work a pool of N sub-agent definitions, each with a distinct name — rocq-prover-1.md … rocq-prover-N.md, declaring servers rocqprover1 … rocqproverN. The harness then spawns N separate rocq-mcp processes, and the orchestrator hands distinct pool members to concurrently-running slots (round-robin the sub-agent type, capping concurrency at N). The pool is additive — keep a plain rocq-mcp reference for sequential/shared runs — and size N to your parallelism budget (pets are RAM-heavy; pair with ROCQ_MAX_PET_RSS_MB).

# .claude/agents/rocq-prover-1.md  (repeat for -2 … -N, bumping the number)
mcpServers:
  - rocqprover1:
      type: stdio
      command: rocq-mcp
      env:
        ROCQ_MAX_PET_RSS_MB: "8000"

Two caveats. Registration happens at startup — Claude Code snapshots the agent registry when the session begins, so newly-added rocq-prover-*.md files are not selectable until you restart the client (claude --continue keeps the conversation). And plugin sub-agents ignore mcpServers — sub-agents provided by a plugin silently drop the mcpServers / hooks / permissionMode frontmatter, so the pool must live in plain .claude/agents/ files.

Server-side multi-tenancy is not an alternative here: over stdio the harness gives one server process a single connection carrying interleaved calls with no per-caller identity, so rocq-mcp cannot tell sub-agents apart from inside one process. The name-keyed pool (or separate top-level claude invocations) is the only reliable isolation lever.

Worktree per pool member. A pool member isolates its own pet subprocess; for filesystem isolation — so concurrent sub-agents can edit .v files without staling each other’s interactive sessions (see Stale file warning above) — pair each member’s mcpServers entry with a separate git worktree, and point ROCQ_WORKSPACE at it:

mcpServers:
  - rocqprover1:
      type: stdio
      command: rocq-mcp
      env:
        ROCQ_WORKSPACE: /path/to/worktree-1

Each worktree carries its own checkout, its own auto-generated _RocqProject (see Prerequisites), and its own scratch files — neither sub-agent can clobber the other’s interactive sessions through a file edit, and _RocqProject regeneration in one worktree does not invalidate the other’s load paths.

Per-call timeout override. Pytanque-based tools (those routed through _run_with_pet: rocq_query, rocq_start, rocq_step_multi, rocq_check, rocq_assumptions, rocq_toc, rocq_notations) accept a timeout= kwarg that overrides ROCQ_PET_TIMEOUT for that one call (clamped to ROCQ_QUERY_TIMEOUT_CAP). On a timeout, prefer bumping timeout= per-call rather than raising the global default.

Briefing sub-agents

When spawning a sub-agent that will write or check Rocq/Coq proofs, prefix its task prompt with this preamble. Without it, sub-agents fall into a Write → coqc /tmp/.v → bash grep error loop that re-pays the import cost on every iteration; with it, they use the held-pet primitives and keep heavy imports (e.g. mathcomp, stdpp) warm across attempts.

Before any Write or `coqc` on a .v file:
  1. Consult any project-specific Rocq guidance first (e.g. a project
     CLAUDE.md, AGENTS.md, or Skill if your environment has one).
  2. For scratch iteration on a single proof, use rocq-mcp:
       rocq_start file=/tmp/.v theorem=
       rocq_step_multi tactics=[...]   (NOT  coqc /tmp/.v)
  3. Use `coqc` only for: full-project rebuilds, axiom audits via
     `Print Assumptions`, and final compile verification.

Environment Variables

Security Model

The verification tool (rocq_verify) uses defense in depth with three verification phases and multiple security layers.

Verification phases

rocq_verify tries up to three phases in sequence, falling back to the next if the previous one times out:

1. Phase 1 – Module M sandbox. The proof is wrapped inside Module M. ... End M.. The theorem is re-stated outside and proved via exact M.. This is the strongest sandbox but can time out on compute-heavy proofs.

2. Phase 2 – Shared-defs template. For problems with Inductive/Record/Definition types, type definitions are placed outside Module M to avoid nominal typing mismatches, while the proof stays inside the sandbox. Uses pytanque’s toc to extract problem structure. Falls back from Phase 1 when type incompatibilities are detected.

3. Phase 3 – Direct verification. When Phase 1 or Phase 2 times out or fails, the proof is compiled standalone (no Module M) with the full original timeout budget. Correctness is verified by comparing Check . output against the problem statement’s expected type after normalization. Additional security checks compensate for the lack of a sandbox (see below). This phase handles compute-heavy proofs that are too slow under Module M wrapping.

Layer 1: Module M sandbox (Phases 1 & 2)

The Module M sandbox prevents:

• Type redefinition cheating – Inductive/Record types are generative in Rocq, so redefining nat as bool inside Module M creates an incompatible type that cannot unify with the real nat outside.
• Axiom spoofing – User-declared axioms receive an M. prefix in Print Assumptions output, which the stdlib whitelist rejects.
• Admitted/Abort usage – Caught by Print Assumptions.
• Module escape – End M. and Reset/Back/Undo are forbidden commands (see Layer 2).

Layer 2: Forbidden command scanning

Source code is scanned for dangerous commands after stripping comments. The comment scanner matches Rocq’s lexer exactly, including string literal tracking inside comments (preventing desynchronization attacks like (* " (* " *) End M.). Comments are replaced with spaces to preserve word boundaries.

Forbidden commands:

Layer 3: Print Assumptions axiom whitelist

After compilation, Print Assumptions is checked against a whitelist of standard library axioms (classical logic, functional extensionality, Reals axioms, primitive int/float/array/string operations, mathcomp.classical re-exports, etc.). Axioms with qualified names must have a recognized stdlib prefix (Coq.*, Rocq.*, Stdlib.*, Corelib.*, the full mathcomp.classical.boolp.* / mathcomp.classical.classical_sets.*, or known module prefixes like ClassicalDedekindReals.*). Bare module-name prefixes (e.g. a workspace-supplied boolp.v) are intentionally not trusted, so a user Axiom EM : False. cannot be auto-trusted just because it mimics mathcomp’s short form. The M. prefix on user-declared axioms inside Phase 1 / 2 Module M sandboxing ensures they are always rejected.

Printing flags (Set Printing All, Set Printing Universes, Set Printing Width) are reset after End M. to prevent corruption of Print Assumptions output format.

Phase 3 security checks

Without the Module M sandbox, Phase 3 applies additional checks to compensate:

• Forbidden commands – Same scanning as Phases 1 & 2 (Layer 2).
• Incomplete proof rejection – Admitted, admit, and give_up in the proof source are rejected outright.
• Axiom-introducing commands blocked – Axiom, Parameter, and Conjecture declarations are rejected. (Variable and Hypothesis are allowed since they are section-local and become parameters after End Section, not global axioms.)
• Print Assumptions check – Same axiom whitelist as Phases 1 & 2 (Layer 3). However, without the M. prefix from Module M, user-declared axioms could potentially spoof whitelisted names.
• Type comparison – The proven type (via Check @. with Set Printing All) is normalized and compared to the expected type from the problem statement. Universe annotations are stripped before comparison.

Known limitations of Phase 3:

• Without Module M, type redefinition attacks are not caught (e.g., redefining nat as bool then proving a trivially true statement).
• Notation/scope redefinition before identically-texted definitions can change kernel semantics without being detected by type comparison.
• Stdlib function shadowing (redefining functions called by the problem’s definition) is not covered.

The verification_method field in the result indicates which phase was used ("module_m", "shared_defs", or "direct").

Trusted anchor

Important: The problem_statement parameter is treated as a trusted anchor. The server verifies that the proof proves the given statement, but does NOT verify that the statement itself is the correct problem. Callers must ensure problem_statement comes from a trusted source (e.g., a file on disk), not from the LLM being evaluated.

Path validation

All tools that accept file paths validate that resolved paths stay within the configured workspace directory (preventing path traversal attacks).

Project file security

When _RocqProject or _CoqProject is present, the server parses it for coqc load-path flags (-Q, -R, -I). For dune projects (no project file but a dune-project file exists), the server runs dune coq top (legacy (coq.theory ...) stanzas) or dune rocq top (modern (using rocq ...) / (rocq.theory ...) stanzas) once per theory stanza in the workspace and unions the resulting flags into a generated _RocqProject so coq-lsp also picks them up. Querying every theory is required for multi-theory workspaces; querying just one would leave cross-theory imports broken. This generated file (marked with a # Auto-generated by rocq-mcp from dune header) stays in the workspace and should be added to .gitignore. Existing user-created project files are never overwritten. For safety:

• -arg allowlist – Only known-safe flags are passed through (e.g., -noinit, -w, -impredicative-set). Dangerous flags like -load-vernac-source are silently dropped.
• Path containment – For _RocqProject/_CoqProject, directories in -Q/-R/-I must resolve within the workspace. Absolute paths and ../ traversals outside the workspace are rejected. For dune-detected paths, containment is checked against the dune project root (the directory containing dune-project), since build artifacts typically live in _build/ at the project root.

Running

The server uses stdio transport:

rocq-mcp

MCP client configuration

Add to your MCP client configuration (e.g., Claude Desktop, Claude Code):

{
  "mcpServers": {
    "rocq-mcp": {
      "command": "rocq-mcp",
      "env": {
        "ROCQ_WORKSPACE": "/path/to/your/rocq/project"
      }
    }
  }
}

Running Tests

uv run pytest

Tests for pytanque-based tools (rocq_query, rocq_assumptions, rocq_start, rocq_check, rocq_step_multi, rocq_toc, rocq_notations) require pet to be installed. Integration tests will be skipped automatically if it is not available.

Project Structure

src/rocq_mcp/
  __init__.py            Package init
  server.py              MCP server, 13 @mcp.tool wrappers, pet subprocess management
  compile.py             coqc-based tools: compile, compile_file, verify
  compile_enrichment.py  Compile-error-state orchestration (PET state capture)
  diag.py                rocq_diag snapshot builder (pet uptime, memory, recent errors)
  health.py              rocq_health / rocq_switch backing: opam-switch detection, toolchain probe
  interactive.py         pytanque-based tools: start, check, step_multi, query, assumptions, toc, notations
  verify.py              Rocq lexer scanner, Module M. verification, Print Assumptions parsing
tests/
  conftest.py           Shared fixtures
  test_compile.py       Tests for rocq_compile
  test_compile_file.py  Tests for rocq_compile_file
  test_verify.py        Tests for rocq_verify
  test_assumptions.py   Tests for rocq_assumptions
  test_auto_solve.py    Tests for sentence utilities and step_multi auto-solving
  test_server.py        Tests for server helpers (_format_error, _parse_project_flags, etc.)
  test_format_error.py  Tests for error formatting
  test_query.py         Tests for rocq_query (requires pet)
  test_start.py         Tests for rocq_start (requires pet)
  test_check.py         Tests for rocq_check (requires pet)
  test_step_multi.py    Tests for rocq_step_multi
  test_toc.py           Tests for rocq_toc
  test_notations.py     Tests for rocq_notations
  test_health.py        Tests for rocq_health / rocq_switch + switch detection
  test_timeout.py       Tests for timeout handling
  test_integration.py   Integration tests

License

Apache 2.0 – see LICENSE for details.