Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Scala Code Generation

Email Gateway (Aug 18 2022 at 18:12):

From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi all,

since Isabelle2011 there is the possibility to generate Scala code from
HOL theories. Some minor problems can be circumvented by a suitable
patch and will disappear in the next release.

Apart from that, is there any further feedback (positive or negative) on
code generation for Scala? I would like to announce it on the Scala
mailing list after the next release, but for this I need some evidence
that it is really working.

Thanks for any feedback,
Florian
signature.asc

Email Gateway (Aug 18 2022 at 18:16):

From: Thomas Genet <Thomas.Genet@irisa.fr>
Dear Florian,

as I already mentioned to you, we will use Isabelle2011 and Scala export
for teaching on the second semester here at Rennes 1 University at
master level. We already experimented a bit with the scala export in
order to integrate formally developed components (in Isabelle) into Java
software. For the moment everything is OK... but it is true that we will
use only simple things: integers, strings, lists, etc... no exotic
Isabelle theory :-)

Best regards,

Thomas

Email Gateway (Aug 18 2022 at 18:19):

From: René Thiemann <rene.thiemann@uibk.ac.at>
Dear Florian,

concerning our formalization IsaFoR/CeTA we can give the following picture:

• the generated code has quite some size (Haskell: 600k source, Scala: 1200k source)
• compilation for both Haskell and Scala without problems
• running the programs on example library runs smoothly with Haskell, but there are problems with Scala:
  • Haskell binary can run all examples without problems
  • almost all examples crash with Scala binary with Stack-overflow
  • after setting Stack-size to 2000m, roughly 1/5 of examples still crashes
  • rewriting the corresponding function to tail-recursive variant did not help much
  • whole benchmark requires 2s with Haskell binary, 40s with Scala binary

(as a side remark: we have similar problems with OCaml-code where large
strings have to be converted from OCaml-strings to character lists)

Cheers,
Chris and René

Email Gateway (Aug 18 2022 at 18:20):

From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi René,

thanks for those interesting figures.

I would guess that the scalability matter indeed has to do with
packing/unpacking strings to character lists, which is a no-op in
Haskell. The factor 2 in code size seems plausible.

Have you ever tried to generate the whole application without the
explicit parsing?

Cheers,
Florian
signature.asc

Last updated: Apr 20 2024 at 12:26 UTC