[isabelle-dev] NEWS: limited name space accesses

[Christian Sternagel]

Very nice!

I'll wait until the naming issue is settled before replacing my many 
uses of "hide_const (open) ...".

A further naming suggestion:

  (a) private/hidden
  (b) qualified

the latter is akin to Haskell's "qualified" import.

cheers

chris

PS: I'm still waiting for

   isabelle build -n -a -d '$AFP' -k qualified

to finish (but I guess proper checking, taking semantics into account, 
is just expensive). Oops, while writing this email I obtained:

*** java.lang.OutOfMemoryError: Java heap space
0:03:32 elapsed time, 0:05:46 cpu time, factor 1.63

(Maybe because in parallel I am still waiting on

   isabelle build -v -n -a -d '$AFP' -k hidden -k private

? Which seems to "hangs" at "Session Pure/RAW" now for several minutes.)

On 04/07/2015 02:07 PM, Makarius wrote:
> * Local theory specification commands may have a 'private' or
> 'restricted' modifier to limit name space accesses to the local scope,
> as provided by some "context begin ... end" block. For example:
>
>    context
>    begin
>
>    private definition ...
>    private definition ...
>    private lemma ...
>
>    lemma ...
>    lemma ...
>    theorem ...
>
>    end
>
>
> This refers to Isabelle/83071f4c8ae6.
>
> After more than 10 years in the pipeline, and never-ending efforts to
> localize almost all tools, there is now the long anticipated limitation
> of name space accesses. There are presently two example applications:
>
> (1) Local tool setup with some auxiliary constants: "induct_forall" etc.
> in
> http://isabelle.in.tum.de/repos/isabelle/file/83071f4c8ae6/src/HOL/HOL.thy#l1377
>
>
> (2) Plain specifications that are meant to produce theory-qualified
> names: AList.update etc. in
> http://isabelle.in.tum.de/repos/isabelle/file/e83ecf0a0ee1/src/HOL/Library/AList.thy#l11
>
>
>
> I am still not 100% sure about the choice of keywords.  There are two
> concepts that are supported: (a) totally inaccessible name space entry,
> (b) name space entry that is only accessible by qualified names, not the
> base name.
>
> Presently we have:
>
>    (a) 'private'
>    (b) 'restricted'
>
> I first started out implementing 'private' for the sake of Eisbach,
> which really needs that.  Then I noticed that in practice one mostly
> uses 'restricted' to eliminated old "hide (open)", but this keyword is a
> bit awkward.
>
> Here are some possible alternatives:
>
>    (a) 'hidden'    (like Long_Name.hidden according to Isabelle/ML
> terminology)
>    (b) 'private'   (like 'private' in Java/Scala, in non-serious mode)
>
> or:
>
>    (a) 'private'   (like 'private' on Java/Scala in serious mode)
>    (b) 'local'     (like an ancient Isabelle command of that name)
>
>
> By non-serious mode I mean the rather easy way to bypass 'private'
> declarations on the JVM via reflection.  Likewise our logical
> environment always allows to access inaccessible names, after some
> tweaking of the name space, e.g. via aliases.  This could justify the
> use of 'private' for what is now 'restricted', or it might be just too
> confusing to users.
>
>
> Note that it is now releatively easy to test feasibility of new keywords
> like this:
>
>    $ isabelle build -n -a -d '$AFP' -k hidden -k local
>
>
>      Makarius
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev