feature request: (more) incremental builds

[charles-cooper]

iiuc build caching in hol4 works at the file level -- if a file is proved, then its artifacts can be reused. this issue is a feature request for inter-file caching. if there is a change at line X+1, lines X and previous do not need to be re-proved(!)

more sophisticated and better would be to only require re-proving dependencies (direct+transitive) of changed theorems (including in downstream files -- if there is no changed theorem in a theorem's dependency tree it should not require re-proving).

[xrchz]

I don't think Holmake knows anything about within-theory dependencies. The information does exist at the kernel level though, I think (thanks to tictactoe..). Seems like this issue is pretty related to #488 or #554

[mn200]

This would actually require work at the level of hol more than with Holmake. If a file has been changed, it will need to be reprocessed, but the suggestion is that as the changed file is processed, some of its prefix can be skipped and theorems simply asserted rather than reproved. Some sort of hash-based cache might be required.