Skip to content

AGENTS.md

Latest commit

 

History

History
158 lines (118 loc) · 6.72 KB

AGENTS.md

File metadata and controls

158 lines (118 loc) · 6.72 KB
Raw

AGENTS.md

Purpose

This repository hosts the pre-stable Beam Lean plugin, wrapper, and local broker tooling.

Treat the repo as public but still experimental: prefer conservative, well-tested changes over feature sprawl.

Current public status and limitations live in docs/STATUS.md. Compatibility policy lives in docs/COMPATIBILITY.md. User setup lives in docs/SETUP.md. Exact MCP behavior lives in docs/MCP.md, and exact sync/save/diagnostic behavior lives in docs/SYNC_AND_DIAGNOSTICS.md.

Product Priorities

In order:

  1. dead-simple public API
  2. rock-solid stability
  3. type-safe boundaries
  4. isolation of each request
  5. performance

Performance matters, but not at the cost of correctness or stability.

Public API Guardrails

The core public request should remain conceptually:

  • runAt(pos, "lean text")

Rules:

  • no required public mode flag for command vs tactic execution
  • backend selection is internal
  • keep request and response structures small and typed
  • use transport errors for invalid params, stale state, cancellation, and internal faults
  • avoid exposing internal execution details unless a concrete client need forces it

Follow-up handle APIs exist, but they are pre-stable extensions around the basic request, not the main story of the project.

Execution Model

Each request should behave like an isolated sandbox:

  • never mutate the document's real elaboration state
  • never depend on side effects from a previous request
  • never leak internal mutable state through the base API
  • discard derived execution state unless the request explicitly stores a follow-up handle

Testing Priorities

Tests matter more than cleverness.

Focus on:

  • position selection and boundary behavior
  • whitespace and comment positions
  • proof-vs-command basis selection
  • stale snapshot and file-changed behavior
  • nested tactic cases
  • no state leakage across requests
  • cancellation behavior
  • handle invalidation when handle behavior is touched

If a behavior is subtle, encode it in tests before optimizing it.

Common Code Smells

  • do not stringify typed errors or responses and later parse the rendered exception text to recover control flow; keep Response, BrokerFailure, or structured error data typed across async/pending boundaries, and stringify only at transport, CLI, or diagnostic display edges
  • do not add useless backward compatibility support; this pre-stable project has no legacy users, so remove obsolete aliases, inferred envelope shapes, and compatibility branches unless they support an explicitly listed Lean/Rocq/tooling/protocol version or another target named in docs/COMPATIBILITY.md

Skill Boundaries

Keep the Lean and Rocq skills fully separate.

  • lean-beam must stay Lean-only and must not require Rocq setup or Rocq concepts
  • rocq-beam must stay Rocq-only and must not require Lean-specific workflow guidance
  • do not introduce a shared skill helper, common skill file, or mixed Lean/Rocq skill layer
  • if a short instruction is needed in both skills, duplicate it instead of coupling the two skills

Public Writing

Docs, skill text, and PR descriptions should be readable without local worktree history or private review context.

  • define project-specific terms before using them as shorthand
  • name concrete commands, CI jobs, fixtures, or failure codes when making testing claims
  • separate current behavior from unsupported cases, planned work, and safe follow-ups
  • in agent-facing skill text, prefer exact commands, stop conditions, stdout/stderr behavior, and known stale-state recovery paths
  • do not describe aspirational or planned MCP/CLI behavior as if it already exists

Local Tooling

The repo includes:

The Codex harness scripts are maintainer workflow helpers for this repository. They are not part of the public lean-beam API or the installed skill surface.

When working locally:

  • start new Codex tasks from ./scripts/codex-harness.sh session start <task-id> so the task runs in a dedicated git worktree instead of the primary checkout
  • let the harness keep its default persistent worktree root under <repo>/.codex-worktrees/lean-beam; do not place long-lived task worktrees under /tmp
  • keep destructive shell cleanup scoped to owned temp/worktree paths; do not use broad rm or rm -rf against repo-local .beam, install caches, or user homes as part of normal workflows
  • for LSP request / handle / scenario changes, run bash tests/test-lsp.sh
  • for Beam broker protocol / stream / barrier changes, run bash tests/test-beam-fast.sh first
  • for Beam wrapper / install / bundle-resolution changes, also run bash tests/test-beam-slow.sh
  • for supported Lean toolchain changes, add bash tests/test-beam-toolchain-compat.sh <toolchain>
  • for Rocq broker / wrapper changes, use bash tests/test-beam-rocq.sh
  • for risky local install / wrapper validation, prefer bash scripts/validate-defensive.sh so slow suites run in a cloned /tmp sandbox with fake homes and guarded path operations
  • use bash tests/test-beam.sh when you want the aggregate default Beam suite
  • prefer the wrapper over raw LSP when the task fits
  • use Rocq only through coq-lsp
  • if a file is open in the broker, do not edit it out of band
  • if Lean reports stale or rebuild trouble unexpectedly, stop and surface it loudly

Pull Request Messages

  • Before opening or editing a PR, run scripts/pr-message.sh and use the emitted title/body scaffold as the source of truth.
  • Keep the public PR title/body suitable as the final squash commit message.
  • Start PR bodies with a short paragraph beginning This PR ...; summarize the problem and useful outcome instead of pasting local status notes.
  • Do not add generator or tool prefixes such as [codex] to public PR titles.
  • Keep local worktree names, write-scope notes, command transcripts, and routine validation logs out of public PR bodies.
  • Do not add a Testing or Validation section for checks that CI already runs; mention tests only for rare validation that CI cannot represent, and explain why that result matters to review.

Helpful repo docs: