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

[Matt Kaufmann]

Hi, Camm --

Thanks very much for the info.  I'm a bit confused.  You say that Jun's
instructions are up-to-date.  But you also say that "gcl should compile out of
the box on macosx", and then:

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

So I'm wondering if you're saying that the -37_powerpc.deb will work on Mac OS
X without needing to follow Jun's steps 1-7.  Also I can imagine that ordinary
compilation of ACL2 2.8 (i.e., just "make LISP=gcl) will work rather than
needing to follow something like steps 8-10 (which I see now pertain to ACL2
2.7); is that right?

Thanks --
-- Matt
   Cc: address@hidden, address@hidden,
           Aurelien Chanudet <address@hidden>
   From: Camm Maguire <address@hidden>
   Date: 18 Apr 2004 21:51:48 -0400
   User-Agent: Gnus/5.09 (Gnus v5.9.0) Emacs/21.2
   Content-Type: text/plain; charset=us-ascii
   X-SpamAssassin-Status: No, hits=-4.4 required=5.0
   X-UTCS-Spam-Status: No, hits=-78 required=180

   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