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 <noreply@anthropic.com>
This commit is contained in:
co-authored by
Claude Sonnet 5
parent
1a2ec565e8
commit
e535346504
+22
-3
@@ -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.
|
||||
|
||||
Reference in New Issue
Block a user