[Gcl-devel] Re: Compilation of ACL2 using GCL on Mac OS X

[Matt Kaufmann]

Jun, Camm --

Some questions for each/both of you.

[Jun, Camm] Are the instructions included in Jun's email below (sent last
October) still up-to-date, as far as you know?

[Jun] If so, then Jun, do you mind if we put them up on an an ACL2 web page?

[Camm] Or perhaps instead, can one simply obtain GCL from
ftp://ftp.debian.org/debian/pool/main/g/gcl/gcl_2.6.1-33_powerpc.deb if one is
using Mac OS X?

[Camm] Will there be an ACL2/GCL debian package for ACL2 2.8?  If so, will the
"Power PC" version be usable on Mac OS X so that Jun's instructions below will
no longer be needed?

Thanks --
-- Matt
   From: address@hidden
   X-Authentication-Warning: arlab176.austin.ibm.com: sawada owned process 
doing -bs
   cc: address@hidden
   Date: Tue, 28 Oct 2003 11:22:36 -0600
   Reply-To: address@hidden
   Sender: address@hidden
   X-Listprocessor-Version: 8.2.10/020311/17:52 -- ListProc(tm) by CREN

   Recently, GCL has been ported to Mac OS X by Aurelien Chanudet and ACL2
   can be compiled using Camm Maguire's patch to ACL2.  I think some people
   want to run the ACL2 on their Mac, so I will share the tips and patches
   for the compilation.

   --Jun Sawada


   How to compile ACL2 on GCL on Mac OS X.

   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, an 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 :pserver:address@hidden:/cvsroot/gcl login
       % cvs -d :pserver:address@hidden:/cvsroot/gcl co gcl

     When asked for a password, just type return. 

     For details, see 

       http://savannah.gnu.org/projects/gcl

   3.  Apply a patch to the GCL source code. 
       Store the following patch into a file named patch-gcl, and apply it
       as:
         % cd gcl
         % patch -p1 < ../patch-gcl

   ---------------------- patch-gcl ----------------------------------
   diff -ru gcl.orig/o/main.c gcl/o/main.c
   --- gcl.orig/o/main.c        Sat Sep 13 21:43:07 2003
   +++ gcl/o/main.c     Mon Oct 27 15:28:41 2003
   @@ -111,6 +111,11 @@
        struct rlimit rl;
    #endif

   +#if defined(DARWIN)
   +    extern void init_darwin_zone_compat ();
   +    init_darwin_zone_compat ();
   +#endif
   +
    #ifdef RECREATE_HEAP
        RECREATE_HEAP
    #endif
   diff -ru gcl.orig/o/sgbc.c gcl/o/sgbc.c
   --- gcl.orig/o/sgbc.c        Sat Sep 13 21:43:08 2003
   +++ gcl/o/sgbc.c     Mon Oct 27 15:36:40 2003
   @@ -48,6 +48,10 @@

    #endif

   +#if defined(DARWIN)
   +#include <sys/ucontext.h>
   +#endif
   +
    #include <signal.h>

    /*  void segmentation_catcher(void); */
   @@ -1440,9 +1444,15 @@
    #ifndef  BSD
      INSTALL_MPROTECT_HANDLER;
    #endif
   +
   +#if !defined(DARWIN)
      /* if (SIGSEGV == SIGPROTV) */
      segmentation_catcher(SIGSEGV);
   -
   +#else
   +  /* segmentation_catcher(SIGBUS,code,scp); */
   +  /* for the sake of exactness */
   +  segmentation_catcher(SIGBUS);
   +#endif
    }

    static void
   diff -ru gcl.orig/o/unixfasl.c gcl/o/unixfasl.c
   --- gcl.orig/o/unixfasl.c    Sat Sep 13 21:43:08 2003
   +++ gcl/o/unixfasl.c Mon Oct 27 15:30:10 2003
   @@ -282,7 +282,7 @@
    static int
    faslink(object faslfile, object ldargstring)
    {
   -#if defined(__linux__) && defined(__ELF__)
   +#if (defined(__linux__) && defined(__ELF__)) || defined(DARWIN)
      FEerror("faslink() not supported for ELF yet",0);
      return 0;
    #else
   diff -ru gcl.orig/unixport/makefile gcl/unixport/makefile
   --- gcl.orig/unixport/makefile       Wed Sep 24 11:30:12 2003
   +++ gcl/unixport/makefile    Mon Oct 27 15:35:30 2003
   @@ -18,6 +18,7 @@

    libgclp.a: $(ODIR)/gcllib.a
           cp $< $@
   +    ranlib $@

    gmpfiles: $(shell find ../$(GMPDIR) -name "*.o" |grep -v '\.lib')
           rm -rf gmp
   @@ -116,26 +117,26 @@

    libgcl.a: $(FIRST_FILE) $(OBJS) sys_gcl.o $(LAST_FILE) gmpfiles bfdfiles
           rm -rf $@
   -    ar rs $@ $(filter %.o,$^) $(shell find gmp bfd -name "*.o")
   +    libtool -static -o $@ $(filter %.o,$^) $(shell find gmp bfd  -name 
"*.o")

    libpre_gcl.a: $(FIRST_FILE) $(OOBJS) sys_pre_gcl.o $(LAST_FILE) gmpfiles 
bfdfiles
           rm -rf $@
   -    ar rs $@ $(filter %.o,$^) $(shell find gmp bfd -name "*.o")
   +    libtool -static -o $@ $(filter %.o,$^) $(shell find gmp bfd  -name 
"*.o")

    libmod_gcl.a: $(FIRST_FILE) $(OBJS) $(MODOBJS) sys_mod_gcl.o $(LAST_FILE) 
gmpfiles bfdfiles
           rm -rf $@
   -    ar rs $@ $(filter %.o,$^) $(shell find gmp bfd -name "*.o")
   +    libtool -static -o $@ $(filter %.o,$^) $(shell find gmp bfd  -name 
"*.o")

    libxgcl.a: libgcl.a
           ln -snf $< $@

    libansi_gcl.a: $(FIRST_FILE) $(OBJS) $(ANSIOBJS) sys_ansi_gcl.o 
$(LAST_FILE) gmpfiles bfdfiles
           rm -rf $@
   -    ar rs $@ $(filter %.o,$^) $(shell find gmp bfd -name "*.o")
   +    libtool -static -o $@ $(filter %.o,$^) $(shell find gmp bfd  -name 
"*.o")

    libpcl_gcl.a: $(FIRST_FILE) $(OBJS) $(PCLOBJS) sys_pcl_gcl.o $(LAST_FILE) 
gmpfiles bfdfiles
           rm -rf $@
   -    ar rs $@ $(filter %.o,$^) $(shell find gmp bfd -name "*.o")
   +    libtool -static -o $@ $(filter %.o,$^) $(shell find gmp bfd  -name 
"*.o")

    raw_%: lib%.a libgclp.a $(SYSTEM_OBJS) $(EXTRAS)
           $(CC) -o raw_$*$(EXE) $(filter %.o,$^) \
   ---------------------- patch-gcl ----------------------------------


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


   5. Run configure in the GCL source directory
        % ./configure --enable-machine=powerpc-macosx --enable-debug \
             --disable-statsysbfd --enable-custreloc

   6. Compile GCL.

        % make  

   7. Install GCL

        % make install

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

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

   8. Download ACL2 source and patch file from the Debian site. Go to

      http://packages.debian.org/unstable/math/acl2.html

      and download acl2_2.7.orig.tar.gz and acl2_2.7-7.diff.gz.

   9.  Expand source code and apply patch.  Applying patch is done by

        % cd acl2-sources
        % patch -p1 < ../acl2_2.7-7.diff

   10.  Compile ACL2 by

        % make -f debian/rules saved_acl2

        Ordinary makefile does not work, because si::save-system does not 
        work with the current version of GCL for Mac OS X.  You must
        specify "-f debian/rules" to make sure that GCL uses compiler::link
        to save the image. 

   11.  Compile ACL2 books by

        % (cd books ; make )

   12.  Install ACL2 by making shell script /usr/local/bin/acl2 like

          #!/bin/bash
          <installed dir>/saved_acl2