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

Attachment: smime.p7s
Description: S/MIME cryptographic signature

_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Reply via email to