Re: [isabelle-dev] NEWS: limited name space accesses
On 04/17/2015 12:04 AM, Makarius wrote: On Tue, 7 Apr 2015, Christian Sternagel wrote: 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.) Maybe this is just the normal behaviour of the JVM under low-memory conditions. I routinely have local settings like this: ISABELLE_BUILD_JAVA_OPTIONS=-Xms1024m -Xmx4096m -Xss4m Thanks for the hint! This even worked with two checks running in parallel (each of which finished in less than 4 minutes). cheers chris ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] NEWS: limited name space accesses
On Tue, 7 Apr 2015, Christian Sternagel wrote: 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.) Maybe this is just the normal behaviour of the JVM under low-memory conditions. I routinely have local settings like this: ISABELLE_BUILD_JAVA_OPTIONS=-Xms1024m -Xmx4096m -Xss4m This can't be as aggressive by default, because it means it won't work at all on small / 32bit machines. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] NEWS: limited name space accesses
On Tue, 7 Apr 2015, Makarius wrote: On Tue, 7 Apr 2015, Tobias Nipkow wrote: On 07/04/2015 14:37, Christian Sternagel wrote: (b) qualified That gets my vote because it expresses clearly the description Makarius gave: name space entry that is only accessible by qualified names It is definitely good to collect keyword candidates from other well-known languages. I had qualified on my list of possibilities at first, but was hesitating to use it, because there is yet another concept (c) that has no Isar notation so far. It is called Binding.qualified in ML and could solve problems like https://lists.cam.ac.uk/mailman/htdig/cl-isabelle-users/2015-February/msg00038.html qualified lemma a: ... lemma b (qualified c): ... lemma e (qualified f!): ... After thinking about this again, it looks like the following is feasible: now: private lemma a: ... -- no name space accesses qualified lemma a: ... -- only qualified name space accesses later, after the release: lemma x.y.a: -- qualified 'base' name leading to mandatory accesses This means Binding.qualified is not involved here at all. The second reform merely allows Binding.name / Binding.make with already qualified names. There will be further consequences from this that we can explore after the release, such as Free variables with qualified names. The 'private' / 'qualified' command above prefixes are technically already there, and I will just make one more round of renaming before we get onto the release lane. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] NEWS: limited name space accesses
On 07/04/2015 16:28, Makarius wrote: A real danger in the whole affair is that we need to proceed towards the Isabelle2015 release very soon, i.e. this week. Which in the past would have meant not to include the new concept. But maybe you want to set a precedent. Tobias smime.p7s Description: S/MIME Cryptographic Signature ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] NEWS: limited name space accesses
* 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-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] NEWS: limited name space accesses
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-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] NEWS: limited name space accesses
On 07/04/2015 14:37, Christian Sternagel wrote: (b) qualified That gets my vote because it expresses clearly the description Makarius gave: name space entry that is only accessible by qualified names Tobias smime.p7s Description: S/MIME Cryptographic Signature ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] NEWS: limited name space accesses
On Tue, 7 Apr 2015, Tobias Nipkow wrote: On 07/04/2015 14:37, Christian Sternagel wrote: (b) qualified That gets my vote because it expresses clearly the description Makarius gave: name space entry that is only accessible by qualified names It is definitely good to collect keyword candidates from other well-known languages. I had qualified on my list of possibilities at first, but was hesitating to use it, because there is yet another concept (c) that has no Isar notation so far. It is called Binding.qualified in ML and could solve problems like https://lists.cam.ac.uk/mailman/htdig/cl-isabelle-users/2015-February/msg00038.html as follows: locale test begin lemma foo (qualified bar!): ... end In principle there could be a dual-use of 'qualified' as Binding.qualified (with argument) and Name_Space.restricted (without argument), or rather Name_Space.qualified after another tuned signature change. qualified lemma a: ... lemma b (qualified c): ... lemma e (qualified f!): ... This does not work in outer syntax though, since the new command prefix category (keywords that may occur before a command) needs to be disjoint from other minor keywords in the command body. (After the dismissal of Proof General, command spans have become a bit more flexible, but cannot be stretched arbitrarily.) One could try to invent another notation for x (qualified y!) above. Note that the ! is the mandatory flag (like in locale interpretation syntax). We don't have notation for such flags within qualified names themselves. Otherwise one could use c.b directly. A real danger in the whole affair is that we need to proceed towards the Isabelle2015 release very soon, i.e. this week. As a summary, here is the collection of nice keywords so far, without any assignment of meanings yet: private local hidden qualified Anything else? Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
