Re: [isabelle] cannot run sledgehammer



On Fri, 9 May 2008, Andrei Popescu wrote:

> I have just installed the E prover (downloaded it from the Isabelle site)
> on my computer under Linux. When I try to run sledgehammer from proof
> general,
> I get the following error:
> 
> *** SysErr ("fork failed", SOME ENOMEM)
> *** At command "sledgehammer"

Maybe it helps to reduce the initial heap size of your Poly/ML session.  
In Isabelle2007/etc/settings the default for ML_OPTIONS is rather hight -- 
500 MB.  Saying ML_OPTIONS="-H 100" here increases the chance that it 
works with low-memory systems.

You may also try to increase your swap space.


	Makarius






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