Re: [isabelle] cannot run sledgehammer



The error code indicates that you have run out of memory. If your machine has one gigabyte you should be okay. However you may have a a lot of other processes clogging up your system.
Larry Paulson


On 10 May 2008, at 03:33, Andrei Popescu wrote:

Hello,

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"

In my setting file, I have

E_HOME=$(choosefrom "$ISABELLE_HOME/contrib/E/E/x86-linux/" "")

Thanks in advance for any help with this,
   Andrei





Be a better friend, newshound, and know-it-all with Yahoo! Mobile. Try it now.






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