[Gcl-devel] (no subject)

[Camm Maguire]

From: Camm Maguire <address@hidden>
To: Matt Kaufmann <address@hidden>
Cc: address@hidden,  address@hidden, address@hidden
Subject: Re: address@hidden: Re: books/centaur/tutorial/alu16-book.lisp]
References: <address@hidden>
Date: Sat, 11 May 2013 10:58:49 -0400
In-Reply-To: <address@hidden> (Matt
        Kaufmann's message of "Fri, 3 May 2013 08:16:46 -0500")
Message-ID: <address@hidden>
User-Agent: Gnus/5.13 (Gnus v5.13) Emacs/23.4 (gnu/linux)
MIME-Version: 1.0
Content-Type: text/plain; charset=us-ascii

Greetings!

OK, I've installed the #= code at ut, as the 'too many #=' issue was
legitimately standing in the way of the Debian acl2 6.1 package.

seafoam$ /p/bin/gcl
GCL (GNU Common Lisp)  2.6.8 CLtL1    May 11 2013 09:25:55
Source License: LGPL(gcl,gmp), GPL(unexec,bfd,xgcl)
Binary License:  GPL due to GPL'ed components: (XGCL READLINE UNEXEC)
Modifications of this banner must retain notice of a compatible license
Dedicated to the memory of W. Schelter

Use (help) to get some basic information on how to use GCL.
Temporary directory for compiler files set to /tmp/

>(time (with-open-file (s "/tmp/1000.events") (setq a (read s) b nil)))

real time       :     15.739 secs
run-gbc time    :     10.579 secs
child run time  :      0.000 secs
gbc time        :      4.869 secs
NIL

>(setq a nil)

NIL

>(gbc t)

T

>(time (with-open-file (s "/tmp/1000.events") (setq a (read s) b nil)))

real time       :     11.890 secs
run-gbc time    :     10.039 secs
child run time  :      0.000 secs
gbc time        :      1.740 secs
NIL

>(list-length a)

1000

>.

Matt Kaufmann <address@hidden> writes:

> Hi, Camm --
>
> Jared Davis sent me a nice little example, below, which illustrates
> the problem I mentioned (in the message I sent a moment ago) for
> books/centaur/tutorial/alu16-book.lisp.  I can certify this in ACL2(h)
> built on CCL in 2 seconds.  But it stalls out after "End of Pass 1" in
> ACL2(h) built on GCL.  It stalls out even earlier for ACL2 (as opposed
> to ACL2(h)) built on either GCL or CCL, but that's probably not
> surprising, as ACL2 function expansion-alist-pkg-names has an
> optimized definition for ACL2(h).  Maybe your new handling of #n= and
> #n# will solve this for ACL2(h).
>

I don't know if this will solve this problem or not, but I will look
into this small example on a newly built acl2-gcl locally.  It may be
that I should expect a hang here as this is not acl2(h), right?  Do you
have a binary setup at ut for me to look at?  In general, are the acl2
variants now deemed 'no longer experimental' and if so should they be
included in the Debian acl2 package?

Will reply separately to the other issues.

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