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
>
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
