Re: [Gcl-devel] Re: address@hidden: Acl2 on gcl on Mac OS X]

[Gregory Wright]

Hi,

ACL2 builds on Mac OS X under OpenMCL if you use the darwinports system
(similar to fink). See http://darwinports.opendarwin.org. Once you've  
downloaded
and built darwinports, issue the command

sudo port install

from the math/acl2 directory. If you type

sudo port install +certify

it will certify the books. This can take some time (about eight and a  
half hours
on a powerbook G4 800 MHz).

A number of patches are required; these are automatically applied. If  
you're interested
in them look in the math/acl2/files directory.

I'd like to get gcl to build under darwinports (acl2 would then run a  
bit faster) but
haven't found the time to do it yet.

Best Wishes,
Greg Wright


On Jan 1, 2004, at 8:38 PM, Camm Maguire wrote:

> Greetings!  gcl/acl2 on Mac OS X is known to work.  Please see
>
> http://mail.gnu.org/archive/html/gcl-devel/2003-10/msg00156.html
>
> for details, and let me know if you encounter problems.
>
> Take care,
>
> Matt Kaufmann <address@hidden> writes:
>
> > Yes, we are in the process of adding openMCL support for the next  
> > version of
> > ACL2, but not in Version 2.7 (the latest released version of ACL2).   
> > If we hear
> > back from the others that GCL isn't an option, perhaps we can come up  
> > with
> > something.
> >
> > -- Matt
> >    Date: Thu, 1 Jan 2004 15:32:29 -0800 (GMT-08:00)
> >    From: Rance DeLong <address@hidden>
> >    Reply-To: Rance DeLong <address@hidden>
> >    Cc: address@hidden
> >    Content-Type: text/plain; charset=us-ascii
> >
> >    In an attempt to make some progress I downloaded openmcl.  When I  
> > attempt to make acl2:
> >    "make LISP=openmcl" the lisp complains on (load "init.lsp") saying
> >
> > > Error in process listener(1): There is no package named "USER" .
> > > While executing: CCL::SET-PACKAGE
> > > Type :GO to continue, :POP to abort.
> > > If continued: Retry finding package with name "USER".
> >
> >    so that was not fruitful either.
> >
> >    Any insight would be appreciated!
> >    Thanks,
> >    Rance
> >
> >    -----Original Message-----
> >    From: Matt Kaufmann <address@hidden>
> >    Sent: Jan 1, 2004 3:25 PM
> >    To: address@hidden, address@hidden, address@hidden
> >    Cc: address@hidden
> >    Subject: address@hidden: Acl2 on gcl on Mac OS X]
> >
> >    Camm, Warren, Omar --
> >
> >    I don't know the answer to the question below, about GCL for Mac  
> > OS X.  Can
> >    either of you help?  Maybe this works??
> >
> >     
> > ftp://ftp.debian.org/debian/pool/main/g/gcl/gcl_2.6.1-18_powerpc.deb
> >
> >    Thanks --
> >    -- Matt
> >    ------- Start of forwarded message -------
> >    Date: Thu, 1 Jan 2004 13:20:35 -0800 (GMT-08:00)
> >    From: Rance DeLong <address@hidden>
> >    Reply-To: Rance DeLong <address@hidden>
> >    To: address@hidden
> >    Subject: Acl2 on gcl on Mac OS X
> >    Content-Type: text/plain; charset=us-ascii
> >
> >    I'm a faculty member at Santa Clara University preparing to teach  
> > a new course starting Monday.
> >    I want to use acl2 on my new powerbook g4 running Mac OS X.  I  
> > retrieved gcl-2.5.3 but it
> >    won't build on OS X (configure doesn't even complete  
> > successfully).  Do you know if there
> >    is a version of gcl for OS X?  Your assistance is greatly  
> > appreciated.
> >
> >    Rance J. DeLong
> >    ------- End of forwarded message -------
>
> --  
> Camm Maguire			     			address@hidden
> ======================================================================= 
> ===
> "The earth is but one country, and mankind its citizens."  --   
> Baha'u'llah
>
>
> _______________________________________________
> Gcl-devel mailing list
> address@hidden
> http://mail.gnu.org/mailman/listinfo/gcl-devel