HOL-Theorem-Prover
minisat on Windows slows build down painfully; invoke it more carefully
I assume this is because repeated invocations of minisat via the Process.system is slow. (Or it may be that writing and reading files is slow) My feeling is that the underlying code should figure out if invocation is going to be worth it. Many uses of minisat will be on totally trivial problems that the built-in SML code will perform well on.
There are many invocations of minisat just when loading things like bossLib (and in the course of a build, bossLib is loaded a great deal). Another alternative would be to cache minisat's output on disk so that subsequent theory builds would be quicker (this would at least test if the disk was the problem).
Want to back this issue? Post a bounty on it! We accept bounties via Bountysource.
