[Gcl-devel] (no subject)

[Matt Kaufmann]

Hi, Camm --

Thanks for the #= improvements!

For ANSI GCL, you fixed with-compilation-unit (as per an email you
sent me on April 26, and indeed, it worked after that), but it seems
to be broken again.  (I did succeed, however, in building ACL2 for
non-ANSI on your new gcl.)

It might be good to save an old version each time you update, for
comparison.  I tried to find your previous GCL from the backups, but
it looks like maybe the system of links has changed; I'm not sure.

Yes, I think you'll need ACL2(h) in order to run Jared's example.
Regarding your question on "a binary setup", I think you're asking for
an ACL2 executable based on ANSI GCL, which is what I was trying to
build when I hit the with-compilation-unit problem.  (If you meant
something else, please let me know.)  As to your question about
inclusion of ACL2 "experimental extensions" in the Debian package, I'm
not sure; I'll start a conversation with relevant people and get back
to you.  Do you have any statistics on how many people have downloaded
Debian packages for ACL2?

Thanks --
-- Matt
   Date: Sat, 11 May 2013 10:58:50 -0400
   From: Camm Maguire <address@hidden>

   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