← Back to branch summary

~ubuntu-branches/ubuntu/wily/acl2/wily

« back to all changes in this revision

Viewing changes to installation/obtaining-and-installing.html

  • Committer: Package Import Robot
  • Author(s): Camm Maguire
  • Date: 2015-01-16 10:35:45 UTC
  • mfrom: (3.3.26 sid)
  • Revision ID: package-import@ubuntu.com-20150116103545-prehe9thgo79o8w8
Tags: 7.0-1
New upstream release

Show diffs side-by-side

added added

removed removed

Lines of Context:
installation/obtaining-and-installing.html
1
1
<HTML>
2
 
<HEAD><TITLE>ACL2 Version 6.5 Installation Guide: Obtaining and Installing ACL2</TITLE></HEAD>
 
2
<HEAD><TITLE>ACL2 Version 7.0 Installation Guide: Obtaining and
 
3
    Installing <a href="http://www.cs.utexas.edu/users/moore/acl2/v7-0/index.html">ACL2</TITLE></HEAD>
3
4
 
4
 
<BODY TEXT="#000000">
5
 
<BODY BGCOLOR="#FFFFFF">
 
5
<BODY TEXT="#000000" BGCOLOR="#FFFFFF" STYLE="font-family:'Verdana'">
6
6
 
7
7
<H1>Obtaining and Installing ACL2</A></H1>
8
8
 
37
37
    </UL>
38
38
  </UL>
39
39
  <LI><A HREF="#Running">Running Without Building an Executable Image</A>
40
 
  <LI><A HREF="#Summary">Summary of Distribution</A>
 
40
  <LI><A HREF="#Summary">Summary of ACL2 System Distribution</A>
41
41
  <LI><A HREF="#Bleeding-edge">Bleeding-edge Distributions via SVN</A>
42
42
</UL>
43
43
 
44
44
<p><hr size=4 noshade><p>
45
45
 
46
46
ACL2 is more than just the executable image.  In particular, it comes
47
 
with a user's manual, but you will almost certainly want to obtain the
48
 
distributed books.  Start here and we will take you through the whole
49
 
process of obtaining and installing ACL2.
 
47
with
 
48
a <a href="http://www.cs.utexas.edu/users/moore/acl2/v7-0/index.html#User's-Manual">user's
 
49
manual</a>, and the system is distributed with libraries developed by
 
50
the ACL2 community, the
 
51
<i><a href="http://www.cs.utexas.edu/users/moore/acl2/current/combined-manual/?topic=ACL2____COMMUNITY-BOOKS">community
 
52
  books</a></i>.  Start here and we will take you through the whole
 
53
  process of obtaining and installing ACL2.
50
54
 
51
55
<p>
52
56
 
53
 
First, create a directory in which to store ACL2 Version 6.5.  We will
 
57
First, create a directory under which to store ACL2 Version 7.0.  We will
54
58
call this directory <I>dir</I>.  For example, <I>dir</I> might be
55
 
<CODE>/home/jones/acl2/v6-5</CODE>.
 
59
<CODE>/home/jones/acl2/</CODE>.
56
60
 
57
61
<H3>NOTE: If you intend to obtain an incremental release (e.g. 2.9.4 as opposed
58
62
to 2.9), please see the <a href="../new.html">ACL2 News</a> for instructions.
59
63
Otherwise, continue reading here.</H3>
60
64
 
61
 
<p>
62
 
 
63
 
A collection of <em>books</em> (ACL2 input files typically including
64
 
definitions and theorems) has been developed over the years for use
65
 
with ACL2, called the "community books".  It is very useful to
66
 
obtain these books, which are distributed via SVN from the Google
67
 
Code <a href="https://code.google.com/p/acl2-books/">acl2-books
68
 
project website</a> or, as gzipped tarfiles, from
69
 
<code><a href="http://acl2.org">http://acl2.org</a></code>.
70
 
Directions are included below.
71
 
 
72
65
<BR><HR noshade size=8><BR>
73
66
<H2><A NAME="Shortcuts">Pre-built Binary Distributions</A></H2>
74
67
 
79
72
<p>
80
73
 
81
74
WARNING: Some of these packages might be for old version of ACL2.  We
82
 
recommend that you use the latest version of ACL2 (Version 6.5).
 
75
recommend that you use the latest version of ACL2 (Version 7.0).
83
76
 
84
77
<UL>
85
78
 
106
99
the certificate (<code>.cert</code>) files are automatically
107
100
fixed, according to the full pathname of your <code>books/</code> directory.)
108
101
Also see
109
 
the <a href="http://www.cs.utexas.edu/users/moore/acl2/v6-5/combined-manual/index.html?topic=ACL2____ACL2-SEDAN">ACL2
 
102
the <a href="http://www.cs.utexas.edu/users/moore/acl2/v7-0/combined-manual/index.html?topic=ACL2____ACL2-SEDAN">ACL2
110
103
documentation topic on the ACL2 Sedan</a>.
111
104
 
112
105
 
120
113
by <a href="#Build-Particular">the section on Building an Executable
121
114
Image on Some Particular Systems</a> and
122
115
the Shortcut using the ACL2 Sedan, <a href="#Shortcut-acl2s">above</a>.
123
 
See also <a href="../distrib/windows/">information about ACL2 on
 
116
See also <a href="../../distrib/windows/">information about ACL2 on
124
117
Windows</a>.
125
118
 
126
119
<LI><B><A NAME="Shortcut-MacPorts">MacPorts for Mac OS X</A></B>
144
137
they wish as well, e.g. emacs, infix, etc."  Alternatively, Debian GNU
145
138
Linux users may wish
146
139
to <A HREF="http://packages.qa.debian.org/a/acl2.html">download the
147
 
Debian package for Linux</A>.  Or, see following annotated log,
148
 
provided by Camm Maguire, to see another way to proceed.
149
 
 
150
 
<pre>
151
 
     camm@localhost:~$ cd /tmp
152
 
     camm@localhost:/tmp$ mkdir a
153
 
     camm@localhost:/tmp$ cd a
154
 
     camm@localhost:/tmp/a$ wget ftp://ftp.debian.org/debian/pool/main/a/acl2/acl2*5.0*_{i386,all}*b
155
 
 
156
 
     ;;; or ftp, use browser, etc.  I.e. download the .deb files.  Replace
157
 
     ;;; i386 above with amd64 if the target is a 64bit Ubuntu machine.
158
 
     ;;; Other target names should be self explanatory.  The 'all'
159
 
     ;;; designation refers to binary independent data. 
160
 
 
161
 
     camm@localhost:/tmp/a$ ls
162
 
     acl2_5.0-1_i386.deb           acl2-books-certs_5.0-1_all.deb   acl2-doc_5.0-1_all.deb    acl2-infix_5.0-1_i386.deb        acl2-source_5.0-1_all.deb
163
 
     acl2-books_5.0-1_i386.deb  acl2-books-source_5.0-1_all.deb  acl2-emacs_5.0-1_all.deb  acl2-infix-source_5.0-1_all.deb
164
 
     camm@localhost:/tmp/a$ for i in *b; do ar x $i; tar zxf data.tar.gz; done
165
 
 
166
 
     ;;; unpack files in current directory
167
 
 
168
 
     camm@localhost:/tmp/a$ sed -e 's,usr,tmp/a/usr,g' usr/bin/acl2 &gt;tmp && chmod 755 tmp && mv tmp usr/bin/acl2
169
 
 
170
 
     ;;; Edit shell script wrapper to refer to the local path
171
 
 
172
 
     camm@localhost:/tmp/a$ usr/bin/acl2
173
 
     GCL (GNU Common Lisp)  2.6.7 CLtL1    Aug 22 2012 15:25:31
174
 
     Source License: LGPL(gcl,gmp), GPL(unexec,bfd,xgcl)
175
 
     Binary License:  GPL due to GPL'ed components: (XGCL READLINE UNEXEC)
176
 
     Modifications of this banner must retain notice of a compatible license
177
 
     Dedicated to the memory of W. Schelter
178
 
 
179
 
     Use (help) to get some basic information on how to use GCL.
180
 
     Temporary directory for compiler files set to /tmp/
181
 
 
182
 
      ACL2 Version 5.0 built August 25, 2012  11:53:08.
183
 
      Copyright (C) 2012  University of Texas at Austin
184
 
      ACL2 comes with ABSOLUTELY NO WARRANTY.  This is free software and you
185
 
      are welcome to redistribute it under certain conditions.  For details,
186
 
      see the GNU General Public License.
187
 
 
188
 
      Initialized with (INITIALIZE-ACL2 'INCLUDE-BOOK *ACL2-PASS-2-FILES*).
189
 
      See the documentation topic note-5-0 for recent changes.
190
 
      Note: We have modified the prompt in some underlying Lisps to further
191
 
      distinguish it from the ACL2 prompt.
192
 
 
193
 
     ACL2 Version 5.0.  Level 1.  Cbd "/tmp/a/".
194
 
     System books directory "/tmp/a/usr/share/acl2-5.0/books/".
195
 
     Type :help for help.
196
 
     Type (good-bye) to quit completely out of ACL2.
197
 
 
198
 
     ACL2 !&gt;
199
 
</pre>
 
140
ACL2 Debian package for Linux</A>.  An alternate location you might
 
141
want to check
 
142
is <code><a href="http://backports.debian.org">backports.debian.org</a></code>.
200
143
 
201
144
</UL>
202
145
 
203
146
<BR><HR noshade size=8><BR>
204
147
<H2><A NAME="Sources">Obtaining the Sources and Community Books</A></H2>
205
148
 
206
 
Obtain the sources and place them in directory
207
 
<I>dir</I> as follows.
 
149
Here is how to obtain the sources and community books and place them
 
150
in a directory, <I>dir</I>.
208
151
 
209
152
<p>
210
153
 
218
161
 
219
162
<UL>
220
163
 
221
 
<LI>Save <A HREF="http://www.cs.utexas.edu/users/moore/acl2/v6-5/distrib/acl2.tar.gz">
222
 
    acl2.tar.gz</A> on directory <I>dir</I>.  (You can
223
 
    run <code>md5sum</code> and compare
224
 
    with <A HREF="http://www.cs.utexas.edu/users/moore/acl2/v6-5/distrib/acl2-tar-gz-md5sum">
225
 
    acl2-tar-gz-md5sum</A> if you wish to verify the transmission.)
 
164
<LI>Save <A HREF="https://github.com/acl2/acl2/archive/7.0.tar.gz">
 
165
    7.0.tar.gz</A> on directory <I>dir</I>.
226
166
  </LI>
227
167
<BR>
228
168
 
229
 
<LI>Execute the following four Unix commands.  (<b>Note</b>:
230
 
Gnu tar is preferred, as there have been some problems with long file
231
 
names when using tar provided by SunOS.  You may want to use the -i
232
 
option, "<code>tar xpvfi acl2.tar</code>", if you have problems with
233
 
other than Gnu tar.  You can see if you have Gnu tar by running
234
 
"<code>tar -v</code>".)
 
169
<LI>Execute the following four Unix commands to obtain the ACL2 system
 
170
and community books.  (<b>Note</b>: Gnu tar is preferred, as there
 
171
have been some problems with long file names when using tar provided
 
172
by SunOS.  You may want to use the -i option, "<code>tar xpvfi
 
173
7.0.tar</code>", if you have problems with other than Gnu tar.  You
 
174
can see if you have Gnu tar by running "<code>tar -v</code>".)  The
 
175
resulting tarball will consist of approximately 60 MB and its
 
176
extracted directory will consist of approximately 270 MB.  Additional
 
177
space is required to build an executable image, perhaps 85 to 260 MB
 
178
depending on the platform (including the host Lisp); and more will be
 
179
required to <A HREF="using.html#Certifying">certify books</A>.
 
180
 
235
181
 
236
182
<BR><BR>
237
183
<CODE>cd <I>dir</I></CODE><BR>
238
 
<CODE>tar xfz acl2.tar.gz</CODE><BR>
239
 
<CODE>rm acl2.tar.gz</CODE><BR>
240
 
<CODE>cd acl2-sources</CODE><BR>
 
184
<CODE>tar xfz 7.0.tar.gz</CODE><BR>
 
185
<CODE>rm 7.0.tar.gz</CODE><BR>
 
186
<CODE>cd acl2-7.0</CODE><BR>
241
187
<BR>
242
188
</LI>
243
189
 
244
 
<LI><A NAME="Obtaining-books"</A>We strongly suggest that you now
245
 
       install the community books,
246
 
       using <b><font color="red">one</font></b> of the following
247
 
       methods, while still connected to the new <acl2-sources/>
248
 
       directory.
249
 
       <BR><BR>
250
 
 
251
 
<UL>
252
 
 
253
 
  <li><b>Easy download.</b>  Fetch a gzipped tarfile of the community
254
 
    books
255
 
    from <code><a href="http://acl2.org">http://acl2.org</a></code>,
256
 
    and then extract as follows to create a <code>books/</code>
257
 
    subdirectory:<BR>
258
 
 
259
 
    <code>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;tar xfz books-6.5.tar.gz</code>
260
 
  </li>
261
 
 
262
 
  <li><b><font color="red">OR</font></b>, obtain a read-only copy
263
 
    using SVN to be placed in a new subdirectory, <code>books/</code>:<br>
264
 
 
265
 
      <code>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;svn checkout http://acl2-books.googlecode.com/svn/branches/6.5 books</code>
266
 
  </li>
267
 
        
268
 
  <li><b><font color="red">OR</font></b>, for read-write access,
269
 
    become a member of the acl2-books project by contacting one of the
270
 
    project administrators
271
 
    (see <a href="https://code.google.com/p/acl2-books/">the
272
 
    acl2-books project page</a>). Then:<br>
 
190
</UL>
 
191
 
 
192
<p>
 
193
 
 
194
<b>Note</b>: Alternatively, for read-write access, become a member of
 
195
the acl2-books project
 
196
by <a href="https://github.com/acl2/acl2#contributors-wanted">contacting
 
197
one of the project administrators as described on acl2-books project
 
198
page</a>.
273
199
          
274
 
    <code>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;svn checkout https://acl2-books.googlecode.com/svn/branches/6.5 books --username &lt;name&gt;</code>
275
 
  </li>
276
 
  <BR>
277
 
 
278
 
</UL>
279
 
 
280
 
<B><font color="red">NOTE</font></B>:  The second and third methods
281
 
provide all of the community books, but the first omits the
282
 
<code>workshops/</code> subdirectories of these <code>books/</code>,
283
 
which contains books contributed in support of papers presented at
284
 
ACL2 workshops.  You can fetch the gzipped tarball for
285
 
the <code>workshops/</code> directory
286
 
from <code><a href="http://acl2.org">http://acl2.org</a></code>.  Then
287
 
put that gzipped tarfile in the <CODE>acl2-sources/books/</CODE>
288
 
directory, connect to that directory, and extract to create
289
 
a <CODE>workshops/</CODE> subdirectory:<BR>
290
 
 
291
 
<CODE>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;tar xfz workshops-6.5.tar.gz</CODE><BR>
292
 
 
293
 
</UL>
294
 
 
295
200
<BR><HR noshade size=8><BR>
296
201
<H2><A NAME="Create-Image">Creating or Obtaining an Executable Image</A></H2>
297
202
 
300
205
<!-- The following is only for non-incremental releases. -->
301
206
However, you may
302
207
be able to <A HREF="#Pre-Built-Images">take a short cut by downloading an
303
 
ACL2 image</A>, in which case you can skip ahead to <A HREF="#Summary">Summary of
304
 
Distribution</A>.  Otherwise you should click on one of the links just below.
 
208
ACL2 image</A>, in which case you can skip ahead to the page on
 
209
<A HREF="using.html">Using ACL2</A>.  Otherwise you should click on
 
210
one of the links just below.
305
211
<!-- End of only for non-incremental releases. -->
306
212
Choose the last option if you are using a Common Lisp on which you cannot save
307
213
an image (e.g., a trial version of Allegro Common Lisp).
324
230
<H3><A NAME="Pre-Built-Images">Short Cut:  Pre-Built ACL2 Images</A></H3>
325
231
 
326
232
The site <a
327
 
href="http://www.cs.utexas.edu/users/moore/acl2/v6-5/distrib/images/Readme.html">http://www.cs.utexas.edu/users/moore/acl2/v6-5/distrib/images/Readme.html</a>
 
233
href="http://www.cs.utexas.edu/users/moore/acl2/v7-0/distrib/images/Readme.html">http://www.cs.utexas.edu/users/moore/acl2/v7-0/distrib/images/Readme.html</a>
328
234
contains links to ACL2 executables and packages.  Each <code>-md5sum</code> file
329
235
was created using <code>md5sum</code>.  We may add additional
330
236
links from time to time.
345
251
HREF="#Pre-Built-Images">pre-built ACL2 image</A>, you may skip this section.
346
252
<!-- End of only for non-incremental releases. -->
347
253
Connect to <I>dir</I> as above and execute <BR><BR> <CODE>cd
348
 
acl2-sources</CODE><BR> <CODE>make LISP=</CODE><I>xxx</I><BR>
 
254
acl2-7.0</CODE><BR> <CODE>make LISP=</CODE><I>xxx</I><BR>
349
255
<BR>
350
256
where <I>xxx</I> is the command to run your local Common Lisp.
351
257
<P>
352
258
By default, if no <CODE>LISP=</CODE><I>xxx</I> is specified,
353
259
<CODE>LISP=ccl</CODE> is used.  On our hosts, <CODE>ccl</CODE> is the name of
354
 
Clozure Common Lisp (CCL), which can be obtained as explained <a
355
 
href="requirements.html#Obtaining-CCL">in the Requirements document</a>.
 
260
Clozure Common Lisp (CCL), which can be obtained as <a
 
261
href="requirements.html#Obtaining-CCL">explained in the Requirements document</a>.
356
262
 
357
263
<P>
358
264
 
359
 
This will create executable <code>saved_acl2</code> in the
360
 
<code>acl2-sources</code> directory.
 
265
This will create executable <code>saved_acl2h</code> in the
 
266
<code>acl2-7.0</code> directory.
361
267
 
362
268
<P>
363
269
 
364
270
The time taken to carry out this process depends on the host processor
365
271
but may be only a few minutes for a fast processor.  The size of the
366
 
resulting binary image is dependent on which Lisp was used, but it may
 
272
resulting binary image is dependent on which Lisp was used, but it may be
367
273
a couple hundred megabytes or so.
368
274
 
369
275
<P>
370
276
This <CODE>make</CODE> works for the Common Lisp implementations listed
371
277
in <A HREF="requirements.html">Requirements document</A> on systems we
372
 
have tested.  See the file <CODE>acl2-sources/GNUmakefile</CODE> for
 
278
have tested.  See the file <CODE>acl2-7.0/GNUmakefile</CODE> for
373
279
further details.  If this <CODE>make</CODE> command does not work for
374
280
you, please see the instructions below for <A HREF="#Non-Unix">other
375
281
than Unix-like systems</A>.
402
308
 
403
309
Your Common Lisp should be one of those listed in
404
310
<A HREF="requirements.html">Requirements document</A>.  Filenames
405
 
below should default to the <I>dir</I><CODE>/acl2-sources</CODE>
 
311
below should default to the <I>dir</I><CODE>/acl2-7.0</CODE>
406
312
directory; please connect to that directory before continuing.
407
313
 
408
314
<OL>
409
 
<P><LI> Remove file <CODE>nsaved_acl2</CODE> if it exists.</LI>
 
315
<P><LI> Remove file <CODE>nsaved_acl2h</CODE> if it exists.</LI>
410
316
 
411
 
<P><LI> Start up Common Lisp in the <CODE>acl2-sources</CODE> directory
 
317
<P><LI> Start up Common Lisp in the <CODE>acl2-7.0</CODE> directory
412
318
and submit the following sequence of commands.
413
319
 
414
320
<PRE>
419
325
</PRE>
420
326
 
421
327
  The commands above will compile the ACL2 sources and create compiled object
422
 
  files on your <CODE>acl2-sources</CODE> subdirectory.
 
328
  files on your <CODE>acl2-7.0</CODE> subdirectory.  Here we assume
 
329
  that executables have extension <code>.dxl</code>, but this will
 
330
  depend on your host Lisp and operating system.
423
331
</LI>
424
332
 
425
333
<P><LI> Now exit your Common Lisp and invoke a fresh copy of it (mainly to avoid
426
334
  saving an image with the garbage created by the compilation process). Again
427
 
  arrange to connect to the <CODE>acl2-sources</CODE> subdirectory. In the
 
335
  arrange to connect to the <CODE>acl2-7.0</CODE> subdirectory. In the
428
336
  fresh Lisp <a name="initialization-first-pass">type</a>:
429
337
 
430
338
<PRE>
445
353
</LI>
446
354
 
447
355
<P><LI> So now exit your Common Lisp and invoke a fresh copy of it (again arranging
448
 
  to connect to your <CODE>acl2-sources</CODE> subdirectory). Then, in the
 
356
  to connect to your <CODE>acl2-7.0</CODE> subdirectory). Then, in the
449
357
  fresh Lisp type:
450
358
 
451
359
<PRE>
453
361
  (load "init.lisp")
454
362
  (in-package "ACL2")
455
363
  (save-acl2 (quote (initialize-acl2))
456
 
             "saved_acl2")
 
364
             "saved_acl2h")
457
365
</PRE>
458
366
 
459
367
  You have now saved an image.  Exit Lisp now.  Subsequent steps will put the
460
368
  image in the right place.
461
369
 
462
 
<P><LI> Remove <CODE>osaved_acl2</CODE> if it exists.
 
370
<P><LI> Remove <CODE>osaved_acl2h</CODE> if it exists.
463
371
 
464
 
<P><LI> <b>IF</b> <CODE>saved_acl2</CODE> and <CODE>saved_acl2.dxl</CODE> both exist <b>THEN</b>:
 
372
<P><LI> <b>IF</b> <CODE>saved_acl2h</CODE> and <CODE>saved_acl2h.dxl</CODE> both exist <b>THEN</b>:
465
373
<ul>
466
 
     <li>move <CODE>saved_acl2.dxl</CODE> to <CODE>osaved_acl2.dxl</CODE></li>
467
 
     <li>move <CODE>saved_acl2</CODE> to <CODE>osaved_acl2</CODE>
468
 
         and edit <CODE>osaved_acl2</CODE>, changing <CODE>saved_acl2.dxl</CODE>
469
 
         (at end of line) to <CODE>osaved_acl2.dxl</CODE></li>
 
374
     <li>move <CODE>saved_acl2h.dxl</CODE> to <CODE>osaved_acl2h.dxl</CODE></li>
 
375
     <li>move <CODE>saved_acl2h</CODE> to <CODE>osaved_acl2h</CODE>
 
376
         and edit <CODE>osaved_acl2h</CODE>, changing <CODE>saved_acl2h.dxl</CODE>
 
377
         (at end of line) to <CODE>osaved_acl2h.dxl</CODE></li>
470
378
</ul>
471
 
     <b>ELSE IF</b> <CODE>saved_acl2</CODE> exists <b>THEN</b>:
 
379
     <b>ELSE IF</b> <CODE>saved_acl2h</CODE> exists <b>THEN</b>:
472
380
<ul>
473
 
     <li>move <CODE>saved_acl2</CODE> to <CODE>osaved_acl2</CODE></li>
 
381
     <li>move <CODE>saved_acl2h</CODE> to <CODE>osaved_acl2h</CODE></li>
474
382
</ul>
475
383
</LI>
476
384
 
477
 
<P><LI> Move <CODE>nsaved_acl2</CODE> to <CODE>saved_acl2</CODE>.</LI>
 
385
<P><LI> Move <CODE>nsaved_acl2h</CODE> to <CODE>saved_acl2h</CODE>.</LI>
478
386
 
479
387
<P><LI> For some Common Lisps, a
480
 
     file <CODE>nsaved_acl2.</CODE><em>suffix</em> is created for some
 
388
     file <CODE>nsaved_acl2h.</CODE><em>suffix</em> is created for some
481
389
     <em>suffix</em>.
482
 
     Move it to: <CODE>saved_acl2.</CODE><em>suffix</em></LI>
 
390
     Move it to: <CODE>saved_acl2h.</CODE><em>suffix</em></LI>
483
391
 
484
 
<P><LI> Make sure <CODE>saved_acl2</CODE> is executable.  For Windows
 
392
<P><LI> Make sure <CODE>saved_acl2h</CODE> is executable.  For Windows
485
393
this involves two mini-steps:
486
394
 
487
395
<blockquote>
488
396
 
489
 
(a) Remove the <code>"$*"</code> from the <code>saved_acl2</code>
 
397
(a) Remove the <code>"$*"</code> from the <code>saved_acl2h</code>
490
398
script (because Windows does not understand <code>$*</code>).
491
399
Consequently, any arguments you pass to ACL2 via the command line will
492
400
be ignored.
493
401
 
494
402
<p>
495
403
 
496
 
(b) Rename <code>saved_acl2</code> to <code>saved_acl2.bat</code>, for
 
404
(b) Rename <code>saved_acl2h</code> to <code>saved_acl2h.bat</code>, for
497
405
example by executing the following command.<br><br>
498
 
<code>rename saved_acl2 saved_acl2.bat</code>
 
406
<code>rename saved_acl2h saved_acl2h.bat</code>
499
407
 
500
408
</blockquote>
501
409
</LI>
529
437
 
530
438
<p>
531
439
 
532
 
Otherwise here are steps to follow.
 
440
Otherwise here are steps to follow.  (These are quite old and may have
 
441
bugs.  Please report any bugs to
 
442
the <A HREF="mailto:kaufmann@cs.utexas.edu">Matt Kaufmann</A>ACL2
 
443
implementors</A>.)
533
444
 
534
445
<ol>
535
446
<li><b>FIRST</b> get GCL running on your Windows system using <b>ONE</b> of the
571
482
<li><b>THIRD</b>, follow the <A HREF="#Non-Unix">instructions for
572
483
    other than Unix-like systems</A> above, though the resulting file
573
484
    may be called
574
 
<code>saved_acl2.exe</code> rather than <code>saved_acl2</code>.
 
485
<code>saved_acl2h.exe</code> rather than <code>saved_acl2h</code>.
575
486
 
576
 
<!-- NOTE to developers: v6-5 below indicates a normal release, which is OK. -->
 
487
<!-- NOTE to developers: v7-0 below indicates a normal release, which is OK. -->
577
488
<!-- Do not edit that for incremental releases. -->
578
489
 
579
490
<li><b>FINALLY</b>, create a file <code>acl2.bat</code> as explained in
580
 
<code><a href="http://www.cs.utexas.edu/users/moore/acl2/v6-5/distrib/images/Readme.html#acl2-bat">
581
 
http://www.cs.utexas.edu/users/moore/acl2/v6-5/distrib/images/Readme.html</a></code>.
 
491
<code><a href="http://www.cs.utexas.edu/users/moore/acl2/v7-0/distrib/images/Readme.html#acl2-bat">
 
492
http://www.cs.utexas.edu/users/moore/acl2/v7-0/distrib/images/Readme.html</a></code>.
582
493
 
583
494
</ol>
584
495
 
643
554
(If you downloaded a <A
644
555
HREF="#Pre-Built-Images">pre-built ACL2 image</A>, then you may skip this section.)
645
556
<!-- End of only for non-incremental releases. -->
646
 
Connect to subdirectory <CODE>acl2-sources</CODE> of <I>dir</I>,
 
557
Connect to subdirectory <CODE>acl2-7.0</CODE> of <I>dir</I>,
647
558
start up your Common Lisp, and compile by executing the following forms.
648
559
<I>This sequence of steps need only be performed once.</I>
649
560
 
654
565
</PRE>
655
566
 
656
567
Now each time you want to use ACL2, you need only execute the following forms
657
 
after starting up Common Lisp in subdirectory <CODE>acl2-sources</CODE> of
 
568
after starting up Common Lisp in subdirectory <CODE>acl2-7.0</CODE> of
658
569
<I>dir</I>.
659
570
 
660
571
<PRE>
674
585
Now proceed to read more about <A HREF="using.html">Using ACL2</A>.
675
586
 
676
587
<BR><HR noshade size=8><BR>
677
 
<H2><A NAME="Summary">Summary of Distribution</A></H2>
678
 
 
679
 
The ACL2
680
 
    distribution, <code><A HREF="http://www.cs.utexas.edu/users/moore/acl2/v6-5/distrib/acl2.tar.gz">
681
 
    acl2.tar.gz</A></code>, includes the ACL2 source files as well as
682
 
    the following files and directories (and a few others not
683
 
    mentioned here).  Note that a <code>books/</code> directory
684
 
    is <b>not included</b>; see instructions above to fetch the community
685
 
    books.
 
588
<H2><A NAME="Summary">Summary of ACL2 System Distribution</A></H2>
 
589
 
 
590
This section, which is optional, discusses how to browse a
 
591
distribution that includes ACL2 only, without the
 
592
<a href="http://www.cs.utexas.edu/users/moore/acl2/current/combined-manual/?topic=ACL2____COMMUNITY-BOOKS">community
 
593
books</a>.
 
594
 
 
595
<p>
 
596
 
 
597
We discuss <a href="#Sources">above</a> how to obtain a gzipped
 
598
tarfile that contains both the ACL2 sources and
 
599
the <a href="http://www.cs.utexas.edu/users/moore/acl2/current/combined-manual/?topic=ACL2____COMMUNITY-BOOKS">community
 
600
books</a>.  Below we describe the ACL2 distribution only (without the
 
601
community books) from the University of Texas at Austin.  Its files
 
602
are available by exploring the
 
603
<code><a href="http://www.cs.utexas.edu/users/moore/acl2/v7-0/distrib/">distrib/<a></code>
 
604
directory on this website or by obtaining a gzipped tarfile,
 
605
<code><a href="http://www.cs.utexas.edu/users/moore/acl2/v7-0/distrib/acl2.tar.gz">acl2.tar.gz</a></code>,
 
606
which extracts to the contents
 
607
of <code><a href="http://www.cs.utexas.edu/users/moore/acl2/v7-0/distrib/">distrib/acl2-sources/<a></code>,
 
608
which in turn contains the ACL2 source files as well as the following
 
609
(and a few others not mentioned here).
 
610
 
686
611
<PRE>
687
612
  LICENSE       ; ACL2 license file
688
613
  GNUmakefile   ; For GNU make
696
621
 
697
622
<ul>
698
623
 
699
 
<li><code><a href="http://www.cs.utexas.edu/users/moore/acl2/v6-5/distrib/images/">images/</a></code>:
700
 
Some gzip'd tar'd executables; see <code><a href="http://www.cs.utexas.edu/users/moore/acl2/v6-5/distrib/images/Readme.html">images/Readme.html</a></code></li>
 
624
<li><code><a href="http://www.cs.utexas.edu/users/moore/acl2/v7-0/distrib/images/">images/</a></code>:
 
625
Some gzip'd tar'd executables; see <code><a href="http://www.cs.utexas.edu/users/moore/acl2/v7-0/distrib/images/Readme.html">images/Readme.html</a></code></li>
701
626
 
702
 
<li><code><a href="http://www.cs.utexas.edu/users/moore/acl2/v6-5/distrib/split/">split/</a></code>: The result of splitting up <code>acl2.tar.gz</code></li>
 
627
<li><code><a href="http://www.cs.utexas.edu/users/moore/acl2/v7-0/distrib/split/">split/</a></code>: The result of splitting up <code>acl2.tar.gz</code></li>
703
628
 
704
629
</ul>
705
630
 
706
 
<P>
707
 
We estimate that the entire <code>acl2.tar.gz</code> consists of
708
 
approximately 4 MB, which extracts to about 15 MB, and the size of
709
 
gzipped tarfile <code>books-6.5.tar.gz</code> (obtained as described
710
 
<a href="#Obtaining-books">above</a>) is about 15 MB, which extracts
711
 
to about 87 MB.  (Gzipped tarfile <code>workshops-6.5.tar.gz</code>
712
 
and corresponding directory <code>workshops</code>, which are
713
 
mentioned above, have sizes of about 37 MB and 58 MB, respectively.)
714
 
Additional space is required to build an image, perhaps 50 to 300
715
 
megabytes depending on the platform (including the host Lisp); and
716
 
more will be required to <A HREF="using.html#Certifying">certify
717
 
books</A>.
718
 
 
719
 
<p>
720
 
 
721
 
<b><font size="+2">[<a href="installation.html">Back to Installation Guide.</a>]</font></b>
722
 
 
723
631
<BR><HR noshade size=8><BR>
724
 
<H2><A NAME="Bleeding-edge">Bleeding-edge Distributions via SVN</A></H2>
 
632
<H2><A NAME="Bleeding-edge">Bleeding-edge Distributions via Git</A></H2>
725
633
 
726
634
We strongly recommend that ACL2 users update their local copies of the
727
635
system and community books at each ACL2 release.  While that should
728
636
suffice for many ACL2 users, nevertheless for those who prefer to
729
637
obtain the latest developments, the ACL2 source code and community
730
638
books have been made available between ACL2 releases, by way of
731
 
revision control using SVN.
732
 
<i>The authors of ACL2 consider SVN distributions to be experimental;
 
639
revision control using git.
 
640
<i>The authors of ACL2 consider git distributions to be experimental;
733
641
while they will likely be fully functional in most cases, they could
734
642
however be incomplete, fragile, and unable to pass our own
735
 
regression.</i> If you decide to use SVN versions of either the ACL2
736
 
or the community books, then you should use both, as they tend to be
737
 
kept in sync.  See the project
738
 
websites, <code><A HREF="http://acl2-books.googlecode.com/">acl2-books</A></code>
739
 
and <code><A HREF="http://acl2-devel.googlecode.com/">acl2-devel</A></code>,
740
 
for the ACL2 community books and development sources, respectively.
 
643
regression.</i>  See
 
644
the <a href="https://github.com/acl2/acl2">project website</a> for
 
645
more information.
 
646
 
 
647
<BR><HR>
 
648
 
 
649
<b><font size="+2">[<a href="installation.html">Back to Installation Guide.</a>]</font></b>
741
650
 
742
651
<BR><BR><BR><BR><BR><BR><BR><BR><BR><BR><BR><BR><BR><BR><BR><BR><BR><BR><BR><BR>
743
652