[isabelle-dev] [isabelle] Code generation in Isabelle
makarius at sketis.net
Sun Jul 24 16:57:25 CEST 2011
On Thu, 21 Jul 2011, Lukas Bulwahn wrote:
> 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.
I have asked this question several years ago already, but there were a few
reasons not to delete it immediately, which I have forgotten (or not fully
understood in the first place).
Some months ago I have renovated some really old HOL reference manual
material, and moved the new version to the isar-ref. This has included
the code generator, see section 10.15.2 in isar-ref of
Isabelle/521de6ab277a. Apart from repainting the walls and renewing the
wallpapers just before demolition, I've also observed that the old code
generator is still in use in several places: some applications by Stefan
Berghofer (HOL-Proofs/Lambda and Extraction, AFP/POPLmark-deBruijn), and
MicroJava and its clones/descendants in AFP.
Anyway, the standard procedure for removal of old stuff is to start
marking it as "old" or "legacy" in the NEWS, and emitting suitable
legacy_warnings. This can also mean to move the source modules to another
place, like src/HOL/Library/Old_Codegen.thy in this situation. After 1 or
2 full release cycles the material is then removed altogether. Things
that have been there for such a long time cannot be removed abruptly,
without causing damage or confusion somewhere.
Aside: On page 232 of the above-mentioned manual there is an example about
const_code wfrec. The same is still used here in MicroJava:
The source says "Code generator setup (FIXME!)".
The changelog says: "no consts_code for wfrec, as it violates the "code
generation = equational reasoning" principle" (before it was in
Does that mean there is something utterly wrong with MicroJava?
More information about the isabelle-dev