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

[Camm Maguire]

Greetings!

Matt Kaufmann <address@hidden> writes:

> 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

OK, my apologies, I wrote in too much haste.  There should no longer
be any patches required to the GCL source to compile on macosx.  So
step 3 is obsolete. 


Presumably step 1 still holds should one want to build gcl on macosx.

Step 2. will require replacing 'pserver' with 'ext' and making sure
CVS_RSH=ssh is in the environment.  

Step 3 again is obsolete.  

Step 4 is correct to my knowledge.  

Step 5 should no longer require any special configure flags.  One can
optionally add --enable-debug if one wants a slower C debugging
version.  --disable-statsysbfd --enable-custreloc should work, but is
mildly deprecated in favor of the default (i.e. no flags) which is
equivalent to --disable-statsysbfd --enable-locbfd.  Aurelien has
written a macosx backend to bfd which to my knowledge can only be
found in our local copy of the binutils tree.  The --enable-machine
should not be necessary, rather being automatically detected.  

Steps 6-8 are all the same, replacing 2.7 with 2.8 for acl2 of course.

Steps 9 and 10 should no longer be necessary, but should still work.
One should instead be able to follow the default acl2 build procedure.
The alternate build performed in the Debian package and described in
the note below is still required for acl2 2.8, but just not on ppc,
but rather ia64, mips(el), hppa, and alpha only.  This alternate
procedure works on all platforms, as it relies on the native C linker
(ld) to link compiled lisp objects instead of GCL's own linker, which
though preferable, is still not universally ported.  One basically
replaces the last (si::save-system...) call with

(compiler::link
   (list my-compiled-lisp-object-1.o my-compiled-lisp-object-2.o ...)
   "saved_image_name"
   "(any-initialization-lisp-code-than-needs-running-before-image-save
   ...)"
   "my_extra_c_module.o libmy_extra_c_lib.a ..."
   [ t -- initialize all compiled lisp objects explicitly and in order
          at the beginning
     |
     nil -- initialize compiled lisp objects as the initialization
     code in the third argument would otherwise attempt to load them
     ])


To use this, one must either compile with ... :system-p t or (setq
compiler::*default-system-p* t)

This is explained in the gcl-si docs.

For example, the "business end" of the Debian acl2 build procedure is


init.lsp.ori: 
        [ -e $@ ] || mv init.lsp $@

foo.lsp: init.lsp.ori
        echo '(setq compiler::*default-system-p* t)' >$@
        cat $< >> $@

BINARIES:=acl2-fns.o axioms.o basis.o translate.o type-set-a.o type-set-b.o 
rewrite.o simplify.o \
          bdd.o other-processes.o induct.o history-management.o prove.o 
defuns.o proof-checker-a.o\
          defthm.o other-events.o ld.o proof-checker-b.o tutorial.o 
interface-raw.o \
          linear-a.o linear-b.o non-linear.o TMP1.o
BIN:=$(patsubst %,"%",$(BINARIES))

INIT:=(initialize-acl2 (quote include-book) *acl2-pass-2-files* t t)
POST:=(load \"foo.lsp\")\
      (setq compiler::*default-system-p* nil)\
      (in-package \"acl2\")\
      (save-acl2 (quote (initialize-acl2 (quote include-book) 
*acl2-pass-2-files* t)) \"saved_acl2\"))

nsaved_acl2: foo.lsp debian/patches_applied
        echo '(load "foo.lsp")(in-package "acl2")(compile-acl2)' | gcl
        echo '(load "foo.lsp")(in-package "acl2")(load-acl2)$(INIT)' | gcl
        echo '(compiler::link (list $(BIN)) "$@" "$(POST)" "" nil)' | gcl 
        mv nsaved_acl2.gcl $@




In any case, working pre-compiled binaries of both gcl and acl2 (2.8
in the near future) should be available from the Debian ppc archive
and runnable via the 'fink' mechanism, of which I know nothing.

Perhaps Aurelien can add/correct.

Take care,

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

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