Release holbuild v0.8.0 · HOL-Theorem-Prover/holbuild

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.

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.

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.

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