Email Gateway (Aug 18 2022 at 11:51): Email Gateway (Aug 18 2022 at 11:51):From: Andrei Popescu <uuomul@yahoo.com>
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.
Email Gateway (Aug 18 2022 at 11:51):From: Lawrence Paulson <lp15@cam.ac.uk>
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
Email Gateway (Aug 18 2022 at 11:52):From: Makarius <makarius@sketis.net>
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
Last updated: May 03 2024 at 04:19 UTC