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

[Lukas Bulwahn]

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