*** Isar ***
* Command 'interpret' no longer exposes resulting theorems as literal
facts, notably for the \prop\ 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
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev