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
|
<HTML>
<HEAD><TITLE>ACL2 Version 4.3 Installation Guide</TITLE></HEAD>
<BODY TEXT="#000000">
<BODY BGCOLOR="#FFFFFF">
<H1><A NAME="top">ACL2 Version 4.3 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/v4-3/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 Linux/Unix/MacOS</H1>
<b>NOTE:</b> 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:
<ol>
<li>Fetch <A HREF="http://www.cs.utexas.edu/users/moore/acl2/v4-3/distrib/acl2.tar.gz">
acl2.tar.gz</A> into a new directory, say <code>acl2/v4-3/</code>.</li>
<li>Execute the following to create directory <code>acl2-sources/</code>:
<pre>
tar xfz acl2.tar.gz
</pre></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 your <code>acl2-sources/</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 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>. (That said, in builds with
Allegro Common Lisp we have seen problems certifying books with GNU
make version 3.80 that seemed to be solved with version 3.81.)
<pre>
make LISP=<path_to_your_lisp_executable>
</pre></li>
<li>Certify books (this may take a few hours; you can speed this up
with the option <code>-j N</code> if you have an N-core machine, N>1):
<pre>
make regression
</pre>
</ol>
You now have an ACL2 executable called <code>saved_acl2</code> (from step 4)
and access to certified distributed books (from step 5). Enjoy!
<p>
<i>Note</i>: There are many other books available from ACL2 workshops,
available
<a href="http://www.cs.utexas.edu/users/moore/acl2/v4-3/distrib/acl2-sources/books/workshops.tar.gz">here</a>.
<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>
<LI><A HREF="requirements.html#Performance">Performance comparisons</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-Unix">Obtaining the Sources: Unix, Mac OS X, and Linux</A>
<LI><A HREF="obtaining-and-installing.html#Sources-Non-Unix">Obtaining the Sources: Other than Unix, Mac OS X, and Linux Systems</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>
</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>
|
