[isabelle-dev] Shadowing of theorem names in locales

[Makarius]

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