From 5787718c301387df3381cad093b3690673ebe25a Mon Sep 17 00:00:00 2001 From: Robert Allan James Date: Thu, 13 Aug 2026 11:20:39 -0400 Subject: [PATCH] FABRIC-2.md: record Isabelle toolchain replacement + StarForth_Q48_16.thy breakage diagnostic Isabelle2011-1 (genuinely 14+ years old) replaced with Isabelle2025-2 at the same path. Real build attempt: HOL-Library builds clean, StarForth session fails on one root-cause file (StarForth_Q48_16.thy) -- undefined fact, two non-closing proofs, one name collision against a new HOL-Library constant. Everything else is downstream unresolved-import fallout, not independent breakage. Not fixed yet. --- FABRIC-2.md | 33 +++++++++++++++++++++++++++++++++ 1 file changed, 33 insertions(+) diff --git a/FABRIC-2.md b/FABRIC-2.md index 5930095..7c00382 100644 --- a/FABRIC-2.md +++ b/FABRIC-2.md @@ -42,6 +42,39 @@ and recorded. - [ ] **5.2 — Isabelle/HOL.** One datatype, one index space, one conservation theorem. Not started. + > **DIAGNOSTIC 2026-08-13 — toolchain replaced, build attempted, one root-cause file + > found broken; not yet fixed.** The installed Isabelle at + > `/home/rajames/CLionProjects/Isabelle2011-1` was genuinely Isabelle2011-1 (14+ years + > old, from the directory's own timestamps) — essentially guaranteed stale against + > `proof/`'s 23 `.thy` files. Replaced with **Isabelle2025-2** (current stable, Jan + > 2026) at the same path, old install preserved alongside as + > `Isabelle2011-1.old` rather than deleted. `isabelle build -v -D proof/` run for real + > (not a dry run): the `Pure`/`HOL` base heaps loaded fine, `HOL-Library` built clean + > from scratch in ~5 minutes, but the `StarForth` session **failed**. + > + > **One root cause, not sixteen.** `proof/StarForth_Q48_16.thy` — the base theory + > every other theory in the session transitively depends on — fails to load with three + > distinct real problems, all consequences of 14 years of `HOL-Library` changes since + > 2011: + > 1. **Line 75** — `unat_push_bit` is now an undefined fact; that lemma name from the + > old `Word` library appears renamed or removed. + > 2. **Lines 63 and 122** — two `by (simp add: drop_bit_push_bit word_size)` proofs + > (`drop_bit 16 (push_bit 16 n) = n` round-trip lemmas) no longer close, likely the + > same underlying `Word`-library lemma-set drift as #1. + > 3. **Line 144** — a genuine name collision, not proof drift: `q48_accuracy`'s `total` + > parameter now shadow-fails against a same-named `HOL-Library` constant (the + > order-theory "total relation" predicate, type `('a×'a) set ⇒ bool`) that didn't + > exist or wasn't in scope under the 2011 library — Isabelle now resolves the + > identifier to that constant instead of binding it as a fresh parameter, producing a + > real type error at the `definition`. + > + > Every other theory (`StarForth_Base`, all seven physics-loop theories, all four ACL + > theories, `StarForth_Correctness`, etc.) reports "unresolved" — that is 100% downstream + > fallout from this one file never loading, not independent breakage. Not fixed yet — + > next step is repairing `StarForth_Q48_16.thy` against the modern `Word` library. + > Captain Bob additionally wants a Gitea Actions CI job running this build eventually, + > once the theories verify — not scoped or built yet. + - [ ] **5.3 — Shrink the subsystem documents.** `ARTEMIS.md`, `HERMES.md`, `CONSOLE.md`, `TRIPOD.md` need trimming now that `FABRIC-2.md` (via `FABRIC.md`) is the design-of-record. Not started. **Specific pending edit found within this item:** `TRIPOD.md`'s own Immediate