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.
Clemens On 10 February, 2014 16:14 CET, Makarius <makar...@sketis.net> wrote: > 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