| name | goal-dev |
| description | In-loop development guidance for an autonomous /goal Lean-proof loop in SK_EFT_Hawking. This skill should be used when developing Lean 4 proofs inside a goal loop, deciding whether to fan work out to parallel worktree slots or stay solo, resetting a worktree slot, hitting a recurring Lean tactic/ elaboration friction, or sharding the lab notebook. It surfaces the MCP-first proof loop, kernel-purity rules, the worktree fan-out flow, and a symptom-indexed friction catalog. Invoke it at the start of a development stretch and whenever you hit proof-mechanics friction or need the parallel-dev recipe.
|
Developing in a /goal loop (the in-loop dev skill)
This is the in-loop companion to goal-prompt (which only authors the goal at launch). Invoke this
skill while doing the work; its references load on demand. Project conventions in
SK_EFT_Hawking/CLAUDE.md are canonical and override the generic lean4 skill where they differ.
Posture (the always-on stance)
Scope is SETTLED — do the next increment of real work THIS turn. A stop-hook firing is a GO signal,
never a cue to stop/hold/re-scope/hand-back. Legitimate stops are only: a kernel-checked no-go (build
around it; carry one scoped disclosed Prop + a discharge plan) or a genuine user-only decision (ask once,
keep shipping meanwhile). It is not your job to manage the context window — auto-compaction is handled;
quality does not drop across a compaction boundary. Full rationale + worked negative examples:
references/decision-heuristics.md.
The MCP-first proof loop (milliseconds/cycle, not ~15s write→lake-build)
lean_file_outline → orient. 2. Write the statement with sorry; save. 3. lean_goal at the sorry —
see the actual goal. 4. lean_multi_attempt 4–6 candidate tactics; pick the winner. 5. Write it; repeat
from 3. 6. lean_goal → "no goals" ⟹ drop the sorry; lake build to finalize. Search before prove
(lean_local_search first). Hard rules, Aristotle-fallback policy, preemptive-strengthening, and the
substrate-specific gotchas: references/lean-dev.md.
Kernel-purity is the bar (non-negotiable): target axioms exactly {propext, Classical.choice, Quot.sound}; no new project axiom without explicit user sign-off, no new sorry / native_decide /
maxHeartbeats. Verify each substantive brick with lean_verify. A heartbeat wall ⟹ wrong architecture →
decompose into have sub-lemmas (≤ 12-term targets).
Incremental-commit discipline
Maximize per-turn throughput. Land the maximum coherent GREEN progress each turn — as many bricks as you
can finish cleanly, not one; don't artificially atomize (fewer, bigger turns amortize per-turn overhead and
reach auto-compaction slower). The commit cadence below is an orthogonal safety checkpoint (rollback +
notebook durability), not a per-turn cap.
Commit a GREEN kernel-pure increment every ~5–10 bricks (each: zero sorry, lean_verify clean, lake build
clean) — batches of finished bricks, never one giant commit — updating the lab notebook each brick; the
notebook is the compaction-durable source-of-truth.
Never push (user action). The notebook is a two-layer system (a bounded always-loaded INDEX +
chronological shards); maintain it with the /skeft-qa:notebook command — sync each brick, shard
at the checkpoint to keep the active shard under the ~25k-token Read guard automatically. Each brick is its
own ### heading; settled forks / kernel-checked no-gos go in the INDEX's append-only DECISIONS block.
Encode-on-settle (ADR-007 N-E, Invariant #17): a kernel-CHECKABLE no-go additionally lands a backing
refutation/forcing theorem + a KERNEL_NOGO_REGISTRY entry (src/core/constants.py) in the settling turn —
NOT a prose line alone (prose-only recording of a kernel-encodable fork is itself a nogo_substrate_integrity
finding). Policy / route / preference bans stay prose in SETTLED_FORKS.md (not kernel-encodable).
Full model + per-brick discipline: references/lab-notebook.md (the lead curates; workers report up).
Consult the atlas — BOTH fronts (/skeft-qa:frontier)
The atlas (lean/atlas_view.json, derived — cannot drift) is the machine-truth of the substrate, both signs:
- Positive frontier (ADR-005 D-I) — the ranked OPEN assumptions; consult it to aim fan-out at the
highest-impact provable work (the KEYSTONE) instead of roadmap-opaque selection.
- Negative frontier (ADR-007 N-D) — the ranked settled-dead forks (kernel-checked, with their
false_statement); consult it to steer AWAY from provably-false paths. Both are re-injected in the
SessionStart digest and available on demand via /skeft-qa:frontier; the two binding project no-gos are
lattice_arf_bridge_refuted + dataBordism_two_torsion_of_revStr_trivial.
Solo vs. fan-out
Keep a tightly-coupled single-file chain solo with one fast MCP — that is faster than coordinating. Fan
out only when the DAG has genuinely branched into independent sub-chains. To fan out, as lead:
/reset-slot N — resets worktree slot wtN to main, the guardrail-safe way. ⚠️ Never reach for
git reset --hard / git clean on a slot — the auto-mode permission classifier denies them (it's a
Claude Code heuristic, not a dev-harness hook). /reset-slot refuses if the slot holds unmerged commits,
so nothing is lost.Agent(subagent_type="skeft-qa:lean-worker", prompt="SLOT N=…, use mcp__lean-lsp-wtN__*, <one independent sub-chain/BLOCK — as large as is coherently independent — + Lit-Search refs + acceptance + any relevant kernel no-go from the NEGATIVE frontier the worker must not re-derive>") — up to 3 concurrent. Hand
workers as-large-as-coherent blocks, not atomic bricks (bigger blocks = fewer dispatch/merge/reread
cycles + higher per-worker throughput). A fresh worker is the highest-risk re-deriver — name the
dead-forks in its brief.- Merge each
worktree-wtN into main; re-run the full gate; /reset-slot N again for the next brick.
Full flow, why the slots are persistent, and the maintainer caveat: references/parallel-worktrees.md.
When a proof-mechanics error recurs
Grep references/lean-friction-catalog.md for the symptom (motive-not-type-correct, Subsingleton ℝ,
ext over-unfolding, ring on •, quotient mk-coercion, free-variable capture, …) before re-deriving
the fix. Add a new entry the first time a pattern recurs.
References (load on demand)
references/lean-dev.md — the full MCP loop, hard rules, Aristotle policy, substrate gotchas.references/lean-friction-catalog.md — symptom-indexed tactic/elaboration frictions.references/parallel-worktrees.md — worktree-slot fan-out flow + /reset-slot.references/decision-heuristics.md — the settled-scope / anti-escape stance, with worked examples.references/lab-notebook.md — lab-notebook lifecycle (create / maintain / shard / re-orient), the
two-layer INDEX model, and the /skeft-qa:notebook ops.
