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