[isabelle-dev] Slow builds due to excessive heap images

[Makarius]

On 02/11/17 16:11, Lars Hupel wrote:
> 
> Tobias and me have discovered an interesting discrepancy between your
> AFP slow setup and our AFP slow setup. They run on identical hardware
> with the only difference of 6 vs 8 threads. On 6 threads, it runs
> significantly faster. For example, Flyspeck-Tame requires 9:44:16
> (elapsed time on 8 threads) vs 8:50:55 (elapsed time on 6 threads).

It was merely my intuition about the virtual hardware that using less
resources than allocated might help. But I did not make any measurements
with 8 vs. 6 threads, so that guess might be still wrong.

The main observation so far: it works quite well and measurements are
reasonably stable.


> That difference aside, what I also find alarming is that the total
> runtime of Flyspeck-Tame increased by more than 20% after the switch to
> Poly/ML 5.7.

I've had some private email exchange with David Matthews about it. It is
a consequence of a bias towards FixedInt instead of IntInf (= Int) in
the ML code generator. There is some chance that Flyspeck-Tame actually
works with FixedInt, but I did not try it yet.

Which Isabelle codegen options are required to use FixedInt instead of
mathematical Int?

Here is also an experiment to make the present setup
(polyml-test-e8d82343b692) a bit faster:
https://github.com/polyml/polyml/tree/NewTestRegisterSave -- I have some
tests with that still running.


I am more worried about the factor 5 performance loss of Lorenz_C0: now
(3:26:41 elapsed time, 16:49:16 cpu time, factor 4.88). It is unclear if
the problem is related to Flyspeck-Tame. I did not approach it yet,
because the HOL-ODE tower is really huge.

It would greatly help to see the problem in isolated spots. I usually
send David specimens produced by code_runtime_trace.


> This now means that the slow sessions rapidly approach 24 hours
> in build time, which makes it less feasible to run them every day.

That is already an old AFP tradition :-) Applications are constantly
pushing towards the end of it all, but so far the technology has managed
to keep up.

For the non-slow tests, I have already split AFP into two structually
quite stable parts:
http://isabelle.in.tum.de/repos/isabelle/file/fc87d3becd69/src/Pure/Admin/afp.scala#l86

In the worst case, we could split the slow sessions manually by extra
group tags.


	Makarius