Explore Rocq/Coq proof developments as an interactive dependency graph, directly inside VS Code. Rocql parses your .v files, builds a graph of definitions, lemmas, theorems and their references, and renders it in a live, physics-driven canvas next to the editor.

No Python, no server, no external database to run. The graph engine (frogql) ships with the extension as a native module.

Features

Dependency graph of your project. Every top-level entry (Definition, Lemma, Theorem, Fixpoint, Inductive, Record, Instance, ...) becomes a node; every reference in a statement or proof becomes an edge. Inductive constructors and record fields are nested under their parent.
Go to definition (Cmd/Ctrl+Click). Jump from any identifier to where it is defined, resolved through module scopes, aliases and cross-file Require Import.
Find references. List every entry that depends on the symbol under the cursor.
Show in graph (Cmd+K G) / isolate (Cmd+K I). Focus the node for the symbol at the cursor, optionally filtering the canvas to just its neighborhood.
Cursor scope. Narrow the canvas to only what is defined up to the cursor line, so the graph tracks where you are reading.
Admit tracking. Entries closed with Admitted. or containing an admit. tactic are outlined in red, and presets surface them and their dependents.
Auto-graph on save. Toggle it on and the graph rebuilds automatically every time you save a .v file.
GQL queries. The visible graph is driven by a GQL path-pattern query. Presets are built in, and you can type your own to slice the graph.

Getting started

Open a folder containing Rocq/Coq .v files.
Run Rocql: Build graph (textual, fast) from the Command Palette (Cmd/Ctrl+Shift+P).
Run Rocql: Open graph panel to see the graph, or Cmd+K G on any identifier to jump straight to its node.

The textual build needs nothing beyond the .v sources. It works even when the project does not compile.

Commands

Command	Shortcut	What it does
Rocql: Open graph panel		Opens / reveals the graph webview
Rocql: Build graph (textual, fast)		Parses `.v` files (no compiler needed)
Rocql: Build graph (full, with dpdgraph)		Textual + kernel-resolved references
Rocql: Show in graph	Cmd+K G	Focus the node for the symbol under the cursor
Rocql: Show in graph and isolate	Cmd+K I	Focus + filter to its neighborhood
Rocql: Find references		List incoming references
Rocql: Go to definition		Jump to the definition of the symbol
Rocql: Toggle cursor scope		Show only what is defined up to the cursor
Rocql: Toggle auto-graph		Rebuild the graph on every save

All commands are also available from the Rocql submenu in the editor right-click menu.

Full graph (optional)

The full build enriches the graph with references the Rocq kernel resolves (typeclass instances, notations) via coq-dpdgraph. This layer is optional and requires:

The rocq (or coqc) binary on PATH.
coq-dpdgraph installed in your switch: opam install coq-dpdgraph.

Without them, every editor feature and the textual graph still work.

Settings

Setting	Default	Meaning
`rocqGraph.defaultQuery`	(empty)	GQL query run when the panel opens. Empty = full graph.
`rocqGraph.autoGraph.enabled`	`false`	Persisted state of the auto-graph toggle.
`rocqGraph.autoGraph.dpdOnGreen`	`true`	With auto-graph on, run the dpdgraph enrichment once VsRocq stops reporting errors.