Stream: Beginner Questions

Topic: Generated code slower than "value" command

Sage Binder (Jul 30 2024 at 05:41):

Hi all,

I've written an Isabelle algorithm and exported it to Scala. It seems that the Scala code runs much slower than when using the "value" command within Isabelle, even when I compile the Scala with -opt:inline:**.

I thought the "value" command uses Scala behind the scenes, so I expected the performance of the generated code to match the performance of "value". What can I do to get the performance of my generated code, whether in Scala or another language, to match the "value" command's performance?

Thanks

Mathias Fleury (Jul 30 2024 at 09:09):

eval is using Standard ML (more precisely the PolyML compiler)

Mathias Fleury (Jul 30 2024 at 09:14):

Without knowing exactly what you did it is hard to know where the problem comes from. But:

• Scala and java do not immediately JIT compile the code there are using.
• for better code performance you want the native integers instead of the default Peano representation
• (rather unlikely but depends on your code) when using native 32-bit uint, scala suffers from the encoding as there are no unsigned in java

Manuel Eberl (Jul 31 2024 at 19:52):

Wasn't there also an issue about curried functions being slow in scala or has that been resolved?

Mathias Fleury (Aug 01 2024 at 08:41):

I am not aware of an issue, but I though that the generated code was uncurried in scala by default?

Last updated: Dec 21 2024 at 16:20 UTC