[isabelle-dev] \nexists

[Lars Hupel]

> 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