ACL2s Cheat Sheet

UI Actions

Mac OS X Note: The keybindings below are for PC users. The Mac equivalents (if available) are the same except that Ctrl+Shift is replaced by Command+Shift.

Navigation (appear under "Navigate" menu)
"Go To" | "Corresponding ..." Ctrl+Shift+O (the letter "O")
"Go To" | "Matching Character" Ctrl+Shift+P
"Down/Up to Next/Previous Session Input" (.a2s only) Ctrl+Shift+Up and Ctrl+Shift+Down
"Down/Up to Next/Previous Checkpoint/Input" (.a2s only) Ctrl+Shift+Right and Ctrl+Shift+Left.
"Previous/Next Command in History" (.a2s only) Ctrl+Shift+, (comma) and Ctrl+Shift+. (period)
"Last Command in History" (.a2s only) Ctrl+Shift+/ (slash)
Submit Immediate Enter (at end of Session editor; assuming immediate form is complete) Ctrl+Enter (anywhere in Session editor; assuming complete)
"Clean Session" Alt+Delete
"(Re)start Session" Alt+Home
"Stop Session" ALT+End
"Interrupt Session" Ctrl+Break
"Undo/cancel all forms"  
"Undo/cancel last form" Ctrl+Shift+U
"Cancel all "todo" forms"  
"Advance todo line" Ctrl+Shift+I (letter before "J")
"Move todo up/down past cursor" (.lisp only) Ctrl+Shift+Enter
Indent code Tab (affects selection or current line)

Important addresses:

ACL2s Web Page:

ACL2s/Eclipse update site:

Command Classifications

EVENT Calls to defun, defmacro, defthm, etc.

Computations that do not change history/state.


Some commands that print information about history/state without changing it.

UNDO, REDO An "undo" or "redo" initiated by ACL2s as a result of line motion.
BAD Ill-formed based on history (e.g. "no function by that name").
COMMAND Forms that modify things we know how to undo, but are not events (e.g. ":set-guard-checking nil").
IN-PACKAGE An in-package call, which is technically also a COMMAND.
BEGIN-BOOK A begin-book call, which is technically also a COMMAND.
(potentially dangerous!)
These can potentially break things in the user interface. Use with care.

Contact information

The main authors are Peter Dillinger () and Pete Manolios ().

Last modified: 1 September 2008, for ACL2s 0.9.0