[isabelle-dev] Code generation in Isabelle

[Lukas Bulwahn]

On 07/25/2011 10:25 AM, Makarius wrote:
> On Sun, 24 Jul 2011, Alexander Krauss wrote:
>
>>>> 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.
>>
>>> I will follow that standard procedure, once all occurrences of the old
>>> code generator invocations are replaced.
>>
>> Put in legacy warnings already now, as they will alert users who 
>> accidentially type the wrong commands (remember our experience with 
>> the methods "evaluation" vs. "eval" last week). You don't have to 
>> wait with this until all else is resolved.
>
> Yes, waiting until certain things are done tends to pile up a lot of 
> unfinished things.  The system is grown (and reduced) from the bottom 
> up, one well-defined step after another.
>
> The situation "all else is resolved" is only ever achieved 
> asymptotically.
>
Legacy warnings are in place; After the next release, the SML code 
generator will disappear from the HOL image.


Lukas

>
>     Makarius