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