Major Section: MISCELLANEOUS
Example prompt: ACL2 p!s>The prompt printed by ACL2 displays the current package, followed by a space, followed by zero or more of the three characters as specified below, followed by the character
>printed one or more times, reflecting the number of recursive calls of
ld. The three characters in the middle are as follows:
p ; when (default-defun-mode (w state)) is :program ! ; when guard checking is on s ; when (ld-skip-proofsp state) is tSee default-defun-mode, see set-guard-checking, and see ld-skip-proofsp.
Also see ld-prompt to see how to install your own prompt.
Here are some examples with
ACL2 !> ; logic mode with guard checking on ACL2 > ; logic mode with guard checking off ACL2 p!> ; program mode with guard checking on ACL2 p> ; program mode with guard checking offHere are some examples with
ACL2 > ; guard checking off, ld-skip-proofsp nil ACL2 s> ; guard checking off, ld-skip-proofsp t ACL2 !> ; guard checking on, ld-skip-proofsp nil ACL2 !s> ; guard checking on, ld-skip-proofsp tFinally, here is the prompt in raw mode (see set-raw-mode), regardless of the settings above: