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.

Note: For technical reasons, we require that you first execute :q, to exit the ACL2 read-eval-print loop, before evaluating a save-exec call.

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