Re: [isabelle] What may Isabelle be doing behind my back?



AutoQuickCheck and AutoSolve only come into effect when you execute a
theory step by step. If you load a whole theory, they are disabled.

Tobias

Andrei Popescu wrote:
> I am using Isabelle2009-1 with emacs22-gtk, admittedly in a very poor environment:
> 
> Ubuntu 8.10
> Intel(R) Core(TM) 2 CPU T5500 @ 1.66 Ghz
> Memory: 493.2 MiB
> 
> Free disk space: 69 MiB
> (I only use Ubuntu on a small disk partition)
> 
> The problem is that occasionally Isabelle takes a very long time while performing operations such as moving to a new theory or theorem or digesting a new definition, and I don't know what she is *really* doing then. (By a long time, I mean minutes, and sometimes tens of minutes.)
> This tends to occur more often when I am trying to process whole buffers, when Isabelle takes 10-15-minute breaks from time to time.  
> I also noticed that when I set AutoQuickCheck, AutoSolve and ParallelProofs off, such problems occur less often, but still do.  
> Also, the problem seems to increase with the size of the graph of theories on which the current theory depends on, but has a large degree of randomness.  I did not have these problems with the previous release.  
> 
> A related problem is that trying to run a (large-enough) session takes forever.  
> 
> I shall eventually get a better computer system, but until then I would really like to survive with what I have here.  (Notice also that my disk status does not really allow me to install new things.)  Help!  
> 
> Best regards, 
>    Andrei 
> 
> 
> 
> 
> 
>       
> 






This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.