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
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
|
<HTML>
<HEAD><TITLE>ACL2 Version 8.6 Installation Guide: Using ACL2</TITLE></HEAD>
<BODY TEXT="#000000" BGCOLOR="#FFFFFF" STYLE="font-family:'Verdana'">
<H1>Using <a href="http://www.cs.utexas.edu/users/moore/acl2/v8-6/index.html">ACL2</a></A></H1>
<b><font>[<a href="installation.html">Back to main page of Installation Guide.</a>]</font></b>
<p>
<B>Table of Contents</B><BR>
<UL>
<LI><A HREF="#Invoking">Invoking ACL2</A>
<UL>
<LI><A HREF="#Starting">When ACL2 Starts Up</A>
</UL>
<LI><A HREF="#Testing">Testing ACL2</A>
<LI><A HREF="#Certifying">Certifying ACL2 Books</A>
<LI><A HREF="#Documentation">Documentation</A>
<LI><A HREF="#Emacs">Emacs</A>
</UL>
<p><hr size=3 noshade><p>
Here we begin with a discussion of how to <A HREF="#Invoking">invoke ACL2</A>
interactively. We then discuss <A HREF="#Testing">testing</A> as well as the
<A HREF="#Certifying">certification</A> of
ACL2 <i><a href="http://www.cs.utexas.edu/users/moore/acl2/v8-6/combined-manual/?topic=ACL2____COMMUNITY-BOOKS">community
books</a></i>. We conclude with a discussion of
the <A HREF="#Documentation">documentation</A>.
<BR><HR>
<H3><A NAME="Invoking">Invoking ACL2</A></H3>
We assume that you have followed the installation instructions to
install, under some directory <I>dir</I>, a subdirectory <code>acl2-8.6</code>.
The sources and perhaps an executable image are located on that subdirectory.
However, if you have not saved an image but instead use the directions
for <A HREF="obtaining-and-installing.html#Running">Running Without Building an Executable Image</A>, skip
to <A HREF="#Starting">When ACL2 Starts Up</A> below.
<P>
The executable image is called <code>acl2-8.6/saved_acl2</code>. You can
invoke ACL2 by running that image, e.g.,
<BR><BR>
<CODE>mycomputer% </CODE><I>dir</I><CODE>/acl2-8.6/saved_acl2</CODE>
<BR><BR>
If you on a Unix-like system, then to make it easy to invoke ACL2 by
typing a short command, e.g.,
<BR><BR>
<CODE>mycomputer% acl2</CODE>
<BR><BR>
you may want to install an executable file on your path, e.g.,
<code>/usr/local/bin/acl2</code>, containing the following two lines:
<BR><BR>
<CODE>#!/bin/csh -f</CODE><BR>
<I>dir</I><CODE>/acl2-8.6/saved_acl2</CODE><BR>
<BR><BR>
Note: A carriage return in the file after the last line above may be important!
<P>
<BR>
<H4><A NAME="Starting">When ACL2 Starts Up</A></H4>
When you invoke ACL2, you should see the host Common Lisp
print a header concerning the ACL2 version, license and copyright.
<P>
Most or all hosts then automatically enter the ACL2 ``command loop,'' an ACL2
read-eval-print loop with the prompt:
<PRE>
ACL2 !>
</PRE>
If however a host leaves you in Common Lisp's read-eval-print loop,
then you'll need to evaluate the Common Lisp expression
<CODE>(ACL2::LP)</CODE> or simply <CODE>(LP)</CODE> if the current
package is <CODE>"ACL2"</CODE>.
<P>
Once in the ACL2 command loop, you can type an ACL2 term, typically
followed by ``return'' or ``enter,'' and ACL2 will evaluate the term,
print its value, and prompt you for another one. Below are three
simple interactions:
<PRE>
ACL2 !>t
T
ACL2 !>'abc
ABC
ACL2 !>(+ 2 2)
4
</PRE>
<P>
To get out of the ACL2 command loop, type the <code>:q</code> command.
This returns you to the host Common Lisp. We sometimes call this
``raw Lisp.'' You may re-enter the command loop with
<code>(LP)</code> as above.
<P>
Note that when you are in raw Lisp you can overwrite or destroy ACL2
by executing inappropriate Common Lisp expressions. <B>All bets are
off once you've exited our loop.</B> That said, many users do it.
For example, you might exit our loop, activate some debugging or trace
features in raw Lisp, and then reenter our loop. While developing
proofs or tracking down problems, this is reasonable behavior.
<P>
Now you are ready to <A HREF="#Testing">test</A> your image.
<BR><HR>
<H3><A NAME="Testing">Testing ACL2</A></H3>
<P>
An easy way to test the theorem prover is to
type the following term to the ACL2 command loop:
<PRE>
:mini-proveall
</PRE>
This will cause a moderately long sequence of commands to be processed, each of
which is first printed out as though you had typed it. Each will print some
text, generally a proof of some conjecture. None should fail.
<P>
A more elaborate test is to <A NAME="#Certifying">certify
the <a href="http://www.cs.utexas.edu/users/moore/acl2/v8-6/combined-manual/?topic=ACL2____COMMUNITY-BOOKS">community
books</a>, which is a good idea anyhow; this is our next
topic. On a Unix-like system, you can also certify just a
small but useful subset of the books in a few minutes by
executing, in directory
<i>dir</i>/<code>acl2-8.6</code>:
<pre>
make basic
</pre>
<BR><HR>
<H3><A NAME="Certifying">Certifying ACL2 Books</A></H3>
The <i><a href="http://www.cs.utexas.edu/users/moore/acl2/v8-6/combined-manual/?topic=ACL2____COMMUNITY-BOOKS">community
books</a></i>, which reside in subdirectory <code>books/</code>, have
been contributed mainly by users. The general topic of books is
discussed thoroughly in the ACL2
<A HREF="http://www.cs.utexas.edu/users/moore/acl2/v8-6/combined-manual/index.html?topic=ACL2____BOOKS">books
documentation</A>.
<P>
Books should be <i>certified</i> before they are used. We do not
distribute certificates with our books, mainly because certification
produces compiled code specific to the host. You should certify the
books locally, both as a test of your ACL2 image and because books
generally need to be certified before they can be used. Our main
installation page
contains <A HREF="installation.html#certify-books">simple
instructions</A> for how to perform this certification. For
additional explanation and further options, see the documentation
for <A HREF="http://www.cs.utexas.edu/users/moore/acl2/v8-6/combined-manual/index.html?topic=ACL2____BOOKS-CERTIFICATION">BOOKS-CERTIFICATION</A>.
<P>
Next proceed to the section on <A HREF="#Documentation">Documentation</A>.
<BR><HR>
<H3><A NAME="Documentation">Documentation</A></H3>
Documentation is discussed in the section on
the <A HREF="../../home-page.html#User's-Manual">User's Manual</A> on
the ACL2 home page.
<BR><HR>
<H3><A NAME="Emacs">Emacs</A></H3>
Emacs users may find it helpful to load into emacs the file
</CODE><I>dir</I><CODE>/acl2-8.6/emacs/emacs-acl2.el</CODE> for Emacs 25
or the file
</CODE><I>dir</I><CODE>/acl2-8.6/books/emacs/emacs-acl2.el</CODE> for
later Emacs versions. Utilities
offered by this file are documented near the top of the file. In
particular, this file automatically loads the
<A HREF="../../manual/index.html?topic=ACL2____ACL2-DOC">ACL2-Doc
Emacs browser</A>.
<BR><HR>
<b><font size="+2">[<a href="installation.html">Back to Installation Guide.</a>]</font></b>
<BR><BR><BR><BR><BR><BR><BR><BR><BR><BR><BR><BR><BR><BR><BR><BR><BR><BR><BR><BR>
</BODY>
</HTML>
|
