Major Section: OTHER
Save-exec saves your ACL2 state so that you can immediately re-start
later in that same state. This utility can be useful for a project with
books to be included every time ACL2 is started, to avoid time taken to
include-book. Another use of
save-exec is to save an
executable that takes command-line arguments beyond those normally passed to
the host Lisp executable. All arguments of a call of
Examples: ; Save an executable script named my-saved_acl2, with the indicated message ; added to the start-up banner: (save-exec "my-saved_acl2" "This saved image includes Version 7 of Project Foo.") ; Same as above, but instead with a generic comment in the start-up banner: (save-exec "my-saved_acl2" nil) ; Arrange that the generated script passes the indicated arguments to be ; processed by the Lisp (ACL2) executable (where this example is specific to ; the case that CCL is the host Lisp): (save-exec "my-saved_acl2" nil :host-lisp-args "--no-init -Z 256M") ; Arrange that the generated script passes along the indicated arguments ; to Lisp (ACL2), but that they are not processed by Lisp other than to ; record the additional arguments (see (6) below). (save-exec "my-saved_acl2" nil :inert-args "abc xyz -i foo") ; Combining the preceding two examples: (save-exec "my-saved_acl2" nil :host-lisp-args "--no-init -Z 256M" :inert-args "abc xyz -i foo") ; Immediately exit the ACL2 read-eval-print loop after starting up. (save-exec "my-acl2" nil :return-from-lp t) ; Immediately exit the ACL2 read-eval-print loop after starting up and ; defining function FOO in the logic. (save-exec "my-acl2" "Start with foo defined." :return-from-lp '(with-output :off :all (defun foo (x) x))) ; Immediately exit the ACL2 read-eval-print loop after starting up and ; defining variable xxx in raw Lisp. (save-exec "my-acl2" "Start with xxx defined." :return-from-lp '(with-output :off :all (ld '((set-raw-mode-on!) (defvar xxx (make-list 10)) (set-raw-mode nil) (u)))))
Each example above generates a file named "my-saved_acl2". That file is
quite similar in form to the script generated when building ACL2 directly
from source code; details are below. For example, here are the contents of
that generated file if the host Lisp is CCL (but where dates and pathnames
are specific to one's environment). Here, we break lines using `\', but the
exec command is actually on a single line.
#!/bin/sh # Saved August 16, 2013 23:06:49 # then August 17, 2013 11:01:56 export CCL_DEFAULT_DIRECTORY="/projects/acl2/lisps/ccl/15542/ccl" exec "/projects/ccl/lx86cl64" -I "/u/smith/my-saved_acl2.lx86cl64" \ -Z 64M -K ISO-8859-1 -e "(acl2::acl2-default-restart)" \ --no-init -Z 256M \ -- \ abc xyz -i foo \ "$@"
General Form: (save-exec exec-filename extra-startup-string :host-lisp-args host-lisp-args :inert-args inert-args :return-from-lp return-from-lp)where the keyword arguments are optional, and arguments are as follows.
Exec-filenameis the filename of the proposed executable.
Extra-startup-stringis a non-empty string to be printed after the normal ACL2 startup message when you start up the saved image. However,
extra-startup-stringis allowed to be
nil, in which case a generic string will be printed instead.
nil(the default), but if it is a non-
nilvalue, then it is a string to be inserted into the command line in the saved script, specifying additional arguments that are to be processed by the host Lisp executable. (Note for SBCL only: these are runtime options; for toplevel options, see (8) below.)
nil(the default), but if it is a non-
nilvalue, then it is a string to be inserted into the command line in the saved script, specifying additional arguments that are not to be processed by the host Lisp executable.
nil by default. Regardless of the value of
return-from-lp, ACL2 starts up and enters its read-eval-print loop as
usual; see lp. Normally you'll stay inside that loop, but if
return-from-lp is not
nil, then it is evaluated in the loop, which is
then exited, leaving you in raw Lisp. Evaluation of
ld options that minimize output; also see with-output to
minimize output. Suggestion: let
t if you simply
want to exit the read-eval-print loop at startup, without evaluating any
The remainder of this documentation focuses on the options other than
(1) You must first exit the ACL2 read-eval-print loop, typically by executing
:q, before evaluating a
save-exec call; otherwise an error occurs.
(2) The image will be saved so that in the new image, the raw Lisp package
and the package in the ACL2 read-eval-print loop (see lp) will be the same
as their respective values at the time
save-exec is called.
Save-exec generates a small script file (e.g.,
in the examples above), similar in form (see (4) below) to the script
generated when building ACL2 directly from source code, but with a comment
line indicating the time at which the new script is written.
also saves an associated binary file. The binary file's name is obtained by
putting a suffix on the script filename; for example, if the host Lisp is GCL
running on a Linux or Darwin (MacOS) system, then that binary file has the
my-saved_acl2.gcl in the examples above.
nil (for example if keyword
omitted), then when the generated ACL2 script is invoked with command line
arguments, those arguments will be passed to the host Lisp; otherwise they
will not. Thus for the example above, suppose we invoke the generated script
my-saved_acl2 -a bcd -e fghIf
my-saved_acl2was generated using a
save-execcommand with a non-
nilvalue specified for keyword
:inert-args, then the arguments ``
-a bcd -e fgh'' will not be passed to the host Lisp; otherwise, they will be. Note that for ACL2 executable scripts generated by an ordinary ACL2 build from sources, the latter case (i.e., without
inert-args) takes place.
(5) The generated script, which specifies execution with
generally contain a line of one of the following forms. (But for SBCL,
see (8) below.) In the examples that follow,
ACL2_options is a suitable
list of command-line arguments given to the ACL2 executable. The quoted
"$@" is intended to allow the user to pass additional
command-line arguments to that executable.
inert-argsare omitted (or
nil):exec <lisp_executable> <ACL2_options> "$@"
host-lisp-argsis inserted immediately after
<ACL2_options>, but only if it is non-
nil(hence a string). If
nil, we thus get:exec <lisp_executable> <ACL2_options> host-lisp-args "$@"If
host-lisp-argsredefines a value from
<ACL2_options>, then it is up to the host lisp which value to use. For example, experiments show that in CCL, if
-Zappears twice, each with a legal value, then the second value is the one that is used (i.e. it does indeed override the original value written out by ACL2 in
<ACL2_options>. But experiments also show that in LispWorks, where ``
-init -'' is included in
<ACL2_options>, then inclusion of ``
-init foo.lisp'' in
The remaining cases below are for a non-
inert-args. In each case, if
nilthen it should be omitted from the displayed command.
tthen an additional argument, `
--', indicates that when ACL2 is given command line arguments, these should not be processed by the host Lisp (other than recording them; see (6) below):exec <lisp_executable> <ACL2_options> host-lisp-args -- "$@"
inert-argsis a string then the result is similar to the above, except that
inert-argsis added immediately after `
--':exec <lisp_executable> <ACL2_options> host-lisp-args -- inert-args "$@"
(6) See community books
books/oslib/argv for a utility that returns a
list of all
inert-args from an invocation of ACL2.
(7) Suppose that you invoke an ACL2 script, say
was generated by
save-exec, and then optionally evaluate some forms.
Then you may save a new ACL2 script with
save-exec. The new script will
contain comment lines that extend comment lines in
a new write date, but otherwise will be identical to the script that would
have been generated by executing the new
save-exec call after invoking
the original ACL2 executable (built directly from ACL2 sources) instead of
"my-saved_acl2". In other words, the options added by the earlier
save-exec call that created
"my-saved_acl2" are discarded by the
save-exec call. However, the
.core file will built on top of the
.core file that was consulted when
"my-saved_acl2" was invoked.
(8) The following note pertains only to the case that the host Lisp is SBCL.
For SBCL, the scripts written are analogous to, but slightly different from,
those shown above. Please note that for SBCL, the
what the SBCL manual calls ``runtime options''. For SBCL only, an extra
:toplevel-args, may be used for specifying what the
SBCL manual calls ``toplevel options. As with
toplevel-args, should be
nil (the default) or a string. Here
is an example.
(save-exec "my-saved_acl2" nil :host-lisp-args "--dynamic-space-size 12000" :toplevel-args "--eval '(print \"HELLO\")'" :inert-args "--my-option my-value")The script generated by this example call of
save-execcontains a line such as the following (with the same convention for `\' as before)
exec "/projects/sbcl-1.1.7-x86-64-linux/src/runtime/sbcl" \ --dynamic-space-size 2000 --control-stack-size 8 \ --core "/u/smith/my-saved_acl2.core" --dynamic-space-size 12000 \ --end-runtime-options \ --no-userinit --eval '(acl2::sbcl-restart)' \ --eval '(print "HELLO")' \ --end-toplevel-options \ --my-option my-value \ "$@"
In general, the generated script is of one of the following forms (with the same convention for `\' as before).
For the case that
nil:exec <lisp_executable> \ <ACL2_runtime_options> host-lisp-args --end-runtime-options \ <ACL2_toplevel_options> host-lisp-args \ "$@"
For the case that
nil:exec <lisp_executable> \ <ACL2_runtime_options> host-lisp-args --end-runtime-options \ <ACL2_toplevel_options> host-lisp-args --end-toplevel-options \ inert-args "$@"
Notice that as before, when the generated script is invoked (for example, at
the shell), additional command-line arguments provided at that time are
passed to Lisp if and only if
nil. For SBCL, when they
are passed to Lisp they are passed as toplevel options, not as runtime