*** 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 _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
