[Top][All Lists]

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

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

From: Gregory Wright
Subject: Re: [Gcl-devel] Re: address@hidden: Acl2 on gcl on Mac OS X]
Date: Thu, 1 Jan 2004 22:05:56 -0500


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


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

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

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


   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

reply via email to

[Prev in Thread] Current Thread [Next in Thread]