File: installation.html

package info (click to toggle)
acl2 3.1-1
  • links: PTS
  • area: main
  • in suites: etch, etch-m68k
  • size: 36,712 kB
  • ctags: 38,396
  • sloc: lisp: 464,023; makefile: 5,470; sh: 86; csh: 47; cpp: 25; ansic: 22
file content (1345 lines) | stat: -rw-r--r-- 51,684 bytes parent folder | download | duplicates (2)
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
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
863
864
865
866
867
868
869
870
871
872
873
874
875
876
877
878
879
880
881
882
883
884
885
886
887
888
889
890
891
892
893
894
895
896
897
898
899
900
901
902
903
904
905
906
907
908
909
910
911
912
913
914
915
916
917
918
919
920
921
922
923
924
925
926
927
928
929
930
931
932
933
934
935
936
937
938
939
940
941
942
943
944
945
946
947
948
949
950
951
952
953
954
955
956
957
958
959
960
961
962
963
964
965
966
967
968
969
970
971
972
973
974
975
976
977
978
979
980
981
982
983
984
985
986
987
988
989
990
991
992
993
994
995
996
997
998
999
1000
1001
1002
1003
1004
1005
1006
1007
1008
1009
1010
1011
1012
1013
1014
1015
1016
1017
1018
1019
1020
1021
1022
1023
1024
1025
1026
1027
1028
1029
1030
1031
1032
1033
1034
1035
1036
1037
1038
1039
1040
1041
1042
1043
1044
1045
1046
1047
1048
1049
1050
1051
1052
1053
1054
1055
1056
1057
1058
1059
1060
1061
1062
1063
1064
1065
1066
1067
1068
1069
1070
1071
1072
1073
1074
1075
1076
1077
1078
1079
1080
1081
1082
1083
1084
1085
1086
1087
1088
1089
1090
1091
1092
1093
1094
1095
1096
1097
1098
1099
1100
1101
1102
1103
1104
1105
1106
1107
1108
1109
1110
1111
1112
1113
1114
1115
1116
1117
1118
1119
1120
1121
1122
1123
1124
1125
1126
1127
1128
1129
1130
1131
1132
1133
1134
1135
1136
1137
1138
1139
1140
1141
1142
1143
1144
1145
1146
1147
1148
1149
1150
1151
1152
1153
1154
1155
1156
1157
1158
1159
1160
1161
1162
1163
1164
1165
1166
1167
1168
1169
1170
1171
1172
1173
1174
1175
1176
1177
1178
1179
1180
1181
1182
1183
1184
1185
1186
1187
1188
1189
1190
1191
1192
1193
1194
1195
1196
1197
1198
1199
1200
1201
1202
1203
1204
1205
1206
1207
1208
1209
1210
1211
1212
1213
1214
1215
1216
1217
1218
1219
1220
1221
1222
1223
1224
1225
1226
1227
1228
1229
1230
1231
1232
1233
1234
1235
1236
1237
1238
1239
1240
1241
1242
1243
1244
1245
1246
1247
1248
1249
1250
1251
1252
1253
1254
1255
1256
1257
1258
1259
1260
1261
1262
1263
1264
1265
1266
1267
1268
1269
1270
1271
1272
1273
1274
1275
1276
1277
1278
1279
1280
1281
1282
1283
1284
1285
1286
1287
1288
1289
1290
1291
1292
1293
1294
1295
1296
1297
1298
1299
1300
1301
1302
1303
1304
1305
1306
1307
1308
1309
1310
1311
1312
1313
1314
1315
1316
1317
1318
1319
1320
1321
1322
1323
1324
1325
1326
1327
1328
1329
1330
1331
1332
1333
1334
1335
1336
1337
1338
1339
1340
1341
1342
1343
1344
1345
<HTML>
<HEAD><TITLE>ACL2 Version 3.1 Installation Guide</TITLE></HEAD>

<BODY TEXT="#000000">
<BODY BGCOLOR="#FFFFFF">

<H1><A NAME="top">ACL2 Version 3.1 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/v3-1/new.html">recent changes to
this page</a> link on the ACL2 home page for more information.</H3>

<hr>

<B>Table of Contents</B><BR>
<UL>
<LI><A HREF="#Requirements">REQUIREMENTS</A>
<UL>
  <LI><A HREF="#Obtaining-Lisp">Obtaining Common Lisp</A>
  <UL>
    <LI><A HREF="#Obtaining-GCL">Obtaining GCL</A>
    <LI><A HREF="#Obtaining-Allegro">Obtaining Allegro Common Lisp</A>
    <LI><A HREF="#Obtaining-CMUCL">Obtaining CMU Common Lisp</A>
    <LI><A HREF="#Obtaining-SBCL">Obtaining SBCL</A>
    <LI><A HREF="#Obtaining-CLISP">Obtaining CLisp</A>
    <LI><A HREF="#Obtaining-OpenMCL">Obtaining OpenMCL</A>
    <LI><A HREF="#Obtaining-Lispworks">Obtaining Lispworks</A>
  </UL>
  <LI><A HREF="#Performance">Performance comparisons</A>
</UL>
<LI><A HREF="#Obtaining">OBTAINING AND INSTALLING ACL2</A>
<UL>
  <LI><A HREF="#Shortcuts">Pre-built Binary Distributions</A>
  <UL>
    <LI><A HREF="#Shortcut-debian">Debian GNU Linux</A>
    <LI><A HREF="#Shortcut-windows">Windows Installer</A>
  </UL>
  <LI><A HREF="#Sources-Unix">Obtaining the Sources: Unix and Linux</A>
  <LI><A HREF="#Sources-Non-Unix">Obtaining the Sources: Other than Unix and Linux Systems</A>
  <LI><A HREF="#Create-Image">Creating 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 or Linux System</A>
    <LI><A HREF="#Non-Unix">Building an Executable image on Other than Unix and Linux Systems</A>
    <LI><A HREF="#Build-Particular">Building an Executable Image on Some Particular Systems</A>
    <UL>
      <LI><A HREF="#Mac-OS-X-GCL">Special Case: Building an Executable Image on Mac OS X using GCL</A>
      <LI><A HREF="#Windows-GCL">Special Case: Building an Executable Image on a Windows System using GCL</A>
      <LI><A HREF="#Windows-GCL-Jared">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 Distribution</A>
  <LI><A HREF="#Saving-Space">Saving Space</A>
</UL>
<LI><A HREF="#Using">USING ACL2</A>
<UL>
  <LI><A HREF="#Invoking">Invoking ACL2</A>
  <UL>
    <LI><A HREF="#Starting">When ACL2 Starts Up</A>
  </UL>
  <LI><A HREF="#Testing">Testing ACL2</A>
  <LI><A HREF="#Certifying">Certifying ACL2 Books</A>
  <LI><A HREF="#Documentation">Documentation</A>
</UL>
<LI><A HREF="#Miscellaneous">MISCELLANEOUS INFORMATION</A>
<UL>
  <LI><A HREF="#Problems">Problems</A>
  <LI><A HREF="#ACL2r">Reasoning about the Real Numbers</A>
  <LI><A HREF="#Addresses">Links and Mailing Lists</A>
  <LI><A HREF="#Export">Export/Re-Export Limitations</A>
  <LI><A HREF="#License-and-Copyright">License and Copyright</A>
</UL>
</UL>
<P>

<BR><HR><BR>
<H2><A NAME="Requirements">REQUIREMENTS</A></H2>

ACL2 Version 3.1 Copyright (C) 2006 University of Texas at Austin.  ACL2
is licensed under the terms of the GNU General Public License.  See <A
HREF="#License-and-Copyright">below</A> for details.
<P>
ACL2 works on Unix/Linux, Macintosh, and some Windows operating systems (at
least including Windows 98, Windows 2000, and Windows XP).  It can be built on
top of any of the following Common Lisps:

<ul>
<LI><A HREF="#Obtaining-GCL">GCL</A></B><P>
<LI><A HREF="#Obtaining-Allegro">Allegro Common Lisp</A></B><P>
<LI><A HREF="#Obtaining-CMUCL">CMU Common Lisp</A></B><P>
<LI><A HREF="#Obtaining-SBCL">SBCL</A></B><P>
<LI><A HREF="#Obtaining-CLISP">CLisp</A></B><P>
<LI><A HREF="#Obtaining-OpenMCL">OpenMCL</A></B><P>
<LI><A HREF="#Obtaining-Lispworks">Lispworks</A></B><P>
</ul>

<H3><A NAME="Obtaining-Lisp">Obtaining Common Lisp</A></H3>

ACL2 runs on top of most or all of the major Common Lisp implementations.
These are enumerated below, with links.  Often we put timing comparisons
between different lisps in the <a href="new.html">ACL2 News</a>.

<P><B><A NAME="Obtaining-GCL">Obtaining GCL</A></B><P>

Gnu Common Lisp (GCL) has probably been the most commonly-used platform for
ACL2, certainly among non-commercial Lisps.  IMPORTANT: Here we are referring
to the non-ANSI version (sometimes called the "CLtL1 version") of GCL.  It
is probably impossible to build ACL2 with ANSI GCL as of December 2005, but
recent GCL advances suggest that this may be possible soon.

<P>

<B>Debian package.</B> You do not need to fetch GCL if you <A
HREF="http://packages.qa.debian.org/a/acl2.html">download the binary Debian
package for ACL2</A>.  Thanks to Camm Maguire for maintaining this package.

<P>

GCL may be fetched from <code><a
href="http://www.gnu.org/software/gcl/">http://www.gnu.org/software/gcl/</a></code>.
If that site goes down, you may be able to find useful information from the <a
href="http://people.debian.org/~camm/gcl/">GCL Temporary Distribution Site</a>.

GCL maintainer Camm Maguire suggests the following, in order of preference
(most to least):

<ol>
<li>apt-get -q install gcl gcl-doc if running Debian
<li>Download and install the prebuilt binaries otherwise (if available for your platform)
<li>Download the latest (stable) source tarball and build yourself otherwise
<li>Download the latest (stable) cvs branch and build yourself
</ol>

As of December 2005, the latest recommended version is 2.6.7, and the latest
development version is 2.7.0.  But see <A HREF="#gcl-mac">below</A> for
suggestions for building GCL on a Macintosh running OS X.

<p>

You may obtain recent CVS versions by executing the following commands if you
have CVS installed on your system, which will retrieve the latest
development/unstable cvs sources by default.

<pre>
export CVS_RSH=ssh [or, if using csh: setenv CVS_RSH ssh]
cvs -d:ext:anoncvs@subversions.gnu.org:/cvsroot/gcl co gcl
</pre>

If you happen to know a particular version of GCL that you wish to obtain,
perhaps by following GCL mailing lists, you can replace the commands
above by commands such as the following.

<pre>
export CVS_RSH=ssh [or, if using csh: setenv CVS_RSH ssh]
cvs -d:ext:anoncvs@subversions.gnu.org:/cvsroot/gcl co -r Version_x_y_z -d gcl-x.y.z gcl
</pre>

<P>

<A NAME="gcl-mac"><B>Macintosh.</B></A> Robert Krug has provided instructions
for building GCL on Mac OS X, which we include here (very slightly modified, in
part with help from Camm Maguire) in case others find them helpful.

<pre>
The normal build process for GCL on Mac OS X assumes that
you have installed fink on your Mac.  (If you do not know
what this is, don't worry; you probably don't have it or
want it.)  Here we give instructions that have worked for
building GCL on OS X without fink.

   A. Obtain recent sources (there is a problem, e.g., with
      gcl-2.6.7).  For example, you can do the following:

      export CVSROOT=:pserver:anonymous@cvs.sv.gnu.org:/sources/gcl
      cvs -z9 -q co -d gcl-2.6.8pre -r Version_2_6_8pre gcl

      At some point you may be able to obtain GCL from
      ftp://ftp.gnu/org/, cd gnu, cd gcl, get
      gcl-2.6.8.tar.gz, tar xfz gcl-2.6.8.tar.gz)

   B. Make sure that /usr/local/bin is in your PATH; if not, run:
      PATH="$PATH:/usr/local/bin"

   C. cd &lt;gcl directory&gt;

   D. You now need to patch file h/powerpc-macosx.defs (this might not be
      necessary starting with GCL 2.6.8):

      Replace the line:
      LIBS := `echo $(LIBS) | sed -e 's/-lncurses/ /'` /sw/lib/libintl.dylib
      With:
      LIBS := `echo $(LIBS) | sed -e 's/-lncurses/ /'` /usr/local/lib/libintl.dylib

   E. Configure and start to build gcl:
      ./configure
      make

   F. Install gcl:
      sudo make install
</pre>

<P><B><A NAME="Obtaining-Allegro">Obtaining Allegro Common Lisp</A></B><P>

Allegro Common Lisp is probably the most commonly-used commercial platform for
ACL2.  You may be able to obtain a trial version from its web site,
<code><a href="http://www.franz.com/">http://www.franz.com/</a></code>.

<P><B><A NAME="Obtaining-CMUCL">Obtaining CMU Common Lisp</A></B><P>

CMU Common Lisp (sometimes called CMUCL) is a non-commercial Common Lisp
implementation, available from <code><a
href="http://www.cons.org/cmucl/">http://www.cons.org/cmucl/</a></code>.

<P><B><A NAME="Obtaining-SBCL">Obtaining SBCL</A></B><P>

SBCL (Steel Bank Common Lisp) is a non-commercial Common Lisp
implementation, available from <code><a
href="http://sbcl.sourceforge.net/">http://sbcl.sourceforge.net/</a></code>.

<P><B><A NAME="Obtaining-CLISP">Obtaining CLISP</A></B><P>

CLISP is a non-commercial Common Lisp implementation, available from <code><a
href="http://clisp.cons.org/">http://clisp.cons.org/</a></code>.

<P><B><A NAME="Obtaining-OpenMCL">Obtaining OpenMCL</A></B><P>

OpenMCL, a free Common Lisp implementation that runs on Macintosh OS X, is
available from <code><a
href="http://openmcl.clozure.com/">http://openmcl.clozure.com/</a></code>.

<P><B><A NAME="Obtaining-Lispworks">Obtaining Lispworks</A></B><P>

Lispworks is a commercial Common Lisp available from
<code><a href="http://www.lispworks.com/">http://www.lispworks.com/</a></code>.

<p>
<i>Lispworks note.</i>  We initially encountered a problem in getting ACL2 to run
under LIspworks 4.2.0.  The Lispworks folks provided a patch and suggested that
we make the following announcement.
<blockquote>
  Users with LispWorks4.2.7 should ask us at lisp-support@xanalys.com
  for the transform-if-node patch. It will be helpful if they quote
  (Lisp Support Call #11372) when doing so. Also, they must send a bug
  form generated from their LispWorks image: instructions at
  http://www.lispworks.com/support/bug-report.html.
</blockquote>

<H3><A NAME="Performance">Performance comparisons</A></H3>

Please go to the <a href="http://www.cs.utexas.edu/users/moore/acl2/">ACL2 home
page</a> and follow the link "Recent changes to this page" to see recent
performance numbers.

<BR><HR><BR>
<H2><A NAME="Obtaining">OBTAINING AND INSTALLING ACL2</A></H2>

ACL2 is more than just the executable image.  You should obtain the standard
books and a local copy of the documentation.  Start here and we will take
you through the whole process of obtaining and installing ACL2.

First, create a directory in which to store ACL2 Version 3.1.  We will
call this directory <I>dir</I>.  For example, <I>dir</I> might be
<CODE>/home/jones/acl2/v3-1</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>

Begin by clicking on one of the following links.

<UL>
<LI><A HREF="#Shortcuts">Shortcuts</A>
<LI><A HREF="#Sources-Unix">Obtaining the Sources: Unix and Linux</A>
<LI><A HREF="#Sources-Non-Unix">Obtaining the Sources: Other than Unix and Linux Systems</A>
</UL>

<p>

The sources come with a <CODE>books</CODE> subdirectory (<A
HREF="http://www.cs.utexas.edu/users/moore/acl2/v3-1/distrib/acl2-sources/books/Readme.html">here</A>
for the latest non-incremental release)
that you may find helpful in your proof development and programming with ACL2.
The following two collections of books are not included with the sources.  You
can extract them in the <CODE>books/</CODE> subdirectory of your ACL2
distribution; see the <A HREF="#Certifying">discussion below on certifying
books</A> for information on using them.

<UL>
<LI><A
HREF="http://www.cs.utexas.edu/users/moore/acl2/v3-1/distrib/acl2-sources/books/workshops.tar.gz">ACL2
Workshops books (gzipped tar file)</A>
<LI><A
HREF="http://www.cs.utexas.edu/users/moore/acl2/v3-1/distrib/acl2-sources/books/nonstd.tar.gz">
Non-standard analysis books (gzipped tar file)</A>
</UL>

<BR><HR><BR>
<H3><A NAME="Shortcuts">Pre-built Binary Distributions</A></H3>

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.

<UL>

<LI><B><A NAME="Shortcut-debian">Debian GNU Linux</A></B>

<p>

For Linux (especially Debian GNU Linux), you can <A
HREF="http://packages.qa.debian.org/a/acl2.html">download the Debian package
for Linux</A>.  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 says: 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.

<p>

<a name="howto-unpack-debs">You</a> can fetch the above package for a linux
system other than Debian and unpack it as follows.  First, connect to the
directory under which you install ACL2 versions and download the
<code>.deb</code> file there.  Then submit these commands (changing
"<code>2.9-7</code>" and "<code>i386</code>" as appropriate).
<pre>
mkdir acl2_2.9-7
cd acl2_2.9-7
mv ../acl2_2.9-7_i386.deb .
ar x acl2_2.9-7_i386.deb
tar xvfz data.tar.gz
</pre>

This will create subdirectory <code>usr/</code>.  Edit
<code>usr/bin/acl2</code> by replacing "<code>/usr</code>" with the full
pathname for "<code>usr</code>".

<p>

Alternatively, you can use the program <code>alien</code> to convert the
<code>.deb</code> file to <code>.rpm</code> format.  Of course, with the method
shown above or with <code>alien</code>, you will not have the benefit of
package maintenance.

<LI><B><A NAME="Shortcut-windows">Windows Installer</A></B>

<p>

Jared Davis has kindly been providing, typically soon after an ACL2 release, a
<A HREF="http://www.cs.utexas.edu/~jared/acl2/">Windows installer for ACL2</A>.
The download includes a Unix environment, pre-certified standard and workshop
books, and a copy of Gnu Emacs.

</UL>

<BR><HR><BR>
<H3><A NAME="Sources-Unix">Obtaining the Sources: Unix and Linux</A></H3>

For a Unix or Linux system, obtain the sources and place them in directory
<I>dir</I> as follows.

<UL>

<LI>Save <A HREF="http://www.cs.utexas.edu/users/moore/acl2/v3-1/distrib/acl2.tar.gz">
acl2.tar.gz</A> on directory <I>dir</I>.  (You can run <code>md5sum</code> and
compare with <A
HREF="http://www.cs.utexas.edu/users/moore/acl2/v3-1/distrib/acl2-tar-gz-md5sum">
acl2-tar-gz-md5sum</A> if you wish to verify the transmission.)

<LI>Execute the following four Unix commands.  (<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
acl2.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>".)

<BR><BR>
<CODE>cd <I>dir</I></CODE><BR>
<CODE>gunzip acl2.tar.gz</CODE><BR>
<CODE>tar xpvf acl2.tar</CODE><BR>
<CODE>rm acl2.tar</CODE><BR>
<BR>

</UL>

Now proceed to <A HREF="#Create-Image">Creating An Executable Image</A>.

<BR><HR><BR>
<H3><A NAME="Sources-Non-Unix">Obtaining the Sources: Other than Unix and Linux Systems</A></H3>

For a non-Unix (and non-Linux) system, obtain the sources and place them in
directory <I>dir</I>.  The easiest way to do this is to fetch
file <CODE><A
HREF="http://www.cs.utexas.edu/users/moore/acl2/v3-1/distrib/acl2.tar.gz">http://www.cs.utexas.edu/users/moore/acl2/v3-1/distrib/acl2.tar.gz</A></CODE>,
and then extract using an appropriate <CODE>tar</CODE> utility.  For example,
for Windows systems you may be able to download a utility such as
<code>djtarnt.exe</code> to be used as follows:
<pre>
djtarnt.exe -x acl2.tar.gz
</pre>
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.

<!-- The following is only for incremental releases. -->
<p>

For a non-incremental release, you may be able to fetch files individually from
directory (and subdirectories, sub-subdirectories, etc., for example as follows:
<CODE><A
HREF="http://www.cs.utexas.edu/users/moore/acl2/v3-1/distrib/">http://www.cs.utexas.edu/users/moore/acl2/v3-1/distrib/acl2-sources/</A></CODE>.
<!-- End of only for incremental releases. -->

<p>

You will find that the ACL2 distribution
contains many files, subdirectories, sub-subdirectories, etc.  We mean
for you to copy over to your local connected directory the entire
structure of files and subdirectories.  Thus, when you have completed
extracting from <CODE>acl2.tar.gz</CODE>, or fetching all files directly
is done, your local connected directory should have a subdirectory
named <CODE>acl2-sources</CODE> under which everything resides.

<P>

Now proceed to <A HREF="#Create-Image">Creating An Executable Image</A>.

<BR><HR><BR>
<H3><A NAME="Create-Image">Creating An Executable Image</A></H3>

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 <A HREF="#Summary">Summary of
Distribution</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 or Linux System</A>
<LI><A HREF="#Non-Unix">Building an Executable Image on Other than Unix and Linux Systems</A>
<LI><A HREF="#Running">Running Without Building an Executable Image</A>
</UL>

<!-- The following is only for non-incremental releases. -->

<BR><HR><BR>
<H4><A NAME="Pre-Built-Images">Short Cut:  Pre-Built ACL2 Images</A></H4>

The site <a
href="http://www.cs.utexas.edu/users/moore/acl2/v3-1/distrib/images/Readme.html">http://www.cs.utexas.edu/users/moore/acl2/v3-1/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>

Note that the Debian images may <a href="#howto-unpack-debs">work with other Linux systems as well</a>.

<p>

Now proceed to <A HREF="#Using">Using ACL2</A>.

<!-- End of only for non-incremental releases. -->

<BR><HR><BR>
<H4><A NAME="Other-Unix">Building an Executable Image on a Unix or Linux System</A></H4>

We assume you have obtained ACL2 and placed it in directory <I>dir</I>, as
described <A HREF="#Sources-Unix">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-sources</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=gcl</CODE> is used.  On our hosts, <CODE>gcl</CODE> is the name of
GNU Common Lisp, which can be obtained as explained <a
href="#Obtaining-GCL">above</a>.

<P>

This will create executable <code>saved_acl2</code> in the
<code>acl2-sources</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 in the vicinity of 17
megabytes.

<P>
This <CODE>make</CODE> works for the Common Lisps listed in <A
HREF="#Requirements">Requirements</A> above on Unix and Linux systems we have
tested.  See the file <CODE>acl2-sources/GNUmakefile</CODE> for further details.
If this <CODE>make</CODE> command does not work for you, please see the
instructions for <A HREF="#Non-Unix">non-Unix/Linux</A> systems below.

<P>
You can now skip to <A HREF="#Using">Using ACL2</A>.
<P>

<BR><HR><BR>
<H4><A NAME="Non-Unix">Building an Executable Image on Other than Unix and Linux Systems</A></H4>

Next we describe how to create a suitable binary image containing ACL2.  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">Requirements</A> above.  Filenames
below should default to the <I>dir</I><CODE>/acl2-sources</CODE>
directory, e.g., for GCL, connect to
<I>dir</I><CODE>/acl2-sources</CODE> before invoking GCL or, after
entering GCL, do <CODE>(si::chdir
"</CODE><I>dir</I><CODE>/acl2-sources/")</CODE>.

<OL>
<P><LI> Remove file <CODE>nsaved_acl2</CODE> if it exists.

<P><LI> Start up Common Lisp in the <CODE>acl2-sources</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-sources</CODE> subdirectory.

<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-sources</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>.)

<P><LI> So now exit your Common Lisp and invoke a fresh copy of it (again arranging
  to connect to your <CODE>acl2-sources</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>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>
</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>
</ul>
</PRE>

<P><LI> Move <CODE>nsaved_acl2</CODE> to <CODE>saved_acl2</CODE>.

<P><LI> For Allegro Common Lisp, Versions 5.0 and later, <CODE>nsaved_acl2.dxl</CODE> should exist;
     move it to <CODE>saved_acl2.dxl</CODE>

<P><LI> Make sure <CODE>saved_acl2</CODE> is executable.
</OL>

<BR><HR><BR>
<H4><A NAME="Build-Particular">Building an Executable Image on Some Particular Systems</A></H4>

Subtopics of this section are as follows.

    <UL>
      <LI><A HREF="#Mac-OS-X-GCL">Special Case: Building an Executable Image on Mac OS X using GCL</A>
      <LI><A HREF="#Windows-GCL">Special Case: Building an Executable Image on a Windows System using GCL</A>
      <LI><A HREF="#Windows-GCL-Jared">Instructions from Jared Davis for
      building ACL2 on Windows using mingw</A>
    </UL>

<BR><HR><BR>
<H4><A NAME="Mac-OS-X-GCL"></A>How to build/install ACL2 on GCL on Mac OS X</H4>

See <A HREF="#gcl-mac">the directions above for bulding GCL on Mac OS X</A>.  Then
follow the usual installation instructions to <A HREF="#Sources-Unix">obtain
the ACL2 sources</A> and <A HREF="#Other-Unix">build an executable image</A> on
a Unix/Linux system.

<BR><HR><BR>
<H4><A NAME="Windows-GCL">Special Case: Building an Executable Image on a Windows System using GCL</A></H4>

You may want to skip this section and instead read <A
href="#Windows-GCL-Jared">Instructions from Jared Davis for building ACL2 on
Windows using mingw</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 GCL/Windows instead of reading this section.
<!-- End of only for non-incremental releases. -->

<hr>

Otherwise here are steps to follow.

<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.1\unixport\saved_gcl.exe -dir C:/gcl/gclm/lib/gcl-2.6.1/unixport/ -libdir  C:/gcl/gclm/lib/gcl-2.6.1/ -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 non-Unix/Linux
systems</A> above, though the resulting file may be called
<code>saved_acl2.exe</code> rather than <code>saved_acl2</code>.

<!-- NOTE to developers: v3-1 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/v3-1/distrib/images/Readme.html#acl2-bat">
http://www.cs.utexas.edu/users/moore/acl2/v3-1/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/Linux.

<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><BR>
<H4><A NAME="Windows-GCL-Jared">Instructions from Jared Davis for building ACL2 on
Windows using mingw</A></H4>

We thank Jared Davis for providing the following instructions for Version_2.8,
which we include verbatim and expect apply to future versions.

<pre>
	      Building ACL2 on Windows from Scratch
   _____________________________________________________________

   Note: The disk space requirements are large.  Not including
   emacs, I had about 275 MB taken up by msys/mingw32/gcl/acl2
   during the build process.  You can probably use much less
   space by removing files after you use them, but I didn't
   bother to do that.

   Here are the steps I took:

   Downloaded emacs 21.3 full distribution and installed
   Downloaded msys 1.10.10, installed to c:\acl2
   Downloaded mingw 3.1.0-1, installed to c:\acl2\mingw
   Downloaded gcl 2.5.3, extracted to c:\acl2\mingw
   Downloaded acl2 2.8, extracted to c:\acl2\sources



   Compiling gcl:

     in msys:

       cd /acl2/ming2/gcl-2.5.3
       ./configure
       make
       make install



   Compiling acl2:

     copy "etags.exe" to /mingw/bin.  you can find this program
     in your emacs folder, under "bin".

     in msys:

       cd /sources
       make



   Certifying ACL2 books:
   This took 111 minutes on my Athlon 2500+

     in msys:

       cd /sources

       mv nsaved_acl2.gcl.exe saved_acl2.exe

       vim books/Makefile-generic, remove "nice" from this line:
	   ACL2=time nice ../../saved_acl2

       make certify-books ACL2=/sources/saved_acl2.exe

</pre>

<BR><HR><BR>
<H3><A NAME="Running">Running Without Building an Executable Image</A></H3>

The most convenient way to use ACL2 is first to install an executable image as
described above for <A HREF="#Other-Unix">Unix/Linux</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">Unix/Linux</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-sources</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-sources</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">Using ACL2</A>.

<BR><HR><BR>
<H3><A NAME="Summary">Summary of Distribution</A></H3>

The distribution includes the following.  A list of all files in
<CODE>acl2-sources</CODE> may be found in the file <CODE>all-files.txt</CODE>
in that directory.
<PRE>
Readme.html; This file
acl2-sources/
  LICENSE  ; GNU General Public License
  GNUmakefile ; For Unix/Linux make.
  TAGS     ; Handy for looking at source files with emacs
  *.lisp   ; ACL2 source files
  all-files.txt    ; List of all files in this directory and subdirectories
  books/   ; Examples, potentially useful in others' proofs.  See books/Readme.html.
  doc/     ; ACL2 documentation in various formats
  emacs/   ; Miscellaneous emacs and file utilities, especially emacs-acl2.el
  init.lisp; Useful for building the system
  interface/
    emacs/ ; Support for ACL2 "proof trees".  See interface/emacs/README.doc.
    infix/ ; ACL2 infix printer by Mike Smith.  See interface/infix/README.
  saved/   ; Empty directory for backing up copies during make; not important
acl2.tar.gz; gzip'd tar file containing all of acl2-sources/ (see below)
images/    ; Some gzip'd tar'd executables; see images/Readme.html
split/     ; The result of splitting up acl2.tar.gz; see split/Readme.html
</PRE>

<P>
The entire acl2.tar.gz is a little more than 6 megabytes, which expands out to nearly
30 megabytes.  Additional space is required to build an image, perhaps 30 to 120
megabytes depending on the Lisp, and to <A
HREF="#Certifying">certify books</A>.

<BR><HR><BR>
<H3><A NAME="Saving-Space">Saving Space</A></H3>

For those really pressed for space, we note that it is not necessary
to fetch the whole <CODE>acl2.tar.gz</CODE> file in order to build
acl2.  That file includes more than just the ACL2 sources proper.  It
suffices, for building ACL2, via the instructions above, to fetch only
the <CODE>acl2-sources/*.lisp</CODE> files, which take up `only' about
5 megabytes, together with the file
<CODE>acl2-sources/GNUmakefile</CODE>.

<BR><HR><BR>
<H2><A NAME="Using">USING ACL2</A></H2>

Here we begin with a discussion of how to <A HREF="#Invoking">invoke ACL2</A>
interactively.  We then discuss <A HREF="#Testing">testing</A> as well as the
<A HREF="#Certifying">certification</A> of ACL2 <em>books</em> that come with
the distribution.  We conclude with a discussion of the <A
HREF="#Documentation">documentation</A>.

<BR><HR><BR>
<H3><A NAME="Invoking">Invoking ACL2</A></H3>

At this point, <I>dir</I> has a subdirectory called <code>acl2-sources</code>.
The sources and perhaps an executable image are located on that subdirectory.
However, if you have not saved an image but instead use the directions above
for <A HREF="#Running">Running Without Building an Executable Image</A>, skip
to <A HREF="#Starting">When ACL2 Starts Up</A> below.

<P>

The executable image is called <code>acl2-sources/saved_acl2</code>.  You can
invoke ACL2 by running that image, e.g.,

<BR><BR>
<CODE>mycomputer% </CODE><I>dir</I><CODE>/acl2-sources/saved_acl2</CODE>
<BR><BR>

If on a Unix/Linux system, then to make it easy to invoke ACL2 by typing a
short command, e.g.,

<BR><BR>
<CODE>mycomputer% acl2</CODE>
<BR><BR>

you may want to install an executable file on your path, e.g.,
<code>/usr/local/bin/acl2</code>, containing the following two lines:

<BR><BR>
<CODE>#!/bin/csh -f</CODE><BR>
<I>dir</I><CODE>/acl2-sources/saved_acl2</CODE><BR>
<BR><BR>

Note: A carriage return in the file after the last line above is important!
<P>

<BR>
<H4><A NAME="Starting">When ACL2 Starts Up</A></H4>

When you invoke ACL2, you should see the host Common Lisp 
print a header concerning the ACL2 version, license and copyright.
<P>
Some hosts then automatically enter the ACL2 ``command loop,'' an ACL2
read-eval-print loop with the prompt:
<PRE>
ACL2 !>
</PRE>
Other hosts will leave you in Common Lisp's read-eval-print loop.
If yours is one of the latter, evaluate the Common Lisp expression
<CODE>(ACL2::LP)</CODE> or simply <CODE>(LP)</CODE> if the current
package is <CODE>"ACL2"</CODE>.
<P>
Once in the ACL2 command loop, you can type an ACL2 term, typically
followed by ``return'' or ``enter,'' and ACL2 will evaluate the term,
print its value, and prompt you for another one.  Below are three
simple interactions:
<PRE>
ACL2 !>t
T
ACL2 !>'abc
ABC
ACL2 !>(+ 2 2)
4
</PRE>
<P>

To get out of the ACL2 command loop, type the <code>:q</code> command.
This returns you to the host Common Lisp.  We sometimes call this
``raw Lisp.''  You may re-enter the command loop with
<code>(LP)</code> as above.

<P>
Note that when you are in raw Lisp you can overwrite or destroy ACL2
by executing inappropriate Common Lisp expressions.  <B>All bets are
off once you've exited our loop.</B> That said, many users do it.
For example, you might exit our loop, activate some debugging or trace
features in raw Lisp, and then reenter our loop.  While developing
proofs or tracking down problems, this is reasonable behavior.

<P>
Now you are ready to <A HREF="#Testing">test</A> your image.

<BR><HR><BR>
<H3><A NAME="Testing">Testing ACL2</A></H3>

<P>
An easy way to test the theorem prover is to
type the following term to the ACL2 command loop:
<PRE>
:mini-proveall
</PRE>
This will cause a moderately long sequence of commands to be processed, each of
which is first printed out as though you had typed it.  Each will print some
text, generally a proof of some conjecture.  None should fail.

<P>
A more elaborate test is to <A NAME="#Certifying">certify the ``books''</A>
that come with the distribution, which is a good idea anyhow; this is our next
topic.  On a Unix/Linux system, you can also certify just a small but useful
subset of the books in a few minutes by executing, in directory
<i>dir</i>/<code>acl2-sources</code>:
<pre>
make certify-books-short
</pre>

<BR><HR><BR>
<H3><A NAME="Certifying">Certifying ACL2 Books</A></H3>

<!-- NOTE to developers: v3-1 below indicates a normal release, which is OK. -->
<!-- Do not edit that for incremental releases. -->

The ``books'' that come with the distribution have been contributed mainly by
users and are on the subdirectory <CODE>acl2-sources/books</CODE>.  See <A
HREF="http://www.cs.utexas.edu/users/moore/acl2/v3-1/distrib/acl2-sources/books/Readme.html"><CODE>acl2-sources/books/Readme.html</CODE></A>
for information.  The general topic of books is discussed thoroughly in the
ACL2 documentation; see the <CODE>BOOKS</CODE> node in the documentation tree.

<P>
Books should be ``certified'' before they are used.  We do not distribute
certificates with our books, mainly because certification produces compiled
code specific to the host.  You should certify the books locally as a test of
your ACL2 image.

<P>
It is easy to re-certify all the distributed books in Unix/Linux.  We recommend you
do this.  If you have entered ACL2, exit to the operating system, e.g., by
control-d in many systems.

<P>
While connected to <I>dir</I><CODE>/acl2-sources</CODE>, execute
<PRE>
make certify-books
</PRE>

This will generate minimal output to the screen and will probably take an hour
or two.  Failure is indicated by the presence of <code>**CERTIFICATION FAILED**</code> in the log.

<P>

To remove the files thus created, invoke:
<PRE>
make clean-books
</PRE>

<P>
The <CODE>certify-books</CODE> target does not cause workshop books to be
certified.  If you want to certify those books as well, you will first need to
<a
href="http://www.cs.utexas.edu/users/moore/acl2/v3-1/distrib/acl2-sources/books/workshops.tar.gz">download
the gzipped tar file</a> to the <CODE>books/</CODE> directory, and then gunzip
and extract it.  You can certify all the books, including books for the
workshops (including those from the 1999 workshop as described in the
(hardbound) book <A
HREF="http://www.cs.utexas.edu/users/moore/publications/acl2-books/acs/index.html"><EM>Computer-Aided
Reasoning: ACL2 Case Studies</EM></A>), using the command:

<PRE>
make regression
</PRE>

<P>
By default, certification uses the image
<I>dir</I><CODE>/acl2-sources/saved_acl2</CODE>.  You may specify any ACL2
image, as long as it is either a command on your Unix/Linux path or an absolute file
name, for example as follows.

<PRE>
make certify-books ACL2=my-acl2

make regression ACL2=/u/smith/projects/acl2/saved_acl2
</PRE>

<P>
We apologize to non-Unix/Linux users: we do not provide non-Unix/Linux
instructions for recertifying the distributed books.  The
certification methods provided by the authors of the books vary
greatly and we codified them in the Unix/Linux makefile (GNUmakefile) used above.  Most
subdirectories of <CODE>acl2-sources/books</CODE> contain either a
<CODE>README</CODE> file or a <CODE>certify.lsp</CODE> file.  Users
who wish to certify one of these books and who cannot figure out (from
these scant clues) what to type to ACL2 should not hesitate to contact
the authors.

<P>
Next proceed to the section on <A HREF="#Documentation">Documentation</A>.

<BR><HR><BR>
<H3><A NAME="Documentation">Documentation</A></H3>

<P>
ACL2's documentation is a hypertext document that, if printed in book
form, is about 1100 pages or more than 2 megabytes of text.  Its
hypertext character makes it far more pleasing to read with an
interactive browser.  The documentation is available in four formats:
HTML, Texinfo, Postscript and ACL2 documentation strings.  All of this
material is copyrighted by the University of Texas at Austin and is
derived under the GNU General Public License from material copyrighted
by Computational Logic, Inc.

<P>
Two Web-based guided tours of ACL2 are available from the home page
noted below.  If you are already familiar with Nqthm, you might find
it useful to look at the documentation node
<CODE>NQTHM-TO-ACL2</CODE>.  Another useful documentation topic for
beginning ACL2 users is the node <CODE>TUTORIAL</CODE>.

<P>
<B>HTML</B>
<P>
The ACL2 Home Page is
<P>
<CODE><A HREF="http://www.cs.utexas.edu/users/moore/acl2/index.html">http://www.cs.utexas.edu/users/moore/acl2/index.html</A></CODE>
<P>

The home page provides a selected bibliography, a search button (near the top
of the page), guided tours of the system, and the complete hypertext
documentation tree.

<P>
Once you have installed ACL2, the HTML form of the documentation is
available locally as
<I>dir</I><CODE>/acl2-sources/doc/HTML/acl2-doc.html</CODE>.
<BR><BR>
We urge you to browse your local copy of the documentation rather than
our Web copy, simply to reduce Web traffic and the demand on our
server.  (Macintosh users using MacOS 9 and earlier may, however, find
filenames being truncated and hence will want to avoid the local
documentation.)

<P><B>Emacs Info</B><P>

This is a very convenient format for accessing the ACL2 documentation from
within Emacs.  In Emacs, invoke
<PRE>
meta-x info
</PRE>
and then, if you are unfamiliar with Info, type
<PRE>
control-h m
</PRE>
to see a list of commands available.  In particular, type
<BR><BR>
<CODE>g (</CODE><I>dir</I><CODE>/acl2-sources/doc/EMACS/acl2-doc-emacs.info)TOP</CODE><BR><BR>
to enter the ACL2 documentation.  Alternatively, your system administrator can
add an ACL2 node to the top-level Info menu.  The appropriate entry might read:
<BR><BR>
<CODE>* ACL2 i.j: (</CODE><I>dir</I><CODE>/acl2-sources/doc/EMACS/acl2-doc-emacs).</CODE><BR>
&nbsp &nbsp &nbsp &nbsp &nbsp <CODE>Documentation for ACL2 version i.j.</CODE>
<BR><BR>

Note: The Emacs Info and Postscript versions of our documentation were
created using the file <CODE>acl2-sources/doc/texinfo.tex</CODE> which
is copyrighted by the Free Software Foundation, Inc.  (See that file
for copyright and license information.)

<P>

Users new to emacs may find it helpful to load into emacs the file
</CODE><I>dir</I><CODE>/acl2-sources/emacs/emacs-acl2.el</CODE>.  Utilities
offered by this file are documented near the top of the file.

<P><B>Postscript</B><P>

The Postscript version of the documentation is not included in our normal
distribution because it is so much less useful than the hyper-text versions.
But a <A
HREF="http://www.cs.utexas.edu/users/moore/publications/acl2-book.ps.gz">gzipped
Postscript (1.2 MB)</A> version is available.  It prints as a book of about 1000
pages and contains a Table of Contents and an index to all documented topics.

<P><B>ACL2 Documentation Strings</B><P>

The ACL2 system has facilities for browsing the documentation.  When you are in
the ACL2 command loop, you may query the documentation on a given topic by
typing the command
<BR><BR>
<CODE>:doc </CODE><I>topic</I>
<BR><BR>
where <I>topic</I> is the Lisp symbol naming the topic you want to
learn about.  To learn more about the on-line documentation, type
<CODE>:help</CODE> and then return.

<P>
Note, however, that you may find it more convenient to view the documentation
in a web browser (starting at <CODE>doc/HTML/acl2-doc.html</CODE>) or in Emacs
info (starting at <CODE>doc/EMACS/acl2-doc-emacs.info</CODE>).

<P>
This completes the installation of ACL2 Version 3.1.  You may wish to
return to the <A HREF="#top">Table of Contents</A>.

<BR><HR><BR>
<H2><A NAME="Miscellaneous">MISCELLANEOUS INFORMATION</A></H2>

Please <A HREF="mailto:kaufmann@cs.utexas.edu,moore@cs.utexas.edu">let us know</A> if there is
other information that you would find of use in this guide.

<BR><HR><BR>
<H3><A NAME="Problems">Problems</A></H3>

If you are having problems using the <CODE>make</CODE> utility, be sure that
you are using GNU <CODE>make</CODE>.

<BR><HR><BR>
<H3><A NAME="ACL2r">Reasoning about the Real Numbers</H3>

ACL2 supports rational numbers but not real numbers.  However, starting
with Version  2.5, a variant of ACL2 called "ACL2(r)" supports the real
numbers by way of non-standard analysis.  ACL2(r) was conceived and
first implemented by Ruben Gamboa in his Ph.D. dissertation work,
supervised by Bob Boyer with active participation by Matt Kaufmann.
See the documentation topic <CODE>REAL</CODE> for information about this
extension and how to build it, and a warning about its experimental nature.

<P>

if you care to use ACL2(r), first
<A
HREF="http://www.cs.utexas.edu/users/moore/acl2/v3-1/distrib/acl2-sources/books/nonstd.tar.gz">
download the non-standard analysis books (gzipped tar file)</A> to the
<code>books/</code> subdirectory of your copy of the ACL2 distribution, say,
<I>dir</I>/acl2-sources/books/<code>.  Then run:
<pre>
tar xvfz nonstd.tar.gz
</pre>
<p>
Next build an executable image and certify books.  First, connect to your
<I>dir</I><code>/acl2-sources/</code> directory and execute<BR><BR> <CODE>cd
acl2-sources</CODE><BR> <CODE>make large-acl2r 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=gcl</CODE> is used.  On our hosts, <CODE>gcl</CODE> is the name of
GNU Common Lisp, which can be obtained as explained <a
href="#Obtaining-GCL">above</a>.
<P>
This will create executable <code>saved_acl2r</code> in the
<I>dir</I><code>/acl2-sources</code> directory (notice the trailing
~code>r</code> in the executable filename).

<P>

Finally, to certify books under directory
<I>dir</I>/acl2-sources/books/nonstd/<code> with ACL2(r), stand in the
</CODE><I>dir</I><CODE>/acl2-sources/</CODE> directory and execute the
following command.
<pre>
make regression-nonstd ACL2=<I>dir</I>/acl2-sources/saved_acl2r
</pre>

<BR><HR><BR>
<H3><A NAME="Addresses">Links and Mailing Lists</A></H3>

There are two mailing lists for ACL2 users.  You can post messages to these
lists only if you are a member.
<ul>
<li><CODE><A
HREF="mailto:acl2-help@lists.cc.utexas.edu">acl2-help@lists.cc.utexas.edu</A></CODE><br>
ACL2 help list, for questions about using ACL2.
<li><CODE><A
HREF="mailto:acl2@lists.cc.utexas.edu">acl2@lists.cc.utexas.edu</A></CODE><br>
General ACL2 list for users and others interested in ACL2.
</ul>

You may subscribe to or unsubscribe from these
lists at
<CODE><A HREF="http://www.cs.utexas.edu/users/moore/acl2/admin/forms/email.html">
http://www.cs.utexas.edu/users/moore/acl2/admin/forms/email.html</A></CODE>.
You should receive a confirmation of the request a short time later, 
along with instructions for use (e.g., how to retrieve 
archive messages). If you need further assistance, please 
send a message to
<CODE><A HREF="mailto:acl2-request@lists.cc.utexas.edu">
acl2-request@lists.cc.utexas.edu</A></CODE>.
<P>
You can retrieve archive files or search the archives using a web interface
from 
<CODE><A HREF="http://www.cs.utexas.edu/users/moore/acl2/admin/forms/archive.html">
http://www.cs.utexas.edu/users/moore/acl2/admin/forms/archive.html</A></CODE>.
<P>
You can search the ACL2 documentation, workshops, and publications online from
<CODE><A HREF="http://www.cs.utexas.edu/users/moore/acl2/admin/forms/search.html">
http://www.cs.utexas.edu/users/moore/acl2/admin/forms/search.html</A></CODE>.
<P>
Finally, please report bugs in ACL2 to
<CODE><A HREF="mailto:acl2-bugs@lists.cc.utexas.edu">acl2-bugs@lists.cc.utexas.edu</A></CODE>.

<BR><HR><BR>
<H3><A NAME="Export">Export/Re-Export Limitations</A></H3>

ACL2 may be exported to any countries except those subject to embargoes under
various laws administered by the Office of Foreign Assets Control ("OFAC") of
the U. S. Department of the Treasury.

<BR><HR><BR>
<H3><A NAME="License-and-Copyright">License and Copyright</A></H3>

ACL2 Version 3.1 -- A Computational Logic for Applicative Common Lisp<BR>
Copyright (C) 2006  University of Texas at Austin
<P>
This version of ACL2 is a descendent of ACL2 Version 1.9, Copyright
(C) 1997 Computational Logic, Inc.
<P>
This program is free software; you can redistribute it and/or modify
it under the terms of the <A
HREF="LICENSE">GNU General Public License</A> as published by
the Free Software Foundation; either version 2 of the License, or
(at your option) any later version.
<P>
This program is distributed in the hope that it will be useful,
but WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
GNU General Public License for more details.
<P>
You should have received a copy of the GNU General Public License
along with this program; if not, write to the Free Software
Foundation, Inc., 675 Mass Ave, Cambridge, MA 02139, USA.
<P>
Matt Kaufmann (Kaufmann@cs.utexas.edu)<BR>
J Strother Moore (Moore@cs.utexas.edu)<BR>
<BR>
Department of Computer Sciences<BR>
University of Texas at Austin<BR>
Austin, TX 78712-1188 U.S.A.<BR>
<BR>

</BODY>
</HTML>