save an executable image and (for most Common Lisps) a wrapper script
Major Section:  OTHER

See saving-and-restoring for an explanation of why one might want to use this function.

; Save an executable named my-saved_acl2:
(save-exec "my-saved_acl2"
           "This saved image includes Version 7 of Project Foo.")

; Same as above, but with a generic comment instead: (save-exec "my-saved_acl2" nil)

General Form: (save-exec exec-filename extra-startup-string)

where exec-filename is the filename of the proposed executable and 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.


1. For technical reasons, you must first exit the ACL2 read-eval-print loop, for example by executing :q, before evaluating a save-exec call.

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. For most Common Lisps, the specified file (e.g., "my-saved_acl2" in the examples above) will be written as a small script, which in turn invokes a saved image to which an extension has been appended (e.g., my-saved_acl2.gcl for the examples above, when the underlying Common Lisp is GCL on a non-Windows system).