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

Makarius makarius at sketis.net
Sun Feb 25 13:32:28 CET 2018

*** Isar ***

* Command 'interpret' no longer exposes resulting theorems as literal
facts, notably for the \<open>prop\<close> notation or the "fact" proof
method. This
improves modularity of proofs and scalability of locale interpretation.
Rare INCOMPATIBILITY, need to refer to explicitly named facts instead
(e.g. use 'find_theorems' or 'try' to figure this out).

This refers to Isabelle/2d9918f5b33c, it is merely the visible tip of
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).

This impacts sessions that use a lot of locales and locale
interpretation, but type classes are also a special case of this. Here
is a notable timing example:


  ML_OPTIONS="--minheap 4G --maxheap 32G"

  Isabelle/67e5deb9e290 + AFP/e9f2114df805
  Finished JinjaThreads (0:34:14 elapsed time, 2:43:34 cpu time, factor

  Isabelle/e9f2114df805 + AFP/e9f2114df805
  Finished JinjaThreads (0:27:03 elapsed time, 2:20:17 cpu time, factor

The incompatibility mentioned above is really rare -- here are the
minimal changes for Isabelle + AFP:


For significant applications we could provide "interpret (open)", but I
think it is better to reduce the number of special features in the
system -- we have too many of them already.


More information about the isabelle-dev mailing list