On Thu, 2 Dec 2010, Alexander Krauss wrote:
I'll have a look at the code and see if packages can reject this from
the user, while still being composable. This applies to all packages.
In fact I've made this error already in 2005, and it was Alex himself who
convinced me more recently that packagages cannot realistically do any
check here, because the thing is so obscure that hardly any package author
will get to the point.
Back to history: in 2005 Brian had a paper on TPHOLs with a footnote about
an unexpected crash of the typedef package due to hidden polymorphism in
the set involved, not the type. What I did then is to make the typedef
package insert "itself" arguments in the way one would think of as a first
idea. This made the problem go away for the moment, although it
complicated the package implementation. When Larry was asking me about
that change of typedef later, I also failed to explain to him both the
problem and its solution.
After Local_Theory.define started handling the problem uniformly once and
for all, I could remove lots of strange code from typedef, and be sure at
the same time that all other (localized) packages would stop crashing
on the same kind of problem.
When we speak about "users" of packages it covers both ML and Isar theory
sources, e.g. the function package is a user of the inductive package.
It is important to keep modularity here.
The system is able to distinguish between things that are visible in the
source vs. internal uses of the same specifciation mechanisms to some
extent, but one needs to look very closely at that when modifying the
behaviour here. We have already a long track record of very abscure
crashes due to errors that are emitted too eagerly, e.g. in declaration
attributes that insist in certain input and choke on the transformed
version after some interpretations.
Part of the inherent complexity of local theory specifications is due to
interpretation wrt. the "target context", which always happens when
writing down specifications like 'definition' or 'inductive'. This is not
the primitive consts + defs that we had many yours ago. And of course,
the extra complexity localized specifications was not introduced for fun,
but to address concrete problems that had accumulated over a couple of
years of less systematic treatment of these issues. Compared to the
situation before it, there are very little problems left that need some
fine tuning.
Makarius
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
