--- name: bedc-codex-auto-dev description: Start and monitor the BEDC paper revision and Lean formalization Codex pipelines on the shared codex-auto-dev integration branch. allowed-tools: Bash, Monitor --- # BEDC shared Codex pipelines Use this skill when the user asks to run both BEDC Codex pipelines together, to use `codex-auto-dev`, or to monitor paper and Lean automation on one shared branch. ## Unattended operation (default mode) **This skill operates UNATTENDED.** The operator has long sessions running the pipeline and explicitly does not want to be paged for every routine decision. Default to autonomous action; only escalate for decisions that change policy or scope. **NEVER use AskUserQuestion / interactive popups in this skill.** Unattended means there is no one watching to click. A popup blocks the loop and is forbidden. For any decision: - If it's in autonomous scope (mechanical fix, prompt/lint/critical_path edit, hot-reloadable change, free-restart daemon) → just do it and report what you did. - If it's operator-scope (the items under "Operator-scope" below: concurrency/resource budget, orchestrator restart, destructive ops, architecture/topology) → do NOT pop a question and do NOT block. Instead: **take the safe default** (usually: leave it untouched / defer to the operator's other codex-led system) and surface the decision as **one or two sentences in your normal text reply** ("X is operator-scope — left untouched; if you want it changed, say so"). The operator reads the transcript asynchronously and will tell you in a later turn. Continue the loop without waiting. - Concurrency / `.pipeline_parallel.json` keys specifically are owned by the operator's external codex-led system — never edit them, never popup about them; just report the observation. ### Auto-fix without asking When you detect a concrete bug or gap from monitor events, CI logs, sync daemon failures, or worker output, and the fix path is mechanical: - **Dispatch codex to implement** the fix in an isolated worktree - **Verify locally** (lake build / bedc_ci.py audit / axiom-purity --strict per applicable scope) - **Merge + push** to `codex-auto-dev` (use `LEAN4_GUARDRAILS_BYPASS=1 git push` to bypass the lean push guardrail — it's a `policy=ask` gate the operator has implicitly cleared by running this skill) - **Clean up worktrees** after merge Do NOT pause to ask "should I dispatch?" / "should I push?" / "should I cleanup?" when the next step is forced by the previous output. Report what you did, not what you're about to do. Examples of issues to auto-fix without confirmation: - Latent infra bugs detected during a status check (merge driver pollution, regen race, stale-state artifacts) - CI failures with a known root cause (missing gate in `bedc_ci.py audit`, stale `.gitattributes`, preamble dup detector gaps) - Sync daemon retry loops caused by a fixable working-tree pollution pattern - Pre-merge gate gaps where a check exists in `make precheck` / `make warn` but isn't in `bedc_ci.py audit` (the orchestrator's only hook) ### Operator-scope (defer + report in text — NEVER popup-ask) These are NOT in autonomous scope. In unattended mode you do NOT act on them unilaterally AND you do NOT pop a question — you take the safe default (leave untouched / defer to the operator's external system) and note it in one sentence in your text reply so the operator can decide later: - **Concurrency / resource budget** — `.pipeline_parallel.json` keys (`paper` / `lean` / `lean_lake` / timeouts). Owned by the operator's external codex-led system. Never edit, never popup. Under memory pressure (e.g. swap-saturation stalling lean's heavy lake-merge), report the diagnosis + that concurrency reduction is the lever, but leave the file to the operator's system. - **Restart decisions** — orchestrator restart loses in-flight workers (~15 worker × 5-15min each). EXCEPTION (still autonomous): restart is in scope when an orchestrator-body change you just shipped needs it, or the pipeline has wedged >30min — then restart without asking. `auto_heal` / `autotune` / `sync` daemons restart freely. - **Architecture choices** — lock-split vs integrator topology, branch-topology changes. Report a recommendation; don't enact a topology change unprompted. - **Anything destructive** — `git push --force`, `git reset --hard origin/...`, deleting non-cleanup worktrees, killing in-flight workers. (Force-killing a wedged/deadlocked orchestrator for a restart is the sanctioned exception, per "manual BASE surgery #2".) ### Pattern stays: analyze → fix → verify The analysis-codex → fix-codex → operator-verifies workflow is unchanged. Unattended mode only removes the "ask before each step" interruptions, not the structural rigor. Always: 1. Read-only analysis codex in isolated worktree (output to `/tmp/`) 2. Operator (you) reads analysis briefly, decides whether mechanical or policy 3. If mechanical: dispatch implementation codex with terse file-whitelisted prompt 4. Operator verifies locally (lake build / audit / axiom-purity per scope) BEFORE merge 5. Merge + push + cleanup If verification fails post-codex, drop the change (don't ship partial). Re-dispatch or escalate. ### Memory: record validated autonomous-action patterns When the operator confirms a non-obvious autonomous action was the right call (e.g. "yes, just fix it" / "for issues like this, don't ask"), save it as a `feedback` memory so future sessions don't re-litigate the same decision. Don't save individual fix transcripts — save the *class* of fix that's been pre-authorized. ## Path convention All shell commands in this skill use `$REPO` as the repo root. Set it once per shell session before running any commands: ```bash export REPO="$(git rev-parse --show-toplevel)" ``` Every subsequent `python3 $REPO/...` / `tail $REPO/...` / `mkdir $REPO/...` then resolves correctly regardless of the user's current working directory or machine layout. ## Branch Always use: ```bash --base-branch codex-auto-dev ``` Do not pass `--peer-branch` to the paper script in this mode. Both pipelines merge directly into the same integration branch. ## Preflight Before starting anything, check whether matching processes are already running: ```bash ps -axo pid,ppid,pgid,stat,etime,command | grep -E 'codex_revise.py|codex_formalize.py' | grep -v grep ``` Then check both pipeline statuses: ```bash python3 $REPO/papers/bedc/scripts/codex_revise.py --base-branch codex-auto-dev --status python3 $REPO/lean4/scripts/codex_formalize.py --base-branch codex-auto-dev --status ``` If either pipeline is already running on `codex-auto-dev`, do not start a duplicate. Report what is already running and monitor it instead. ## Start (background, detached) **Always launch the orchestrators as fully-detached background processes — never inside a `Monitor` and never piped through anything that the harness owns.** The orchestrator must outlive any Claude Code session, Monitor swap, or filter change. Use `nohup … &` plus `disown` so the process re-parents to PID 1 and survives shell exit. Use the `Bash` tool. Do **not** also pass `run_in_background: true` — `nohup … &` + `disown` already detaches; double-backgrounding only confuses cleanup. Paper: ```bash mkdir -p $REPO/papers/bedc/scripts/logs && \ nohup bash -c ' python3 $REPO/papers/bedc/scripts/codex_revise.py \ --base-branch codex-auto-dev --resume && \ python3 $REPO/papers/bedc/scripts/codex_revise.py \ --base-branch codex-auto-dev --continuous --peer-sync-interval 0 ' >> $REPO/papers/bedc/scripts/logs/orchestrator.log 2>&1 & disown ``` Lean: ```bash mkdir -p $REPO/lean4/scripts/logs && \ nohup python3 $REPO/lean4/scripts/codex_formalize.py \ --base-branch codex-auto-dev --continuous \ --phase-b-timeout 3600 --phase-c-timeout 4500 \ >> $REPO/lean4/scripts/logs/orchestrator.log 2>&1 & disown ``` Rollup sync daemon (third default-launched component): ```bash mkdir -p $REPO/scripts/logs && \ nohup bash -c ' while true; do python3 $REPO/tools/sync_with_auto_dev.py 2>&1 \ | sed "s/^/[sync] /" sleep 600 done ' >> $REPO/scripts/logs/sync_daemon.log 2>&1 & disown ``` The sync daemon runs `tools/sync_with_auto_dev.py` every 600s. Its default flow maintains the managed rollup PR from `codex-auto-dev` into `dev`: build a candidate from `origin/dev`, merge `origin/codex-auto-dev`, update the managed rollup branch, open or refresh the PR, and merge it once GitHub reports green checks and a mergeable state. Use the script's `--source-branch`, `--target-branch`, and `--rollup-branch` options only when the operator wants a non-default rollup pair. Keep this daemon on a low-frequency loop; do not tighten the polling interval for routine operation. Concurrency autotune daemon (fourth default-launched component): ```bash mkdir -p $REPO/scripts/logs && \ nohup bash -c ' while true; do ts=$(date "+%Y-%m-%d %H:%M:%S") echo "[autotune] $ts tick" python3 $REPO/tools/auto_tune_concurrency.py 2>&1 sleep 300 done ' >> $REPO/scripts/logs/autotune_daemon.log 2>&1 & disown ``` `tools/auto_tune_concurrency.py` reads `critical_path.py` JSON output (top size, root_unblocks count) and resizes `.pipeline_parallel.json`'s `paper` / `lean` / `lean_lake` keys to match available work supply. Formula: `lean = clamp(top_size, 3, 15)` (no buffer — observed in 2026-05-06 session that `top_size + 3` caused chapter dogpile when supply was tight; multiple workers picked overlapping `BHist*_classifier_transport` neighbors and produced dup-decl lake-build failures); `paper = clamp(root_unblocks + 4, 3, 8)`; `lean_lake = clamp(lean // 5, 1, 3)`. Hot-reload — every round dispatch reads the JSON. Without autotune, static concurrency settings drift out of phase with the changing dep tree as paper rounds unlock chapters and oversubscribe lean workers, burning Phase B / lake build budget on collisions. BASE auto-heal daemon (fifth default-launched component): ```bash mkdir -p $REPO/scripts/logs && \ AUTO_HEAL_CI_POLL_FALLBACK=1 nohup python3 $REPO/tools/auto_heal_base.py >> $REPO/scripts/logs/auto_heal.log 2>&1 & disown ``` **`AUTO_HEAL_CI_POLL_FALLBACK=1` is REQUIRED in the launch** (operator directive 2026-06-04: auto_heal's core job is "whatever turns CI red, codex-fix until green"). Without it the daemon only acts on externally-registered CI watchers (`/tmp/auto_heal_ci_watchers.json`), which in practice are never created → it stays blind to CI reds (logs "CI watch callbacks clean" forever even while `BEDC Build` is failing). With it set, each cycle runs `detect_ci_failures(60min)` across the rollup observation family — `_ci_detection_branches()` = managed rollup branch (`rollup--to-`, host-derived isomorphically to sync's `_rollup_branch_name`), upstream `dev`, BASE `codex-auto-dev`, plus the retired read-only `auto-dev` for compatibility — → for each unseen failure `heal_ci_failure()` (dispatches codex with `gh run view --log-failed`) → `verify_then_push` onto BASE (`codex-auto-dev`), one heal per cycle, with an attempt-cap so a genuinely-unfixable run doesn't thrash codex forever. The failed run's branch is observation context only; the repair always lands on BASE content and is validated by the next rollup candidate the sync daemon rebuilds. BEDC Build runs on rollup-PR `pull_request` events and `dev` pushes — not on `codex-auto-dev` pushes — so the rollup branch is the primary red-signal source. `tools/auto_heal_base.py` runs every 15 min (`AUTO_HEAL_INTERVAL_SECONDS` env override, default 900s). Cycle: fetch + ff codex-auto-dev → run `bedc_ci.py audit` → if dup paper labels detected on BASE, invoke codex with `HEAL_DUP_LABELS_PROMPT` to delete the redundant copy (canonical-site rules: hub vs sibling, semantic stem matching) → then poll CI for failures and codex-heal them (per the flag above). Codex commits the cleanup directly on main checkout, daemon pushes to origin. Without this, a single duplicate-label commit on BASE stalls every subsequent round in audit-fail / SHALLOW-GROWTH cooldown loops indefinitely (observed 2026-05-06: 9 cooldowns × 180s + 36 SHALLOW lints over 30 min before manual surgery resolved). Skips when the working tree is dirty or branch isn't codex-auto-dev — never fights a human edit. Taste curator daemon (sixth default-launched component): ```bash mkdir -p $REPO/scripts/logs && \ nohup bash $REPO/tools/run_taste_curator.sh >> $REPO/scripts/logs/taste_curator.log 2>&1 & disown ``` `tools/run_taste_curator.sh` supervises `tools/taste_curator.py` with exponential backoff. The daemon runs every 60 min (`TASTE_CURATOR_INTERVAL_SECONDS` env override, default from `papers/bedc/taste_curator_config.json`) and keeps an `fcntl` lock on `/tmp/.bedc_taste_curator.pid`; a second daemon exits immediately when the lock is held. Cycle state lives in `/tmp/.bedc_taste_state.json`: MONITOR scans changed concrete-instance chapters and Derived carriers, appends review candidates to `/tmp/.bedc_taste_review_queue.jsonl`, and emits alerts without codex dispatch; ADJUST clusters queued auto-fixable findings and evolves one P/R automation rule; STABILIZE observes heal alerts, audit fail counts, orchestrator failed rate, and new taste alert categories before returning to MONITOR. `AUTO_FIX_WITHOUT_CONFIRMATION` defaults true because ADJUST edits only worker prompts and audit/lint gates, not chapter content; the daemon hot-loads the config on the next natural cycle. Rule evolution path: the daemon handles at most one cluster per cycle (`MAX_AUTO_FIXES_PER_CYCLE=1`). It creates `/tmp/wt-taste-evolve-*` on branch `taste/evolve--`, dispatches codex with the cluster evidence and a rule-evolution prompt, then accepts changes only under the whitelist: `papers/bedc/scripts/prompts/*.txt`, `lean4/scripts/prompts/*.txt`, `lean4/scripts/bedc_ci.py`, `papers/bedc/scripts/phase_paper_gates.py`, `lean4/scripts/phase_d_lint.py`, and `docs/dossier/taste-evolutions.qmd`. It rejects any edit under `papers/bedc/parts/concrete_instances/`, `lean4/BEDC/`, or the P/R orchestrator scripts. Verification is **smart baseline-vs-post audit comparison** (NOT unconditional `make check`): snapshot baseline `bedc_ci.py audit --json` before codex; after codex, compare fail-count keys; a new check key appearing is OK (this is the new gate the evolution added), an existing key's count going up is a regression and rejects, the audit script crashing rejects. `py_compile` of any touched Python is also required. Cleanup on success or failure does `git worktree remove --force` AND `git branch -D` (no orphan branches). Startup also GCs any leftover `taste/evolve-*` branches whose worktree directory is gone. Existing violations are not directly edited by the taste daemon. They are consumed organically when future P/R rounds touch the affected files: the new prompt rule or audit gate flags the pattern, then the orchestrator's post-rebase audit recovery invokes codex to repair the content as part of that round. Each successful rule evolution also **appends a Chinese section** to `docs/dossier/taste-evolutions.qmd` (Quarto page, rendered as part of the dossier site with navbar entry "Taste 演化") documenting 变更原因 / 意义 / 实施情况 / 元数据 — the visible self-improvement iteration log. Confirmed approvals in `papers/bedc/taste_approvals.json` use the same cluster rule-evolution path and are marked `done` or `failed` after the daemon attempt. No P/R orchestrator restart is needed because prompts are re-read each round and audit/lints run as subprocesses. Discovery pipeline daemon: ```bash mkdir -p $REPO/tools/logs && \ nohup python3 $REPO/tools/discovery_pipeline_daemon.py >> $REPO/tools/logs/discovery_pipeline_daemon.stdout.log 2>&1 & disown ``` `tools/discovery_pipeline_daemon.py` runs every 6h (`DISCOVERY_PIPELINE_INTERVAL_SECONDS` env override, default 21600s) under one PID lock at `/tmp/.bedc_discovery_pipeline.pid`. Each cycle builds/probes `structural_dna` once, then runs radar → refutation publisher → adversarial generator → gate evolver in one process. The stage implementations are still the existing `run_once` functions in `tools/discovery_radar_daemon.py`, `tools/discovery_refutation_publisher.py`, `tools/discovery_adversarial_generator.py`, and `tools/discovery_gate_evolver.py`; those scripts keep `--once` for debugging only. The generator writes `tools/logs/proven_pseudos.jsonl`, and the evolver reads that same file later in the same cycle, so proven pseudos do not wait for another 6h activation. Stage failures are logged in `tools/logs/discovery_pipeline_daemon.log` and do not stop later stages. ### Verify restart success (two-step, never skip) After launching, run **two sequential one-shot checks** before declaring the restart healthy. Skipping either check has bitten the operator. **Step 1 — process check:** ```bash ps -axo pid,ppid,pgid,etime,command | grep -E 'codex_revise.py|codex_formalize.py|sync_with_auto_dev.py|auto_tune_concurrency|auto_heal_base|taste_curator.py|discovery_pipeline_daemon.py' | grep -v grep ``` All seven launched processes (paper orchestrator, lean orchestrator, sync daemon, autotune daemon, auto-heal daemon, taste curator, discovery pipeline daemon) must be detached. For the non-supervised processes the python process should appear with `PPID=1`. The taste curator runs **under a supervisor wrapper** (`tools/run_taste_curator.sh`) so the bash supervisor has `PPID=1` and the python daemon is a child of the supervisor (look for both `run_taste_curator.sh` and `taste_curator.py` in `ps`). If `PPID` of any non-supervised process is your shell's PID, `disown` didn't take and a session exit will SIGHUP the orchestrator. If any one is missing entirely, the script crashed before it ever wrote a log line — go read the relevant log tail to see the import / argparse error. **Step 2 — progress check:** ```bash sleep 8 && tail -3 $REPO/lean4/scripts/logs/orchestrator.log; echo '---paper---'; tail -3 $REPO/papers/bedc/scripts/logs/orchestrator.log; echo '---sync---'; tail -3 $REPO/scripts/logs/sync_daemon.log; echo '---taste---'; tail -3 $REPO/scripts/logs/taste_curator.log; echo '---discovery---'; tail -3 $REPO/tools/logs/discovery_pipeline_daemon.log ``` Each log should show recent timestamps (within the last ~10s for orchestrators; within the last ~600s for sync; within the current discovery cycle for discovery) and substantive lines: `Phase B: Target selection...` / `Phase REVIEW: theory audit...` / `Calling codex exec ...` for the orchestrators; `[sync] [sync] rollup: ...` for the daemon; `[discovery-pipeline] stage=...` or `cycle summary` for discovery. **Use one-shot `tail -N`, not persistent `tail -F`.** A persistent `tail -F` blocks forever waiting for output, so if startup actually crashed silently between Step 1 and Step 2 (e.g. PID-lock not released, port in use, env var missing), the persistent monitor never fires a notification — you'd think you were watching it and it'd just be hanging. One-shot tails return immediately and let you verify by inspection. Only after BOTH steps pass — processes alive with PPID=1 AND logs advancing past startup — should you optionally arm a persistent `tail -F` for ongoing observation (see "Monitor" section below). The persistent monitor is for steady-state observation, never for verifying that startup succeeded. `--phase-b-timeout` and `--phase-c-timeout` defaults (2700 / 3600) are too tight under high parallelism: bump to 3600 / 4500. These are CLI-only — restart required to change. ## Tuning concurrency live (no restart) Concurrency is read from `/.pipeline_parallel.json` on every round dispatch — edit the file and the next dispatched round picks up the new value. **CLI `--parallel` and `--lake-parallel` flags are deprecated; the JSON file is the only source of truth at runtime.** ```json {"paper": 8, "lean": 12, "lean_lake": 3} ``` | Key | Effect | Sane range | |---|---|---| | `paper` | Concurrent paper rounds (Phase REVIEW / REVISE / VERIFY / merge overlap; codex-exec children = ~paper) | 5–10 | | `lean` | Concurrent lean rounds | 8–14 | | `lean_lake` | Concurrent `lake build` invocations gated by the lake mutex; was hard-coded 1 historically | 1–3 (3 fits in 16 GB if memory pressure is moderate) | Memory floor is the binding constraint, not CPU — each codex-exec child is ~50–100 MB; each `lake build` is ~1–1.5 GB. With `lean_lake: 3` and 16 GB RAM, leaving `paper + lean ≤ ~20` keeps `vm_stat` "free" above 0.5 GB. The orchestrator's memory_guard kicks in only when `swap > 16 GB AND avail < 1.5 GB`, so the JSON file is your knob, not the guard. **Autotune daemon overrides static settings.** Once `tools/auto_tune_concurrency.py` is launched (5th default daemon, see Start section), it re-writes `paper` / `lean` / `lean_lake` every 300s based on critical_path supply. Manual edits get overwritten on the next tick. To override autotune, either kill the autotune daemon first or change its constants (`LEAN_BUFFER` / `PAPER_BUFFER` / clamp ranges) and let it pick up the new formula. The `lean = top_size` (no buffer) formula is empirical; raising `LEAN_BUFFER` reintroduces chapter dogpile at low supply. Lowering autotune `*_MAX` constants is the right way to cap concurrency under sustained memory pressure. ## Monitor (read-only, never owns the orchestrator) Monitors `tail -F` the log files the detached orchestrators write to. They are pure observers — killing, swapping, or re-launching a Monitor never touches the orchestrator process. ### Token-saving monitor mode (default) Operate in **token-saving** mode by default. Each Monitor event resolves to **one short Chinese sentence** (≤25 字), no diagnostics commands, no log quotes, no tables. The recovery consumer + Phase D lints + closure machinery handle issues automatically, so an event arriving in your transcript is mostly informational — your job is to acknowledge that you saw it and that automation took over, not to investigate. Concrete rules for token-saving replies (filter is already tight — every arriving event is by design escalation-tier, but most still resolve themselves): 1. **`3 consecutive failures` (cooldown)**: one sentence — `cooldown 触发, 180s 自节流`. Don't pull stats unless the same cooldown repeats ≥2 times in 30 min. 2. **`[recovery] unrecoverable / codex crashed / stopped`**: one sentence noting the round/paper id was abandoned. Worktree is in `.worktrees/dead/` if the operator wants to triage later — don't investigate now. 3. **`STALE MARKER` / `SHALLOW GROWTH`**: one sentence. If the same chapter / pattern repeats ≥3 times in 30 min, that's a prompt-rule problem worth flagging. 4. **`memory_guard.*PAUSE`**: one sentence. If it repeats, lower `lean_lake` or `lean` in `.pipeline_parallel.json`. 5. **`[sync] rollup: push ... failed` / `[sync] rollup: gh pr ... failed` / `[sync] codex could not resolve`**: this is real — escalate with one sentence (`sync daemon 更新 rollup PR 失败，下一轮 600s 重试 / 或手动 sync_with_auto_dev.py`). If repeats, manual sync. 6. **`Session complete:` / `draining N in-flight workers` / `Pipeline PID token is not current`**: **orchestrator exited** — run the liveness check and report to the user immediately. Daemon must be restarted. 7. **First occurrence of a novel pattern**: one sentence, flag it — `首次见到 X，观察 1-2 例再决定`. 8. **No actionable events in a tick**: zero output is fine. 9. **Verbose mode override**: only switch to long-form when (a) the user asks `详细分析` / `深入看看` / `report` / `调查 ...`, (b) a self-check `/loop` tick fires, or (c) the same novel pattern repeats ≥3 times in 30 min — then briefly pull stats and propose a prompt edit. Token-saving replies do NOT spawn shell commands unless you actually need data to decide whether action is warranted (rule 5 / 6 / 9). For the default ack path, reply with text alone. Default to a single **unrecoverable error watch** that tails BOTH log files at once and emits only actionable signals where automation has *already failed or is throttling*. Routine round FAILs, merge fails, and Pre-merge hard gate failures are silenced because the recovery consumer auto-picks them — surfacing those wastes transcript tokens and makes the operator chase events the pipeline is already healing. What does still arrive is the escalation tier: cooldown, recovery exhaustion, content-quality gates, daemon state changes, and sync push failures. ```bash tail -F $REPO/papers/bedc/scripts/logs/orchestrator.log \ $REPO/lean4/scripts/logs/orchestrator.log \ $REPO/scripts/logs/sync_daemon.log \ $REPO/scripts/logs/auto_heal.log \ $REPO/scripts/logs/taste_curator.log \ $REPO/tools/logs/discovery_pipeline_daemon.log \ | grep -E --line-buffered \ 'HEAL ALERT|TASTE ALERT|3 consecutive failures|\[recovery\]\s+(unrecoverable|codex crashed|stopped)|STALE MARKER|SHALLOW GROWTH|memory_guard.*PAUSE|axis-confusion|Session complete:|draining [0-9]+ in-flight workers|Pipeline PID token is not current|\[sync\] .*(codex could not resolve|push origin codex-auto-dev failed|merge failed without conflicts)|builder.*FAIL.*(consecutive|persistent)|Codex did not complete.*(persistent|after [0-9]+ attempts)|\[heal\] .*push failed|\[taste\] rule evolution (failed|completed)|\[supervisor\] .* taste_curator.py exited rc=[^0]|\[discovery-pipeline\] stage=.*ERROR|\[discovery-pipeline\] cycle summary .*"ok": false' \ | grep -vE --line-buffered 'queued|picking|RECOVERED' ``` Use `persistent: true`. Describe as `BEDC unrecoverable error watch`. **Excluded by design** (handled by recovery consumer, no operator action needed): - `Round FAILED` — recovery queue auto-picks within seconds - `Merge failed —` — recovery queue auto-picks - `Pre-merge hard gate failed` (audit / lake build / axiom-purity / phase_d_lint) — recovery consumer retries with codex - `[recovery] queued / picking / RECOVERED` — routine consumer cycle - `closure_mark` — paper-side closure proposals (high volume, informational) - `deps_ready_relaxed: True` — critical_path auto-relax (informational) - `Traceback` from `_clone_lake_cache` race — orchestrator immediately FAILs and dispatches a new round; the lost round costs nothing the operator can recover If a problem persists past automation, it surfaces as: `3 consecutive failures` (cooldown), `[recovery] unrecoverable`, repeated `STALE MARKER` / `SHALLOW GROWTH`, or `[sync] push origin codex-auto-dev failed`. Those are the signals the operator must look at. What each surviving pattern means and the cheapest fix: | Pattern | Meaning | Fix without restart | |---|---|---| | `3 consecutive failures` | MainThread cooldown; usually horizon thresholds shifting, .lake clone race burst, or a size-gate violation upstream — wait, then check what 3 prior FAILs were and whether they share a root cause (e.g. a >800-line file blocking all R rounds). Often self-heals once the next round picks the new base. | | `[recovery] unrecoverable / codex crashed / stopped` | Recovery consumer gave up on a ticket after retries; manual triage needed (typically a stuck worktree under `.worktrees/dead/`). | | `STALE MARKER` | Paper marker references missing Lean target — codex prompt issue or paper-side cleanup needed. | | `SHALLOW GROWTH` | Phase D lint detected duplicate / parameter-echo / mechanical-arity — prompt rule issue, edit `phase_c.txt` and bump version. | | `memory_guard.*PAUSE` | Lean orchestrator paused workers due to memory pressure — drop `lean_lake` or `lean` in `.pipeline_parallel.json`. | | `axis-confusion` | codex pipeline reject — paper closure axis written as a function of verification axis or vice versa. Means a recent prompt change broke the two-axis discipline. | | `[sync] codex could not resolve` / `push origin codex-auto-dev failed` | Sync daemon's codex conflict resolution failed or `git push` rejected for a non-ff reason; manual sync may be needed. | | `builder.*FAIL.*(consecutive\|persistent)` | paper_builder_daemon has stacked multiple failures with no recovery — usually preamble macro missing for an upstream-introduced symbol. | | `Codex did not complete.*(persistent\|after N attempts)` | Recovery consumer exhausted retries on a single round. | | `Session complete: N succeeded, M failed` / `draining N in-flight workers` / `Pipeline PID token is not current` | **Orchestrator exited or got swapped out.** Under `--continuous`, neither side should ever print these — they mean the loop terminated and no one will dispatch new rounds. Run the liveness check below and, if a daemon is missing, restart it (see "Start" / "Stop" sections). This is the single most disruptive silent failure mode: paper-side keeps crunching closure_mark while lean side hasn't moved in hours, and `closed_horizons` totals can still drift up from paper alone, masking the outage. | If you need verbose per-phase visibility for a debugging session, swap the filter to `'SUCCESS|FAILED|ERROR|WARNING|Exception|Traceback|Push rejected|Merge conflict|Merging|Merged|[PR][0-9]+'`. Don't leave the verbose filter on a long-running monitor — it produces 20+ events/min during steady state and burns transcript tokens. ### Liveness health check (run at every status query) Whenever the user asks `状态如何` / `现在如何` / `进展` / `report`, **before** computing closure deltas, run a one-shot daemon liveness probe. Four daemon entries must appear with `PPID=1`: ```bash ps -axo pid,ppid,etime,command \ | grep -E 'codex_revise.py|codex_formalize.py|sync_with_auto_dev.py|discovery_pipeline_daemon.py' \ | grep -v grep ``` Expected: - one `codex_revise.py --continuous` (paper) - one `codex_formalize.py --continuous` (lean) - one `sync_with_auto_dev.py` loop wrapper (sync) - one `discovery_pipeline_daemon.py` (discovery) If any of the four is missing, **mention the absence in the same status report** and either restart it or escalate. Do not paper over a missing daemon by reporting only the closure totals — totals can keep climbing from one side alone (e.g. paper publishing closure_mark while lean has been dead for hours), and the user trusts your status replies to catch this. Symptom that should always trigger an immediate `ps` check: - **`paper=N>0, lean=0` for ≥30 min** in your hourly Round-SUCCESS counts. Paper proposing closure marks while lean produces zero rounds is the canonical signature of a dead lean orchestrator. Do not rationalize this as "work pool排空" without first verifying the lean process is actually alive — historical incident 2026-05-09: lean orchestrator naturally exited at 03:10 (`Session complete: 46 succeeded, 14 failed` after a PID-token swap), no one noticed for ~10h, multiple status replies kept saying "lean 端 work pool 长期排空" while the process was simply gone. Only the user's "并发数如何？" query at 13:10 prompted the `ps` that surfaced the outage. The active error watch grep above now includes `Session complete:` / `draining N in-flight workers` / `Pipeline PID token is not current` so this signal arrives in the monitor as soon as it happens — but if you missed it or the monitor was offline, the per-status liveness probe is the safety net. ### Always run a second monitor: daemon liveness change watch Log-stream monitors only see what the orchestrators *write* — when an orchestrator silently exits, its log goes quiet and the log-stream monitor produces zero events (silence ≠ healthy). Pair the active error watch with a second persistent monitor that polls `ps` every 60s and emits **only on liveness state change**: ```bash prev="" while true; do ps_out=$(ps -axo pid,ppid,command 2>/dev/null \ | grep -E 'codex_revise\.py|codex_formalize\.py|sync_with_auto_dev\.py' \ | grep -v grep || true) p=$(echo "$ps_out" | grep -c 'codex_revise\.py') l=$(echo "$ps_out" | grep -c 'codex_formalize\.py') s=$(echo "$ps_out" | grep -c 'sync_with_auto_dev\.py') pa=$([ "$p" -ge 1 ] && echo 1 || echo 0) la=$([ "$l" -ge 1 ] && echo 1 || echo 0) sa=$([ "$s" -ge 1 ] && echo 1 || echo 0) cur="paper=$pa lean=$la sync=$sa" if [ "$cur" != "$prev" ]; then ts=$(date '+%Y-%m-%d %H:%M:%S') if [ "$pa" -eq 0 ] || [ "$la" -eq 0 ] || [ "$sa" -eq 0 ]; then echo "[$ts] DAEMON DOWN — $cur (raw paper=$p lean=$l sync=$s; was: $prev)" else echo "[$ts] daemon liveness OK — $cur (raw paper=$p lean=$l sync=$s; was: $prev)" fi prev=$cur fi sleep 60 done ``` Compare alive-as-boolean (≥1 process matches → 1, else 0), not raw counts. The paper bash wrapper makes `codex_revise.py` match twice; the sync wrapper periodically spawns a Python child that pushes the sync count from 1 to 2 for a few seconds every 600s. Comparing raw counts emits a no-op `liveness OK` event every 10 minutes during steady state. Comparing alive-booleans stays silent and only fires when a daemon actually disappears. `persistent: true`. Description: `BEDC daemon liveness change (paper/lean/sync)`. The `[ "$cur" != "$prev" ]` guard means it stays silent during steady-state (one event at boot to confirm initial state, then nothing until a change). When a daemon dies, you get a `DAEMON DOWN` notification within 60s — the missing log signal becomes a positive `ps` signal. Always run **both** monitors in parallel after starting the pipelines: log-stream (active error watch) + ps-based (daemon liveness change). The two cover orthogonal failure modes — log-stream catches loud failures (Tracebacks, recovery activity, `Session complete:` etc.); ps-based catches silent disappearance (process killed by OS, exit before flushing log, parent shell SIGHUP edge cases). Either alone misses an entire category. **Before arming a fresh monitor pair, sweep stale Monitor children from prior sessions.** Monitor tasks are detached children; a cross-session disconnect leaves the `tail -F …` / `while true; do ps_out=…; done` shells running and re-emitting events into a transcript they no longer belong to (you also see every log line twice when the new monitor lands on top of the old). Sweep first: ```bash ps -axo pid,etime,command \ | grep -E 'tail -F .*orchestrator\.log|while true; do.*ps_out|prev=' \ | grep -v grep ``` Anything older than the current session's start time (`etime` clearly large, e.g. days) belongs to a prior session — `kill ` it before launching the new monitors. The corresponding Monitor task will flip to `failed (exit 144)`, which is the desired outcome. Because Monitor no longer holds the orchestrator, you can freely change the `grep` filter, kill the Monitor, or re-launch it with a different filter without affecting any in-flight round. ## 3-hour open-ended self-check loop While the pipelines run, register a 3-hour recurring self-check that asks open-ended questions about the project rather than a fixed metric checklist. Suggested invocation (the user types this once after pipelines start): ``` /loop 3h Open-ended self-check on BEDC pipelines (skill bedc-codex-auto-dev): 1. 项目运行的顺利吗？(both pipelines healthy, failure / conflict / cooldown rates, any stuck worker) 2. 有什么需要改进的？(recurring pattern in last ~50 commits, missing or over-tight gates, wasted effort like dedup / empty rounds / cooldown) 3. 数学品味如何？(sample 10 most recent merged commits per side; substantive vs shape-saturated bookkeeping; mechanical-arity / parameter-echo residue trend) 4. 有什么有意思的新发现？(skim last ~24h commits + capstones/; cite specific commits / chapters; concrete sentences not platitudes) 5. 如何进一步提升？(critical_path top-3 movement; banned chapter ready to leave SCHEMA_ONLY_HORIZONS; capstone count and quality; highest-leverage single change for math taste / throughput) 6. harness 还有什么提升空间？(Makefile precheck, subprocess lints, prompt HARD GATEs, orchestrator timeouts/parallel — where would a new gate prevent a recurring pattern, where would relaxing a gate save real rounds) Make any harness/prompt adjustments authorized under the skill's "Autonomous adjustment authority" without asking; for each, include the trigger, file edited, version bump, commit SHA. Report concisely (≤ 12 sentences): what's running, what changed since last tick, what mattered, what you adjusted. ``` The 6 open-ended questions force a real read of recent work rather than a metric checklist that can pass while the project drifts. Concrete-sentence rule prevents platitude reports. The user runs `/loop` once and the cadence is then automatic. Suggest it after the pipelines are healthy and observed for ~30 min. Cron auto-expires after 7 days; re-register if the run continues longer. If the user prefers a single autonomous tick rather than recurring, they can also use `/loop` without an interval (dynamic pacing), in which case you self-pace via `ScheduleWakeup` between ticks. 3h is the right steady-state cadence; tighter only when a recent prompt change needs rapid iteration validation. ## Stop commands For an orderly stop, run: ```bash python3 $REPO/papers/bedc/scripts/codex_revise.py --stop python3 $REPO/lean4/scripts/codex_formalize.py --stop ``` Then confirm remaining processes with the preflight process check. If orphaned child process groups remain, terminate only the specific matching process groups after verifying their command lines. ## Monitoring duty: content quality and merge efficiency While the pipelines run, keep watching two axes. When a signal appears, edit the prompts (instant — re-read on each round dispatch) or the pipeline scripts (requires stop + restart) and bump prompt versions so commit bodies record which prompt pair produced them. ### Content-quality signals After every merged commit, sample `git show ` and check for: 1. **Parameter-echo theorems.** Statements that introduce abstract parametric carriers $A,B$ and classifiers $\sim_A,\sim_B$ as universally quantified inputs and conclude with paired field-by-field $\Leftrightarrow$ chains. The proof is "transport hypothesis through the equivalence on each field." This is bookkeeping, not theory growth — `papers/bedc/scripts/prompts/phase_review.txt` (paper) and `lean4/scripts/prompts/phase_c.txt` (Lean discovery insertion) reject these. 2. **Same-file saturation.** Multiple consecutive commits touching the same `papers/bedc/parts//.tex` with `source-equivalence` / `under-source-equivalence` / `_with_fields` / `_alt` siblings. The paper review prompt counts the last 20 paper-side commits; ≥3 hits triggers an extra bar. 3. **Label collision.** Two `\label{thm:X}` with identical X anywhere under `papers/bedc/parts/`. Detect with `python3 lean4/scripts/bedc_ci.py audit` — duplicate labels are now printed on stdout with `