[isabelle-dev] Code generation in Isabelle

Lukas Bulwahn bulwahn at in.tum.de
Mon Jul 25 14:18:43 CEST 2011

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.


>     Makarius

More information about the isabelle-dev mailing list