GOOD-BYE

quit entirely out of Lisp 
Major Section:  OTHER


Example:
ACL2 !>:good-bye
Note: Your entire session will disappear forever when you type :good-bye.

The command :good-bye quits not only out of the ACL2 command loop, but in fact quits entirely out of the underlying Lisp. Thus, there is no going back! You will not be able to re-enter the command loop after typing :good-bye! All your work will be lost!!!

This command may not work in some underlying Common Lisp implementations. But we don't expect there to be any harm in trying. It does work in GCL and Allegro CL, at least as of this writing.

In some systems, typing control-d at the top-level ACL2 prompt (control-c control-d if inside emacs) will call this function.

If you merely want to exit the ACL2 command loop, use :q instead (see q).