[isabelle-dev] Slow builds due to excessive heap images
nipkow at in.tum.de
Fri Nov 17 16:45:10 CET 2017
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.
-------------- next part --------------
A non-text attachment was scrubbed...
Size: 5156 bytes
Desc: S/MIME Cryptographic Signature
More information about the isabelle-dev