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
> 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
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:
In the worst case, we could split the slow sessions manually by extra
isabelle-dev mailing list