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
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
