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
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
|
<HTML>
<HEAD><TITLE>ACL2 Version 8.6 Installation Guide: Obtaining and
Installing <a href="http://www.cs.utexas.edu/users/moore/acl2/v8-6/index.html">ACL2</TITLE></HEAD>
<BODY TEXT="#000000" BGCOLOR="#FFFFFF" STYLE="font-family:'Verdana'">
<H1>Obtaining and Installing ACL2</A></H1>
<b><font>[<a href="installation.html">Back to main page of Installation Guide.</a>]</font></b>
<p/>
<b><font color="red">NOTES</font></b>
<ul>
<li>You may want to skip this page and simply use
the <a href="installation.html#easy-install">instructions for "Easy
Install for Unix-like Systems"</a>.</li>
<li>For information about getting started with ACL2, see
the <a href="http://www.cs.utexas.edu/users/moore/acl2/manuals/latest/index.html?topic=ACL2____START-HERE">"Start
Here" documentation page</a>.</li>
</ul>
<p>
<B>TABLE OF CONTENTS</B><BR>
<UL>
<LI><A HREF="#Shortcuts">Pre-built Binary Distributions</A>
<LI><A HREF="#Sources">Obtaining the Sources and Community Books</A>
<LI><A HREF="#Create-Image">Creating or Obtaining an Executable Image</A>
<UL>
<!-- The following is only for non-incremental releases. -->
<LI><A HREF="#Pre-Built-Images">Pre-Built Images</A>
<!-- End of only for non-incremental releases. -->
<LI><A HREF="#Other-Unix">Building an Executable image on a Unix-like System</A>
<LI><A HREF="#Non-Unix">Building an Executable image on Other than
a Unix-like Systems</A>
<LI><A HREF="#Build-Particular">Building an Executable Image on Some Particular Systems</A>
<UL>
<LI><A HREF="#Windows-GCL">Special Case: Building an Executable Image on a Windows System using GCL</A>
<LI><A HREF="windows-gcl-jared.html">Older instructions from Jared Davis for
building ACL2 on Windows using mingw</A>
</UL>
</UL>
<LI><A HREF="#Running">Running Without Building an Executable Image</A>
<LI><A HREF="#Summary">Summary of ACL2 System Distribution</A>
<LI><A HREF="#GitHub">GitHub Distributions</A>
</UL>
<p><hr size=4 noshade><p>
ACL2 is more than just the executable image. In particular, it comes
with
a <a href="http://www.cs.utexas.edu/users/moore/acl2/v8-6/index.html#User's-Manual">user's
manual</a>, and the system is distributed with libraries developed by
the ACL2 community, the
<i><a href="http://www.cs.utexas.edu/users/moore/acl2/current/combined-manual/?topic=ACL2____COMMUNITY-BOOKS">community
books</a></i>. Start here and we will take you through the whole
process of obtaining and installing ACL2.
<p>
First, create a directory under which to store ACL2 Version 8.6. We will
call this directory <I>dir</I>. For example, <I>dir</I> might be
<CODE>/home/jones/acl2/</CODE>.
<BR><HR noshade size=8><BR>
<H2><A NAME="Shortcuts">Pre-built Binary Distributions</A></H2>
<p>
See <a href='http://www.cs.utexas.edu/users/moore/acl2/manuals/latest/index.html?topic=ACL2____PRE-BUILT-BINARY-DISTRIBUTIONS'>the
ACL2 documentation page on pre-built binary distributions</a>,
which includes discussion of ACL2s binaries, Windows, MacPorts for
Mac OS X, and Debian GNU Linux.</h3>
<BR><HR noshade size=8><BR>
<H2><A NAME="Sources">Obtaining the Sources and Community Books</A></H2>
Here is how to obtain the sources and community books and place them
in a directory, <I>dir</I>.
<p>
(First, a note for Windows users only: we suggest that you obtain a
Unix-like environment or, at least, download a utility such as
<code>djtarnt.exe</code> to use with the <code>-x</code> option on
gzipped tarfiles. WARNING: At least one user experienced CR/LF issues
when using WinZIP, but we have received the suggestion that people
untarring with that utility should probably turn off smart cr/lf
conversion.)
<UL>
<LI>Save <A HREF="https://github.com/acl2-devel/acl2-devel/releases/download/8.6/acl2-8.6.tar.gz">
acl2-8.6.tar.gz</A> on directory <I>dir</I>.
</LI>
<BR>
<LI>Execute the following four Unix commands to obtain the ACL2 system
and community books. (<b>Note</b>: Gnu tar is preferred, as there
have been some problems with long file names when using at least one other tar
program. You may want to use the -i option, "<code>tar xpvfi
8.6.tar</code>", if you have problems with other than Gnu tar. You
can see if you have Gnu tar by running "<code>tar -v</code>".) The
resulting tarball and its extracted directory may consist of
230M+ bytes and 1100M+ bytes, respectively. Additional space is
required to build an executable image, for example,
170M+ bytes if you use CCL and 230M bytes if you use SBCL; and
considerably more will be required
to <A HREF="using.html#Certifying">certify books</A>.
<BR><BR>
<CODE>cd <I>dir</I></CODE><BR>
<CODE>tar xfz acl2-8.6.tar.gz</CODE><BR>
<CODE>rm acl2-8.6.tar.gz</CODE><BR>
<CODE>cd acl2-8.6</CODE><BR>
<BR>
</LI>
</UL>
<p>
<b>Note</b>: You can also fetch the latest GitHub distribution
the ACL2 system and the community books, as shown below.
<pre>
git clone https://github.com/acl2/acl2
</pre>
Moreover, you
can <a href="https://github.com/acl2/acl2#contributors-wanted">contribute
books by joining the GitHub project</a>.
<BR><HR noshade size=8><BR>
<H2><A NAME="Create-Image">Creating or Obtaining an Executable Image</A></H2>
The next step is to create an executable image. The common approach is to
build that image from the sources you have already obtained.
<!-- The following is only for non-incremental releases. -->
However, you may
be able to <A HREF="#Pre-Built-Images">take a short cut by downloading an
ACL2 image</A>, in which case you can skip ahead to the page on
<A HREF="using.html">Using ACL2</A>. Otherwise you should click on
one of the links just below.
<!-- End of only for non-incremental releases. -->
Choose the last option if you are using a Common Lisp on which you cannot save
an image (e.g., a trial version of Allegro Common Lisp).
<P>
PLEASE NOTE: The available memory for ACL2 is determined by the underlying
Common Lisp executable. If you need more memory, refer to your Common Lisp's
instructions for building an executable.
<UL>
<LI><A HREF="#Other-Unix">Building an Executable Image on a Unix-like System</A>
<LI><A HREF="#Non-Unix">Building an Executable Image on Other than a
Unix-like System</A>
<LI><A HREF="#Running">Running Without Building an Executable Image</A>
</UL>
<!-- The following is only for non-incremental releases. -->
<BR><HR><BR>
<H3><A NAME="Pre-Built-Images">Short Cut: Pre-Built ACL2 Images</A></H3>
The site <a
href="http://www.cs.utexas.edu/users/moore/acl2/v8-6/distrib/images/Readme.html">http://www.cs.utexas.edu/users/moore/acl2/v8-6/distrib/images/Readme.html</a>
contains links to ACL2 executables and packages. Each <code>-md5sum</code> file
was created using <code>md5sum</code>. We may add additional
links from time to time.
<p>
Now proceed to <A HREF="using.html">Using ACL2</A>.
<!-- End of only for non-incremental releases. -->
<BR><HR><BR>
<H3><A NAME="Other-Unix">Building an Executable Image on a Unix-like System</A></H3>
We assume you have obtained ACL2 and placed it in directory <I>dir</I>, as
described <A HREF="#Sources">above</A>.
<!-- The following is only for non-incremental releases. -->
If you downloaded a <A
HREF="#Pre-Built-Images">pre-built ACL2 image</A>, you may skip this section.
<!-- End of only for non-incremental releases. -->
Change directory to <I>dir</I> as above and execute <BR><BR> <CODE>cd
acl2-8.6</CODE><BR> <CODE>make LISP=</CODE><I>xxx</I><BR>
<BR>
where <I>xxx</I> is the command to run your local Common Lisp.
<P>
By default, if no <CODE>LISP=</CODE><I>xxx</I> is specified,
<CODE>LISP=ccl</CODE> is used. On our hosts, <CODE>ccl</CODE> is the name of
Clozure Common Lisp (CCL), which can be obtained as <a
href="requirements.html#Obtaining-CCL">explained in the Requirements document</a>.
<P>
This will create executable <code>saved_acl2</code> in the
<code>acl2-8.6</code> directory.
<P>
The time taken to carry out this process depends on the host processor
but may be only a few minutes for a fast processor. The size of the
resulting binary image is dependent on which Lisp was used, but it may be
a couple hundred megabytes or so.
<P>
This <CODE>make</CODE> works for the Common Lisp implementations listed
in <A HREF="requirements.html">Requirements document</A> on systems we
have tested. See the file <CODE>acl2-8.6/GNUmakefile</CODE> for
further details. If this <CODE>make</CODE> command does not work for
you, please see the instructions below for <A HREF="#Non-Unix">other
than Unix-like systems</A>.
<P>
You can now skip to <A HREF="using.html">Using ACL2</A>.
<P>
<BR><HR><BR>
<H3><A NAME="Non-Unix">Building an Executable Image on Other than a
Unix-like System</A></H3>
Next we describe how to create a binary image containing ACL2 without
using the `<code>make</code>' utility. If you are using a <B>trial
version</B> of Allegro Common Lisp, then you may not be able to save
an image. In that case, skip to <A href="#Running">Running Without
Building an Executable Image</A>.
<P>
See also <a href="#Build-Particular">Building an Executable Image on Some Particular
Systems</a>, in case you want to skip directly to the instructions in one of
its subtopics.
<P>
Otherwise, proceed as follows.
<P>
Your Common Lisp should be one of those listed in
<A HREF="requirements.html">Requirements document</A>. Filenames
below should default to the <I>dir</I><CODE>/acl2-8.6</CODE>
directory; please change to that directory before continuing.
<OL>
<P><LI> Remove file <CODE>nsaved_acl2</CODE> if it exists.</LI>
<P><LI> Start up Common Lisp in the <CODE>acl2-8.6</CODE> directory
and submit the following sequence of commands.
<PRE>
; Compile
(load "init.lisp")
(in-package "ACL2")
(compile-acl2)
</PRE>
The commands above will compile the ACL2 sources and create compiled object
files on your <CODE>acl2-8.6</CODE> subdirectory. Here we assume
that executables have extension <code>.dxl</code>, but this will
depend on your host Lisp and operating system.
</LI>
<P><LI> Now exit your Common Lisp and invoke a fresh copy of it (mainly to avoid
saving an image with the garbage created by the compilation process). Again
arrange to change to the <CODE>acl2-8.6</CODE> subdirectory. In the
fresh Lisp <a name="initialization-first-pass">type</a>:
<PRE>
; Initialization, first pass
(load "init.lisp")
(in-package "ACL2")
(load-acl2)
(initialize-acl2)
</PRE>
This will load the new object files in the Lisp image and bootstrap ACL2 by
reading and processing the source files. But the attempt at initialization
will end in an error saying that it is impossible to finish because a certain
file was compiled during the processing, thus dirtying the image yet again.
(If however the attempt ends with an error during compilation of file
<code>TMP1.lisp</code>, see the first troubleshooting tip <a
href="#troubleshooting-TMP1">below</a>.)
</LI>
<P><LI> So now exit your Common Lisp and invoke a fresh copy of it (again arranging
to change to your <CODE>acl2-8.6</CODE> subdirectory). Then, in the
fresh Lisp type:
<PRE>
; Initialization, second pass
(load "init.lisp")
(in-package "ACL2")
(save-acl2 (quote (initialize-acl2))
"saved_acl2")
</PRE>
You have now saved an image. Exit Lisp now. Subsequent steps will put the
image in the right place.
<P><LI> Remove <CODE>osaved_acl2</CODE> if it exists.
<P><LI> <b>IF</b> <CODE>saved_acl2</CODE> and <CODE>saved_acl2.dxl</CODE> both exist <b>THEN</b>:
<ul>
<li>move <CODE>saved_acl2.dxl</CODE> to <CODE>osaved_acl2.dxl</CODE></li>
<li>move <CODE>saved_acl2</CODE> to <CODE>osaved_acl2</CODE>
and edit <CODE>osaved_acl2</CODE>, changing <CODE>saved_acl2.dxl</CODE>
(at end of line) to <CODE>osaved_acl2.dxl</CODE></li>
</ul>
<b>ELSE IF</b> <CODE>saved_acl2</CODE> exists <b>THEN</b>:
<ul>
<li>move <CODE>saved_acl2</CODE> to <CODE>osaved_acl2</CODE></li>
</ul>
</LI>
<P><LI> Move <CODE>nsaved_acl2</CODE> to <CODE>saved_acl2</CODE>.</LI>
<P><LI> For some Common Lisps, a
file <CODE>nsaved_acl2.</CODE><em>suffix</em> is created for some
<em>suffix</em>.
Move it to: <CODE>saved_acl2.</CODE><em>suffix</em></LI>
<P><LI> Make sure <CODE>saved_acl2</CODE> is executable. For Windows
this involves two mini-steps:
<blockquote>
(a) Remove the <code>"$*"</code> from the <code>saved_acl2</code>
script (because Windows does not understand <code>$*</code>).
Consequently, any arguments you pass to ACL2 via the command line will
be ignored.
<p>
(b) Rename <code>saved_acl2</code> to <code>saved_acl2.bat</code>, for
example by executing the following command.<br><br>
<code>rename saved_acl2 saved_acl2.bat</code>
</blockquote>
</LI>
</OL>
<BR><HR><BR>
<H3><A NAME="Build-Particular">Building an Executable Image on Some Particular Systems</A></H3>
Subtopics of this section are as follows.
<UL>
<LI><A HREF="#Windows-GCL">Special Case: Building an Executable Image on a Windows System using GCL</A>
<LI><A HREF="windows7.html">Instructions from David Rager
for building ACL2 on Windows</A>
<LI><A HREF="windows-gcl-jared.html">Older instructions from Jared Davis for
building ACL2 on Windows using mingw</A>
</UL>
<BR><HR><BR>
<H3><A NAME="Windows-GCL">Special Case: Building an Executable Image on a Windows System using GCL</A></H3>
You may want to skip this section and instead
read <A HREF="windows7.html">Instructions from David Rager for
building ACL2 on Windows</A>. See also
additional <a href="../../distrib/windows/">information about ACL2 on
Windows</a>.
<!-- The following is only for non-incremental releases. -->
Or, you may be able to <a href="#Pre-Built-Images">download a pre-built ACL2 image</a>
for Windows instead of reading this section.
<!-- End of only for non-incremental releases. -->
<p>
Otherwise here are steps to follow. (These are quite old and may have
bugs. Please report any bugs to
the <A HREF="mailto:kaufmann@cs.utexas.edu">Matt Kaufmann</A>ACL2
implementors</A>.)
<ol>
<li><b>FIRST</b> get GCL running on your Windows system using <b>ONE</b> of the
following two options. Note that GCL can be unhappy with spaces in filenames,
so you should probably save the GCL distribution to a directory whose path is
free of spaces.
<ul>
<li><b>OR</b>, obtain GCL for Windows systems from <code><a
href="ftp://ftp.gnu.org/gnu/gcl/">ftp://ftp.gnu.org/gnu/gcl/</a></code>
or as explained <a href="#Obtaining-GCL">above</a>. You
may wish to pick a <code>.zip</code> file from the <code>cvs/</code>
subdirectory (containing pre-releases) that has "<code>mingw32</code>" in the
name.
<li><b>OR ELSE</b>, perhaps you can build GCL on your Windows system from the
sources. The mingw tools and the cygnus bash shell have been used to build
distributed GCL executables.
</ul>
<li><b>SECOND</b>, create an appropriate GCL batch file. When we tried running
the script <code>gclm/bin/gclm.bat</code> that came with
<code>gcl-cvs-20021014-mingw32</code> from the above ftp site, a separate
window popped up, and with an error. Many ACL2 users prefer running in an
emacs shell buffer. (We obtained emacs for Windows from <code><a
href="ftp://ftp.gnu.org/gnu/windows/emacs/21.2/emacs-21.2-fullbin-i386.tar.gz">ftp://ftp.gnu.org/gnu/windows/emacs/21.2/emacs-21.2-fullbin-i386.tar.gz</a></code>.)
The following modification of <code>gclm.bat</code> seemed to solve the problem
(your pathnames may vary).
<pre>
@
% do not delete this line %
@ECHO off
set cwd=%cd%
path C:\gcl\gclm\mingw\bin;%PATH%
C:\gcl\gclm\lib\gcl-2.6.2\unixport\saved_gcl.exe -dir C:/gcl/gclm/lib/gcl-2.6.2/unixport/ -libdir C:/gcl/gclm/lib/gcl-2.6.2/ -eval "(setq si::*allow-gzipped-file* t)" %1 %2 %3 %4 %5 %6 %7 %8 %9
</pre>
<li><b>THIRD</b>, follow the <A HREF="#Non-Unix">instructions for
other than Unix-like systems</A> above, though the resulting file
may be called
<code>saved_acl2.exe</code> rather than <code>saved_acl2</code>.
<!-- NOTE to developers: v8-6 below indicates a normal release, which is OK. -->
<!-- Do not edit that for incremental releases. -->
<li><b>FINALLY</b>, create a file <code>acl2.bat</code> as explained in
<code><a href="http://www.cs.utexas.edu/users/moore/acl2/v8-6/distrib/images/Readme.html#acl2-bat">
http://www.cs.utexas.edu/users/moore/acl2/v8-6/distrib/images/Readme.html</a></code>.
</ol>
<p>
We hope that the above simply works. If you experience
problems, the following hints may help.
<p>
<b>TROUBLESHOOTING:</b>
<ul>
<li><a name="troubleshooting-TMP1">We</a> tried building ACL2 on Windows XP on
top of GCL, our attempt broke at the end of the "<a
href="#initialization-first-pass">Initialization, first pass</a>" step, while
compiling <code>TMP1.lisp</code>. That was easily remedied by starting up a
fresh GCL session and invoking <code>(compile-file "TMP1.lisp")</code> before
proceeding to the next step.
<li>Yishai Feldman has provided some nice instructions at <code><a
href="http://www.faculty.idc.ac.il/yishai/reasoning/win-install.htm">http://www.faculty.idc.ac.il/yishai/reasoning/win-install.htm</a></code>,
some of which we have tried to incorporate here. A useful point made there is
that when you want to quit ACL2, use <code>:good-bye</code> (or
<code>(good-bye)</code> which works even in raw Lisp). Or you can use
<code>(user::bye)</code> in raw Lisp. The point is: Avoid <code>control-c
control-d</code>, even thought that often works fine in emacs under
Unix-like systems.
<li>If the above batch file does not work for some reason, an alternate
approach may be to set environment variables. You may be able to add to the
<code>PATH</code> variable <i>gcl-dir</i><code>\gcc\bin</code>, where
<i>gcl-dir</i> is the directory where GCL is installed. To get to the place to
set environment variables, you might be able to go to the control panel, under
system, under advanced. Alternately, you might be able to get there by opening
<code>My Computer</code> and right-clicking to get to <code>Properties</code>,
then selecting the <code>Advanced</code> tab. At one time, when GCL/Windows
was released as Maxima, Pete Manolios suggested adding the system variable
LD_LIBRARY_PATH with the value "maxima-dir\gcc\i386-mingw32msvc\include"; this
may or may not be necessary for your GCL installation (and the path would of
course likely be different).
</ul>
<BR><HR noshade size=8><BR>
<H2><A NAME="Running">Running Without Building an Executable Image</A></H2>
The most convenient way to use ACL2 is first to install an executable image as
described above for <A HREF="#Other-Unix">Unix-like systems</A> and <A
HREF="#Non-Unix">other</A> platforms. However, in some cases this is not
possible, for example if you are using a trial version of Allegro Common Lisp.
In that case you should follow the steps below each time you want to start up
ACL2.
<P>
We assume you have obtained ACL2 and placed it in directory <I>dir</I>, as
described above for <A HREF="#Sources">Unix-like systems</A> or <A
HREF="#Sources-Non-Unix">other</A> platforms.
<!-- The following is only for non-incremental releases. -->
(If you downloaded a <A
HREF="#Pre-Built-Images">pre-built ACL2 image</A>, then you may skip this section.)
<!-- End of only for non-incremental releases. -->
Change to subdirectory <CODE>acl2-8.6</CODE> of <I>dir</I>,
start up your Common Lisp, and compile by executing the following forms.
<I>This sequence of steps need only be performed once.</I>
<PRE>
(load "init.lisp")
(in-package "ACL2")
(compile-acl2)
</PRE>
Now each time you want to use ACL2, execute the following forms
after starting up Common Lisp in subdirectory <CODE>acl2-8.6</CODE> of
<I>dir</I>. This may take a minute or two (which is another reason to
consider installing an executable image as described above, using
`<code>make</code>' if possible).
<PRE>
(load "init.lisp")
(in-package "ACL2")
(load-acl2)
(initialize-acl2)
(lp) ; enter the ACL2 read-eval-print loop
</PRE>
<P>
Now proceed to read more about <A HREF="using.html">Using ACL2</A>.
<BR><HR noshade size=8><BR>
<H2><A NAME="Summary">Summary of ACL2 System Distribution</A></H2>
This section, which is optional, discusses how to browse a
distribution that includes ACL2 only, without the
<a href="http://www.cs.utexas.edu/users/moore/acl2/current/combined-manual/?topic=ACL2____COMMUNITY-BOOKS">community
books</a>.
<p>
We discuss <a href="#Sources">above</a> how to obtain a gzipped
tarfile that contains both the ACL2 sources and
the <a href="http://www.cs.utexas.edu/users/moore/acl2/current/combined-manual/?topic=ACL2____COMMUNITY-BOOKS">community
books</a>. Below we describe the ACL2 distribution only (without the
community books) from the University of Texas at Austin. Its files
are available by exploring the
<code><a href="http://www.cs.utexas.edu/users/moore/acl2/v8-6/distrib/">distrib/<a></code>
directory on this website or by obtaining a gzipped tarfile,
<code><a href="http://www.cs.utexas.edu/users/moore/acl2/v8-6/distrib/acl2.tar.gz">acl2.tar.gz</a></code>,
which extracts to the contents
of <code><a href="http://www.cs.utexas.edu/users/moore/acl2/v8-6/distrib/">distrib/acl2-sources/<a></code>,
which in turn contains the ACL2 source files as well as the following
(and a few others not mentioned here).
<PRE>
LICENSE ; ACL2 license file
GNUmakefile ; For GNU make
TAGS ; Handy for looking at source files with emacs
TAGS-acl2-doc ; Handy for finding code in books, e.g., with the acl2-doc browser
bin/ ; Contains an executable script, bin/acl2, which invokes ACL2
doc/ ; ACL2 documentation
emacs/ ; Some helpful emacs utilities
installation/ ; Installation instructions (start with installation.html)
</PRE>
Also available are the following.
<ul>
<li><code><a href="http://www.cs.utexas.edu/users/moore/acl2/v8-6/distrib/acl2-sources/acl2-customization-files/">ACL2
customization files</a></code>:
These <a href="http://www.cs.utexas.edu/users/moore/acl2/manuals/current/manual/index.html?topic=ACL2____ACL2-CUSTOMIZATION">ACL2
customization</a> files can be useful
for <a href="http://www.cs.utexas.edu/users/moore/acl2/manuals/current/manual/index.html?topic=ACL2____CERTIFY-BOOK">certifying
books</a>, for example
with <a href="http://www.cs.utexas.edu/users/moore/acl2/manuals/current/manual/index.html?topic=ACL2____PARALLELISM">ACL2(p)</a>.</li>
<li><code><a href="http://www.cs.utexas.edu/users/moore/acl2/v8-6/distrib/images/">images/</a></code>:
Some gzip'd tar'd executables; see <code><a href="http://www.cs.utexas.edu/users/moore/acl2/v8-6/distrib/images/Readme.html">images/Readme.html</a></code></li>
<li><code><a href="http://www.cs.utexas.edu/users/moore/acl2/v8-6/distrib/split/">split/</a></code>: The result of splitting up <code>acl2.tar.gz</code></li>
</ul>
<BR><HR noshade size=8><BR>
<H2><A NAME="GitHub">GitHub Distributions</A></H2>
We strongly recommend that ACL2 users update their local copies of the
system and community books at each ACL2 release. While that should
suffice for many ACL2 users, nevertheless for those who prefer to
obtain the latest developments, the ACL2 source code and community
books have been made available between ACL2 releases, by way of
revision control using git. See
the <a href="https://github.com/acl2/acl2">project website</a> for
more information.
<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>
|
