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

[Makarius]

*** 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:

  ISABELLE_BUILD_OPTIONS="threads=8"

  ML_PLATFORM="x86_64-linux"
  ML_HOME="/home/isabelle/contrib/polyml-5.7.1-5/x86_64-linux"
  ML_SYSTEM="polyml-5.7.1"
  ML_OPTIONS="--minheap 4G --maxheap 32G"

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

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


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

http://isabelle.in.tum.de/repos/isabelle/rev/00c436488398
https://bitbucket.org/isa-afp/afp-devel/commits/53b27c2020f8eacb20a97ba5fb38baa1b19b3fbf

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.


	Makarius