On 07/24/2011 04:57 PM, Makarius wrote:
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).
As you have asked this question several years ago, it seems like an
effort that is worthwhile to be continued.
Several years ago, there still were some open issues, execution of
inductive predicates, executing partial functions, program extraction,
which now should all be resolved -- or only minor issues remain, that
could now be fixed easily.
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.
I will look at these applications, and can probably replace them by new
equivalent operations with the new code generator.
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.
I will follow that standard procedure, once all occurrences of the old
code generator invocations are replaced.
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?
I will look into this issue and can report here, in the changelog, or in
the NEWS about its solution.
Lukas
Makarius
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev