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

[Andreas Lochbihler]

Hi Makarius,

On 08/11/17 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.

My AFP entry Native_Word basically provides the setup for unsigned fixed-size integers, 
but as a separate type uintXX. The same could be done for signed fixed-size integers. The 
problem is how to get from int to uintXX. There are basically two options:

1. Just axiomatize that int are implemented with uintXX. This is potentially unsound.

2. Prove that actually no overflow occurs in the computations. The AFP entry 
Berlekamp-Zassenhaus does that for factoring polynomials over finite fields. The basic 
setup is there, but applying it to a particular instance requires quite some work.

FixedInt has the additional challenge that the width is implementation dependent, so this 
requires a few tricks similar to the formalisation of uint in the AFP entry.

In summary: In principle it could be possible to use FixedInt in Flyspec-Tame in a sound 
way, but it would be quite a bit of work.

Andreas