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
