HOL
HOL copied to clipboard
Explictly track files that Holmake fails to build in the HOL repo
It would be useful if bin/build -t3 can track which bits of the HOL repo has bit rotted.
I think your issue title is inaccurate: if build tries and fails to build in a directory, then build will fail overall, and that is caught by the regression tests.
As per the text of your issue, the issue is bit-rotting of stuff that build doesn't even attempt to build. This is meant to be detected by checkbuilds, and what I'd do, I think, is have an option to build that causes checkbuilds to be called after the usual build completes. If that then produces unexpected output, the whole process can fail.