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.



Attachment: smime.p7s
Description: S/MIME Cryptographic Signature

isabelle-dev mailing list

Reply via email to