[isabelle-dev] Slow builds due to excessive heap images
andreas.lochbihler at inf.ethz.ch
Wed Nov 8 14:44:39 CET 2017
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.
More information about the isabelle-dev