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

[Makarius]

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:
http://isabelle.in.tum.de/repos/isabelle/annotate/eee4fa79398f/src/HOL/MicroJava/J/TypeRel.thy#l100

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 
src/HOL/Wellfounded.thy).

Does that mean there is something utterly wrong with MicroJava?


 	Makarius