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

[Fabian Immler]

I should have sent the message below also to isabelle-dev, sorry about that.
Has anything changed about integers in Poly/ML 5.7.1?

Lorenz_C0 did slow down by a factor of 5, which I find quite extreme.

Best,
Fabian

> Am 28.10.2017 um 23:57 schrieb Fabian Immler <immler at in.tum.de>:
> 
> Lorenz_C0 is one of those "much slower" sessions.
> If it helps, this is how I would characterize it:
> It is essentially one long computation where the code (IIRC about 15000 lines in SML) was generated in the parent session Lorenz_Approximation via @{computation_check ...}). The computation depends heavily on IntInf operations (but mostly in the <64 bit range)
> 
> Fabian
> 
>> Am 28.10.2017 um 22:45 schrieb Makarius <makarius at sketis.net>:
>> 
>> On 28/10/17 22:26, Makarius wrote:
>>> We are presently testing Poly/ML 5.7.1 by default (see
>>> Isabelle/aefaaef29c58) and there are already interesting performance
>>> figures, e.g. see:
>>> 
>>> http://isabelle.in.tum.de/devel/build_status
>>> http://isabelle.in.tum.de/devel/build_status/Linux_A
>>> http://isabelle.in.tum.de/devel/build_status/AFP
>> 
>> The daily "AFP slow" timing has arrived just now, 4h hours later than
>> with Poly/ML 5.6:
>> http://isabelle.in.tum.de/devel/build_status/AFP_slow_64bit_6_threads
>> 
>> I still need to investigate, why some sessions require much longer now.
>> It might be due massive amounts of generated code.
>> 
>> 
>> 	Makarius
>> _______________________________________________
>> isabelle-dev mailing list
>> isabelle-dev at in.tum.de
>> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
> 

-------------- 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/20171102/e2af6b01/attachment.bin>