Re: [isabelle-dev] [isabelle] Code generation in Isabelle
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
Re: [isabelle-dev] [isabelle] Code generation in Isabelle
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
Re: [isabelle-dev] [isabelle] Code generation in Isabelle
Actually, there is a third code generator hidden somewhere in Isabelle. - Steven On 21.07.2011, at 12:18, Lukas Bulwahn wrote: > Hello all, > > > 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. > > > Any thoughts? > > > Lukas > > > ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] [isabelle] Code generation in Isabelle
We moved recently to the new code-generator. Burkhart Am 21.07.2011 um 12:18 schrieb Lukas Bulwahn: > Hello all, > > > 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. > > > Any thoughts? > > > Lukas > > > ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
