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

[Matt Kaufmann]

Thanks.  But I presume that you aren't distributing modified ACL2 lisp source
files (if I'm wrong then we should talk), and I wouldn't expect ACL2 Version
2.7 (the latest release) to work under openMCL.  We have made several changes
to those sources that will show up when ACL2 2.8 is released, so that ACL2 2.8
should work under OpenMCL.

Thanks --
-- Matt
   Content-Type: text/plain; charset=US-ASCII; delsp=yes; format=flowed
   Cc: address@hidden, address@hidden,
           Matt Kaufmann <address@hidden>, address@hidden,
           address@hidden
   From: Gregory Wright <address@hidden>
   Date: Thu, 1 Jan 2004 22:05:56 -0500

   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
   >