From: Camm Maguire <[email protected]> To: Matt Kaufmann <[email protected]> Cc: [email protected], [email protected], [email protected] Subject: Re: [[email protected]: Re: books/centaur/tutorial/alu16-book.lisp] References: <[email protected]> Date: Sat, 11 May 2013 10:58:49 -0400 In-Reply-To: <[email protected]> (Matt Kaufmann's message of "Fri, 3 May 2013 08:16:46 -0500") Message-ID: <[email protected]> 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 <[email protected]> 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 [email protected] ========================================================================== "The earth is but one country, and mankind its citizens." -- Baha'u'llah _______________________________________________ Gcl-devel mailing list [email protected] https://lists.gnu.org/mailman/listinfo/gcl-devel
