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 _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
