[isabelle-dev] Slow builds due to excessive heap images
nipkow at in.tum.de
Wed Nov 8 15:36:21 CET 2017
On 08/11/2017 14:13, Makarius wrote:
> On 08/11/17 12:35, Tobias Nipkow wrote:
>> On 07/11/2017 23:13, Makarius wrote:
>>> For Flyspeck-Tame a small performance loss remains. It might be worth
>>> trying to configure the Isabelle/HOL codegen to use FixedInt instead of
>>> regular (unbounded) Int. Thus it could become faster with Poly/ML 5.7.1
>>> than with 5.6.
>> Just as for Isabelle itself, I don't want generated code to abort with
>> overflow or even worse to overflow silently.
> I also don't want to see FixedInt used routinely instead of proper
> mathematical Int.
> The idea above is to provide an option for the HOL codegen that is used
> specifically for applications like Flyspeck-Tame. It is mainly a
> question to codegen experts, if that can be done easily.
Then I misunderstood. An optional use of FixedInt for languages where overflow
raises an exception is fine with me.
> If the answer is "no", I personally don't mind. Flyspeck-Tame runs
> de-facto only in background builds: 1-2h more or less does not matter so
> much. Its classic runtime was actually 10h total, now we are at 7h.
In which case I would say that providing such an option should be balanced with
the complexity it requires or introduces.
-------------- next part --------------
A non-text attachment was scrubbed...
Size: 5156 bytes
Desc: S/MIME Cryptographic Signature
More information about the isabelle-dev