admin/LithosAnanake
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

FABRIC-2.md: record Isabelle toolchain replacement + StarForth_Q48_16.thy breakage diagnostic

Browse Source 
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.
This commit is contained in:
Robert Allan James
2026-08-13 11:20:39 -04:00
parent ebdf3726e6
commit 5787718c30
1 changed files with 33 additions and 0 deletions
Download Patch File Download Diff File Expand all files Collapse all files
FABRIC-2.md
+33
View File
@@ -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