Re: [isabelle] should this use of the datatype package produce an error?

On Fri, 16 Apr 2010, Brian Huffman wrote:

A feature request: If the name of a constant contains a space or other illegal character, the datatype package should issue an error (or at the very least, a warning message).

This known problem shows up once a year or so.  By using the proper local theory layer for the package, it will just dissappear, because there are sanity checks built in.  Numerous other problems will be solved by localizing old-style packages.

So your recommendation is to wait until the datatype package has been converted to use local theories, rather than adding any new (temporary) error checks. OK.

So far it is just another motivitation to start moving towards a localized version. The datatype package is very complex, and Stefan Berghofer is probably the only one who can update it without causing collateral damage.

Anyway, I think Stefan is already trying some small-scale improvements, although such long standing oddities are hard to reform. For example, old-style mixfix notation involves constant names with spaces and with non-identifier characters, e.g. "op #". Due to earlier spring cleaning it might actually work out this time.

Maybe now is a good time for some spring cleaning, before we get too close to the next Isabelle release.  (It is already > 4 months after Isabelle2009-1.)

So will the conversion of the datatype package be part of this "spring cleaning"? Has anyone committed to doing the conversion? Of course, I'll take responsibility for converting the domain package, but I need to have the datatype package done first, so I can see how it's done.

Full localization is certainly beyond the spring cleaning, it will take more time. If you want to do some moves towards it for the domain package, I can point to some spots that are probably easy to update.


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