More precise control of Holmake --fast

[SOwens]

When running a Holmake --fast on a project that relies on unbuilt theories in HOL's own examples directory, it builds those theories cheated, which affects other projects where you might not want the cheats. It would be nice to have the option of still running the proofs for things in HOL/examples.

--- Want to back this issue? **[Post a bounty on it!](https://www.bountysource.com/issues/39259598-more-precise-control-of-holmake-fast?utm_campaign=plugin&utm_content=tracker%2F495335&utm_medium=issues&utm_source=github)** We accept bounties via [Bountysource](https://www.bountysource.com/?utm_campaign=plugin&utm_content=tracker%2F495335&utm_medium=issues&utm_source=github).

[xrchz]

There is a workaround: build the early dependencies with Holmake and only use Holmake --fast after they are built. This workaround could potentially be automated with a wrapper script.

Do you have any suggestion of how you'd want the Holmake interface for this functionality to look? Maybe an --exclude=pattern command line option; but I'm not sure the complexity for gain ratio is that good.