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
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