AutoArchon is a Codex-first Lean 4 proving system for long-running benchmark and formalization campaigns. It keeps the inner plan -> prover -> review loop, then adds an outer control plane for operator guidance, watchdog recovery, proof export, postmortem archiving, and lesson accumulation.
For comment-only formalization and open-problem inputs, acceptance is no longer based on "it compiles and changed a file" alone. The autoformalize stage now has to preserve the stated mathematical objects and constraints through a formalization contract, so a weaker surrogate definition will stay in attention/needs_relaunch instead of being finalized as a proof.
The recommended outer path is now interactive:
interactive campaign-operator -> mission brief + resolved spec + operator journal -> watchdog -> orchestrator-agent -> supervisor-agent
campaign-operatoris the only user-facing outer owner name.watchdogis the mechanical reliability wrapper around the orchestrator.teachermeans the Codex session that carries onesupervisor-agent; it is not a separate logical runtime role.manager-agentis not part of the default runtime path. The archived future note lives in docs/archive/manager-agent.md.
flowchart TD
H[Human] --> OP[interactive campaign-operator]
OP --> BRIEF[control/mission-brief.md]
OP --> SPEC[control/launch-spec.resolved.json]
OP --> JOURNAL[control/operator-journal.md]
SPEC --> WD[watchdog]
WD --> ORCH[orchestrator-agent]
ORCH --> RUNS[runs/<id>/]
RUNS --> CTRL[control/launch-teacher.sh]
CTRL --> TEACHER[teacher Codex session]
TEACHER --> SUP[supervisor-agent]
SUP --> LOOP[autoarchon-supervised-cycle]
LOOP --> PLAN[plan-agent]
PLAN --> PROVER[prover-agent]
PROVER --> REVIEW[review-agent]
PROVER --> VALIDATOR[statement-validator]
PROVER -. optional bounded help via runtime-config.toml .-> HELPER[helper-prover-agent]
VALIDATOR --> FINAL[reports/final/]
WD --> POST[reports/postmortem/]
FINAL --> LESSONS[reports/final/lessons/lesson-records.jsonl]
POST --> POSTLESSONS[reports/postmortem/lessons/lesson-records.jsonl]
LESSONS -. future retrieval .-> MATHLIB[mathlib-agent]
git clone <your-fork-or-upstream-url>
cd AutoArchon
./setup.sh
uv sync --all-groups
bash scripts/install_repo_skill.shsetup.sh verifies uv, elan, lean, lake, and codex. After installing repo skills, start a fresh Codex session so $archon-orchestrator and $archon-supervisor are available.
Use GitHub as the primary source of truth for code and the HF datasets as the migration/failover bundle for local config, curated campaign state, and operator session archives.
The current recovery runbook lives in docs/migration-recovery.md. It covers:
- downloading the public and private HF dataset bundles
- verifying checksums and decrypting
*.gpgarchives - restoring
examples/helper.env, curatedruns/campaigns/, and Codex session archives - re-cloning pinned upstream benchmark repos from
manifests/repo-lock.json - validating the rebuilt host with
uv,lean, helper healthcheck, and a launch-contract probe
Minimal entrypoint:
hf download Garydesu/AutoArchon_Public --repo-type dataset --local-dir /path/to/restore/hf-public
hf download Garydesu/AutoArchon_Private --repo-type dataset --local-dir /path/to/restore/hf-privateThis is the main user path.
- Create the local helper env once:
cp /path/to/AutoArchon/examples/helper.env.example /path/to/AutoArchon/examples/helper.env
$EDITOR /path/to/AutoArchon/examples/helper.envscripts/start_campaign_operator.sh and scripts/start_fate_overnight_watchdogs.sh will auto-load examples/helper.env when it exists, so later launches inherit helper and progress-surface defaults without extra shell setup.
For the direct interactive Codex path below, load it yourself with source examples/helper.env.
For ARCHON_HELPER_API_KEY_ENV and ARCHON_HELPER_BASE_URL_ENV, you may provide either existing environment-variable names such as OPENAI_API_KEY / OPENAI_BASE_URL, or direct inline values. Generated teacher launchers normalize inline values back into provider-default env vars before init.sh and codex exec, so future run workspaces avoid storing secrets as literal runtime-config values.
Run a bounded probe once after editing it so helper failures surface before a long campaign:
uv run --directory /path/to/AutoArchon autoarchon-helper-healthcheck \
--env-file /path/to/AutoArchon/examples/helper.envIf your provider is intentionally OpenAI-compatible but serves non-OpenAI models, that can be fine, but autoarchon-validate-launch-contract --probe-helper will still tell you whether the transport actually works.
- Prepare benchmark clones under one root, for example:
/path/to/benchmarks/FATE-M-upstream
/path/to/benchmarks/FATE-H-upstream
/path/to/benchmarks/FATE-X-upstream
- Load helper env and start an interactive Codex session directly:
cd /path/to/AutoArchon
source examples/helper.env
codex -C /path/to/AutoArchon --model gpt-5.4 --config "model_reasoning_effort=xhigh"-
Fill the prompt template in docs/templates/campaign-operator-prompt-template.md, then paste it into the interactive Codex session.
-
Let
campaign-operatordo the intake work. A good first message is:
Use $archon-orchestrator to own this AutoArchon campaign.
Repository root: /path/to/AutoArchon
Source root: /path/to/benchmarks/FATE-M-upstream
Campaign root: /path/to/runs/campaigns/20260414-fate-m-full
Reuse lake from: /path/to/benchmarks/FATE-M-upstream
Real user objective:
- run a benchmark-faithful FATE-M campaign
- keep helper enabled unless the benchmark contract forbids it
- use single-file or micro-shard teachers
- ask intake questions if scope, regex, success criteria, or monitoring policy is unclear
The operator should then:
- turn that intake into
control/mission-brief.md - resolve
control/launch-spec.resolved.json - append the first decision block to
control/operator-journal.md - validate the contract before launch with
autoarchon-validate-launch-contract - only then launch or resume the watchdog
- If you want a deterministic intake scaffold before the operator reviews it, write the three control files in one shot:
uv run --directory /path/to/AutoArchon autoarchon-init-operator-intake \
--repo-root /path/to/AutoArchon \
--campaign-root /path/to/runs/campaigns/20260414-fate-m-full \
--source-root /path/to/benchmarks/FATE-M-upstream \
--objective "Run a benchmark-faithful FATE-M campaign on the warmed local clone." \
--campaign-mode benchmark_faithful \
--match-regex '^FATEM/.*\\.lean$' \
--shard-size 8 \
--run-id-prefix teacher-mThis writes:
control/mission-brief.mdcontrol/launch-spec.resolved.jsoncontrol/operator-journal.md
The interactive operator should still review and refine that intake bundle before unattended launch.
- Validate the launch contract explicitly when you want a deterministic preflight:
uv run --directory /path/to/AutoArchon autoarchon-validate-launch-contract \
--campaign-root /path/to/runs/campaigns/20260414-fate-m-full \
--probe-helper- The operator should leave behind these three files before the watchdog starts:
control/mission-brief.mdcontrol/launch-spec.resolved.jsoncontrol/operator-journal.md
If you prefer a thin shell wrapper that auto-loads examples/helper.env and pins the default model/reasoning settings, keep using:
ARCHON_ROOT=/path/to/AutoArchon \
MODEL=gpt-5.4 \
REASONING_EFFORT=xhigh \
bash /path/to/AutoArchon/scripts/start_campaign_operator.shscripts/start_campaign_operator.sh is only a convenience wrapper now. The primary path is direct interactive codex.
If you want a fully rendered, paste-ready prompt instead of free-form intake, use the prompt renderer.
- Generate a paste-ready operator prompt:
uv run --directory /path/to/AutoArchon autoarchon-render-operator-prompt \
--repo-root /path/to/AutoArchon \
--source-root /path/to/benchmarks/FATE-M-upstream \
--campaign-root /path/to/runs/campaigns/20260414-fate-m-full \
--reuse-lake-from /path/to/benchmarks/FATE-M-upstream \
--template /path/to/AutoArchon/campaign_specs/fate-m-full.json \
--match-regex '^FATEM/.*\\.lean$' \
--shard-size 8 \
--run-id-mode index \
--run-id-prefix teacher-m- Paste the rendered prompt into the interactive Codex session. It will look like:
Use $archon-orchestrator to own this AutoArchon campaign.
Repository root: /path/to/AutoArchon
Source root: /path/to/benchmarks/FATE-M-upstream
Campaign root: /path/to/runs/campaigns/20260414-fate-m-full
Reuse lake from: /path/to/benchmarks/FATE-M-upstream
Helper env file: /path/to/AutoArchon/examples/helper.env
Match regex: '^FATEM/.*\\.lean$'
Shard size: 8
Run id mode: index
Before launching anything:
- create or refresh `control/mission-brief.md`
- create or refresh `control/launch-spec.resolved.json`
- append the initial decision to `control/operator-journal.md`
- keep helper enabled by default unless the run contract explicitly forbids it
Then:
- launch or resume the watchdog
- monitor progress
- prefer deterministic recovery commands
- finalize only validation-backed proofs and blockers
Control-plane commands are terminal commands for machine-readable state. They are not the web UI. The file-backed summaries are the canonical observability surface for long campaigns; the browser UI is supplementary inspection only.
For a quick loop:
bash scripts/watch_campaign.sh /path/to/runs/campaigns/20260414-fate-m-fullFor a one-shot snapshot:
uv run --directory /path/to/AutoArchon autoarchon-campaign-overview \
--campaign-root /path/to/runs/campaigns/20260414-fate-m-full \
--markdownFor a lightweight browser mirror that keeps refreshing the same canonical files:
uv run --directory /path/to/AutoArchon autoarchon-campaign-observe \
--campaign-root /path/to/runs/campaigns/20260414-fate-m-full \
--bind 0.0.0.0 \
--port 8765That command also refreshes these lightweight observability surfaces by default:
control/progress-summary.mdcontrol/progress-summary.jsoncontrol/progress-summary.html
The campaign summary is the canonical observability surface: control/progress-summary.json is the source of truth, control/progress-summary.md is the terminal-friendly mirror, and control/progress-summary.html is a browser-friendly supplementary inspection page generated from the same payload. autoarchon-campaign-observe only refreshes and serves those same files; it does not create a second state store. Together they now show ETA, restart count, active runs, recent finalized targets, a ranked operator queue, and a lightweight likelyBottleneck risk summary. Each run also keeps workspace/.archon/supervisor/progress-summary.{md,json} with live phase, active prover rows, helper-note breakdowns, and task-result kind counts.
Each run also writes runs/<id>/control/helper-effective-config.json at launch time so helper provider/model/env binding mismatches can be diagnosed without opening the shell wrapper.
The optional web UI remains useful for supplementary inspection of one run:
bash ui/start.sh --project /path/to/run-root/workspaceFor a single run without the campaign layer:
bash scripts/watch_run.sh /path/to/run-root/workspaceAfter autoarchon-finalize-campaign, use these paths:
- Final accepted proofs:
reports/final/proofs/<run-id>/<rel-path>.lean - Final accepted formalization scaffolds:
reports/final/formalizations/<run-id>/<rel-path>.lean - Final accepted blocker notes:
reports/final/blockers/<run-id>/<file>.md - Final validation payloads:
reports/final/validation/<run-id>/<rel-path_escaped>.json
acceptedFormalizations means the run preserved the source object faithfully and landed a validated declaration scaffold, but it is not counted as a completed mathematical proof. Run-level artifacts/proofs/ may still contain intermediate edited files from partial-progress or blocker runs. Treat reports/final/ as the acceptance boundary.
For comment-only/open-problem autoformalization, the live declaration contract now lives at runs/<id>/workspace/.archon/formalization/<rel-path-with-slashes-replaced>.json, and the matching live route note lives at runs/<id>/workspace/.archon/informal/<rel-path-with-slashes-replaced-and-.lean-removed>-autoformalize.md. If a run weakens the mathematical object, the control plane reopens the run and reroutes from those live assets instead of treating the compileable surrogate as accepted.
If you already know the exact scope and just want a reproducible shortcut, keep using the spec path.
Generate a resolved launch spec from a tracked template:
uv run --directory /path/to/AutoArchon autoarchon-init-campaign-spec \
--template /path/to/AutoArchon/campaign_specs/fate-m-full.json \
--benchmark-root /path/to/benchmarks \
--campaigns-root /path/to/runs/campaigns \
--run-specs-root /path/to/runs/campaigns/_run_specs \
--date-tag 20260414-nightly \
--model gpt-5.4 \
--reasoning-effort xhighThen launch:
uv run --directory /path/to/AutoArchon autoarchon-launch-from-spec \
--spec-file /path/to/runs/campaigns/_run_specs/20260414-nightly-fate-m-full.launch.jsonFor formalization or open-problem style runs, use the generic source-root flag and the non-benchmark template:
uv run --directory /path/to/AutoArchon autoarchon-init-campaign-spec \
--template /path/to/AutoArchon/campaign_specs/formalization-default.json \
--source-roots-root /path/to/source-roots \
--source-subdir riemann-upstream \
--campaign-slug riemann-local-formalization \
--campaigns-root /path/to/runs/campaigns \
--run-specs-root /path/to/runs/campaigns/_run_specs \
--date-tag 20260414-open \
--model gpt-5.4 \
--reasoning-effort xhighFor a pure open-problem campaign, swap the template:
uv run --directory /path/to/AutoArchon autoarchon-init-campaign-spec \
--template /path/to/AutoArchon/campaign_specs/open-problem-default.json \
--source-roots-root /path/to/source-roots \
--source-subdir riemann-upstream \
--campaign-slug riemann-open-problem \
--campaigns-root /path/to/runs/campaigns \
--run-specs-root /path/to/runs/campaigns/_run_specs \
--date-tag 20260414-open \
--model gpt-5.4 \
--reasoning-effort xhigh--source-subdir lets one generic root hold many warmed Lean project clones, and --campaign-slug decouples the campaign name from the tracked template name.
If your upstream source is a JSON problem pack with informal_statement and formal_statement fields, materialize a standard Lean source root first. This is the current bridge from FATE-X.json style data into the operator path:
uv run --directory /path/to/AutoArchon autoarchon-materialize-problem-pack \
--input-json /path/to/benchmarks/FATE-X-upstream/FATE-X.json \
--output-root /path/to/benchmarks/Natural-language/fatex-natural-smoke \
--problem-id 1 \
--problem-id 2 \
--forceThat command writes a self-contained Lean root with lakefile.lean, lean-toolchain, per-problem .lean files, QUESTIONS.md, and problem-pack.json. You can then point autoarchon-init-campaign-spec or autoarchon-init-operator-intake at that generated source root exactly like any other non-benchmark formalization project.
If your upstream source is a markdown question table such as Questions.md from an open-problem note pack, materialize a declaration-free Lean source root instead:
uv run --directory /path/to/AutoArchon autoarchon-materialize-markdown-problem-pack \
--questions-markdown /path/to/benchmarks/Open-problem/motivic-flag-maps/Questions.md \
--output-root /path/to/benchmarks/Open-problem-generated/motivic-flag-maps-q1 \
--problem-id 1 \
--forceThis writes comment-only .lean files with no declarations yet. That is intentional: the generated project enters autoformalize stage truthfully, so the run starts by formalizing a declaration from the informal question instead of pretending a theorem statement already exists.
That template enables route reuse by default:
{
"preloadHistoricalRoutes": true
}preloadHistoricalRoutes enables --preload-historical-routes in generated teacher assets, which seeds accepted proof and blocker routes from older finalized campaigns into the new run. This is useful for non benchmark-faithful formalization, open-problem exploration, and repeated engineering campaigns because the system starts from its own validated prior knowledge instead of a cold start.
Keep it off for benchmark-faithful evaluation runs, because it intentionally reuses prior accepted .archon knowledge and therefore changes the measurement boundary.
For the bundled nightly three-campaign shortcut:
export MODEL=gpt-5.4
export REASONING_EFFORT=xhigh
export BENCHMARK_ROOT=/path/to/benchmarks
export CAMPAIGNS_ROOT=/path/to/runs/campaigns
export RUN_SPECS_ROOT=/path/to/runs/campaigns/_run_specs
export FATE_DATE_TAG=$(date +%Y%m%d-nightly)
bash scripts/start_fate_overnight_watchdogs.shFor one isolated run without the full campaign layer, go straight to $archon-supervisor and docs/operations.md.
uv run --directory /path/to/AutoArchon autoarchon-supervised-cycle \
--workspace /path/to/run-root/workspace \
--source /path/to/run-root/source \
--plan-timeout-seconds 180 \
--prover-timeout-seconds 240 \
--tail-scope-objective-threshold 4 \
--tail-scope-plan-timeout-seconds 300 \
--tail-scope-prover-timeout-seconds 360 \
--prover-idle-seconds 90 \
--no-reviewSingle-run progress lands in:
workspace/.archon/supervisor/progress-summary.mdworkspace/.archon/supervisor/progress-summary.json
Campaign-level browser inspection lands in:
control/progress-summary.html
In the exact-route tail-scope case, those files now tell you whether the planner was skipped intentionally:
planFastPathApplied = trueplanFastPathReason = "known_routes"- live
phase,planStatus,proverStatus, and active prover rows underliveRuntime
Each initialized workspace now gets:
.archon/runtime-config.toml.archon/tools/archon-helper-prover-agent.py.archon/tools/archon-informal-agent.py
runtime-config.toml is the canonical runtime policy file. The easiest path is to seed it from env before init.sh:
cp /path/to/AutoArchon/examples/helper.env.example /path/to/AutoArchon/examples/helper.env
$EDITOR /path/to/AutoArchon/examples/helper.env
source /path/to/AutoArchon/examples/helper.env
./init.sh /path/to/lean-projectIf you launch through scripts/start_campaign_operator.sh or scripts/start_fate_overnight_watchdogs.sh, that local examples/helper.env file is sourced automatically when present.
The example env uses:
ARCHON_HELPER_ENABLE=1
ARCHON_HELPER_PROVIDER=openai
ARCHON_HELPER_MODEL=gpt-5.4
ARCHON_HELPER_API_KEY_ENV=OPENAI_API_KEY
ARCHON_HELPER_BASE_URL_ENV=OPENAI_BASE_URLinit.sh writes those values into .archon/runtime-config.toml, which then becomes the durable per-workspace config surface. The generated file includes helper policy for both the plan and prover phases, note-reuse heuristics, and observability toggles such as write_progress_surface.
ARCHON_HELPER_API_KEY_ENV and ARCHON_HELPER_BASE_URL_ENV normally hold environment-variable names such as OPENAI_API_KEY and OPENAI_BASE_URL. If a local ignored examples/helper.env file stores literal values instead, the generated launcher normalizes them back into the provider-default bindings before it writes helper-effective-config.json.
OpenAI-compatible providers such as DeepSeek should still use provider = "openai" in .archon/runtime-config.toml, then point api_key_env and base_url_env at the compatible endpoint. Legacy .archon/helper-provider.json is still accepted as a fallback, but new workspaces should use the TOML file.
If you want bounded helper failover, add fallback transports explicitly:
[helper]
enabled = true
provider = "openai"
model = "deepseek-reasoner"
api_key_env = "DEEPSEEK_API_KEY"
base_url_env = "DEEPSEEK_BASE_URL"
[[helper.fallbacks]]
provider = "gemini"
model = "gemini-3.1-pro-preview"The helper wrapper will keep the primary transport first and only try the next configured provider when that call fails. Acceptance ownership still stays with the normal proof loop; helper output remains advisory only.
When the helper is enabled, use phase-aware auto note routing rather than ad hoc files:
.archon/tools/archon-helper-prover-agent.py \
--phase prover \
--rel-path FATEM/42.lean \
--reason lsp_timeout \
--prompt-pack auto \
--write-note auto \
"Prove the goal without residue calculus; stay within Lean 4 Mathlib."Use --phase plan for planner-side calls. --prompt-pack auto selects a task-class template from the phase and reason, so repeated failures, external-reference gaps, missing infrastructure, and LSP timeouts do not all hit the side model with the same generic wording. In auto note mode the wrapper writes a metadata-backed Markdown note into the configured notes_dir for that phase. Passing an explicit --write-note /path/to/file.md still works and keeps the old bare-text compatibility path.
By default, repeated calls with the same phase + file + reason will reuse the newest matching helper note instead of paying for the same side-model query again. Use --force-fresh-call only after the context has materially changed.
If the helper transport already failed for the same phase + file + reason + config, the wrapper now skips the repeated call until credentials, endpoint, or model change. This prevents plan/prover loops from burning cycles on identical provider-side outages.
- Mutable proof search happens only under
runs/<id>/workspace/. - Immutable originals stay under
runs/<id>/source/. - Per-run exported bundles live under
runs/<id>/artifacts/. - Campaign-level accepted outputs live under
reports/final/. - Archived stopped or degraded samples live under
reports/postmortem/.
Concrete paths:
- live edited theorem file:
runs/<id>/workspace/<rel-path>.lean - live task report:
runs/<id>/workspace/.archon/task_results/<rel-path-with-slashes-replaced>.md - live validation record:
runs/<id>/workspace/.archon/validation/<rel-path-with-slashes-replaced>.json - live formalization contract:
runs/<id>/workspace/.archon/formalization/<rel-path-with-slashes-replaced>.json - live autoformalize route note:
runs/<id>/workspace/.archon/informal/<rel-path-with-slashes-replaced-and-.lean-removed>-autoformalize.md - exported per-run proof bundle:
runs/<id>/artifacts/proofs/<rel-path> - exported per-run accepted formalization bundle:
runs/<id>/artifacts/proofs/<rel-path>with validationacceptedKind = formalization reports/final/proofs/<run>/reports/final/formalizations/<run>/reports/final/blockers/<run>/reports/final/validation/<run>/reports/final/lessons/lesson-records.jsonlreports/final/lessons/lesson-clusters.jsonreports/final/lessons/lesson-clusters.mdreports/final/lessons/lesson-reminders.jsonreports/final/lessons/lesson-reminders.mdreports/final/runs/<run>/run-summary.jsonreports/postmortem/postmortem-summary.jsonreports/postmortem/lessons/lesson-records.jsonlreports/postmortem/lessons/lesson-clusters.jsonreports/postmortem/lessons/lesson-clusters.mdreports/postmortem/lessons/lesson-reminders.jsonreports/postmortem/lessons/lesson-reminders.md
For mathematician review, prefer exported proofs and validation-backed artifacts under artifacts/ or reports/final/, not the live workspace alone.
For debugging an active teacher, inspect the live workspace first; for acceptance or human review after a run is done, prefer artifacts/ and reports/final/.
To rebuild lesson hotspots manually:
uv run --directory /path/to/AutoArchon autoarchon-lesson-clusters \
--campaign-root /path/to/runs/campaigns/20260414-fate-m-full \
--markdownTo audit helper usage, repeated helper failures, and per-campaign lesson context before changing helper policy:
uv run --directory /path/to/AutoArchon autoarchon-helper-analysis \
--campaign-root /path/to/runs/campaigns/20260415-rerun12-fatem-42-45-94 \
--campaign-root /path/to/runs/campaigns/20260415-183503-motivic-flag-maps-q1-fixed-open-problem \
--markdownAdd --write-default-files to write helper-analysis.json and helper-analysis.md under the campaign's default diagnostics root, which is reports/postmortem/helper-analysis/ for archived samples and reports/final/helper-analysis/ for finalized samples.
If the working tree grows very large, the usual culprit is rebuildable Lean caches under runs/**/workspace/.lake or older standalone run roots with a top-level .lake, not the repo itself.
Audit first:
uv run --directory /path/to/AutoArchon autoarchon-storage-report \
--root /path/to/math/runs \
--markdownFor a top-level retention view across runs, benchmarks, temp roots, and legacy workspaces:
uv run --directory /path/to/AutoArchon autoarchon-storage-report \
--root /path/to/math \
--retention \
--markdownBy default, the retention report treats canonical benchmark clones under benchmarks/ as shared Lean projects to keep, not disposable run roots.
That is also the current shared-build strategy: campaigns should reuse a warmed benchmark clone via --reuse-lake-from, while clone-level .lake deduplication stays out of scope until there is a documented rehydrate path.
Dry-run a safe reclaim plan:
uv run --directory /path/to/AutoArchon autoarchon-storage-report \
--root /path/to/math/runs \
--prune-workspace-lake \
--prune-broken-prewarmExecute the same plan:
uv run --directory /path/to/AutoArchon autoarchon-storage-report \
--root /path/to/math/runs \
--prune-workspace-lake \
--prune-broken-prewarm \
--executeThis only targets cache-heavy workspace/.lake directories on inactive runs plus broken .lake.prewarm-* directories. It does not delete exported proofs, validation artifacts, or final reports.
The report now also distinguishes stale active leases from genuinely protected live runs, which makes overnight cleanup much easier to trust.
For future unattended runs, the terminal path can prune automatically too:
uv run --directory /path/to/AutoArchon autoarchon-orchestrator-watchdog \
--campaign-root /path/to/campaign-root \
--prune-workspace-lake \
--prune-broken-prewarmautoarchon-finalize-campaign and autoarchon-campaign-archive expose the same two flags. The tracked FATE full-campaign templates now opt into that explicit post-terminal prune so overnight runs do not keep historical workspace/.lake caches by default.
AutoArchon/
├── agents/
├── archonlib/
├── campaign_specs/
├── docs/
├── scripts/
├── skills/
├── tests/
└── ui/
agents/: explicit runtime and future role contracts.archonlib/: control-plane and runtime library code.campaign_specs/: tracked benchmark launch templates.scripts/: publicuv runentrypoints and operator shell wrappers.skills/: repo-owned Codex skills for outer-owner and teacher sessions.docs/: architecture, operations, operator workflow, and archive notes.tests/: runtime, CLI, watchdog, docs-contract, and registry coverage.
- docs/campaign-operator.md: recommended interactive operator workflow, control files, recovery, and closeout.
- docs/templates/campaign-operator-prompt-template.md: fill-in prompt template for the direct interactive Codex path.
- docs/architecture.md: global workflow, state surfaces, artifact boundaries, and extension points.
- docs/operations.md: single-run operational baseline, prewarm, soak-test commands.
- docs/teacher-agents.md: one-run-per-teacher launch and monitoring.
- docs/agent-registry.md: runtime role contracts and future role notes.
- docs/roadmaps/control-plane-phase7.md: launch-contract validation, operator intake, helper budgeting, reminders, and mathlib research skeleton.
- docs/roadmaps/control-plane-phase6.md: next-phase plan for operator productization, helper policy, observability, and knowledge capture.
- docs/roadmaps/control-plane-phase5.md: current unattended-phase roadmap and remaining high-ROI work.
- docs/postmortem-20260415-rerun12-fatem-42-45-94.md: fresh finalized rerun evidence on the hardened path.
- docs/archive/manager-agent.md: archived note for the future multi-campaign policy role.