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

[Manuel Eberl]

If there are fixed-size integers in ML that raise an exception on
overflow, it should be possible to just do appropriate code_printing
setup similar to what Code_Target_Numeral does. We already have to
somehow magically map Isabelle's "int" type to ML's "IntInf" type, so
all we have to do is to locally map it to ML's fixed size "int" instead,
I think.

Manuel


On 2017-11-08 15:36, Tobias Nipkow wrote:
>
>
> On 08/11/2017 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.
>
> Then I misunderstood. An optional use of FixedInt for languages where
> overflow raises an exception is fine with me.
>
>> 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.
>
> In which case I would say that providing such an option should be
> balanced with the complexity it requires or introduces.
>
> Tobias
>
>>
>>     Makarius
>>
>
>
>
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20171108/33887230/attachment-0002.html>