Re: [isabelle] datatype_compat in Isabelle2018-RC0

Hi Gerwin,

> The datatype_compat command used to generate the old-style definition of the “size” constant in Isabelle2017 (potentially only when  size did not yet exist). This no longer seems to be the case.
> Is this intentional? I couldn’t find anything relevant in NEWS.

The reason why the old-style definitions were supported for so long at all was for the benefit of the "old_datatype" command. The thread "Any users of 'Old_Datatype.thy' or 'Old_SMT.thy'?" (started in December 2017) didn't reveal any users, so when I removed the legacy "old_datatype", I also removed the old-style size infrastructure (which itself is an important step towards removing the last left-overs from the old datatype package from Isabelle, to keep the Isabelle code in a not too messy state).

> I’m using this a few times — not very often, but it’s annoying enough to recreate manually (see email thread on that around Isabelle2017..) that it’s worth checking at least.

I would like to know more about your use case. It seems like you found a corner case of the datatype package -- namely, you're presumably disabling "size" first, then invoking "datatype_compat" to produce an old-style "size". Is your main motivation for the use of old-style "size" definitions compatibility (i.e. no need to port old scripts), or do you find the old definitions intrinsically better?

The reason I'm asking is that there are advantages and disadvantages to both schemes, and it may be worthwhile to just support both, e.g. via an option.



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