1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
|
<html>
<head><title>PROOF-TREE-EMACS.html -- ACL2 Version 3.1</title></head>
<body text=#000000 bgcolor="#FFFFFF">
<h2>PROOF-TREE-EMACS</h2>using emacs with proof trees
<pre>Major Section: <a href="PROOF-TREE.html">PROOF-TREE</a>
</pre><p>
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.
<p>
<ul>
<li><h3><a href="PROOF-TREE-BINDINGS.html">PROOF-TREE-BINDINGS</a> -- using emacs with proof trees
</h3>
</li>
</ul>
To get started you add a single autoload form to your .emacs file and
then issue the corresponding M-x command. The file
<code>emacs/emacs-acl2.el</code> under the ACL2 distribution contains everything
you need to get started, and more. Alternatively put the following
into your <code>.emacs</code> file, first replacing `<code>v2-x</code>' in order to point
to the current ACL2 release.
<pre>
(setq *acl2-interface-dir*
"/projects/acl2/v2-x/acl2-sources/interface/emacs/")<p>
(autoload 'start-proof-tree
(concat *acl2-interface-dir* "top-start-shell-acl2")
"Enable proof tree logging in a prooftree buffer."
t)
</pre>
Once the above is taken care of, then to start using proof trees you
do two things. In emacs, evaluate:
<pre>
M-x start-proof-tree
</pre>
Also, in your ACL2, evaluate
<pre>
:start-proof-tree
</pre>
If you want to turn off proof trees, evaluate this in emacs
<pre>
M-x stop-proof-tree
</pre>
and evaluate this in your ACL2 session:
<pre>
:stop-proof-tree
</pre>
When you do <code>meta-x start-proof-tree</code> 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 <code>.emacs</code> file. The defaults are
as shown, but you can of course change them.
<pre>
(setq *acl2-proof-tree-height* 17)
(setq *checkpoint-recenter-line* 3)
(setq *mfm-buffer* "*shell*")
</pre>
Proof tree support has been tested in Emacs 18, 19, and 20 as well as
in Lemacs 19.<p>
Once you start proof trees (meta-x start-proof-tree), you will have
defined the following key bindings.
<pre>
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
</pre>
Ordinary emacs help describes these in more detail; for example, you
can start with:
<pre>
C-h k C-z h
</pre>
Also see <a href="PROOF-TREE-BINDINGS.html">proof-tree-bindings</a> for that additional documentation.<p>
The file <code>interface/emacs/README.doc</code> 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 <a href="PROOF-TREE.html">proof-tree</a>. Thanks to Mike Smith for
his major role in providing emacs support for proof trees.
<br><br><br><a href="acl2-doc.html"><img src="llogo.gif"></a> <a href="acl2-doc-index.html"><img src="index.gif"></a>
</body>
</html>
|
