[isabelle-dev] Code generation in Isabelle
makarius at sketis.net
Mon Jul 25 10:25:49 CEST 2011
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
>> 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.
More information about the isabelle-dev