Skip to content

docs(vrs): specify the doctor subsystem from the code and its tests - #32

Closed
schickling-assistant wants to merge 2 commits into
mainfrom
schickling-assistant/2026-07-28-doctor-vrs
Closed

docs(vrs): specify the doctor subsystem from the code and its tests#32
schickling-assistant wants to merge 2 commits into
mainfrom
schickling-assistant/2026-07-28-doctor-vrs

Conversation

@schickling-assistant

@schickling-assistant schickling-assistant commented Jul 28, 2026

Copy link
Copy Markdown
Contributor

Why

doctor is the only way to ask whether a catalog is healthy on a host, and it
gates real operational decisions — yet it had no VRS coverage at all. Grepping
doctor across docs/vrs/ returned nothing. Its contract lived only in the
subcommand, tests/doctor.rs, the doctor part of tests/native_only.rs, and a
single INVARIANTS.md row for retirement health. That makes it easy to change
doctor's definition of "healthy" without noticing the definition moved.

What

Adds docs/vrs/02-doctor/, the first subsystem node under docs/vrs/:

  • requirements.md — the durable guarantees. What counts as healthy and
    unhealthy for tooling, supervision, catalog structure, task liveness,
    presence, and retirement; the exit contract; and what doctor must never do
    (write, repair, hang, or touch its caller's stdin).
  • spec.md — the mechanism. Catalog and host resolution, the ordered check
    sequence with what each check inspects and when it fails, the per-declaration
    split between retired and live declarations, the output shape, an evidence
    table mapping each guarantee to its proof, and the open questions.

Docs only. No code, and no change to docs/vrs/vision.md, docs/vrs/requirements.md,
docs/vrs/spec.md, or INVARIANTS.md.

The 02- prefix leaves 01- free for a subsystem node already in flight.

How

Everything was derived from the implementation and the tests, not from intent:

  • Behaviour comes from reading doctor_cmd in src/main.rs end to end, plus
    the modules it calls — presence reading and the derived-unknown rule, the
    per-(catalog, host) pid lock, catalog discovery, and the bounded
    non-interactive session probe with its union of both task backends.
  • Each guarantee that a test pins is listed in an evidence table in spec.md
    with the qualified test name. Retirement health cites the same three tests
    INVARIANTS.md already names.
  • Guarantees that hold by construction but that no test isolates are stated as
    such in a sentence directly under the evidence table, rather than being
    presented as proven.

What was deliberately left out

Anything not established by the code or a test is recorded as an open question
in spec.md instead of being written into the contract:

  • DOCTOR-DQ1 — the read-only guarantee is established by inspecting the
    doctor path, not by a check. No test asserts the catalog and runtime-state
    directories are unchanged after a run, the way materialization proves its
    tracked-target guarantee.
  • DOCTOR-DQ2 — discovery warnings, notably a path-vs-content disagreement
    about identity or host, are surfaced by validate and ignored by doctor.
    Whether that is correct scope or a gap is unsettled.
  • DOCTOR-DQ3pty is checked unconditionally and is the only tool
    checked, even though a host running only terminal-free tasks does not need it.
    No test covers a missing tool.
  • DOCTOR-DQ4 — retirement looks for residue; a live declaration only checks
    that its declared tasks are alive. A session belonging to no declaration on
    this host is invisible.
  • DOCTOR-DQ5 — there is no machine-readable report, so the exit status is
    the entire machine contract.

Rationale

Requirements and spec are split so the two questions have separate homes: what
must hold for doctor to be correct, versus how it currently establishes that.
The check sequence, output strings, and probe bound are mechanism and live only
in spec.md; the guarantees they serve live in requirements.md and would
survive a rewrite of the mechanism.

IDs are namespaced (DOCTOR-R01, DOCTOR-A01, …) so a subsystem node never
collides with the root documents' bare R01-style IDs.

axe vrs check --profile strict docs/vrs reports zero diagnostics, and
nix flake check passes locally.

For the owner

Two things this PR deliberately does not do, both of which are yours to decide.

A root requirement may be missing. The root VRS never names doctor. R04 assigns host-local health observation, diagnosis, bounded recovery, and escalation to the root agent, and describes the st2 loop as the deterministic half. Doctor is a third thing: a deterministic, on-demand health check that needs no running supervisor. DOCTOR-R02's "manual/--once mode is healthy" arm only makes sense against a root-level requirement that host health is inspectable on demand — and no such requirement exists today. This node references R03/R04/R08 by ID and writes nothing into the root files, since docs/vrs/spec.md requires explicit approval to change them.

Presence semantics stay with R08. Doctor reads presence, so there was a standing temptation to specify the states and the staleness window that produces the derived unknown here. It does not: this node only decides which readings count as healthy. Moving presence detail into the doctor node would give R08 and this file two owners for one contract.

Posted on behalf of @schickling
field value
agent_name cl2-cedar
agent_session_id e5217740-eef6-48eb-a794-3e5e11939e4d
agent_tool Claude Code
agent_tool_version 2.1.220
agent_runtime Claude Code 2.1.220
agent_model claude-opus-5
runtime_profile /nix/store/i8y8b542cyqi385ywcjw5fvsq24f75v4-coding-agent-runtime-profile/share/coding-agents/profile.json
skills_manifest /nix/store/i81qxhzlrzcxrrdwpp6i8hagka2gby8y-agent-skills-corpus/share/agent-skills/manifest.json
worktree dotfiles/schickling/2026-07-20-cos-misc
machine dev3
tooling_profile dotfiles@unknown-dirty

Doctor had no VRS coverage: it existed only as a subcommand, two test
files, and one INVARIANTS row. Add `docs/vrs/02-doctor/` with the durable
guarantees in requirements.md and the mechanism in spec.md, derived from
the doctor path and the tests that pin it.

What is proven by a test is cited in the evidence table; what holds only
by construction is named as such, and what nothing establishes is
recorded as an open question rather than written into the contract.
@schickling
schickling requested a review from myobie July 28, 2026 13:48
@schickling
schickling marked this pull request as ready for review July 28, 2026 13:48
@schickling

Copy link
Copy Markdown
Contributor

@codex

@chatgpt-codex-connector chatgpt-codex-connector Bot left a comment

Copy link
Copy Markdown

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

💡 Codex Review

Here are some automated review suggestions for this pull request.

Reviewed commit: 1c21ced9be

ℹ️ About Codex in GitHub

Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you

  • Open a pull request for review
  • Mark a draft as ready
  • Comment "@codex review".

If Codex has suggestions, it will comment; otherwise it will react with 👍.

Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".

Comment thread docs/vrs/02-doctor/requirements.md Outdated
Comment thread docs/vrs/02-doctor/requirements.md Outdated
Comment thread docs/vrs/02-doctor/spec.md Outdated
Comment thread docs/vrs/02-doctor/spec.md Outdated
Comment thread docs/vrs/02-doctor/spec.md Outdated
An automated review on #32 found five places where the node modelled the
pty path and over-generalized it to both backends. All five confirmed
against the code.

- DOCTOR-A02 claimed liveness never comes from st2's own records. It does
  for exec: `ExecBackend::list` enumerates st2-written `.pid` files and
  probes each recorded pid, and skips any record it cannot read, so a
  live exec process with a missing record reads as dead. Split the
  assumption per backend and state the hiding failure mode.
- Check 4's hard stop is pty-only. `ExecBackend::list` has no error path
  at all — an unreadable state dir returns an empty list — so
  `SystemRunner::list_sessions` succeeds and the exec side reaches the
  per-declaration checks as an ordinary empty result. Corrected the check
  table and DOCTOR-T01.
- DOCTOR-R10's bound is pty-only: only `PtyCli::list_sessions` runs under
  `output_with_timeout`. Narrowed it and said plainly that exec-record
  enumeration is unbounded.
- DOCTOR-R04 promised "readable". `status::read_state` falls back to
  `offline` for an unreadable or unparseable file, so a fresh broken file
  passes as `offline`. Documented the fallback, including that staleness
  is evaluated before contents are read, so a broken *and* old file still
  fails.
- The compact-form task ID is computed from the declaration's own host
  before the checked host is known, so a hostless declaration stores a
  bare identity while doctor reports the host-qualified name. Added the
  exception.

Adds DOCTOR-DQ6 for the root cause the five share: the exec backend fails
open, so its failures become wrong verdicts rather than problems —
including reporting a retired declaration's exec tasks absent, which is
what retirement health exists to prevent. No test covers the exec path.

`axe vrs check --profile strict docs/vrs` stays green.

agent-session-id: e5217740-eef6-48eb-a794-3e5e11939e4d
agent-tool: Claude Code
agent-tool-version: 2.1.220
agent-model: claude-opus-5
agent-runtime-profile: /nix/store/i8y8b542cyqi385ywcjw5fvsq24f75v4-coding-agent-runtime-profile/share/coding-agents/profile.json
agent-skills-manifest: /nix/store/i81qxhzlrzcxrrdwpp6i8hagka2gby8y-agent-skills-corpus/share/agent-skills/manifest.json
tooling-profile: dotfiles@unknown-dirty
@myobie

myobie commented Jul 28, 2026

Copy link
Copy Markdown
Contributor

Closing per stable-main hygiene disposition: documentation scope is preserved on main history; no merge required.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

3 participants