[isabelle-dev] NEWS: 'interpret' vs. literal facts and locale performance

Makarius makarius at sketis.net
Sun Feb 25 13:49:51 CET 2018

On 25/02/18 13:32, Makarius wrote:
> various performance improvements of the locale infrastructure leading up
> to that changeset (e.g. performance tuning for instantiate_free
> operations and lazy entries in the facts environment).

Some more notes on this.

Facts emerging from locale interpretation are always lazy, unless there
are attributes attached to them (this requires to update the context on
the spot, e.g. a [simp] declaration).

Global facts within the theory will always be forced in the final
consolidation of (forked) proofs that have been recorded. In particular,
 a session image will have all facts stored in evaluated form.

Local facts stemming from hypothetical interpretations (e.g. 'interpret'
within a proof, probably also 'sublocale') are only forced when they get
used. When the local context closes, there is no permanent result.

This explains, why I did not add anything to the NEWS concerning lazy
facts -- these details should not relevant to users, everything should
work as before.


More information about the isabelle-dev mailing list