PROOF-TREE-EMACS

using emacs with proof trees 
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.

To get started you add a single autoload form to your .emacs file and then issue the corresponding M-x command. The file emacs/emacs-acl2.el under the ACL2 distribution contains everything you need to get started, and more. Alternatively put the following into your .emacs file, 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/")


(autoload 'start-proof-tree
  (concat *acl2-interface-dir* "top-start-shell-acl2")
  "Enable proof tree logging in a prooftree buffer."
  t)
Once the above is taken care of, then to start using proof trees you do two things. In emacs, evaluate: 
   M-x start-proof-tree
Also, in your ACL2, evaluate 
  :start-proof-tree
If you want to turn off proof trees, evaluate this in emacs 
   M-x stop-proof-tree
and evaluate this in your ACL2 session: 
  :stop-proof-tree
When you do meta-x start-proof-tree for 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 .emacs file. 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 ?               help
Ordinary emacs help describes these in more detail; for example, you can start with: 
  C-h k C-z h
Also see proof-tree-bindings for that additional documentation.

The file 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.