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

[sawada]

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