[isabelle-dev] Shadowing of theorem names in locales

[Clemens Ballarin]

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.

Clemens


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 
> required.
> 
> 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.
> 
> 
>  	Makarius