SAVE-EXEC

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 run 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 save-exec are evaluated.

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)

Exec-filename is the filename of the proposed executable.

Extra-startup-string is a non-empty string to be printed after the normal ACL2 startup message when you start up the saved image. However, extra-startup-string is allowed to be nil, in which case a generic string will be printed instead.

Host-lisp-args can be nil (the default), but if it is a non-nil value, 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.)

Inert-args can be nil (the default), but if it is a non-nil value, 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.

Return-from-lp is 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 return-from-lp is done with ld options that minimize output; also see with-output to minimize output. Suggestion: let return-from-lp be t if you simply want to exit the read-eval-print loop at startup, without evaluating any (nontrivial) form.

The remainder of this documentation focuses on the options other than return-from-lp.

Details:

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

(3) Save-exec generates a small script file (e.g., "my-saved_acl2" 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. Save-exec 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 name my-saved_acl2.gcl in the examples above.

(4) If inert-args is nil (for example if keyword :inert-args is 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 as follows.

my-saved_acl2 -a bcd -e fgh

(5) The generated script, which specifies execution with /bin/sh, will 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 string "$@" is intended to allow the user to pass additional command-line arguments to that executable.

If host-lisp-args and inert-args are omitted (or nil):

exec <lisp_executable> <ACL2_options> "$@"

More generally, host-lisp-args is inserted immediately after <ACL2_options>, but only if it is non-nil (hence a string). If inert-args is nil, we thus get:

exec <lisp_executable> <ACL2_options> host-lisp-args "$@"

If host-lisp-args redefines 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 -Z appears 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 host-lisp-args is ignored.

The remaining cases below are for a non-nil value of inert-args. In each case, if host-lisp-args is nil then it should be omitted from the displayed command.

If inert-args is t then 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 -- "$@"

If inert-args is a string then the result is similar to the above, except that inert-args is 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 "my-saved_acl2", that 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 "my-saved_acl2" with 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 new 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 host-lisp-args are what the SBCL manual calls ``runtime options''. For SBCL only, an extra keyword argument, :toplevel-args, may be used for specifying what the SBCL manual calls ``toplevel options. As with :host-lisp-args, this value, 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")

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 inert-args is nil:

exec <lisp_executable> \
     <ACL2_runtime_options> host-lisp-args --end-runtime-options \
     <ACL2_toplevel_options> host-lisp-args \
     "$@"

For the case that inert-args is non-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 inert-args is nil. For SBCL, when they are passed to Lisp they are passed as toplevel options, not as runtime options.