Re: [isabelle] thread creation failed

Thank you very much, I'll try these.

Actually, what would clearly solve my problem in an almost platform-independent 
way would be the ability 

to remove completely (i.e., just delete from everywhere, including all the 
databases, etc.) some 

of the theorems, *even if remaining theorems are based on them*.  E.g., all of 
the theorems 

from a certain intermediate theory.  Note that such an operation would be 
acceptable from a foundational / certification point of 

view, just as acceptable as not storing proof terms, and would be IMO highly 
appreciated by users who write 

their Isabelle development employing several layers, where each layer offers an 
interface independent  from previous layers.  

(I'll stop here from making this case though, since maybe such a feature is 
already there and I don't know if it.)

Best regards, 

From: Makarius <makarius at>
To: Andrei Popescu <uuomul at>
Cc: cl-isabelle-users at
Sent: Mon, August 23, 2010 4:52:29 AM
Subject: Re: [isabelle] thread creation failed

On Sat, 21 Aug 2010, Andrei Popescu wrote:

> I have a fairly large Isabelle development and I am trying to create html and 
>latex documents based on it. 
> However, attempting to run the session results (after running for a while) in 
>the following error: "thread creation failed". 
> I also attach the log file produced.  Presumably the problem is caused by the 
>size of the development. (?)   

Yes, this is just a typical out-of-memory problem.  You can try something like 

  * Enlarge Cygwin heap size according to -- 1.0 .. 1.5 GB
    usually works, but I have hardly ever got beyond that on Windows.

  * Compactify the Poly/ML while running, i.e. via invoking
    share_common_data() in your ROOT.ML after loading some of the
    theories, and then continue with more of them.

> under Windows 7, with a processor Intel(R) Core(TM) i5 CPU M540 @ 2.53GHz and 
>RAM 4GB (2.43 GB usable).

This looks like fairly nice hardware for Linux / x86_64.  Unlike Windows, 64bit 
mode really works for Linux -- you will be able to use all of your physical 
memory.  Nonetheless, the Poly/ML binaries should be those for x86 for best 
memory utilization in this scenario.



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