[isabelle-dev] Shadowing of theorem names in locales
makarius at sketis.net
Mon Feb 10 16:14:36 CET 2014
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