Re: [isabelle] Isabelle2014-RC0 available for testing



Am 06.07.2014 um 10:14 schrieb Yannick Duchêne (Hibou57) <yannick_duchene at yahoo.fr>:

> So `datatype_new` will always be named the same? I though it will be renamed to just `datatype` and replace the old one.

Hopefully not always. ;) For the 2014 release, our goal was to have "datatype_new" inside "Main" [*]. We've succeeded with that. For the following release (presumably 2015), I hope we can rename "datatype_new" to "datatype" and move the old command to "src/HOL/Library", but this is a delicate operation, and it may be that it takes more than one release cycle before we get there.

On the positive side, "list" and "option" are already defined using the new command, and the large IsaFoR library has been successfully ported. There's also more and more infrastructure that can deal with "datatype_new", including "fun", Lifting & Transfer, Nitpick -- and the "datatype_compat" command, which registers new-style datatypes as old-style ones, now works better than ever.

Jasmin

[*] This was, in fact, a goal for Isabelle2013-1 (cf. my 30 July 2013 email to the mailing list), but we ran out of time (moving "datatype_new" to "Main" required reducing its dependencies significantly, among other things), and the whole plan presented in that email got postponed by one release.





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.