		Search-engine friendly clone of the ACL2 documentation.

Good-bye

Quit entirely out of Lisp

Examples:
ACL2 !>(good-bye)
; [ACL2 is exited]

ACL2 !>(good-bye 3)
; [ACL2 is exited with Unix exit status 3]

Note: Your entire session will disappear forever when you evaluate (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. In such cases, there is no harm in trying; ACL2 will let you know how to proceed if it cannot exit.

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

The optional argument for good-bye (default 0) indicates the Unix (Linux) exit status. If it is not an integer, it will be treated as 0.

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

We conclude with the following technical remark, to be ignored unless you are trying to do things in raw Lisp that involve quitting the session. The mechanism that ACL2 and Lisp use for quitting the session is slightly involved. In particular, if you trace the underlying raw Lisp function exit-lisp, you may see that it is called twice; the second call happens while cleaning up from an unwind-protect call.

Subtopics

Exit: Quit entirely out of Lisp
Quit: Quit entirely out of Lisp