[isabelle-dev] NEWS: Isabelle/jEdit (19e1c6e922b6)
hoelzl at in.tum.de
Thu Sep 22 16:27:26 CEST 2011
On Tue, 20 Sep 2011, Makarius wrote:
> In the meantime I have investigated this a little bit. It seems that
> HOL-Probability requires quite some memory even in minimalistic batch mode --
> approx. 2GB on my 4GB machine. With Isabelle/jEdit one needs further 600 MB
> for the editor process and the same (and more) for the fully persistent
> document state within ML. So it adds up to something > 4 GB such that it
> becomes infeasible to edit the full session live on a "small" laptop with
> "only" 4 GB.
I tried to reduce the runtime requirement of HOL-Probability by
removing some of the sublocale instantiations. As a lot of time is spend
in locale interpretation inside proofs.
For example currently I had:
locale A = ...
locale B = A + ...
(0) locale C = A + th
sublocale C < B
I assume replacing (0) by:
locale C = B + th
lemma [Pure.intros!]: "C <-> A /\ th"
should fasten up locale interpretation?
But how is it in the following case:
locale prodA = A M1 + A M2
(1) locale prodB = B M1 + B M2
sublocale prodB < prodA
locale prodC = C M1 + C M2
sublocale prodC < prodB
locale prodD = D M1 + D M2
sublocale prodD < prodA
Or should this be:
(2) locale prodB = prodA + B M1 + B M2
locale prodC = prodB + C M1 + C M2
locale prodD = prodC + D M1 + D M2
as a user the difference should not be visible, and I thought (1) would be
slower than (2) but after updating Probability it seams like (2) is slower
More information about the isabelle-dev