search

HOL-Theorem-Prover / HOL

Canonical sources for HOL4 theorem-proving system. Branch develop is where “mainline development” occurs; when develop passes our regression tests, master is merged forward to catch up.
https://hol-theorem-prover.org
Other
617 stars 138 forks source link

More precise control of Holmake --fast #371

Open SOwens opened 7 years ago

SOwens commented 7 years ago

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 commented 7 years ago

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.