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
|
<HTML>
<HEAD><TITLE>ACL2 Version 8.6 Installation Guide</TITLE></HEAD>
<BODY TEXT="#000000" BGCOLOR="#FFFFFF" STYLE="font-family:'Verdana'">
<H1><A NAME="top"><a href="http://www.cs.utexas.edu/users/moore/acl2/v8-6/index.html">ACL2</a> Version 8.6 Installation Guide</A></H1>
<!-- If an incremental release is made, consider adding something here --
-- like the following: --
<H3>NOTE: From time to time we may provide so-called <i>incremental
releases</i> of ACL2. Please follow the <a
href="http://www.cs.utexas.edu/users/moore/acl2/v8-6/HTML/new.html">recent changes
to this page</a> link on the <a
href="http://www.cs.utexas.edu/users/moore/acl2/">ACL2 home page</a> for more
information.</H3>
-->
<hr size=3 noshade>
<a name="easy-install"><H1>Easy Install for Unix-like Systems</H1></name>
Here, "Unix-like Systems" includes Unix, GNU-Linux, and MacOS X. Note
that a quicker and even easier install may be possible, by instead
obtaining
a <a href="obtaining-and-installing.html#Shortcuts">pre-built binary
distribution</a> if one is available for your platform. Otherwise,
you can follow the directions below, which start by fetching a file
hosted at <a href="https://github.com/acl2/acl2/">the github ACL2
System and Books website</a>. The result is a directory containing
not only the ACL2 system but, in the <code>books/</code> subdirectory,
the <i><a href="http://www.cs.utexas.edu/users/moore/acl2/current/combined-manual/?topic=ACL2____COMMUNITY-BOOKS">community
books</a></i> (libraries). The ACL2 <i>system</i> is developed at the
University of Texas at Austin
and <a href="obtaining-and-installing.html#Summary">can also be
obtained or explored separately</a>.
<ol>
<li>Change to a directory whose full pathname contains no whitespace
and which does not already contain a subdirectory
named <code>acl2</code> or <code>acl2-8.6</code>. Then use
<font color="red">either</font> of the following two methods to obtain
the ACL2 source code and community books.
<ul>
<li>(<font color="red">Recommended</font> if you don't plan to
update from git)<br/>Fetch
<a href="https://github.com/acl2-devel/acl2-devel/releases/download/8.6/acl2-8.6.tar.gz">gzipped
tar file <code>acl2-8.6.tar.gz</code> from GitHub</a> and
then execute the following (the <code>rm</code> command is just
to make sure you don't already have a subdirectory
named <code>acl2-8.6</code>):<br/>
<code>rm -rf acl2-8.6</code><br/>
<code>tar xfz acl2-8.6.tar.gz</code><br/>
This will create a subdirectory named <code>acl2-8.6</code>.
Change to that directory.</li>
<li>(<font color="red">Development snapshot</font>, required if
you want
to <a href="http://www.cs.utexas.edu/users/moore/acl2/manuals/latest/index.html?topic=ACL2____GITHUB-COMMIT-CODE-USING-PULL-REQUESTS">update
from GitHub</a>)<br/>Execute the following (the <code>rm</code> command is just
to make sure you don't already have a subdirectory
named <code>acl2</code>):<br/>
<code>rm -rf acl2-8.6</code><br/>
<code>git clone https://github.com/acl2/acl2</code><br/>
This will create the subdirectory <code>acl2</code>.
Change to that directory.
</li>
</ul>
</li><p/>
<li><a href="requirements.html">Obtain a Common Lisp implementation</a> if you don't
already have one. (Note: Some of the
ACL2 <a href='https://www.cs.utexas.edu/users/moore/acl2/manuals/latest/?topic=ACL2____COMMUNITY-BOOKS'>community
books</a> depend on quicklisp, and those are only guaranteed to
work with CCL or SBCL.)</li><p/>
<li>Type:
<pre>
make LISP=<path_to_your_lisp_executable>
</pre>
This will create a script in the current directory
for running ACL2. The script is named <code>saved_acl2</code>.<br/>
<font color="red">Note:</font> You will need Gnu make. We have seen
problems on some Linux systems with Version 3.81 of that utility, so
if you encounter errors, please consider
our <a href="installing-make.html">instructions for downloading and
installing GNU make version 3.80</a>.</li><p/>
<li><A NAME="certify-books">Certify some books, for example with
<pre>
make basic
</pre>
or something fancier such as the following:
<pre>
(time nice make -j 8 ACL2=/u/smith/bin/acl2 basic) >& make-basic.log
</pre>
This may take only a few minutes, depending your <tt>-j</tt> value,
your machine, and your
host <a href="requirements.html#Obtaining-Lisp">Common Lisp</a>. The
resulting log should contain no occurrences of the string
``CERTIFICATION FAILED''; a normal exit (status 0) should guarantee
this. If you want further options or additional explanation (e.g.,
you can certify many more books with <code>make regression</code>, and there is a
discussion of avoiding root login), 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>.
</ol>
You now have an ACL2 executable called <code>saved_acl2</code> (from step 3)
and access to certified community books (from step 4). Enjoy!
<hr size=3 noshade>
<b><font size="+2" color="ff0000">THE ABOVE INSTRUCTIONS MAY BE ALL THAT YOU
NEED.</font></b> Otherwise, read on....
<hr size=3 noshade>
<p>
<H1>More Information</H1>
<UL>
<LI><A HREF="requirements.html">REQUIREMENTS</A>
<UL>
<LI><A HREF="requirements.html#Obtaining-Lisp">Obtaining Common Lisp</A>
</UL>
<LI><A HREF="obtaining-and-installing.html">OBTAINING AND INSTALLING ACL2</A>
<UL>
<LI><A HREF="obtaining-and-installing.html#Shortcuts">Pre-built Binary Distributions</A>
<LI><A HREF="obtaining-and-installing.html#Sources">Obtaining the Sources</A>
<LI><A HREF="obtaining-and-installing.html#Create-Image">Creating or Obtaining an Executable Image</A>
<LI><A HREF="obtaining-and-installing.html#Running">Running Without Building an Executable Image</A>
<LI><A HREF="obtaining-and-installing.html#Summary">Summary of Distribution</A>
</UL>
<LI><A HREF="using.html">USING ACL2</A>
<UL>
<LI><A HREF="using.html#Invoking">Invoking ACL2</A>
<UL>
<LI><A HREF="using.html#Starting">When ACL2 Starts Up</A>
</UL>
<LI><A HREF="using.html#Testing">Testing ACL2</A>
<LI><A HREF="using.html#Certifying">Certifying ACL2 Books</A>
<LI><A HREF="using.html#Documentation">Documentation</A>
<LI><A HREF="using.html#Emacs">Emacs</A>
</UL>
<LI><A HREF="misc.html#Miscellaneous">MISCELLANEOUS INFORMATION</A>
<UL>
<LI><A HREF="misc.html#Problems">Problems</A>
<LI><A HREF="misc.html#ACL2r">Reasoning about the Real Numbers</A>
<LI><A HREF="misc.html#Addresses">Links and Mailing Lists</A>
<LI><A HREF="misc.html#Export">Export/Re-Export Limitations</A>
<LI><A HREF="misc.html#License-and-Copyright">License and Copyright</A>
</UL>
</UL>
<P>Note: To build variants of ACL2, see the documentation
topic <a href="http://www.cs.utexas.edu/users/moore/acl2/manuals/latest/index.html?topic=COMMON-LISP____REAL">REAL</a>
for ACL2(r)
and <a href="http://www.cs.utexas.edu/users/moore/acl2/manuals/latest/index.html?topic=ACL2____COMPILING-ACL2P">COMPILING-ACL2P</a>
for ACL2(p).</P>
</BODY>
</HTML>
|
