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

[Tobias Nipkow]

On 16/11/2017 12:43, Florian Haftmann wrote:
> Dear all,
> 
>> 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.
> 
> streamlining execution of Flyspeck-Tame without risking its integrity is
> a struggle now carrying on twelve years.
> 
> The key question to me is whether the integers in the archives (the ML
> files) are actually used for numeric calculation (+, *, …) or are just
> mere identifiers (=, maybe <).  In the latter case there are a couple of
> possibilities not explored so far.

They are just identifiers and I don't think they are computed with. However, I 
don't intend to change formalization beyond a global implementation of int by 
some fixed size integers, if that can be done easily. Otherwise we live with the 
increase in runtime from 7:20 to 8:20.

Tobias

> Cheers,
> 	Florian
> 

-------------- 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/20171117/fd66bff1/attachment.bin>