[isabelle-dev] Shadowing of theorem names in locales

[Makarius]

On Tue, 11 Feb 2014, Clemens Ballarin wrote:

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

In principle there could be arbitrary declarations disguised as 
declaration attributes of facts, but the general sanity assumption is that 
this is not done.  The separate concept of syntax_declaration was 
introduced for that, when we sorted this out several years ago.


> On 10 February, 2014 16:14 CET, Makarius <makarius at sketis.net> wrote:

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

I've done 1-2 rounds through the fact name spaces in the past few weeks, 
and will probably came back to it again soon.

My present idea is to see if the application of notes could be made strict 
but asynchronous (using Execution.fork) like Goal.prove_future, but on the 
application of the composed chain of morphisms.  By retaining strictness 
we have two potential advantages: (1) reliable information about failure 
at the end of the session, and (2) the interactive user can more readily 
access facts in find_theorems (otherwise there could be minutes to wait 
before all propositions of the facts space become available).

This is a bit speculative at the moment, until I dive again into the 
sources again to explore the situation.


 	Makarius