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

[Fabian Immler]

> Am 02.11.2017 um 18:00 schrieb Makarius <makarius at sketis.net>:
> 
> 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.
At least on my Mac, there seems to be a problem with (or induced by) parallelism:
The attached check.sml is the code extracted from Lorenz_C0.
"Check.check xs" does a Par_List.forall on the list xs and Par_list.map in the computation for individual elements.

With isabelle/fc87d3becd69 and polyml-test-e8d82343b692/x86_64-darwin, something goes very wrong: a slowdown by a factor of more than 50, compared to Isabelle2017 .

This seems to be related to parallelism:
In check_seq.sml, I replaced Par_List.forall/Par_list.map with list_all/map. In this case isabelle/fc87d3becd69 behaves more or less like Isabelle2017.

I also tried isabelle/fc87d3becd69 with polyml-5.6-1/x86_64-darwin: this behaves for both parallel and sequential computations like Isabelle2017.

Unfortunately, I failed to reproduce this behavior on Linux.

Any ideas?

Fabian


-------------- next part --------------
A non-text attachment was scrubbed...
Name: Scratch.thy
Type: application/octet-stream
Size: 2011 bytes
Desc: not available
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20171103/9525cacc/attachment-0001.obj>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: check_seq.sml
Type: application/smil
Size: 1025032 bytes
Desc: not available
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20171103/9525cacc/attachment-0002.smi>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: check.sml
Type: application/smil
Size: 1025040 bytes
Desc: not available
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20171103/9525cacc/attachment-0003.smi>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: smime.p7s
Type: application/pkcs7-signature
Size: 4848 bytes
Desc: not available
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20171103/9525cacc/attachment-0001.p7s>