HOL icon indicating copy to clipboard operation
HOL copied to clipboard

Explictly track files that Holmake fails to build in the HOL repo

Open ordinarymath opened this issue 5 months ago • 1 comments

It would be useful if bin/build -t3 can track which bits of the HOL repo has bit rotted.

ordinarymath avatar Jul 15 '25 15:07 ordinarymath

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.

mn200 avatar Jul 16 '25 00:07 mn200