Skip to content

TESTING.md

Latest commit

 

History

History
340 lines (277 loc) · 22 KB

TESTING.md

File metadata and controls

340 lines (277 loc) · 22 KB
Raw

Testing

This is contributor and maintainer documentation. Normal Lean Beam users should not need to read this document to install or use the CLI.

CI is the validation record for routine checks. PR descriptions should mention tests only for rare local validation that CI cannot represent; see CONTRIBUTING.md.

The repository treats testing as three distinct surfaces:

  • LSP: every method registered by the Lean plugin in Beam/LSP/Plugin.lean
  • Beam: broker, daemon/client protocol, CLI wrapper, install/runtime packaging, MCP, toolchain support, and Rocq support
  • Maintainer: local workflow helpers and defensive validation wrappers that are not part of the product surface

This split is organizational. It is also the supported top-level test layout.

Importable Lean test code lives under tests/lean/BeamTest and is exposed to Lake as the BeamTest library. The rest of tests contains shell and Python entrypoints, scenario scripts, interactive golden inputs, fixture projects, and shared test helper scripts.

When a test copies tests/save_olean_project, it excludes the fixture's untracked .beam directory. That directory may contain large machine-local runtime bundles from an earlier run; it is cache state, not fixture input, and copying it can hide cold-start behavior or exhaust disk space.

For public CLI failure behavior, pair a cheap typed or parser-level test with the focused wrapper test that exercises the real command line. Run that focused entrypoint after the final error assertion is written; a pass obtained before the assertion or through a neighboring suite does not validate the public wording or exit path.

The LSP surface also has a lightweight coverage registry under tests/lsp-coverage. The registry ties every method registered by Beam/LSP/Plugin.lean to concrete test pointers and required coverage tags such as isolation, stale-edit, cancellation, handle lifecycle, and mixed concurrency. Method-isolated Lean request tests live under tests/lean/BeamTest/LSP/Requests, with tests/lean/BeamTest/LSP/RequestSurfaceTest.lean remaining as the aggregate request-surface runner.

Race-Test Discipline

Race and concurrency regressions should wait for observable state, not for guessed wall-clock delays. Prefer request IDs plus cancellation acknowledgements, wrapper progress text, registry files, non-empty response files, and Lean-side sentinel files that prove a slow command reached the intended phase. Use tests/lib/beam-wrapper-common.sh helpers for repeated shell polling patterns. Prefer its JSON assertion helpers for wrapper response checks so failures print payloads and captured context consistently.

Keep fileProgress and readiness distinct in assertions. For lean-beam sync, lean-beam save, and lean-beam close-save, completed progress is part of the diagnostics/save barrier contract. For other wrapper requests, progress text is a useful synchronization marker only; it is not proof that the file or request has reached a stronger semantic readiness state.

Fixed sleeps are acceptable only when the behavior under test is explicitly elapsed-time behavior, such as "the daemon remains live after a short idle interval". When a test is trying to observe startup, overlap, cancellation, or a stale-state transition, add a bounded polling helper or a fixture sentinel instead.

LSP Surface

Primary entrypoint:

Current LSP coverage includes:

Run the LSP surface when the change touches request semantics, proof-vs-command basis selection, positions, cancellation, handles, stale snapshots, per-request isolation, or any method in Beam/LSP/Plugin.lean.

Beam Surface

Default Beam entrypoints:

Additional Beam lanes:

Current Beam coverage includes:

  • fast Beam daemon smoke, broker stream ordering, save-stream, wrapper-readiness codec checks, backend-startup failure with provisional backend cleanup, tracked-diagnostic dedup, exact broker request-handle lifetime, identity-matched daemon-generation probes, terminal shutdown response delivery, shutdown after the requesting TCP client resets its connection, protocol tests, and validated-toolchain/release-line CI policy consistency through tests/test-beam-fast.sh
  • wrapper coverage through tests/test-beam-wrapper.sh, which reports focused probe, runtime, sync/save, handle, and diagnostic slices independently
  • focused daemon lifecycle coverage in tests/test-beam-wrapper-daemon.sh, including the no-implicit-start contract, duplicate-owner rejection, authenticated generation probes, interruption of a request whose authenticated endpoint stops reading during send, mode-0700 session-directory and mode-0600 descriptor publication, rejection of symlinked or non-private existing session paths without mutating their targets, stable missing-path canonicalization, wrong-root status classification and recovery rejection with byte-for-byte descriptor preservation, unauthorized-shutdown rejection without listener teardown, oversized-frame and first-message limits, cross-root unsafe-registry preservation that does not affect the daemon serving the other root, configuration-drift preservation of the owner and active request, explicit stop, committed-state reporting after shutdown delivery failure, cancellation of requests active during shutdown or owner loss, exact-generation cleanup that preserves a replacement registry, idempotent repeated stop, a published draining fence while a daemon is paused, rejection of attachment or replacement while that generation remains published, forced process-group cleanup of the daemon and its backend, holder reporting and recovery-required projection after an unexpected daemon crash, abrupt owner death through inherited-pipe EOF, read-only crash-fence lookup, four-state status projection, ambiguity-safe human root inference, explicit-root lifecycle commands, exact-generation non-signalling recovery, exact session-directory selection, and self-termination after the project worktree disappears without recreating it
  • Linux-only PID-isolated sandbox wrapper coverage in tests/test-beam-wrapper-sandbox.sh, including cross-namespace endpoint attachment, duplicate-owner rejection, a paused owner without time-based expiry, explicit stop, killed-owner EOF cleanup, fail-closed preservation of an unavailable foreign-domain descriptor before explicit recovery, distinct generation identity, and the absence of legacy lease/retirement artifacts
  • zero-build save replay, structured-setup support, batch-only-argument rejection, and stale-save race coverage in tests/test-beam-save-olean.sh
  • install flow, installed runtime layout, manifest metadata, exact/compatible toolchain selection, shell/Lean owned-root marker parity, required artifact and executable-mode validation, content-addressed runtime reuse, reused-runtime source-commit refresh and clearing, schema-2 reuse rejection and cleanup compatibility, validated-toolchains, compatible-release-lines, doctor, installed-state pruning, and installed MCP wrapper coverage in tests/test-beam-install.sh, with focused prune safety and invalid-runtime identity cases in tests/test-beam-prune.sh
  • MCP protocol-family selection, projection, modern and legacy stdio, HTTP bridge, self-check, released official-client interoperability, and external legacy/modern conformance coverage
  • Rocq wrapper and broker smoke coverage in tests/test-beam-wrapper-rocq.sh and tests/lean/BeamTest/Broker/RocqSmokeTest.lean

Run the Beam surface when the change touches broker protocol or transport, request/progress/diagnostics streams, daemon session or restart logic, wrapper CLI behavior, bundle resolution, install layout, doctor, validated-toolchains, save replay, save barriers, MCP, or Rocq integration.

For save-only work, use tests/test-beam-save-olean.sh as the local development loop. The slow and aggregate Beam suites remain useful CI or pre-release signals, but save replay by itself does not require running them locally.

The user-facing installer behavior, write locations, MCP registration paths, and toolchain options are documented in SETUP.md. The notes below cover maintainer test fixtures and offline validation knobs.

tests/test-beam-install.sh uses fresh fake homes, so first runs may otherwise download Lean toolchains repeatedly. By default it opportunistically pre-seeds each fake ELAN_HOME with symlinks to matching toolchains already present in the host elan cache. Set BEAM_INSTALL_TEST_PRESEED_ELAN=0 to force fully fresh fake homes, or set BEAM_INSTALL_TEST_PRESEED_ELAN=require when working on a slow/offline connection and you want the test to fail fast if an exact validated toolchain is missing from the host cache.

Installer tests should keep filesystem side effects inside their fake homes and owned temp roots. Use tests/lib/install-fixtures.sh for installer-specific fixtures and tests/lib/tmp-guards.sh for generic shell-test cleanup guards. New tests that remove temp paths should declare their expected /tmp prefix explicitly and use the guard helpers instead of raw rm -rf; the helpers also allow the nested /tmp/beam-validate-*/tmp/... layout used by scripts/validate-defensive.sh.

For slow or offline validation, pre-seed the host elan cache before running installer tests. A typical setup is:

grep -v '^[[:space:]]*#' validated-lean-toolchains | sed '/^[[:space:]]*$/d' |
  while IFS= read -r toolchain; do
    elan toolchain install "$toolchain"
  done

BEAM_INSTALL_TEST_PRESEED_ELAN=require bash tests/test-beam-install.sh

Use tests/test-beam-toolchain-compat.sh to validate one supported bundle lane at a time. The lane also checks that Lean's stale-import diagnostic wording still matches Beam's temporary text-based detector while the structured Lean stale-dependency API is pending. If bundle installation stalls on a slow machine, raise BEAM_TOOLCHAIN_COMPAT_TIMEOUT from its default 600 seconds. On failure, the test prints the fake home, agent homes, bundle directory, platform, and captured build/bundle/stale-diagnostic log tails so the bundle or stale-diagnostic state can be diagnosed from the test log. Set BEAM_TOOLCHAIN_COMPAT_KEEP_TMP_ON_FAILURE=1 to preserve the fake roots for local inspection after a failed run.

Save Replay Timeout Investigation

tests/test-beam-save-olean.sh includes a save-race case that injects a slow Lean command into SaveSmoke/B.lean. The command writes LEAN_BEAM_SAVE_RACE_SENTINEL when elaboration reaches the intended race window, then sleeps long enough for the shell test to edit the source file while close-save is still in flight.

If the sentinel is not written before BEAM_SAVE_RACE_SENTINEL_TIMEOUT (default 60 seconds), the test now dumps the active save PID, runner CPU/platform context, Beam/Lean process snapshot, current SaveSmoke/B.lean, the sentinel file state, daemon registry, daemon log tail, and captured save stdout/stderr. The race and cancel-sentinel cases start their daemon with broker trace enabled by default (BEAM_SAVE_RACE_BROKER_TRACE=1) and a diagnostics-barrier watchdog (BEAM_SAVE_RACE_WAIT_DIAGNOSTICS_WATCHDOG_MS=10000) so macOS/low-core stalls preserve useful phase information in the daemon log.

MCP Stdio Timeout Investigation

When investigating MCP stdio timeouts, prefer the focused descriptor-bound sync repro before rerunning the full smoke suite:

lake build Beam.LSP:shared beam-daemon lean-beam-mcp
PYTHONDONTWRITEBYTECODE=1 python3 tests/test-mcp-stdio.py \
  --scenario progress-sync \
  --repro-runs 100 \
  --timeout 30 \
  --slow-threshold 5 \
  --server-trace

That scenario runs lean_sync with an explicit workspace descriptor and a progress token, then checks the resulting progress notifications. On failure, the timeout report includes the client label, pending request parameters, recent completed requests, recent server requests received from lean-beam-mcp, recent notifications, runner CPU/platform context, relevant CI and Lean thread env vars, the stderr tail, and a Beam/Lean process snapshot.

For the same-process concurrency contract, run:

lake build Beam.LSP:shared beam-daemon lean-beam-mcp
PYTHONDONTWRITEBYTECODE=1 python3 tests/test-mcp-stdio.py \
  --scenario concurrent-dispatch \
  --timeout 40

This scenario covers out-of-order tool responses, exact string/numeric request-ID separation, duplicate active-ID suppression, repeated asynchronous request-ID reuse after terminal responses, exact modern and legacy broker cancellation, per-request progress ordering, deterministic overlap between a gated request in one workspace and a fast request in another, single-flight first use, simultaneous cold first use of distinct roots, stateless multi-root isolation, non-cancellable cache eviction with ordering on both sides of the global fence, lazy recreation, and EOF cancellation and teardown. The full stdio suite also checks modern request-ID reuse, synchronous and workspace-control closed-output teardown, and rejects a proof handle carried across an MCP process restart. The slow Beam suite runs --scenario multi-toolchain-workspaces after installing both fixture toolchains and verifies that one MCP process keeps both project-specific Lean sessions active.

If this scheduler-sensitive timeout appears on an unrelated CI PR, copy the timeout headline and diagnostic excerpt to #110 so repeated occurrences can be correlated in one place. Include the PR URL and branch, failing run URL, failing job URL, job name, runner OS/arch, run attempt, commit SHA, failing test or scenario, relevant request/progress or sentinel diagnostics from the log, and the rerun URL plus whether it passed or reproduced. The optional --server-trace flag enables opt-in lean-beam-mcp and broker trace lines in that stderr tail without changing normal test stderr expectations. To look for scheduler-sensitive behavior locally, prefer a low-core or CPU-contended run. On a large local machine, run CPU load in one shell:

stress-ng --cpu 24 --timeout 90s --metrics-brief

Then run the focused scenario in another shell while the stressors are active.

For the scheduler-sensitive progress-smoke path that has reproduced timeouts locally, use the parallel repro scenario while the stressors are active:

PYTHONDONTWRITEBYTECODE=1 python3 tests/test-mcp-stdio.py \
  --scenario progress-smoke-parallel \
  --parallel-workers 8 \
  --repro-runs 10 \
  --timeout 30 \
  --slow-threshold 5

Set --server-trace to add MCP/broker trace lines to the timeout dump, and set LEAN_BEAM_BROKER_WAIT_DIAGNOSTICS_WATCHDOG_MS=10000 to emit an opt-in broker trace if a waitForDiagnostics barrier is still pending after that many milliseconds. The regular CI Beam suites run the stdio smoke with BEAM_MCP_STDIO_TIMEOUT defaulting to 60 seconds, enable BEAM_MCP_SERVER_TRACE=1 for the stdio harness by default, and set the diagnostics-barrier watchdog to BEAM_MCP_STDIO_WAIT_DIAGNOSTICS_WATCHDOG_MS=10000. Set BEAM_MCP_STDIO_SERVER_TRACE=0 only when intentionally checking the quiet stderr path. The fast suite's installed-wrapper self-check uses BEAM_MCP_SELF_CHECK_TIMEOUT_MS, defaulting to 120 seconds, because first-time bundle setup may build the local fixture under CI contention. Keep --timeout 30 for local repro attempts unless you are specifically checking the CI budget. The focused daemon lifecycle fixture explicitly prebuilds its toolchain into one owned shared cache before timing daemon startup, so cold bundle compilation is not misdiagnosed as a daemon-readiness timeout. The focused CLI daemon test also checks that a failed stderr evidence sink does not stop pipe draining, that sink failure observation is synchronized, and that a pipe held open past leader exit produces a bounded pipeStillOpen outcome rather than an unbounded task join.

The focused harness also accepts no-progress-sync to isolate whether a timeout depends on MCP progress notifications or the underlying lean_sync / waitForDiagnostics path.

Maintainer Surface

The maintainer surface covers local workflow helpers:

The aggregate maintainer runner skips tests/test-codex-harness.sh when the current checkout has tracked edits, because that harness regression intentionally verifies that new task worktrees start from a clean primary checkout.

Run these when the change touches scripts/codex-harness.sh, scripts/codex-session-start.sh, or scripts/validate-defensive.sh.

CI Map

The current GitHub Actions workflow maps to the testing surfaces like this:

Coverage Gaps

The main current gaps are:

  • search-style LSP coverage is correctness-heavy, but not yet a larger benchmark-style workload with much deeper branching pressure
  • maintainer-surface regressions are documented and runnable, but separate from the default product CI lanes