Holmake to rebuild based on theory hashes rather than timestamps

[xrchz]

This would for example avoid cascading rebuilds if you just add a comment to a script file (and it produces exactly the same theory).

[xrchz]

In my vision for this, it would also obviate a rebuild in the following situation. barTheory depends on fooTheory. You add a theorem to fooTheory which is not used in barTheory. Then barTheory does not need to be rebuilt even after fooTheory is rebuilt to include the new theorem.

[mn200]

This seems unlikely. Presumably foo's hash has just changed. In that situation, bar has to rebuild. However, its hash won't change (I suppose). If baz only depends on bar, it won't need to be rebuilt. On the other hand, suppose the change to foo has redefined an important constant that bar uses, but the theorems that bar states have the same statements so that when bar is rebuilt it doesn't change its external nature. (Say the tactics proving bar's theorems are robust in the face of whatever change was made.)

Now theory baz is only explicitly a descendent of bar (so the graph records a link form bar to baz, but not from foo to baz), but it does have a theorem in it that depends on foo. Maybe that theorem is now false... So, we actually have to rebuild everything in baz too (though there'd be lots of similar seeming situations when we'd prefer not to).

[marioxcc]

If this is implemented, it would be better to move the old theory and then compare the new and the old file byte for byte, file instead of overwriting it with the new theory file and then comparing hashes. Although probably theory hashes will never collide in practice, this is not provable, and thus if one were to model the build process, including this optimization, one could not prove that it is correct, not even probabilistically (in cryptography it is common to assume that the hash is a function chosen at random; this approach is used under the name of “pseudorandom function model” but note that this assumption does not match reality).