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
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
