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.
DIRrefers to your ACL2 source directory (typically called
(load "DIR/emacs/emacs-acl2.el")Then you can start the proof tree display by issuing the following emacs command:
If you prefer not to load the ACL2 emacs file as shown above, you can instead
put the following forms in your
~/.emacs file (where
DIR is as
above) and then issue the above
(setq *acl2-interface-dir* "DIR/interface/emacs/")Once the above is taken care of, then to start using proof trees you do two things. In emacs, start a shell (
(autoload 'start-proof-tree (concat *acl2-interface-dir* "top-start-shell-acl2") "Enable proof tree logging in a prooftree buffer." t)
meta-x shell) and evaluate:
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
M-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*")Alternatively, you can put the following in your
~/.emacs filein order to start proof trees without any queries.
Once you start proof trees (meta-x start-proof-tree), you will have defined
the key bindings shown by executing
C-z h in emacs. Also
see proof-tree-bindings for that additional documentation.
If you want proof-trees to be displayed in a separate emacs frame to the
side, then you can put the following forms in your
.emacs file above the
emacs-acl2.el described above. But you may wish to edit the
second form, in particular the number 2048.
(start-proof-tree-noninteractive "*shell*") (cond ((and (eq window-system 'x) (fboundp 'x-display-pixel-width) (= (x-display-pixel-width) 2048) ; for a wide monitor ) (delete-other-windows) (if (boundp 'emacs-startup-hook) ; false in xemacs (push 'new-prooftree-frame emacs-startup-hook))))
interface/emacs/README-mouse.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.