Aspects of ACL2 User Interaction

Matt Kaufmann (joint work with J Strother Moore), UITP'08, August, 2008


Users of the ACL2 theorem prover typically interact with the system in many ways beyond submitting definitions and proving theorems. This talk will show some examples to provide a sense of the diversity of ACL2 user interaction. A few more in-depth examples may be found in the TPHOLS 2008 ACL2 tutorial.

Certainly we will consider the narrow sense of "user interface" as control of input and output. Users traditionally interact efficiently with ACL2 through Emacs, and we will demonstrate some Emacs customizations provided with the system. More recently, two Eclipse-based interfaces have been developed by other groups for teaching purposes: the ACL2 Sedan (ACL2s) and DrACuLa. Beyond the choice of editor (or terminal) is the issue of how to control ACL2 output, traditionally through generated English commentary. A proof-tree display illustrates proof structure and provides help for navigating that commentary. But a recent gag-mode enhancement is probably much more effective for debugging failed proof attempts.

Other useful output includes error and warning messages, which often point to user documentation. But ACL2 supports effective user interaction in ways beyond the above notions of input/output control.

A separate question, not addressed in this talk, is how to communicate proof results effectively to non-users. Our focus is on interface support for effective usage.