Rocq Beam

Rocq Beam

Use this skill when a Rocq project needs the narrow Rocq-facing surface that lean-beam already exposes, especially while porting Rocq developments to Lean. This is an optional auxiliary mode of the lean-beam toolchain, not a separate product or a second full workflow stack.

The goal is cheap Rocq proof-state inspection through coq-lsp, without turning Rocq support into a broad standalone interface.

Do not use coqtop or any fallback executor. Only coq-lsp is trusted. This is the Rocq-only skill. It should stay focused on Rocq and should not require Lean-specific workflow guidance. Do not factor shared Lean/Rocq skill instructions into a common helper; duplicate short guidance if both skills need it.

Setup

From the lean-beam repo root:

./scripts/install-beam.sh --codex --rocq-skill

Use --claude --rocq-skill, --pi --rocq-skill, --opencode --rocq-skill, or --vibe --rocq-skill instead when installing for Claude Code, Pi Agent, OpenCode, or Mistral Vibe. Use --all-skills --rocq-skill when you want every supported agent skill target.

The installer puts lean-beam in ~/.local/bin, stages the self-contained runtime under BEAM_INSTALL_ROOT (default ~/.local/share/beam), and installs the optional Rocq skill only when --rocq-skill is paired with a selected agent skill target.

Restart active agent sessions after installation.

The user-facing setup and installer reference is docs/SETUP.md. The Rocq status and setup page is docs/ROCQ.md.

Rocq Setup

Rocq-specific setup:

cd /path/to/lean-beam
bash tests/setup-rocq-opam.sh

Skill Surface

This skill documents the current Rocq-facing lean-beam workflow surface. Keep the surface narrow: the current wrapper is for goal inspection against saved files, not for hidden proof-session mutation.

Supported command families:

• start and own a Rocq wrapper session: lean-beam serve rocq
• inspect the selected session state: lean-beam status
• inspect goals after an existing sentence: lean-beam rocq-goals-after
• inspect goals before a sentence or after speculative sentence text within that basis: lean-beam rocq-goals-prev
• inspect tracked files and daemon state: lean-beam open-files, lean-beam stats

What to treat as the current agent workflow surface:

• default command: lean-beam rocq-goals-after
• intermediate-state command: lean-beam rocq-goals-prev with extra text when needed
• operational introspection: lean-beam open-files, lean-beam stats

Core workflow contract:

• use lean-beam, not raw JSON and not raw LSP
• before issuing wrapper probes, start one foreground lean-beam serve rocq process and keep it running; interrupt it or run lean-beam --root ROOT stop when finished
• save the .v file before every new probe after a real edit
• lean-beam only sees the on-disk file, not unsaved editor buffers
• treat <line> <character> as LSP-style coordinates for the saved file: line 0 is the first line, character 0 is the first character position on that line, and on a truly empty line only character 0 is valid
• there is no Rocq sync command in the current wrapper
• there is no Rocq handle or continuation surface in the current wrapper
• there is no Rocq run-at command in the current wrapper; use the goal probes instead
• do not assume hidden mutable proof-session state carries across requests
• do not use coqtop or a fallback executor; only coq-lsp is trusted

Use lean-beam, not raw JSON and not raw LSP.

lean-beam for Rocq:

• infers the target project root from the current directory or --root
• keeps one owner per resolved workspace and session-directory selector; the default descriptor is <root>/.beam/beam-daemon.json
  • in sandboxed or read-only project trees, set BEAM_SESSION_ROOT to a writable directory
  • for an exact stable alternate location, pass the same absolute path with --session-dir DIR to the owner and every attaching command; Beam does not search alternate session directories
• gives daemon startup authority only to lean-beam serve rocq; ordinary commands attach to its registry generation and never start a daemon implicitly
• owns stopping and descriptor handling
• preserves ambiguous crash state until explicit recover --generation ID; recovery does not signal persisted PIDs
• resolves coq-lsp from the target project's local _opam when available
• the explicit owner starts a Rocq-capable Beam daemon with startup args instead of relying on inherited editor state
• wrapper commands talk to the per-project Beam daemon over localhost TCP; they are not direct in-process Rocq calls
• in Codex-style sandboxes, Beam daemon startup may still require elevated permissions even when all paths resolve correctly
• in the same environments, localhost TCP bind/connect for the Beam daemon and client may also require elevated permissions
• if startup fails with operation not permitted, treat that as a sandbox capability problem first, not as a missing install
• lean-beam --root ROOT stop requires an explicit root; lean-beam status and lean-beam stats may infer a unique root

Default rules:

• use lean-beam, not raw JSON and not raw LSP
• start with lean-beam rocq-goals-after
• save the file before every new probe after a real edit
• keep coordinates 0-based; do not guess editor-specific 1-based lines or columns
• if you think you want a Rocq run-at, use lean-beam rocq-goals-prev with extra text or rocq-goals-after instead
• use lean-beam rocq-goals-prev plus text when you need an intermediate state inside a sentence
• do not assume any hidden proof-session state carries across requests

Workflow

Start the Rocq wrapper-session owner in one terminal or long-lived agent process, then inspect it from another:

# terminal/session 1: keep running
lean-beam serve rocq

# terminal/session 2
lean-beam stats

Inspect goals after a sentence:

lean-beam rocq-goals-after "Demo.v" 2 8

Inspect goals before a sentence:

lean-beam rocq-goals-prev "Demo.v" 2 8

For a tactic sentence like a; b, inspect the intermediate state after a with:

lean-beam rocq-goals-prev "Demo.v" 2 8 "a."

Source-file model:

• lean-beam rocq-goals-* does not edit Demo.v
• edit the file normally, save it, then probe again
• lean-beam only sees the on-disk Rocq file, not unsaved editor buffers
• actual source edits happen through the normal file-edit workflow
• there is no Rocq sync command in the current wrapper; saving the file is the important step before the next probe

Execution model:

• every lean-beam rocq-goals-* request is an isolated read-only probe against the current saved file
• do not expect hidden mutable proof-session state to carry from one probe to the next
• the Beam daemon may reopen or resync the on-disk file before a probe, but saving the file is still the real boundary you control
• there is no Rocq lean-beam sync equivalent in the wrapper, so after edits the important step is: save, then probe again
• if the file changes while a request is pending or coq-lsp state becomes stale, expect to rerun from the saved file instead of relying on recovery inside the old request

Default loop:

# with `lean-beam serve rocq` running in another process
lean-beam rocq-goals-after "Demo.v" 12 4

# make a real edit, save the file
lean-beam rocq-goals-after "Demo.v" 12 4

Use cases:

1. Inspect the current proof state after a sentence

# with `lean-beam serve rocq` running in another process
lean-beam rocq-goals-after "Demo.v" 12 4

2. Inspect an intermediate tactic state inside one sentence

# with `lean-beam serve rocq` running in another process
lean-beam rocq-goals-prev "Demo.v" 12 4 "intro x."
lean-beam rocq-goals-prev "Demo.v" 12 4 "split."

3. Check the effect of a small real edit

Save the file first, then probe again from the saved document.

# with `lean-beam serve rocq` running in another process
lean-beam rocq-goals-after "Demo.v" 12 4

# make a real edit in Demo.v and save it
lean-beam rocq-goals-after "Demo.v" 12 4

Policy

• default to lean-beam rocq-goals-after
• use lean-beam rocq-goals-prev plus text for intermediate-state probing
• keep ppFormat as Str
• do not treat lean-beam as a source editor; actual .v edits happen through the normal file-edit workflow
• do not assume one goal probe mutates the basis of the next probe; each request starts from the current saved document state
• if coq-lsp reports stale or broken state unexpectedly, stop and report it loudly

Stats

Use:

lean-beam open-files
lean-beam stats

lean-beam open-files shows the files currently tracked by the Beam daemon for the current project. For tracked files the broker already knows about, the wrapper checks status incrementally against the current on-disk text, and open-files also reports the last compact fileProgress observed for that tracked version.

Stats are in-memory only and scoped to the current project Beam daemon.

Upstream Rocq Features Not Yet Wrapped

Useful petanque/* methods we may expose later:

• petanque/get_state_at_pos
• petanque/run_at_pos
• petanque/goals
• petanque/premises
• petanque/ast_at_pos
• petanque/list_notations_in_statement
• petanque/proof_info_at_pos