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

[Fabian Immler]

> Am 03.11.2017 um 14:56 schrieb Fabian Immler <immler at in.tum.de>:
> 
> 
>> 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.

I think I could reproduce the problem on lxcisa0 (with ML_OPTIONS="--minheap 1600 --maxheap 4000" if that is relevant).
Invoked with "isabelle build -d . -othreads=8" for the theory below.

polyml-test-e8d82343b692/x86_64-linux: (0:02:37 elapsed time, 0:18:11 cpu time, factor 6.94)
polyml-5.6-1/x86_64-linux: (0:00:30 elapsed time, 0:02:24 cpu time, factor 4.70)

Both are in isabelle/123670d1cff3

--

theory Check
imports Pure
begin

ML_file \<open>check.sml\<close>
ML \<open>timeap Check.check (0 upto 7)\<close>

end


-------------- next part --------------
A non-text attachment was scrubbed...
Name: smime.p7s
Type: application/pkcs7-signature
Size: 4848 bytes
Desc: not available
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20171103/aac2e60e/attachment.bin>