HOL

Conventions, build commands, and idioms for working on the HOL4 codebase as software — editing `.sml`/`.sig`/`*Script.sml` files, running `bin/build` or `Holmake`, refactoring modules, cleaning up dead code or stale comments, and navigating HOL4's directory structure. Trigger this skill whenever the working directory is a HOL4 checkout and the task touches source files, the build system, code style, or module/identifier naming — even if the user doesn't say "HOL4" explicitly. Covers development-side concerns only; writing theorems, designing proofs, and picking tactics are a separate concern that this skill deliberately doesn't address.

Working on Holmake itself — modifying `tools/Holmake/`, diagnosing why a target rebuilds spuriously, debugging the dep graph, understanding the three-phase `bin/build` flow, the heap-as-implicit-dep mechanism, BIC node semantics, the `HFS_NameMunge` `.hol/objs/` indirection, `--rebuild=mtime` vs `--rebuild=cachekey`, mosml/poly portability of `HM_Cline` options, and how to write Holmake regression tests. Use this skill whenever the task touches `tools/Holmake/**`, `tools-poly/build.sml`, `tools/sequences/*`, Holmakefile syntax, build-order diagnostics, or "why is this rebuilding?" investigations.