SBCL Dynamic Memory Allocation

[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.