File: obtaining-and-installing.html

package info (click to toggle)
acl2 4.3-3
links: PTS
area: main
in suites: wheezy
size: 76,444 kB
sloc: lisp: 951,371; makefile: 3,491; sh: 1,669; perl: 1,639; ansic: 358; cpp: 245; csh: 125; haskell: 17; java: 12
file content (744 lines) | stat: -rw-r--r-- 28,858 bytes
parent folder | download | duplicates (2)
<HTML>
<HEAD><TITLE>ACL2 Version 4.3 Installation Guide: Obtaining and Installing ACL2</TITLE></HEAD>

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

<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-debian">Debian GNU Linux</A>
    <LI><A HREF="#Shortcut-MacPorts">MacPorts for Mac OS X</A>
    <LI><A HREF="#Shortcut-windows">Windows Installer</A>
  </UL>
  <LI><A HREF="#Sources-Unix">Obtaining the Sources: Unix, Mac OS X, and Linux</A>
  <LI><A HREF="#Sources-Non-Unix">Obtaining the Sources: Other than Unix, Mac OS X, and Linux Systems</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, Mac OS X, or Linux System</A>
    <LI><A HREF="#Non-Unix">Building an Executable image on Other than Unix, Mac OS X 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>

<p><hr size=4 noshade><p>

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 4.3.  We will
call this directory <I>dir</I>.  For example, <I>dir</I> might be
<CODE>/home/jones/acl2/v4-3</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">Pre-built Binary Distributions</A>
<LI><A HREF="#Sources-Unix">Obtaining the Sources: Unix, Mac OS X, and Linux</A>
<LI><A HREF="#Sources-Non-Unix">Obtaining the Sources: Other than Unix, Mac OS X, and Linux Systems</A>
</UL>

<p>

<!-- Do not change the following "v4-3" for incremental releases. -->

The sources come with a <CODE>books</CODE> subdirectory, in particular
<CODE>books/Readme.html</CODE> (<A
HREF="http://www.cs.utexas.edu/users/moore/acl2/v4-3/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="using.html#Certifying">discussion on certifying
books</A> for information on using them.

<UL>
<LI><A
HREF="http://www.cs.utexas.edu/users/moore/acl2/v4-3/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/v4-3/distrib/acl2-sources/books/nonstd.tar.gz">
Non-standard analysis books (gzipped tar file)</A>
</UL>

<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.

<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-MacPorts">MacPorts for Mac OS X</A></B>

<p>

ACL2 versions are sometimes made available under MacPorts (formerly
darwinports) for Mac OS X, courtesy of Greg Wright, who has graciously provided
the initial version of the following insructions.

<p>

ACL2 can be built on OS X using the MacPorts system.  For more information on
MacPorts, including instructions on downloading and installing the
MacPorts infrastructure, see <code><a
href="http://macports.org">http://macports.org</a></code>. One thing to
remember is to add MacPorts executable directory (<code>/opt/local/bin</code>
by default) to your path.

<p>

Once MacPorts is installed, do the following.  You can stand in any directory
when executing these commands, as the installation is independent of where
these commands are run.  You can skip the first three if you haven't installed
previous versions of MacPorts or DarwinPorts.
<pre>
	   # sudo port clean --all acl2
           # sudo port uninstall acl2 +certify
           # sudo port uninstall acl2 +regression
	   # sudo port install acl2 +certify
</pre>
It's not necessary to obtain a Lisp implementation first, as one is
automatically downloaded and built as a dependency of ACL2.

<p>

To build the system without certifying books (though you probably will want to
certify books, by using the preceding install command), change the install
command to:

<pre>
	   # sudo port install acl2
</pre>

<p>

To build the system and certify the workshop books in addition to the
distributed books, change the install command to the following (but note that
this full regression takes a long time, more than 12 hours on a
PowerBook G4 800 MHz).

<pre>
	   # sudo port install +regression
</pre>

<p>

The default build uses SBCL, which works for both Intel and PPC.  If you want
to use CCL on PPC, add <code>+ccl</code> to your install command.

<p>

To build ACL2(r) -- Ruben Gamboa's extension of ACL2 for reasoning about the
real numbers using non-standard analysis -- use the following command, which
will build both ACL2 and ACL2(r) and will certify books for ACL2(r).
<pre>
	   # sudo port install +nonstd
</pre>

<p>

Once ACL2 is installed, it can be invoked using '<code>acl2</code>' at the
command prompt.  (Use '<code>acl2r</code>' for ACL2(r) instead.)

<p>

<b>More on dealing with old versions (for MacPorts).</b>

<p>

If you have an old version around from MacPorts or DarwinPorts, an
alternative to <code>uninstall</code> is <code>deactivate</code>.  Greg Wright
explains as follows:

<blockquote>

The only difference between "uninstall" and "deactivate" is that
uninstall saves the files in a tarball and deletes the installed files.
Deactivate, by contrast, keeps the files in an internal directory and
unlinks them from the user-visible directory.  You can reactivate
by using "port activate", which is faster than a reinstall from the  
tarball.
Of course, only one version of a port may be active at a time.

</blockquote>

If an attempt to use <code>uninstall</code> or <code>deactivate</code> reports
an error, then you may need to provide a version as suggested by the error
message, e.g.:

<pre>
	   # sudo port deactivate acl2 @3.0_1+certify
</pre>

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

<p>

The <A HREF="../distrib/windows">Windows Installer for ACL2</A> includes a Unix
environment, pre-certified standard and workshop books, and a copy of Gnu
Emacs.

</UL>

<BR><HR noshade size=8><BR>
<H2><A NAME="Sources-Unix">Obtaining the Sources: Unix, Mac OS X, and Linux</A></H2>

For a Unix, Mac OS X, 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/v4-3/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/v4-3/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 or Obtaining an Executable Image</A>.

<BR><HR noshade size=8><BR>
<H2><A NAME="Sources-Non-Unix">Obtaining the Sources: Other than Unix, Mac OS X, and Linux Systems</A></H2>

For a non-Unix (and non-Linux, non-Mac-OS-X) 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/v4-3/distrib/acl2.tar.gz">http://www.cs.utexas.edu/users/moore/acl2/v4-3/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.

<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 or Obtaining an Executable Image</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 <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, Mac OS X, or Linux System</A>
<LI><A HREF="#Non-Unix">Building an Executable Image on Other than Unix, Mac OS X,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>
<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/v4-3/distrib/images/Readme.html">http://www.cs.utexas.edu/users/moore/acl2/v4-3/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.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, Mac OS X, or Linux System</A></H3>

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="requirements.html#Obtaining-GCL">in the Requirements document</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.html">Requirements document</A> on 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.html">Using ACL2</A>.
<P>

<BR><HR><BR>
<H3><A NAME="Non-Unix">Building an Executable Image on Other than Unix, Mac OS X, and Linux Systems</A></H3>

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.html">Requirements document</A>.  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.</LI>

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

<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>
     <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 Allegro Common Lisp, Versions 5.0 and later, <CODE>nsaved_acl2.dxl</CODE> should exist;
     move it to <CODE>saved_acl2.dxl</CODE></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="#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="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="Mac-OS-X-GCL"></A>How to build/install ACL2 on GCL on Mac OS X</H3>

If you want to build/install ACL2 on Mac OS X, you may find it easier to do so
on top of <a href="requirements.html#Obtaining-CCL">CCL</a> rather than
<a href="requirements.html#Obtaining-GCL">GCL</a>.  Otherwise, see <A
HREF="requirements.html#gcl-mac">the directions 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>
<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 GCL/Windows instead of reading this section.
<!-- End of only for non-incremental releases. -->

<p>

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: v4-3 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/v4-3/distrib/images/Readme.html#acl2-bat">
http://www.cs.utexas.edu/users/moore/acl2/v4-3/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 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/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.html">Using ACL2</A>.

<BR><HR noshade size=8><BR>
<H2><A NAME="Summary">Summary of Distribution</A></H2>

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 about 12 megabytes, which extracts to
about 70 megabytes.  Additional space is required to build an image,
perhaps 50 to 300 megabytes depending on the platform (including the
host Lisp); and more will be required to <A
HREF="using.html#Certifying">certify books</A>.

<p>

<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>