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