Aspects of ACL2 User Interaction
Matt Kaufmann, UITP'08, August, 2008
ACL2
("A
Computational
Logic
for
Applicative
Common
Lisp"):
Joint work by Matt Kaufmann and J Strother Moore, with
early contributions from Bob Boyer.
Goal today: Give a sense of how ACL2 supports effective user
interaction.
Today we'll touch on numerous aspects of user interaction with ACL2, using
small examples to illustrate as time permits. You can obtain a gzipped tar file of the four examples
linked to below. Most of the other links below are to topics in the
ACL2 documentation.
For fewer examples in a little more depth,
see the TPHOLs
2008 ACL2 tutorial.
Narrowest sense of "user interface": Delivering input and output
- Typically Emacs for experienced users, perhaps with distributed
customization
file. Efficient!
- Two Eclipse-based
interfaces have been developed by other groups for teaching purposes:
- Work in
progress: Connect
with LabVIEW from National Instruments (example)
ACL2 prover output:
- Traditionally through generated English commentary
- Proof-tree
display for proof structure and navigation
- Gag-mode,
especially the summary now provided
- And of course (?), helpful error and warning messages, which often point to
user documentation
Controlling ACL2: