holbuild v0.10.2

This release improves HOL toolchain caching, recovery, and dependency build performance.

Remote HOL toolchain caching

When a remote cache is configured, holbuild can now restore a missing HOL toolchain from that cache. A successfully built local toolchain is published automatically after a remote miss.

Toolchain cache entries are matched against their exact installation path, platform, Poly/ML executable identity, kernel variant, and analyser identity. Restored entries are staged and validated before use.

Remote cache hits are trusted build inputs and may execute cached binaries. Use an authenticated HTTPS endpoint with trusted writers.

More robust toolchain builds

Interrupted or incomplete toolchain cache builds now self-heal automatically instead of requiring manual cache removal.

Toolchain mutations are protected against concurrent or orphaned child processes, and failed builds clean up incomplete entries before retrying.

Faster dependency builds

Proof instrumentation is now limited to theories in the root package. Dependency-package theories build using plain proof execution, without proof-step checkpoints, tactic timeouts, execution-plan targeting, step tracing, or failure REPL support.

To debug an individual dependency with proof instrumentation, build that package as the root project.

Tracing-kernel context inspection

holbuild context --trknl now resolves and displays the tracing-kernel project context without building the HOL toolchain.

Archive and cache safety

• Toolchain archives use deterministic tar metadata.
• Downloaded blobs are checked for size, SHA-1, and SHA-256 integrity.
• HBX and remote-cache documentation now clarifies that cached Poly/ML artifacts must come from trusted publishers.
• Large toolchain transfers use a longer timeout than ordinary theory-cache transfers.

Fixes

• Added regression coverage for resumed diagnostics containing NUL bytes.
• Build context now consistently respects tracing-kernel selection.

What's Changed

• Fix some issues by @xrchz in #144
• Add regression coverage for resumed diagnostic NULs by @xrchz in #145
• Self-heal interrupted toolchain cache builds by @charles-cooper in #148
• Add remote caching for same-path HOL toolchains by @charles-cooper in #150

Full Changelog: v0.10.1...v0.10.2

holbuild v0.10.1

This patch release improves Proof-IR failure handling and failed-prefix checkpoint recovery.

Fixes

• Preserve and report the final goal context when every alternative of a Proof-IR choice fails.
• Report useful proof context when failed-prefix replay or resumed proof execution fails.
• Make failed-prefix checkpoint reuse safer after structural proof edits by validating a canonical dependency-prefix signature.
• Rewind resumed proofs by actual proof-history operations rather than successful Proof-IR leaf count, fixing recovery when structural operations create
  multiple history entries.
• Retain sufficient proof history to support structural prefix rewind across heap resume.
• Avoid an infix-keyword warning in project graph processing.

Compatibility note

Failed-prefix checkpoint metadata has been upgraded. Checkpoints created by earlier metadata versions will be ignored and rebuilt as needed.

Testing

Added regression coverage for:

• failed-prefix diagnostics,
• exhausted choice diagnostics,
• structural edits to failed proof prefixes,
• structural prefix rewind and resumed proof history.

What's Changed

• Improve failed prefix diagnostics by @xrchz in #141
• Fix issues in checkpoint replay semantics by @xrchz in #143

Full Changelog: v0.10.0...v0.10.1

holbuild v0.10.0

This release adds tracing-kernel support and substantially refactors and optimizes package resolution, source discovery, build planning, hashing, cache handling, and checkpoint maintenance.

Highlights

Tracing-kernel builds

• Added --trknl support:

    holbuild buildhol --trknl
    holbuild build --trknl MyTheory

• Standard and tracing HOL toolchains have separate identities and caches.
• Tracing builds track Theory.tr.gz as a normal output, including cache publication and restoration.
• Added tracing-kernel CI coverage.

Faster planning and hashing

• Added broad memoization and indexing across build-plan keys, dependency closures, source lookup, external keys, and scheduler bookkeeping.
• Optimized source discovery, dependency parsing, generator graph processing, cache materialization, and theory-parent checks.
• Introduced persistent stat-hash cache infrastructure; the hit path is currently disabled pending a sufficiently portable file-identity criterion.
• Added --no-stat-cache and --emit-output-hashes diagnostic options.

Package and planning architecture

• Separated immutable package definitions from machine-local configuration and resolved package instances.
• Added typed package provenance, canonical package/component identities, and a reusable resolved project graph.
• Split generator preparation from read-only source discovery.
• Added canonical source inventories and a component-provider layer.
• Planning now materializes a shared selected dependency graph and stable structural/resolved plan identities.
• holbuild context reports richer canonical identity and provenance information.

Cache and checkpoint reliability

• Cache blobs are now verified by default across filesystem-cache hits, exports, heaps, and retained manifests.
• Improved handling of corrupt, truncated, stale, and concurrently materialized cache data.
• Hardened checkpoint indexing, recovery, budget accounting, eviction, and parallel-build scheduling.
• Reduced checkpoint protection to active node families, keeping parallel checkpoint usage bounded.
• Improved recovery after interrupted vendored-HOL publication.
• Disabled unnecessary per-theory HTML generation during theory export.

Manifest changes

This release tightens manifest validation:

• [holbuild].minimum_version is now required.
• The legacy schema = 2 marker is optional.
• The required_version alias is no longer accepted.
• project.name is required for every package.
• Dependency keys must match the resolved package’s project.name.
• Glob patterns in build.exclude are rejected; use build.exclude_globs.
• Package-relative filesystem inputs must remain under the package root and cannot contain ...
• Local build exclusions apply only to the root package.
• A from/path/manifest shim cannot be overridden directly; override its direct from dependency instead.
• Stale generated HOL manifests are migrated where possible.

Example:

  [holbuild]
  minimum_version = "0.10.0"

  [project]
  name = "example"

Existing projects using required_version, omitting minimum_version or project.name, or placing globs in build.exclude must update their manifests.

Additional fixes

• Preserved generator scheduling order and validated action policies before generator execution.
• Hardened analyser response framing and file-ID validation.
• Fixed ordering-only theory dependencies and parent-hash handling.
• Improved compatibility with HOL revisions lacking the reduced build sequence.
• Fixed default Make target and golden-test setup.
• Made vendored-HOL refresh idempotent and safer under interruption.
• Added extensive regression coverage and a toolchain-independent golden action-key harness.

What's Changed

• Add --trknl support for traced HOL toolchains by @xrchz in #79
• Optimize build planning, hashing, and cache materialization by @lukaszcz in #136
• Refactor by @xrchz in #132

Full Changelog: v0.9.0...v0.10.0

holbuild v0.9.0

Highlights

Reduced HOL toolchains and on-demand HOL sources

Schema-2 projects now build shared HOL toolchains with HOL's reduced
tools/sequences/upto-hol sequence rather than a full default HOL build:

bin/build --no-helpdocs --seq=tools/sequences/upto-hol

Sources from the remainder of HOL's default build are exposed through the
implicit package hol and built on demand. The generated HOL source manifest is
cached per toolchain.

This substantially reduces initial toolchain construction while preserving
access to theories and libraries that were previously available after a full HOL
build.

Compatibility note: selected HOL revisions must provide
tools/sequences/upto-hol. Toolchain cache identities have changed, so upgrading
may cause a one-time HOL toolchain rebuild.

Build groups

Manifests can now define phony build groups:

  [build]
  root_groups = ["@generated"]

  [build.groups.generated]
  include = ["gen/fixtures"]
  include_globs = ["gen/*Script.sml"]
  exclude = ["gen/fixtures/known-broken"]
  exclude_globs = ["gen/*ExperimentalScript.sml"]
  allow_empty = false

Group references such as @generated are supported in:

• CLI build targets;
• build.roots and build.root_groups;
• heap object lists;
• executable object lists.

Groups expand to ordinary logical targets after generation and source discovery.
They do not create aggregate HOL theories.

Faster dependency planning

Dependency hashing and extraction now operate only on nodes reachable from the
selected build roots. Newly reached dependency frontiers are still analyzed in
batches, preserving analyzer throughput without processing unrelated package
sources.

REAPI-compatible remote action cache keys

Remote action-cache keys are now mapped to domain-separated SHA-256 values,
making /ac/... requests compatible with REAPI cache servers such as
bazel-remote.

This starts a new remote action-cache namespace. Local action-cache keys and CAS
object addressing are unchanged.
Other changes

• Clarified the distinction between build.members and build.roots:
  • members are discoverable and buildable on demand;
  • roots define default build entry points.
• When no package declares roots or root groups, default builds select sources
  from the root project package only, rather than dependency package sources.
• Empty explicit target selections no longer mean “build every discovered
  source.”
• Root tactic timeout handling now supports extensionless roots and grouped
  roots.
• Explicit heap and executable object ordering is preserved when no group
  expansion is required.
• The proof runtime no longer depends on HOL's post-toolchain smlExecute and
  smlTimeout modules.
• CI now uses holbuild buildhol itself to populate shared HOL toolchain caches.
• Added HOLBUILD_KEEP_TEST_LOGS=1 support for retaining test logs and selected
  test temporary directories during debugging.

What's Changed

• Reduce HOL sequence and expose remaining HOL sources on demand by @xrchz in #122
• Add phony build groups for holbuild targets by @lukaszcz in #123
• Map remote action-cache keys to SHA-256 for REAPI compatibility by
  @charles-cooper in #126
• Analyze dependencies only for reachable build nodes by @xrchz in #127

Full Changelog:
v0.8.3...v0.9.0

holbuild v0.8.3

What's Changed

• Support executable heap targets via HOL buildheap by @xrchz in #115
• Support local dependency overrides by @lukaszcz in #117
• Speed up checkpoint budget maintenance and build execution by @lukaszcz in #118
• Support project-local remote cache defaults by @xrchz in #119

New Contributors

• @lukaszcz made their first contribution in #117

Full Changelog: v0.8.2...v0.8.3

holbuild v0.8.2

holbuild v0.8.2

Added

• Added optional Bazel-style HTTP remote cache support via --remote-cache and HOLBUILD_REMOTE_CACHE_URL.
• Remote cache entries use /ac/<action-key> metadata and /cas/<sha256> content blobs.
• CAS transfers support zstd compression where available.
• Added support for HOLBUILD_REMOTE_CACHE_CURL_CONFIG to pass curl configuration, useful for private cache authentication.
• Added build.exclude_globs for package-relative glob exclusions.

Changed

• build.exclude now represents concrete package-relative paths/subtrees. Glob patterns in build.exclude are still accepted but deprecated and produce a
  warning.
• Source discovery now ignores nested holbuild subprojects by default, unless explicitly listed as members.
• Checkpoint budget enforcement now runs during builds between completed nodes and avoids evicting checkpoint families that may be in active use.

Fixed

• Prevented parent projects from accidentally discovering sources inside nested holbuild subprojects.
• Improved checkpoint budget behavior for long builds and retained proof-edit checkpoints.

Documentation

• Updated README, design notes, manifest/local config references, and holbuild skill documentation for remote cache, excludes, and checkpoint retention.

What's Changed

• Align build.exclude semantics and add exclude_globs by @xrchz in #87
• Add SHA256 hash utilities by @charles-cooper in #90
• Add remote cache configuration by @charles-cooper in #91
• Add Bazel remote cache HTTP client by @charles-cooper in #92
• Restore cache entries from remote cache by @charles-cooper in #93
• Publish cache entries to remote cache by @charles-cooper in #94
• Document and test remote cache workflow by @charles-cooper in #95
• Use zstd for remote CAS transfers by @charles-cooper in #98
• Ignore nested holbuild subprojects during discovery by @xrchz in #111
• Enforce checkpoint budget during builds by @xrchz in #114

Full Changelog: v0.8.1...v0.8.2

holbuild v0.8.1

co-authored by gpt 5.5

What's Changed

• Work on checkpoint budget issues by @xrchz in #82
• Add hbx cache archive helpers by @charles-cooper in #65
• Add hbx export/import commands by @charles-cooper in #66
• Enrich hbx archive manifests by @charles-cooper in #84
• Emit hbx registry metadata sidecars by @charles-cooper in #85
• Document hbx release registry workflow by @charles-cooper in #86

Full Changelog: v0.8.0...v0.8.1

holbuild v0.8.0

Highlights

• Added holbuild build --watch
  • Runs an initial build, then watches project inputs and rebuilds after changes.
  • Build failures are reported but the watcher stays alive for the next edit.
  • Uses inotifywait, so it currently requires Linux/inotify-tools.
  • Watch mode intentionally rejects unsupported combinations with --json, --dry-run, and --repl-on-failure.
• Made build the default command
  • holbuild now builds the default project targets.
  • holbuild MyTheory now builds a logical target directly.
  • The explicit form remains supported: holbuild build MyTheory.
• Improved CLI help
  • Replaced the long top-level usage output with grouped help.
  • Added command-specific help via holbuild COMMAND --help.
  • Handles help requests before project/toolchain discovery where possible.
  • Avoids treating arbitrary help arguments as global help.

Testing and reliability

• Added end-to-end watch mode tests covering:
  • Initial build.
  • No immediate self-triggering.
  • Rebuild after source edits.
  • Failed rebuilds keeping the watcher alive.
  • Recovery after fixing the source.
  • Prompt SIGINT termination.
• Added checkpoint resume regression tests for edited proofs, including:
  • Failed-prefix resume after edits that introduce NO_TAC.
  • Direct proofs, replaced prefix leaves, structural branches, dynamic ORELSE replay, and focused/live subgoals.
  • Ancestor-context cases where changes to imported theories affect resumed proof behavior.
• Added support for running selected test cases:
  • make test TESTS="case-name ..."
  • Unknown test case names now fail early with a list of available cases.

Internal/cache infrastructure

• Added a cache entry transfer helper for copying cache action entries and referenced blobs between cache backends.
• Added cache_transfer.sml to the build.
• Exposed package manifest paths for watch set computation.

Documentation

• Updated README examples for the new default build behavior.
• Documented common global options.
• Documented watch mode requirements and unsupported option combinations.

What's Changed

• Add cache entry transfer helper by @charles-cooper in #64
• Add more tests by @xrchz in #75
• Add inotifywait build watch mode by @xrchz in #77
• Improve holbuild help and make build the default by @xrchz in #78

Full Changelog: v0.7.2...v0.8.0

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

holbuild v0.7.1

• Accept [holbuild].required_version as a schema 2 alias for the holbuild version requirement; reject manifests that set both aliases.
• Bump holbuild to 0.7.1.
• Let the test runner resolve the schema 2 HOL toolchain cache automatically and fail fast.