Quoting Florian Haftmann <florian.haftm...@informatik.tu-muenchen.de>:
Let those thoughts sink further few days. If there is no veto until Apr
7th, I would go ahead to turn the patches upstream.
You have proposed a change about which doubts were raised. I don't
consider it acceptable to then announce a deadline after which you
will go ahead and push. People simply may not be able to respond in
time, especially in a vacation period.
Regarding interpretation vs sublocale
We are talking about user interface design, and this means choosing
appropriate metaphors for what certain commands do. People familiar
with the history of locales may remember that the precursor of the
sublocale command was
interpretation l < e
before I changed that to sublocale in the reimplementation. This
change was motivated by the realisation that interpretation between
locales essentially means changing the module hierarchy. This is a
remarkable feature for a module system, which deserves emphasis and
isn't really appropriately described by 'interpretation'. In
contrast, interpretation in theories just interprets locales in
theories (even though with "subscription"), there is no additional
value.
From this perspective (which is the perspective of the designer!) it
seems wrong to put interpretation in locales and theories in one
category, and local interpretation (as it might be called) in locale
contexts and in proof contexts in the other. Even, if this made some
aspects of the implementation more elegant. Let me note that, of
course, the user interface design should not make the implementation
unnecessarily complicated (but I believe we are far away from that).
In this light, if a version of the sublocale command seems necessary
in context blocks, why no call it 'sublocale'? Of course, the global
version should remain
sublocale l < e.
It should not be turned into
sublocale (in l) e
because the former much more clearly indicates the change to the
locale hierarchy. This design has the additional benefits that users
don't need to change existing proof documents, terminology in the
literature remains up to date, and, most importantly, the sublocale
command is clearly recognisable in context blocks.
There were two more aspects in the recent discussion. I will pick
them up in separate e-mails since this has got too long already.
Clemens
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
