|
| 1 | +<!-- SPDX-License-Identifier: MPL-2.0 --> |
| 2 | +<!-- SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk> --> |
| 3 | +# Session handoff — 2026-06-15 |
| 4 | + |
| 5 | +Snapshot of the estate-reconciliation work (echidna + echidnabot) for the next |
| 6 | +session. Master tracker **echidna#238 is closed**; remaining work is split into |
| 7 | +discrete issues, captured below by normative tier (MUST / INTEND / WISH). |
| 8 | + |
| 9 | +Legend: **done** = merged this campaign · **open** = tracked issue · **owner** = |
| 10 | +needs the repo owner (policy/SPDX/branch-delete) · **blocked** = gated on another item. |
| 11 | + |
| 12 | +## Status — ECHIDNA |
| 13 | + |
| 14 | +| Tier | Item | Status | Ref | |
| 15 | +|------|------|--------|-----| |
| 16 | +| MUST | Proof corpus repaired + CI-gated (Coq/Lean/Agda/Idris2) | done | #234 / #244 | |
| 17 | +| MUST | Every workflow job has `timeout-minutes` | done | #247 (closed #241) | |
| 18 | +| MUST | `hooks/` dir (RSR pre-commit-enforcement requirement) | this PR | #254·2 | |
| 19 | +| MUST | `src/rust/main.rs` SPDX hook blocks *all* commits to it | open · owner 1-liner | #216 | |
| 20 | +| MUST | `creusot-verify` CI red (`alt-ergo` not apt-installable) | open | #250 | |
| 21 | +| MUST | `salt/`/Python rule stale vs standards (no `salt/` exists) | open · owner doc | #254·1 | |
| 22 | +| MUST | Prover-count drift (48/105/113/128 vs `PROVER_COUNT.md`) | open · owner (R5a) | #251 | |
| 23 | +| INTEND | `--features verisim` 22 compile errors | open | #245 | |
| 24 | +| INTEND | machine_readable + contractile currency audit | open | #252 | |
| 25 | +| INTEND | Reconcile remaining RSR divergences (lang-tier undeclared) | open | #254·3 | |
| 26 | +| INTEND | Delete 6 reconciled stale branches | open · owner (proxy 403) | #253 | |
| 27 | +| INTEND | Wire 13 dispatcher adapters | blocked by #216 | `feat/corpus-dispatcher-all-17-adapters` | |
| 28 | +| INTEND | Structural-drift stale paths; ReScript→AffineScript migration | open | #242, #240, #266 | |
| 29 | +| WISH | Split Rust/FFI/proof safety alerts by risk class | open | #239 | |
| 30 | +| WISH | GNN-at-scale; Cap'n Proto / Chapel-full / coprocessors; 8-stage endpoint | aspirational | `docs/ROADMAP.md` | |
| 31 | + |
| 32 | +## Status — ECHIDNABOT |
| 33 | + |
| 34 | +| Tier | Item | Status | Ref | |
| 35 | +|------|------|--------|-----| |
| 36 | +| MUST | README test-count 129→184 + ProverSlug | done | #86 | |
| 37 | +| MUST | `echidna-fuzz` rate-limit-check timeout | done | #89 | |
| 38 | +| MUST | `LICENSE` missing SPDX header (Licence-consistency fails every PR) | open · owner-only | #87 | |
| 39 | +| MUST | `.gitignore`/`.gitattributes` PMPL→MPL SPDX drift | open · owner-only | #83 | |
| 40 | +| MUST | `gitbot-shared-context` path dep (no bare-clone build) | accepted debt — do not fix | #18 | |
| 41 | +| MUST-NOT | `admitted_stub.v` / `sorry_stub.lean` | intentional dogfood failures — leave | — | |
| 42 | +| INTEND | Post-checkpoint hygiene (STATE dual-truth, SESSION_SUMMARY, contractiles, `.scm`, SONNET-TASKS, `curl\|sh`) | open | #88 | |
| 43 | +| INTEND | `proof-debt.md` TBD→rationale; cflite shared-context vendoring | open | #68, #67 | |
| 44 | +| WISH | Codeberg adapter; pre-built Podman images; K8s distributed; full bot-modes | aspirational | #62, #61, #59 | |
| 45 | + |
| 46 | +## Hard constraints (carry forward — these OVERRIDE defaults) |
| 47 | +- **Languages:** no Python (the `salt/` exception was removed upstream), no TypeScript, no Go. Use Rust / Julia / Idris2 / Agda / Zig / Chapel / AffineScript / Nickel per `CLAUDE.md`. |
| 48 | +- **Build:** Justfile primary (RSR-H14). **Containers:** Podman + `Containerfile`, never Docker/`Dockerfile` (RSR-H15). **Packaging:** Guix; **no Nix** (`flake.nix`/`flake.lock` banned estate-wide). |
| 49 | +- **SPDX / LICENSE edits are owner-only, manual, file-by-file** (#216 / #83 / #87) — never automate; automated sweeps must not touch licence headers. |
| 50 | +- **echidnabot dogfood stubs** (`admitted_stub.v`, `sorry_stub.lean`) are intentional failures — never "fix". |
| 51 | +- **echidnabot** cannot `cargo build` from a bare clone (path-dep #18) — for code work use a `gitbot-fleet` monorepo checkout; doc work is fine standalone. |
| 52 | +- **Branch ref-deletes return HTTP 403** via the session git proxy and the GitHub MCP has no delete-branch tool, so branch cleanup (#253) is **owner-only**. |
| 53 | +- Develop on `claude/<topic>` branches; open **draft** PRs; be **frugal** with GitHub comments. |
| 54 | + |
| 55 | +## Prompt for the next session |
| 56 | + |
| 57 | +Copy-paste the block below to the next Claude: |
| 58 | + |
| 59 | +> Continue estate maintenance on `hyperpolymath/echidna` + `hyperpolymath/echidnabot`. |
| 60 | +> |
| 61 | +> **First read:** echidna issue #238 (closed master checkpoint), `docs/handover/SESSION-HANDOFF-2026-06-15.md`, `AFFIRMATION.adoc`, and both repos' `CLAUDE.md` (their rules OVERRIDE defaults). |
| 62 | +> |
| 63 | +> **Where things stand:** the multi-language proof corpus is repaired, CI-gated, and green on `main`; the master checkpoint is closed; all this campaign's PRs merged. Remaining work is in discrete issues, grouped MUST / INTEND / WISH in the handoff doc. |
| 64 | +> |
| 65 | +> **Pick up in this order:** |
| 66 | +> 1. *Flag to the owner (don't auto-do — SPDX/policy/branch-delete):* #216 (main.rs SPDX hook — unblocks the `feat/corpus-dispatcher-all-17-adapters` branch), echidnabot #87 + #83 (LICENSE/SPDX), #251 (prover-count — fix the GitHub repo description first), #253 (delete the 6 stale branches). |
| 67 | +> 2. *Doable now, as draft PRs:* #250 (install `alt-ergo` via opam in `formal-verification.yml`), #245 (`--features verisim` — 22 compile errors), #252 (machine_readable + contractile currency audit — run a Haiku scout before bulk edits), #254 (reconcile the RSR divergences: drop the stale `salt/` wording, declare the polyglot language set as an out-of-template adaptation), echidnabot #88 (hygiene). |
| 68 | +> |
| 69 | +> **Honor the hard constraints** in the handoff doc (SPDX = owner-only; dogfood stubs intentional; Podman/Justfile/Guix; no Python/TS/Go). Develop on `claude/<topic>` branches, open draft PRs, keep GitHub comments frugal. |
| 70 | +
|
| 71 | +--- |
| 72 | +_Generated 2026-06-15. Source of truth for status: the linked issues + `CHANGELOG.md` + git log; this snapshot drifts._ |
0 commit comments