holbuild v0.7.2

This release is mostly focused on making proof-step execution the default, structural Proof-IR path more faithful to HOL semantics, easier to debug, and more robust under failed-prefix replay.

Highlights

• Proof-IR is now the default proof-step engine. Legacy GoalFrag runtime/planning code and naming have been removed or renamed. --skip-proof-steps remains the opt-out; deprecated GoalFrag flags now warn or fail with guidance.
• New execution-plan terminology and tooling. --goalfrag-plan has been removed in favor of execution-plan THEORY:THEOREM; --trace-steps is the supported tracing flag. Documentation and tests were updated from “GoalFrag” to “proof steps” / “Proof-IR”.
• Much improved structural proof replay. Failed-prefix checkpoint reuse now tracks structural Proof-IR paths, leaf signatures, runtime focus state, and dynamic replay events. When a proof suffix changes, holbuild can opportunistically rewind to the longest still-valid prefix and resume from the current plan, falling back safely if metadata is stale.
• Better preservation of HOL tactic semantics. The Proof-IR runtime now handles structural branches, selectors, each, THENL suffix scoping, residual goal ordering, by subgoals, repeat/control constructs, opaque tactic/list-step labels, and list-tactic structure more faithfully.
• Diagnostics are cleaner and more precise. Failed structural close locations are preserved, duplicate finish diagnostics after step failure are avoided, branch/list-step plan display was polished, and trace/debug output better reflects the actual executable structure.
• Cache internals were refactored. A cache backend interface was introduced, with the filesystem implementation moved behind it. Action/blob publication and transfer paths are now clearer and better isolated for future backend work.
• Compatibility/build fixes. The Makefile was adjusted for older make shell parsing, and numerous regression/golden tests were added or refreshed for checkpoint replay, branch composition, structural selector behavior, by, chained equality, stale failed-prefix metadata, and Proof-IR formatting.

Notes for users

Most normal builds should behave the same, but proof-step execution is now the standard path and may produce improved plan/trace output. Scripts or documentation using old GoalFrag-oriented options should be updated to the new proof-step / execution-plan names.

What's Changed

• Fix Makefile shell parsing on older make by @charles-cooper in #57
• Refactor cache filesystem backend by @charles-cooper in #61
• Add cache action publication policy by @charles-cooper in #63
• Rework Proof IR by @xrchz in #71

Full Changelog: v0.7.1...v0.7.2