[isabelle-dev] Shadowing of theorem names in locales
ballarin at in.tum.de
Tue Feb 11 18:20:16 CET 2014
For the processing of locale expression, facts are not really required. Having all information related to syntax should be sufficient. I cannot tell, though, whether facts may contain syntax in disguise of certain attributes.
On 10 February, 2014 16:14 CET, Makarius <makarius at sketis.net> wrote:
> On Fri, 10 Jan 2014, Clemens Ballarin wrote:
> >> This does not exhibit itself until the compromised locale context is
> >> (re-)entered, and I think this is not desirable. My first spontaneous
> >> thought is that strictness should not apply during the initialisation
> >> of a locale context.
> > I wouldn't want to add special treatment for this. Currently we can
> > only ensure that a locale is intact by visiting its context. It would
> > be better if integrity checking could be done in an incremental fashion.
> > But that would require much more sophistication.
> There is a more general problem behind this: re-initializing a locale
> context is quite expensive, but we traditionally do this at certain
> important checkpoints when processing locale expressions. For example, in
> AFP/JinjaThreads the time for defining some huge locales is dominated by
> that re-init phase for the imports, and later only few facts are actually
> Several minutes (hours?) could probably be saved by maintaining facts
> within the context in a lazy manner: the name space is strict, but its
> values are only produced on demand. I have no clear idea, though, how
> that would impact practical realiablity of locale expressions.
> Or is that actually an answer to the problem above: assuming that re-init
> is fast, it could be done more often to check the name space, but its
> transformed results remain unchecked.
More information about the isabelle-dev