gcl-devel
[Top][All Lists]
Advanced

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Gcl-devel] (no subject)


From: Camm Maguire
Subject: [Gcl-devel] (no subject)
Date: Sat, 11 May 2013 18:34:04 -0400
User-agent: Heirloom mailx 12.5 6/20/10

From: Camm Maguire <address@hidden>
To: Matt Kaufmann <address@hidden>
Cc: address@hidden,  address@hidden,  address@hidden
Subject: Re: none
References: <address@hidden>
        <address@hidden>
Date: Sat, 11 May 2013 18:34:04 -0400
In-Reply-To: <address@hidden> (Matt
        Kaufmann's message of "Sat, 11 May 2013 10:41:09 -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!

Matt Kaufmann <address@hidden> 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 <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
>
>
>
>
>

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



reply via email to

[Prev in Thread] Current Thread [Next in Thread]