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
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.)
From: Makarius <makarius at sketis.net>
To: Andrei Popescu <uuomul at yahoo.com>
Cc: cl-isabelle-users at lists.cam.ac.uk
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
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