From e53534650408e80163d24613f2c2f19b7ec3f969 Mon Sep 17 00:00:00 2001 From: Robert Allan James Date: Tue, 18 Aug 2026 22:50:03 -0400 Subject: [PATCH] FABRIC-2.md: record verified clean Isabelle/HOL rebuild (52 theories, genuinely green) Ran isabelle build -c (clean, forces fresh rebuild bypassing any cached heap) for real, per the agreed sequencing (code sweeps -> HOL green -> POST coverage). All 52 theories rebuilt from scratch in 42s, zero errors/failures/sorry/oops anywhere in the log -- upgrades the earlier entry's static-inspection-only inference to an actual verified result. Co-Authored-By: Claude Sonnet 5 --- FABRIC-2.md | 25 ++++++++++++++++++++++--- 1 file changed, 22 insertions(+), 3 deletions(-) diff --git a/FABRIC-2.md b/FABRIC-2.md index ee2a859..2c8cce1 100644 --- a/FABRIC-2.md +++ b/FABRIC-2.md @@ -1414,6 +1414,25 @@ reconciliation above for the Isabelle/HOL findings): **Not covered by this pass, honestly:** non-static dead-function cross-referencing (needs symbol-by-symbol call-site verification across ~150+ C files, out of budget), C99 smell -categories beyond warnings (magic numbers, function length, duplication), actually running -`isabelle build` end-to-end (static inspection only), and the bulk of `docs/formal/`/ -`docs/patent/`/`docs/working/` beyond the specific files named above. +categories beyond warnings (magic numbers, function length, duplication), and the bulk of +`docs/formal/`/`docs/patent/`/`docs/working/` beyond the specific files named above. + +**Addendum, same evening: `isabelle build` actually run end-to-end, genuinely green.** The +item above was flagged as "static inspection only, not run" — run for real immediately +after, per Captain Bob's explicit sequencing ("finish code sweeps, then do the Isabelle/HOL +stuff... after HOL is green we update POST testing"). Memory-safety procedure from +`feedback_isabelle_build_memory_safe.md` followed: `-o threads=1`, backgrounded, watched via +the `Monitor` tool rather than manual polling. A local Gitea Actions CI run (`act`, triggered +automatically by this session's earlier pushes) was caught actively running a +`git checkout --force` at the same time — investigated before proceeding: it operates in its +own fully isolated clone (`~/.cache/act/.../hostexecutor/`), never touches this working tree, +confirmed harmless, and the session waited for it to finish before starting the memory-heavy +build anyway rather than stack two heavy processes. + +First invocation without `-c` finished in 4 seconds — a cache hit against an already-built +heap image, not proof. Re-run with `-c` (clean, forces a genuine fresh rebuild, discarding any +cached session heap): **all 52 theories rebuilt from scratch, 0:00:42 total elapsed, zero +occurrences of `error`/`fail`/`sorry`/`oops`/`exception`/`abort` anywhere in the full build +log.** This is the real, current, verified state — not inferred from file/`ROOT` consistency +as the earlier entry above had to settle for. The 52-theory count itself (vs. `FINDINGS.md`'s +stale "53") is confirmed correct by this run too.