samowre
commented
2 months ago Hi
This is (partially) discussed in Section 3.2.3 of the SBCL document (https://www.sbcl.org/manual/#Saving-a-Core-Image), under :save-runtime-options. The problem is that --dynamic-space-size and --control-stack-size can't be changed in a running SBCL image, and if the image was built using save-lisp-and-die, it will ignore these arguments.
The bottom line is that you need to change this at build time, i.e., in the Makefile. Look for SBCL_SPACE_SIZE, which is currently set to 6 Gb, and change it to whatever you want. This is also the place to change the SBCL_STACK_SIZE if you're running out of stack space.
I tested it by setting it to 30 Gb on my 16 Gb Linux laptop with 2 Gb of swap, and it started right up. You can see that it's virtual size is 30 Gb, though it's resident set size is only 149 Mb.
USER PID %CPU %MEM VSZ RSS TTY STAT START TIME COMMAND owre 1309476 1.6 0.9 30980736 148624 pts/10 Sl+ 14:44 0:00 bin/ix86_64-Linux/runtime/pvs-sbclisp --no-userinit
I'm not exactly sure what the trade-offs are for making it larger by default, but I'm happy to hear any suggestions. Note that increasing the stack size will increase your resident set size.
Sam
nmoore771
Greetings,
While grinding my way through a large theorem, I ran into an issue where SBCL (the Lisp backend that I am using) runs out of memory for garbage collection. This causes a hard crash of the prover environment, kicking me into the Lisp debugger. There's a command line argument for sbcl that increases this limit, and it is possible to insert it by replacing in emacs/pvs-ilips.el
(defun pvs-program () pvs-image)on lines 145 and 146 with
(defun pvs-program () (format "%s --dynamic-space-size 2048" pvs-image))This seems like a kludgy way of doing this, and perhaps someone who knows the system (and emacs Lisp) a bit better would be able to come up with a better solution (in particular, giving it a 2GB limit, hard coded, is not going to be a good solution for everyone).
Thanks for your time.