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

[Tobias Nipkow]

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.

Tobias

> 
> 	Makarius
> 

-------------- next part --------------
A non-text attachment was scrubbed...
Name: smime.p7s
Type: application/pkcs7-signature
Size: 5156 bytes
Desc: S/MIME Cryptographic Signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20171108/5b97ce94/attachment.bin>