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

2018-02-25 Thread Makarius 
On 25/02/18 13:32, Makarius wrote:
> 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).

Some more notes on this.

Facts emerging from locale interpretation are always lazy, unless there
are attributes attached to them (this requires to update the context on
the spot, e.g. a [simp] declaration).

Global facts within the theory will always be forced in the final
consolidation of (forked) proofs that have been recorded. In particular,
 a session image will have all facts stored in evaluated form.

Local facts stemming from hypothetical interpretations (e.g. 'interpret'
within a proof, probably also 'sublocale') are only forced when they get
used. When the local context closes, there is no permanent result.

This explains, why I did not add anything to the NEWS concerning lazy
facts -- these details should not relevant to users, everything should
work as before.


Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

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

2018-02-25 Thread Makarius 
*** 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