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

[Camm Maguire]

Greetings!

Matt Kaufmann <address@hidden> writes:

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

To my knowledge, yes.

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

We're up to -37 now, and I'm reasonably sure this will be the last
before 2.6.2.


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

An acl2 2.8 for Debian should appear shortly.  My understanding is
that ppc versions of both this and gcl itself should work on mac osx
via the 'fink' mechanism.  I'm cc'ing Aurelien as he is the expert
here.  In any case, gcl should compile out of the box on macosx, and
compile acl2 2.8 there without special instructions.  The special
instructions in my generic debian build rules is to cover the cases of
ia64, hppa, mips(el) and alpha where gcl cannot yet dump previously
loaded binary object code.  GCL does support such saved images on
both Debian ppc and macosx ppc, making these special compile commands
unnecessary here, though workable.

Take care,


> 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
> 
> 
> _______________________________________________
> Gcl-devel mailing list
> address@hidden
> http://mail.gnu.org/mailman/listinfo/gcl-devel
> 
> 
> 

-- 
Camm Maguire                                            address@hidden
==========================================================================
"The earth is but one country, and mankind its citizens."  --  Baha'u'llah