How to build/install ACL2 on GCL on Mac OS X

Jun Sawada has provided information for building and installing ACL2 on GCL on Mac OS X. This information has been updated according to feedback from Camm Maguire received April 2004. Thanks to them both. After some editing primarily for HTML format, the result is below.

The following steps are how you can install ACL2 on Mac OS X 10.2. I have not yet tried to compile it on Mac OS X 10.3 or other versions. As far as I know, it works on any modern Mac running OS X including Power Mac G5. 1. Install gcc and GNU sed. I used gcc 3.1 and GNU sed 4.0.5. You can download Apple's developer tools including gcc from http://developer.apple.com. You must register as an ADC member to download software. Once you login to the ADC webpage, go to

    "download software"-> "developer tools"

and download "Mac OS X developer tools".

You also want to install GNU sed using Fink, a Unix tool installer. Fink is available from http://fink.sourceforge.net. Go to "download" and get Fink binary installer. Install it. The sourceforge web site includes extensive documentations and tutorials. Use it to install GNU sed. (For those who don't want to read documentations, dselect is an easy way. Set environtment variable TERM to xterm-color and run /sw/bin/dselect You can 'Update', 'Select' sed, and 'Install'.)

From now on, I assume that GNU version of sed is installed as /sw/bin/sed.

2. Obtain GCL source code from the CVS depository. The easiest way to obtain the most recent code is to run the following cvs command .

   % cvs -d :ext:anoncvs@subversions.gnu.org:/cvsroot/gcl login
   % cvs -d :ext:anoncvs@subversions.gnu.org:/cvsroot/gcl co gcl



 When asked for a password, just type return.



 For details, see http://savannah.gnu.org/projects/gcl.



3.  Set the compilation environment. I assume we are using bash in
   the following script.
   % ulimit -s 8192
   % export PATH=/sw/bin:/sw/sbin:/usr/local/bin:$PATH
   % export MACOSX_DEPLOYMENT_TARGET=10.2
   % export LIBRARY_PATH=/sw/lib
   % export C_INCLUDE_PATH=/sw/include
   % export CPPFLAGS="-no-cpp-precomp"




4. Run configure in the GCL source directory.
    % ./configure


One can
optionally add --enable-debug if one wants a slower C debugging
version.  --disable-statsysbfd --enable-custreloc should work, but is
mildly deprecated in favor of the default (i.e. no flags) which is
equivalent to --disable-statsysbfd --enable-locbfd.



5. Compile GCL.
    % make  




6. Install GCL.
    % make install


  By default, make installs gcl to
  /usr/local/bin.  You can change it by using the
  --prefix option for configure at step 5.



  Make sure at this moment, the installed gcl is in your
  PATH and you can run gcl.



7. Follow the usual ACL2
installation instructions to obtain the ACL2 sources and build an
executable image on a Unix/Linux system.