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
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
|
<HTML>
<HEAD><TITLE>ACL2 Version 7.2 Installation Guide: Obtaining and
Installing <a href="http://www.cs.utexas.edu/users/moore/acl2/v7-2/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>Table of Contents</B><BR>
<UL>
<LI><A HREF="#Shortcuts">Pre-built Binary Distributions</A>
<UL>
<LI><A HREF="#Shortcut-acl2s">Linux/Mac/Windows Binaries in ACL2s</A>
<LI><A HREF="#Shortcut-windows">Windows</A>
<LI><A HREF="#Shortcut-MacPorts">MacPorts for Mac OS X</A>
<LI><A HREF="#Shortcut-debian">Debian GNU Linux</A>
</UL>
<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="#Bleeding-edge">Bleeding-edge Distributions via SVN</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/v7-2/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 7.2. We will
call this directory <I>dir</I>. For example, <I>dir</I> might be
<CODE>/home/jones/acl2/</CODE>.
<H3>NOTE: If you intend to obtain an incremental release (e.g. 2.9.4 as opposed
to 2.9), please see the <a href="../new.html">ACL2 News</a> for instructions.
Otherwise, continue reading here.</H3>
<BR><HR noshade size=8><BR>
<H2><A NAME="Shortcuts">Pre-built Binary Distributions</A></H2>
Visit the "Recent changes to this page" link on the <A
HREF="http://www.cs.utexas.edu/users/moore/acl2/">ACL2 home page</A> to see if
there are other shortcuts available.
<p>
WARNING: Some of these packages might be for old version of ACL2. We
recommend that you use the latest version of ACL2 (Version 7.2).
<UL>
<LI><B><A NAME="Shortcut-acl2s">Linux/Mac/Windows Binaries in ACL2s</A></B>
<p>
The <a href="http://acl2s.ccs.neu.edu/acl2s/doc/">ACL2 Sedan</a>
(ACL2s) is an Eclipse-based IDE for ACL2 that is distributed with pre-certified
books and pre-built binaries. If you
use an alternative development environment (such as Emacs), you
can still <a href="http://acl2s.ccs.neu.edu/acl2s/src/acl2/">fetch a
tarball</a> for your x86-based Linux/Mac/Windows system that contains a
pre-built binary of (pure) ACL2, using the following instructions
based on information kindly provided by Harsh Raju Chamarthi.
Just extract the
appropriate tarball (using <code>tar xfz</code> on Linux or Mac
and <code>unzip</code> on Windows)
under a path with <i>no</i> spaces.
Then run the script you will
find, <code>run_acl2</code> on Linux or Mac
and <code>run_acl2.exe</code> on Windows, to start an ACL2 session.
(Note that The first time you execute that command,
the certificate (<code>.cert</code>) files are automatically
fixed, according to the full pathname of your <code>books/</code> directory.)
Also see
the <a href="http://www.cs.utexas.edu/users/moore/acl2/v7-2/combined-manual/index.html?topic=ACL2____ACL2-SEDAN">ACL2
documentation topic on the ACL2 Sedan</a>.
<LI><B><A NAME="Shortcut-windows">Windows</A></B>
<p>
In the past, a Windows Installer for ACL2 has included a Unix
environment, pre-certified standard and workshop books, and a copy of
Gnu Emacs. This capability has largely been superseded
by <a href="#Build-Particular">the section on Building an Executable
Image on Some Particular Systems</a> and
the Shortcut using the ACL2 Sedan, <a href="#Shortcut-acl2s">above</a>.
See also <a href="../../distrib/windows/">information about ACL2 on
Windows</a>.
<LI><B><A NAME="Shortcut-MacPorts">MacPorts for Mac OS X</A></B>
<p>
ACL2 versions have sometimes been made available under MacPorts. If
we learn that an up-to-date version is available, we will add
instructions here.
<LI><B><A NAME="Shortcut-debian">Debian GNU Linux</A></B>
<p>
A Debian Gnu Linux package is available, which is likely to work on
other Linux systems as well. Thanks to Camm Maguire for maintaining
this package, and for pointing out that as Debian packages are simply
ar and tar archives, they can be unpacked on any linux system, and who
has said: "If someone is running Debian, all they want to do is
'apt-get install acl2', doing likewise for any optional add-on package
they wish as well, e.g. emacs, infix, etc." Alternatively, Debian GNU
Linux users may wish
to <A HREF="http://packages.qa.debian.org/a/acl2.html">download the
ACL2 Debian package for Linux</A>. An alternate location you might
want to check
is <code><a href="http://backports.debian.org">backports.debian.org</a></code>.
</UL>
<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/7.2/acl2-7.2.tar.gz">
acl2-7.2.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 tar provided
by SunOS. You may want to use the -i option, "<code>tar xpvfi
7.2.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 will consist of approximately 64 MB and its
extracted directory will consist of approximately 206 MB. Additional
space is required to build an executable image, perhaps 110 to 260 MB
depending on the platform (including the host Lisp); and 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-7.2.tar.gz</CODE><BR>
<CODE>rm acl2-7.2.tar.gz</CODE><BR>
<CODE>cd acl2-7.2</CODE><BR>
<BR>
</LI>
</UL>
<p>
<b>Note</b>: Alternatively, for read-write access, become a member of
the acl2-books project
by <a href="https://github.com/acl2/acl2#contributors-wanted">contacting
one of the project administrators as described on acl2-books project
page</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/v7-2/distrib/images/Readme.html">http://www.cs.utexas.edu/users/moore/acl2/v7-2/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. -->
Connect to <I>dir</I> as above and execute <BR><BR> <CODE>cd
acl2-7.2</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-7.2</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-7.2/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-7.2</CODE>
directory; please connect 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-7.2</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-7.2</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 connect to the <CODE>acl2-7.2</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 connect to your <CODE>acl2-7.2</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>.
<!-- 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: v7-2 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/v7-2/distrib/images/Readme.html#acl2-bat">
http://www.cs.utexas.edu/users/moore/acl2/v7-2/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 release 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. -->
Connect to subdirectory <CODE>acl2-7.2</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, you need only execute the following forms
after starting up Common Lisp in subdirectory <CODE>acl2-7.2</CODE> of
<I>dir</I>.
<PRE>
(load "init.lisp")
(in-package "ACL2")
(load-acl2)
(initialize-acl2)
</PRE>
<I>Note.</I> The resulting process includes the ACL2 documentation, and hence
will probably be considerably larger (perhaps twice the size) than the result
of running an executable image created as described <A
HREF="#Create-Image">above</A>.
<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/v7-2/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/v7-2/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/v7-2/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
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/v7-2/distrib/images/">images/</a></code>:
Some gzip'd tar'd executables; see <code><a href="http://www.cs.utexas.edu/users/moore/acl2/v7-2/distrib/images/Readme.html">images/Readme.html</a></code></li>
<li><code><a href="http://www.cs.utexas.edu/users/moore/acl2/v7-2/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="Bleeding-edge">Bleeding-edge Distributions via Git</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.
<i>The authors of ACL2 consider git distributions to be experimental;
while they will likely be fully functional in most cases, they could
however be incomplete, fragile, and unable to pass our own
regression.</i> 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>
|
