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
|
<HTML>
<HEAD><TITLE>ACL2 Version 7.2 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/v7-2/index.html">ACL2</a> Version 7.2 Installation Guide</A></H1>
<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/v7-2/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>
<H1>Easy Install for Unix-like Systems</H1>
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>Fetch a <a href="https://github.com/acl2-devel/acl2-devel/releases/download/7.2/acl2-7.2.tar.gz">gzipped tar file from GitHub</a> containing ACL2 Version 7.2 and the
corresponding Community Books, which will download
file <code>acl2-7.2.tar.gz</code> onto your system. Put that file
in a directory whose pathname does not contain whitespace.</li>
<li>Execute the following to create
subdirectory <code>acl2-7.2/</code>. (These installation
instructions assume that you don't rename the new subdirectory,
though you are welcome to do so.)<br>
<code>tar xfz acl2-7.2.tar.gz</code></li>
<li><a href="requirements.html">Obtain a Common Lisp implementation</a> if you don't
already have one.</li>
<li>Build by connecting to the new <code>acl2-7.2/</code> directory
and typing the following, which may take a few minutes to complete.
<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>.
<pre>
make LISP=<path_to_your_lisp_executable>
</pre></li>
This will create a script in your <code>acl2-7.2</code>
directory for running ACL2, named <code>saved_acl2</code>.
<li><A NAME="certify-books">Certify books, for example with
<pre>
make certify-books
</pre>
or something fancier such as the following:
<pre>
(time nice make -j 8 ACL2=/u/smith/bin/acl2 certify-books) >& make-certify-books.log
</pre>
This may take up to several hours. The resulting log
file, <code>make-certify-books.log</code>, should contain no
occurrences of the string ``CERTIFICATION FAILED''; a normal exit
(status 0) should guarantee this. If you want additional explanation
and further options, see the documentation
for <A HREF="http://www.cs.utexas.edu/users/moore/acl2/v7-2/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 4)
and access to certified community books (from step 5). 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#Performance">Performance comparisons</A>
<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>
</BODY>
</HTML>
|
