[Top][All Lists]

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

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

From: sawada
Subject: [Gcl-devel] Compilation of ACL2 using GCL on Mac OS X
Date: Tue, 28 Oct 2003 11:22:36 -0600

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 


    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


    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 
3.  Apply a patch to the GCL source code. 
    Store the following patch into a file named patch-gcl, and apply it
      % 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;
+#if defined(DARWIN)
+    extern void init_darwin_zone_compat ();
+    init_darwin_zone_compat ();
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 @@
+#if defined(DARWIN)
+#include <sys/ucontext.h>
 #include <signal.h>
 /*  void segmentation_catcher(void); */
@@ -1440,9 +1444,15 @@
 #ifndef  BSD
+#if !defined(DARWIN)
   /* if (SIGSEGV == SIGPROTV) */
+  /* segmentation_catcher(SIGBUS,code,scp); */
+  /* for the sake of exactness */
+  segmentation_catcher(SIGBUS);
 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;
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 
 libpre_gcl.a: $(FIRST_FILE) $(OOBJS) sys_pre_gcl.o $(LAST_FILE) gmpfiles 
        rm -rf $@
-       ar rs $@ $(filter %.o,$^) $(shell find gmp bfd -name "*.o")
+       libtool -static -o $@ $(filter %.o,$^) $(shell find gmp bfd  -name 
 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 
 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 
 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 
 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 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


   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
       <installed dir>/saved_acl2

reply via email to

[Prev in Thread] Current Thread [Next in Thread]