[isabelle-dev] NEWS: Isabelle/jEdit (19e1c6e922b6)

[Johannes Hoelzl]

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