Re: [isabelle] Scala Code Generation



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é

Am 11.08.2011 um 15:00 schrieb Florian Haftmann:

> 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
> 
> -- 
> 
> Home:
> http://www.in.tum.de/~haftmann
> 
> PGP available:
> http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
> 






This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.