[isabelle-dev] NEWS: 'interpret' vs. literal facts and locale performance
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
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