Major Section: PROOF-TREE
Within emacs, proof trees provide a sort of structure for the linear proof transcript output by the ACL2 prover. Below we explain how to get proof trees set up in your emacs environment.
emacs/emacs-acl2.elunder the ACL2 distribution contains everything you need to get started, and more. Alternatively put the following into your
.emacsfile, first replacing `
v2-x' in order to point to the current ACL2 release.
(setq *acl2-interface-dir* "/projects/acl2/v2-x/acl2-sources/interface/emacs/")Once the above is taken care of, then to start using proof trees you do two things. In emacs, evaluate:
(autoload 'start-proof-tree (concat *acl2-interface-dir* "top-start-shell-acl2") "Enable proof tree logging in a prooftree buffer." t)
M-x start-proof-treeAlso, in your ACL2, evaluate
:start-proof-treeIf you want to turn off proof trees, evaluate this in emacs
M-x stop-proof-treeand evaluate this in your ACL2 session:
:stop-proof-treeWhen you do
meta-x start-proof-treefor the first time in your emacs session, you will be prompted for some information. You can avoid the prompt by putting the following in your
.emacsfile. The defaults are as shown, but you can of course change them.
(setq *acl2-proof-tree-height* 17) (setq *checkpoint-recenter-line* 3) (setq *mfm-buffer* "*shell*")Proof tree support has been tested in Emacs 18, 19, and 20 as well as in Lemacs 19.
Once you start proof trees (meta-x start-proof-tree), you will have defined the following key bindings.
C-z z Previous C-z key binding C-z c Go to checkpoint C-z s Suspend proof tree C-z r Resume proof tree C-z a Mfm abort secondary buffer C-z g Goto subgoal C-z h help C-z ? helpOrdinary emacs help describes these in more detail; for example, you can start with:
C-h k C-z hAlso see proof-tree-bindings for that additional documentation.
interface/emacs/README.doc discusses an extension of ACL2
proof trees that allows the mouse to be used with menus. That
extension may well work, but it is no longer supported. The basic
proof tree interface, however, is supported and is what is described
in detail elsewhere; see proof-tree. Thanks to Mike Smith for
his major role in providing emacs support for proof trees.