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

[Makarius]

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.

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.


	Makarius