[isabelle-dev] Code generation in Isabelle
bulwahn at in.tum.de
Thu Jul 21 12:18:04 CEST 2011
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.
More information about the isabelle-dev