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

[Camm Maguire]

Greetings!  Glad to here of your progress!  In general, my
understanding is that GCL is faster than clisp (gcl compiles to native
machine code, clisp to interpreted bytecode), and is likely more
widely used in the acl2 community.  It is probably somewhat less ansi
compatible than clisp.  Both are good, of course.

Take care,

"Rance J. DeLong" <address@hidden> writes:

> Camm, thanks for the info.  I will get the gcl 2.6.1 you mentioned, even 
> though at 4AM
> this morning I finally succeeded in getting acl2 to work.  I was trying 
> everything and was
> not going to stop until I had succeeded or passed out.  I installed the Fink 
> tool which
> I then used to download and build CLISP, which seemed to successfully build 
> acl2
> (I got the acl2 prompt and went to bed happy instead of depressed, though I
> haven't run a proveall as yet.)  What's the difference (both historically and 
> functionally,
> between CLISP and GCL?  What's the advantage of one vs the other with respect
> to acl2?
> Thanks again,
> Rance
> PS: Thanks again to all for the quick responses on a holiday!
> Camm Maguire wrote:
> 
>           Greetings!  This instructions I believe were against version 2.6.1,
> the latest stable, or version 2.7.0, the latest unstable.  We have
> only recently regained access to ftp.gnu.org and therefore have been
> unable to update the version there for months.  This will be addressed
> shortly, with the current 2.6.1 CVS branch tagged and released as
> 2.6.2.  Until this is completed, you can either retrieve a source
> tarball from
> 
> http://ftp.debian.org/debian/pool/main/g/gcl/gcl_2.6.1.tar.gz
> 
> or via cvs
> 
> cvs -d:ext:address@hidden:/cvsroot/gcl -r Version_2_6_1 \
>  -d gcl-2.6.1 gcl
> 
> Please note that the gcl patch mentioned in the post I referenced has
> now been included in both branches.  GCL should compile out of the
> box.  You are likely to still need the acl2 patch as mentioned in
> that post.
> 
> Please let me know if problems persist.  
> 
> Take care,
> 
> Rance DeLong <address@hidden> writes:
> 
>   
> 
>                     Camm,
> Thanks for your reply.
> Unfortunately, I was not able to successfully apply the patch.
> I am using gcl-2.5.3.  After extracting the tar file the directory is 
> gcl-2.5.3.
> I edited down the instructions to just include the stuff betw the --- 
> patch-gcl --- lines.
> I did not get GNU sed because my system had a sed (I don't know if this was 
> the problem).
> I put patch-gcl "next to" the gcl-2.5.3 directory.  I cd'd to the gcl-2.5.3 
> directory.
> When I attempted to run patch it said:
> 
> missing header for unified diff at line 4 of patch
> patching file o/main.c
> Hunk #1 succeeded at 124 with fuzz 2 (offset 13 lines).
> missing header for unified diff at line 19 of patch
> patching file o/sgbc.c
> Hunk #1 FAILED at 48.
> Hunk #2 succeeded at 1243 (offset -201 lines).
> 1 out of 2 hunks FAILED -- saving rejects to file o/sgbc.c.rej
> missing header for unified diff at line 50 of patch
> patching file o/unixfasl.c
> Hunk #1 FAILED at 282.
> 1 out of 1 hunk FAILED -- saving rejects to file o/unixfasl.c.rej
> missing header for unified diff at line 62 of patch
> patching file unixport/makefile
> Hunk #1 FAILED at 18.
> patch: **** malformed patch at line 79: bfdfiles
> 
> I tried the same thing renaming the gcl-2.5.3 directory to gcl and gcl.orig
> without success.  I re-extracted the tar file after each attempt.
> I looked through the patch file and joined a few lines that appeared to
> have been split along the way.  Still no-go.
> Looks like a non-starter to me.
> 
> Regards,
> Rance
> 
> -----Original Message-----
> From: Camm Maguire <address@hidden>
> Sent: Jan 1, 2004 5:38 PM
> To: Matt Kaufmann <address@hidden>
> Cc: address@hidden, address@hidden, address@hidden, 
>       address@hidden
> Subject: Re: address@hidden: Acl2 on gcl on Mac OS X]
> 
> 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
> 
> 
> 
>     
> 
> 
>        
> 
> 
> 
> -- 
> Rance J. DeLong
> Tel: 408-353-4102
> Fax: 408-715-2531
> 
> **********NOTE**********
> The information contained in this email message is intended only
> for use of the individual or entity named above.  If the reader
> of this message is not the intended recipient, or the employee or
> agent responsible to deliver it to the intended recipient, you
> are hereby notified that any dissemination, distribution or
> copying of this communication is strictly prohibited.  If you
> have received this communication in error, please immediately
> notify me by return email, and destroy the original message.
> Thank you.
> 
> 

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