		Search-engine friendly clone of the ACL2 documentation.

Save-exec

Save an executable image and a wrapper script

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 (see build::using-extended-ACL2-images), 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.

At the end of this topic we discuss how to use the `make' utility to invoke save-exec.

Examples:

; Save an executable script named my-saved_acl2, with the indicated message
; added below the words "MODIFICATION NOTICE" under 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 under the modification
; notice:
(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")

; Arrange that ACL2 evaluates (with LD) the three forms shown.
; In this example, the THM form fails, but that does not stop the definition
; of BAR from being evaluated: LD continues on, just as the top-level loop
; lets you continue after a failure.
(save-exec "my-acl2" "test"
           :init-forms
           '((defun foo (x) (reverse x))
             (thm (equal (foo x) x))
             (defun bar (x) x)))

; Essentially as just above, except that the call of LD returns after the THM
; failure, so BAR does not get defined.
(save-exec "my-acl2" "test"
           :init-forms
           '((ld '((defun foo (x) (reverse x))
                   (thm (equal (foo x) x))
                   (defun bar (x) x))
                 :ld-pre-eval-print t :ld-verbose nil)))

; 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
           :init-forms init-forms)

where the keyword arguments are optional, and arguments are as follows.

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 and init-forms are nil by default. Regardless of their value, ACL2 starts up and enters its read-eval-print loop in the usual way; see lp. Normally you'll stay inside that loop, but if return-from-lp or init-forms is not nil, then the indicated forms are evaluated in the ACL2 read-eval-print loop: a single form in the case of return-from-lp, and a list of forms in the case of init-forms. (Essentially, the ld special standard-oi is provided to a call of ld as a list with the indicated forms on the front.) Moreover, if the case of return-from-lp, the loop is exited after evaluation of the form, 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.

NOTE: It is illegal to supply non-nil values for both :return-from-lp and :init-forms. But if you add (value :q) to the end of your list of :init-forms, and your other forms do not result in an error, then you will be left in raw Lisp (as was presumably intended if you were planning to use :return-from-lp).

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

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. If inert-args is supplied a string, then although those arguments will be appended to the supplied arguments (see (5) below), they will be ignored by the host Lisp (except for being recorded; see (6) below). Inert-args is nil by default (that is, when omitted). The other legal value of inert-args, t, is discussed in (5) below. Thus for the example above, suppose we invoke the generated script as follows.

my-saved_acl2 -a bcd -e fgh

If my-saved_acl2 was generated using a save-exec command with a non-nil value 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 /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 oslib::argv for a utility that returns a list of all inert-args from an invocation of ACL2. See also getopt for a convenient way to parse these arguments.

(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 50000"
           :toplevel-args "--eval '(print \"HELLO\")'"
           :inert-args "--my-option my-value")

The script generated by this example call of save-exec contains a line such as the following (with the same convention for `\' as before). Notice that :host-lisp-args can be modified at startup (without save-exec) by setting environment variable SBCL_USER_ARGS.

exec "/projects/sbcl-1.1.7-x86-64-linux/src/runtime/sbcl" \
     --dynamic-space-size 24000 --control-stack-size 64 \
     --core "/u/smith/my-saved_acl2.core" --dynamic-space-size 50000 \
     ${SBCL_USER_ARGS} \
     --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.

Finally, note that save-exec can be invoked using the `make' utility in the main ACL2 directory by using the save-exec target. That target will first build an ACL2 executable in the normal way if it is out of date. Then it will start that executable, using the value of ACL2_CUSTOMIZATION (as a `make' or environment variable) — which must be specified — as the ACL2-customization file, before making a save-exec call. By default, that call is (save-exec "custom-saved_acl2" "Saved with additions from <file>"), where <file> is the value of ACL2_CUSTOMIZATION. (Except, in ACL2(p) and ACL2(r), "custom-saved_acl2" is replaced by "custom-saved_acl2p" and "custom-saved_acl2r", respectively.) However, you can specify the first argument as the value of ACL2_SAVED (as a `make' or environment variable), and you can specify the remaining arguments as the value of ACL2_SAVED_ARGS (also as a `make' or environment variable). Here is an example one could run at the shell prompt; notice the careful quoting.

make save-exec \
  ACL2_CUSTOMIZATION=~/temp/foo.lsp \
  ACL2_SAVED=my-acl2 \
  ACL2_SAVED_ARGS='"My custom image" \
                   :init-forms (quote ((defun foo (x) (reverse x))))'

WARNING: It is a good idea to look at the log file noted in the `make' output, to check that your customization file loaded as intended (presumably, without errors).