From: Camm Maguire <[email protected]> To: Matt Kaufmann <[email protected]> Cc: [email protected], [email protected], [email protected] Subject: Re: none References: <[email protected]> <[email protected]> Date: Sat, 11 May 2013 18:34:04 -0400 In-Reply-To: <[email protected]> (Matt Kaufmann's message of "Sat, 11 May 2013 10:41:09 -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! Matt Kaufmann <[email protected]> writes: > 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.) > This was an oops, should be fixed now. > 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've been overwriting, apologies. I had tried installing a new tree earlier and ran out of space. > 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 per separate email, I now have the acl2(h) certifying Jared's example with pretty good performance, it seems. > 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? http://qa.debian.org/popcon.php?package=acl2 Take care, > > Thanks -- > -- Matt > Date: Sat, 11 May 2013 10:58:50 -0400 > From: Camm Maguire <[email protected]> > > 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 > > > > > -- 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
