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 this:

  * Enlarge Cygwin heap size according to
    http://cygwin.com/cygwin-ug-net/setup-maxmem.html -- 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.


	Makarius


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