[isabelle-dev] [isabelle] Code generation in Isabelle

[Burkhart Wolff]

We moved recently to the new code-generator.

Burkhart

Am 21.07.2011 um 12:18 schrieb Lukas Bulwahn:

> Hello all,
> 
> 
> at the moment, we have two code generators in Isabelle:
> 
> 1. An ancient code generator in Isabelle by Stefan Berghofer - limited to SML without supporting type classes.
> Commands to invoke it were code_module and code_library.
> 
> 2. A generic code generator in Isabelle by Florian Haftmann - extenible to multiple target languages, supporting type classes, basic integration of reflection and abstraction mechanisms
> Commands to invoke it are export_code, value, code_reflect, and some others.
> 
> 
> The second subsumes the first, so we intend to remove the first code generator from the next Isabelle distribution if there are not any strong defenders of the ancient code generator.
> 
> 
> Any thoughts?
> 
> 
> Lukas
> 
> 
>