[isabelle-dev] New (Co)datatypes: Status & Plan (FYI)

[Florian Haftmann]

Hi Jasmin,

> There will be a high level of compatibility between the old and the
new package.
> For nonnested recursive datatypes, compatibility is quasi-100%; and for nested
> datatypes, the package will support an optional "nested to mutual" reduction to
> simulate the old package, so that the same theorems as before are available
> (albeit under different names).

has an explicit need for a »nested to mutual« mode ever been
articulated?  In my personal opinion this construction has always
appeared counter-intuitive, because the inherent redundancy with an
existing type springs to your eyes after you have done this game a few
times.  Maybe a chance to save some work.

> A rough, optimistic time plan follows.

Overall, a realistic and reasonable schedule.

> October--December 2013 (?):
>     Release Isabelle2013-1 with both "datatype" and "datatype_new"
> 
> Spring 2014:
>     Rename {"datatype" |-> "legacy_datatype", "datatype_new" |-> "datatype"}
>
> Summer/Fall 2014:
>     Release Isabelle2014 with both "legacy_datatype" and "datatype"

Is there any experimental evicdence how many datatype specifications
would break by a drop-in replacement (real applications, not
demonstration examples)?  If this is significantly little, I would even
think about doing the switch {"datatype" |-> "legacy_datatype",
"datatype_new" |-> "datatype"} immediately.  The »_new« suffix has a
strange connotation of »almost done… ad multos annos«.

Cheers,
	Florian

-- 

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 261 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20130804/c738b76b/attachment.sig>