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 <[email protected]> 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
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
