> In contrast, a full "build -a" for the formal content is vital. The > shorter that takes, the more it becomes second nature to do it > frequently -- I often do it for every single changeset (before the local > commit).
Not all of us have the appropriate hardware to do that. Speaking about TUM, everyone has at most a quad-core laptop. That's why the testboard is equipped with a total core count of 22, so that "hg push -f testboard" may become "second nature". > That also depends on good physical measurements: that was historically > done without Latex getting in between. I would be the first person to decouple LaTeX processing from the build, but it is impossible as it stands today. You cannot run LaTeX standalone without also running a full build. Speaking about physical measurements: Here are the last build times of JinjaThreads from the past five days: 0:57:36 elapsed time, 3:48:46 cpu time, factor 3.97 0:57:30 elapsed time, 3:48:31 cpu time, factor 3.97 0:58:36 elapsed time, 3:51:08 cpu time, factor 3.94 0:58:36 elapsed time, 3:51:08 cpu time, factor 3.94 0:57:43 elapsed time, 3:48:49 cpu time, factor 3.96 (timings on a VM with threads=8) And for another arbitrary session (Incompleteness): 0:12:08 elapsed time, 0:22:53 cpu time, factor 1.89 0:12:03 elapsed time, 0:22:39 cpu time, factor 1.88 0:12:00 elapsed time, 0:22:52 cpu time, factor 1.90 0:12:26 elapsed time, 0:23:43 cpu time, factor 1.91 0:11:52 elapsed time, 0:22:39 cpu time, factor 1.91 (dedicated machine with threads=2) I'll let others judge whether the variance here is small enough to be useful. Cheers Lars _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev