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
smime.p7s
Description: S/MIME Cryptographic Signature
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
