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
* 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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and