On 25/10/17 14:29, Chun Tian wrote: > HOL doesn’t rebuild everything when you re-run “bin/build”: it only rebuilds > changed theories and all dependencies. Sometimes you need to re-run “poly < > tools/smart-configure.sml” and rebuild everything, other times you need to > clean everything “bin/build cleanAll” to fix the building process.
How do I know if I have to re-run “smart-configure.sml”? Also, is there some way I can run build jobs in parallel? In my experience when making changes, it rebuilt nearly everything and took approximately the same time as compilation from scratch. Probably that was because I modified the theory “res_quan” which has many descendants. > Anyway, I think by large chances you only need 10 minutes to keep your build > up-to-date. But if I have a poly process with everything loaded, I can > normally use it even when HOL is rebuilding. Running HOL while coiling seems prone to errors. Very probably there are race conditions between the compilation process and interactive loading of HOL files (e.g.: a file can be read while it was being written to). Thanks. -- Do not eat animals; respect them as you respect people. https://duckduckgo.com/?q=how+to+(become+OR+eat)+vegan
signature.asc
Description: OpenPGP digital signature
------------------------------------------------------------------------------ Check out the vibrant tech community on one of the world's most engaging tech sites, Slashdot.org! http://sdm.link/slashdot
_______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
