Release v0.1.3: capture native Codex subagents and telemetry

.gitignore

@@ -25,3 +25,5 @@ subagent_test/
 /codex_error.log
 /codex_test.jsonl
 
+# local manuscript drafts
+/arxiv-paper/

README.md

@@ -7,7 +7,7 @@
 *Workspace-first orchestration for long-horizon Lean 4 formalization agents*
 
 [![Live demo](https://img.shields.io/badge/live%20demo-open%20dashboard-brightgreen?logo=githubpages)](https://frenzymath.github.io/Archon-Horizon/)
-![Version](https://img.shields.io/badge/version-0.1.2-blue)
+![Version](https://img.shields.io/badge/version-0.1.3-blue)
 [![License](https://img.shields.io/badge/Apache-2.0-green)](./LICENSE)
 ![Python](https://img.shields.io/badge/python-3.11%2B-blue)
 ![Lean](https://img.shields.io/badge/domain-Lean%204-1f6feb)
@@ -51,7 +51,7 @@ The **Horizon Agent** owns the proof loop and decides when to dispatch helpers.
 - **Async inboxes, per-team ownership & standing protections.** Humans and agents collaborate through a local filesystem inbox and an optional GitHub shadow-sync, observed only at round boundaries so proof searches are never interrupted mid-flight. Items can be shared or **owned by one task** (a private per-team inbox), carry **per-team read-state** (`inbox read`/`unread`, `list --mine/--unread`), and be **direct-messaged** to another running team. Standing protections soft-freeze foundational signatures and files so autonomous runs can't quietly break your API. → [Inboxes](./docs/inboxes-and-communication/README.md)
 - **Parallel teams on a shared board.** Each `horizon run` is a team (a lead agent plus its subagent workers); parallel teams coordinate through shared state — a roadmap that doubles as a **project board** (owner, milestone labels, pinned commits, a live `/board` view), the inbox, and the commit ledger — rather than synchronous meetings. A stderr **synchronizer** keeps each agent aware of unread messages and other live runs, and launching work for *other* teams is gated by an opt-in `workspace.delegation` policy (default deny). → [Architecture](./docs/architecture/README.md)
 - **Blueprints & dependency graphs.** LaTeX-subset blueprints and Lean sources synchronize into a vendored, plain-files semantic graph. `horizon graph` exposes frontier, dependency, review, and comment operations; the dashboard renders a deterministic chapter-collapsed Graphviz view. → [Blueprints & semantic graphs](./docs/blueprints-and-graph/README.md)
-- **Dashboard & offline search.** A live web dashboard renders the DAG (KaTeX), run logs, and inbox, and can export a self-contained static snapshot for GitHub Pages. `horizon search` runs BM25, Loogle-style name, and signature-pattern search over `.lean` sources with no GPU, API key, or network. → [Dashboard & Search](./docs/dashboard-and-search/README.md)
+- **Dashboard & offline search.** A live web dashboard renders the DAG (KaTeX), run logs, native Codex subagent trees, context compactions, and inbox, and can export a self-contained static snapshot for GitHub Pages. `horizon search` runs BM25, Loogle-style name, and signature-pattern search over `.lean` sources with no GPU, API key, or network. → [Dashboard & Search](./docs/dashboard-and-search/README.md)
 - **Public demo workspace.** A tiny two-chapter Lean/blueprint fixture ships outside the Python package with synthetic Claude Code and Codex runs, so the dashboard can be explored without credentials. → [Open the live demo](https://frenzymath.github.io/Archon-Horizon/)
 
 *More depth on every topic — including the full [`config.yaml`](./docs/configuration/README.md) reference — lives in [`docs/`](./docs/README.md).*
@@ -122,6 +122,8 @@ Every command supports `--json` for machine-readable output on `stdout`. Run `ho
 - `horizon init` — scaffold a workspace or refresh managed files (`--update`).
 - `horizon run <target>` — run autoformalization on a task or project, everything (`*`), or a single role (`ground` / `horizon`, optionally `--backend interactive`).
 - `horizon discuss` — open an interactive session to talk with the workspace: status, recent runs, and edits to projects/tasks/inbox/roadmap on request.
+- `horizon attempt save` — preserve a rejected draft and optional diagnostics as a session artifact.
+- `horizon check` — serialize and record resource-heavy Lean checks across concurrent sessions.
 - `horizon dashboard` — live server, or static HTML export (`--static`).
 
 👉 See the [full CLI reference](./docs/cli-reference/README.md) for all commands and flags.

demo/.archon-horizon/version

@@ -1 +1 @@
-0.1.2
+0.1.3

docs/CHANGELOG.md

@@ -9,6 +9,39 @@ minor releases; `horizon init --update` migrates a workspace's managed files.
 
 ## [Unreleased]
 
+## [0.1.3] — 2026-08-18
+
+### Added
+
+- Live Codex rollout telemetry now discovers native and nested subagents from
+  spawn provenance while the parent is running, records their model/role/depth
+  and terminal status, and surfaces context compactions separately from current
+  request and cumulative token counters.
+- `horizon attempt save` preserves rejected drafts and diagnostics as explicit
+  session artifacts; `horizon check` serializes resource-heavy Lean checks,
+  coalesces identical concurrent requests, enforces timeouts, and records results.
+
+### Changed
+
+- Session change panels distinguish agent and integration commits, rejected
+  attempts, and recorded checks. Long sessions get elapsed-time progress/commit
+  checkpoints, including task/roadmap/inbox writes.
+- The transcript keeps only the newest Codex context snapshot visible while the
+  append-only log retains every raw telemetry event. Current-request, cached,
+  cumulative, context-window, and compaction values remain in session details.
+- Live dashboard state derives large changing transcripts from a bounded tail and
+  only rematerializes subagents when appended rows contain child activity; the
+  latest state-generation timing is available at `/api/performance`.
+
+### Fixed
+
+- Headless Codex runs now reconstruct native and nested subagents from rollout
+  spawn provenance, stream their activity before the parent exits, suppress
+  duplicate reconciliation events, and distinguish completed, failed,
+  interrupted, cancelled, and orphaned children.
+- Both Codex compaction record shapes are normalized without conflating current
+  request input, cached input, cumulative usage, or the model context window.
+
 ## [0.1.2] — 2026-07
 
 The "lightweight harness, finished" release, extended with multi-team
@@ -181,5 +214,6 @@ a **Ground agent** (blueprints, DAG, roadmap, reports, inboxes) and a
 - **Install / update.** `curl … | bash` installer (`install.sh`) and a
   `horizon update` self-update command.
 
-[Unreleased]: https://github.com/frenzymath/Archon-Horizon/compare/v0.1.0...HEAD
+[Unreleased]: https://github.com/frenzymath/Archon-Horizon/compare/v0.1.3...HEAD
+[0.1.3]: https://github.com/frenzymath/Archon-Horizon/compare/v0.1.2...v0.1.3
 [0.1.0]: https://github.com/frenzymath/Archon-Horizon/releases/tag/v0.1.0

docs/architecture/README.md

@@ -112,3 +112,10 @@ When a workspace is initialized or updated (`horizon init --update`, and again a
 - **Subagents** (both engines): Specialized roles such as `ground`, `work-reviewer`, and `blueprint` are compiled to workspace-local `.claude/agents/<name>.md` (Claude) and `.codex/agents/<name>.toml` (Codex). Read-only is engine-enforced (Claude `disallowedTools`; Codex `sandbox_mode = "read-only"`).
 - **Model ownership:** descriptors do not pin a model, tier, or effort. Helpers inherit the parent by default; Horizon chooses a lighter capable model for mechanical work or the same/high-effort model for mathematical review through the engine's native dispatch mechanism.
 - **Skills**: Modular capability guides are provisioned under `.claude/skills/<name>/SKILL.md`. **Claude Code** auto-discovers them. **Codex** has no such discovery, so Horizon inlines a skills index (names, descriptions, and the absolute `SKILL.md` paths to read on demand) into each compiled Codex agent.
+
+Claude reports child events inline. Headless Codex instead writes every native
+child to its own rollout file, so [`CodexHarness`](../../src/archon_horizon/harnesses/codex.py)
+tails the rollout store, discovers direct and nested children from
+`thread_spawn` provenance, assigns source-line event ids for idempotent
+reconciliation, and normalizes child lifecycle, token, and compaction events
+into the backend-neutral transcript model.

docs/cli-reference/README.md

@@ -106,6 +106,26 @@ Read the workspace's standing delegation consent — what a running agent is all
 | :--- | :--- |
 | `--json` | Emit the delegation config as JSON to `stdout`. |
 
+### `horizon attempt`
+
+Preserve a substantial rejected or paused draft outside the working tree so a
+later session can inspect the dead end without treating it as a durable commit.
+Artifacts live under the active session's `attempts/` directory.
+([`commands/attempt.py`](../../src/archon_horizon/commands/attempt.py))
+
+- `horizon attempt save <files...> --reason <text> [--diagnostics <file>] [--json]`
+- `horizon attempt list [--json]`
+
+### `horizon check`
+
+Run `lake build` or one standalone Lean file while holding a workspace-wide
+check lock. Identical concurrent successful requests are reused after waiting;
+results and timeouts are recorded under the active session's `checks/`
+directory. ([`commands/check.py`](../../src/archon_horizon/commands/check.py))
+
+- `horizon check [targets...] [--timeout <seconds>] [--json]`
+- `horizon check --lean <file> [--timeout <seconds>] [--json]`
+
 ---
 
 ## 4. Inbox & communication

docs/configuration/README.md

@@ -136,7 +136,7 @@ harnesses:
 | `options` | Backend-specific options — e.g. `effort` for Codex, or `config_dir` to pin auth/session home (`CLAUDE_CONFIG_DIR` / `CODEX_HOME`). |
 | `options.max_retries` | Transient API errors (rate limit, overload, 5xx, network) are retried with exponential backoff. Default `2` (i.e. 3 attempts); set `0` to disable. A usage/billing limit is never retried — it's labelled and surfaced. |
 | `options.retry_base_seconds` | Base backoff delay in seconds for the retry above (default `8`; doubles each attempt). |
-| `options.inbox_hooks` | Model-visible protection/conversation checkpoints for Claude Code and Codex (default `true`). Horizon injects new messages after the next tool boundary, reminds every five tool calls while attention remains open, pauses a commit for an unread direct conversation, and continues `Stop` once if one remains unread. Set `false` for an older or policy-locked engine. |
+| `options.inbox_hooks` | Model-visible lifecycle checkpoints for Claude Code and Codex (default `true`). Horizon injects new messages after the next tool boundary, reminds periodically while attention remains open, pauses a commit for an unread direct conversation, and continues headless `Stop` once when conversations, uncommitted durable changes, or the final report still need attention. The second Stop always succeeds to prevent a loop. Set `false` for an older or policy-locked engine. |
 
 Codex requires command hooks to be reviewed or explicitly trusted. Horizon's
 hook definition is a constant supplied on the engine command line, so

docs/dashboard-and-search/README.md

@@ -7,6 +7,7 @@ Archon Horizon includes both an interactive Single Page Application (SPA) dashbo
 ## Table of Contents
 
 - [1. Live Web Dashboard Server](#1-live-web-dashboard-server)
+  - [Native Agent & Context Telemetry](#native-agent--context-telemetry)
   - [Clickable Local-Reference Chips](#clickable-local-reference-chips)
   - [Board View (`/board`)](#board-view-board)
   - [Commit Resolution API & Log Ordering](#commit-resolution-api--log-ordering)
@@ -48,6 +49,22 @@ The server is implemented in [`server/app.py`](../../src/archon_horizon/server/a
 - **Inbox Management**: Directly review, triage, and comment on workspace inbox hints and issues.
 - **Clickable reference chips**: Ids and commit SHAs mentioned anywhere in rendered text become links that jump straight to the entity (see [Clickable Local-Reference Chips](#clickable-local-reference-chips)).
 
+### Native Agent & Context Telemetry
+
+Headless Codex stores each native subagent in a separate rollout file. Horizon
+tails those files while the parent is running, reconstructs parent/child and
+nested relationships from spawn provenance, and renders role, nickname, model,
+depth, duration, and terminal status in the same transcript tree used for other
+engines. A child that disappears without a completion record is shown as
+orphaned rather than silently left running.
+
+Codex token-count records distinguish current-request input, cached input,
+cumulative session input, and the model context window; native automatic or
+manual compactions are separate events. Since Codex emits a token-count record
+after nearly every model step, the transcript displays only the newest context
+snapshot. The complete append-only history remains on disk, while the latest
+snapshot and compaction count remain available in session details.
+
 ### Clickable Local-Reference Chips
 
 Rendered prose across the dashboard — inbox bodies, commit messages, session reports, roadmap summaries, and comments — now turns bare references to local entities into clickable, hoverable tag chips that navigate to the matching view. Recognized tokens are roadmap item ids, task ids, inbox ids, blueprint/hgraph node keys, and commit SHAs.

src/archon_horizon/__init__.py

@@ -5,4 +5,4 @@
 # Single source of truth for the package version. ``pyproject.toml`` reads this
 # attribute via setuptools' dynamic version. ``scripts/version.py`` treats this
 # value as authoritative and synchronizes the other checked-in surfaces.
-__version__ = "0.1.2"
+__version__ = "0.1.3"

src/archon_horizon/agents/harness_agents.py

@@ -58,7 +58,12 @@ def _agent_env(role: str, context: HorizonContext) -> dict[str, str]:
     Horizon agent runs from its project dir), and the task/projects so a raw ``git``
     commit the agent makes into the ledger carries full provenance trailers (stamped
     by the ledger's prepare-commit-msg hook)."""
-    env = {"ARCHON_HORIZON_AGENT_ROLE": role}
+    env = {
+        "ARCHON_HORIZON_AGENT_ROLE": role,
+        # A headless run may be launched from an interactive Horizon shell. Do not
+        # inherit that parent's marker or Stop would skip the final-report guard.
+        "ARCHON_HORIZON_INTERACTIVE": "0",
+    }
     env["ARCHON_HORIZON_ROOT"] = str(context.workspace.root.resolve())
     env["ARCHON_HORIZON_SKILL"] = str(
         (context.workspace.root / ".claude" / "skills" / "horizon" / "SKILL.md").resolve()
@@ -206,4 +211,3 @@ def run_task(self, context: HorizonContext) -> HorizonResult:
             artifact_refs=result.artifact_refs,
             metadata=_result_metadata(result),
         )
-

src/archon_horizon/cli.py

@@ -17,7 +17,9 @@
 
 from archon_horizon import __version__
 from archon_horizon.commands import blueprint as blueprint_cmd
+from archon_horizon.commands import check as check_cmd
 from archon_horizon.commands import agent_hook as agent_hook_cmd
+from archon_horizon.commands import attempt as attempt_cmd
 from archon_horizon.commands import dashboard as dashboard_cmd
 from archon_horizon.commands import discuss as discuss_cmd
 from archon_horizon.commands import freeze as freeze_cmd
@@ -142,6 +144,7 @@ def callback(
 app.add_typer(project_cmd.app, name="project")
 app.add_typer(freeze_cmd.app, name="freeze")
 app.add_typer(skills_cmd.app, name="skills")
+app.add_typer(attempt_cmd.app, name="attempt")
 app.command("blueprint")(blueprint_cmd.blueprint)
 app.command(
     "graph",
@@ -156,6 +159,7 @@ def callback(
 app.command("search")(search_cmd.search)
 app.command("sync")(sync_cmd.sync)
 app.command("usage")(usage_cmd.usage)
+app.command("check")(check_cmd.check)
 app.command("permissions")(permissions_cmd.permissions)
 app.command("ps")(ps_cmd.ps)
 app.command("dashboard")(dashboard_cmd.dashboard)