Email Gateway (Aug 18 2022 at 15:53): Email Gateway (Aug 18 2022 at 15:53):From: Andrei Popescu <uuomul@yahoo.com>
Hello,
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. (?)
Thank you in advance for any possible advice on how to work around this.
(Here is some more info: I am working with Cygwin (with the packages recommended
from the Isabelle site)
under Windows 7,
with a processor Intel(R) Core(TM) i5 CPU M540 @ 2.53GHz
and RAM 4GB (2.43 GB usable).
I have tried with both Isabelle-2009-1 and Isabelle-2009-2. Occasionally
I also get this error when working interactively in Isabelle in emacs (just in
the middle of some theory, when
moving to a new definition or lemma), but interactively I am usually able to run
all the scripts.)
Best regards,
Andrei
HOL-Lambda
Email Gateway (Aug 18 2022 at 15:53):From: Makarius <makarius@sketis.net>
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
Email Gateway (Aug 18 2022 at 15:53):From: Andrei Popescu <uuomul@yahoo.com>
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,
Andrei
From: Makarius <makarius@sketis.net>
To: Andrei Popescu <uuomul@yahoo.com>
Cc: cl-isabelle-users@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
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
Email Gateway (Aug 18 2022 at 15:53):From: Makarius <makarius@sketis.net>
On Mon, 23 Aug 2010, Andrei Popescu wrote:
Thank you very much, I'll try these.
One more thing: you can disable multi-threaded processing, which is on by
default. So something like -M1 in usedir options should conserve some
memory.
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
Such workarounds to save memory remind of of the ancient days of 8bit or
16bit machines. At some point MS was very prood to present NT as "32 bit"
operating system. Now that technology is already a bottle neck again, and
the move to full 64 bit address happening right now.
One problem we face here is that Cygwin is for 32 bit only, and will stay
so for quite some time (like most other things on the Windows platform).
Makarius
Last updated: Apr 20 2024 at 08:16 UTC