Re: [Gcl-devel] address@hidden: Re: lstat]

[Camm Maguire]

Greetings, and thanks!  Looking into it now.  In case you run a check
again, try disabling sgc and see if the problem goes away.

Take care,

Matt Kaufmann <address@hidden> writes:

> Hi, Camm --
>
> Thanks very much for rebuilding /p/bin/gcl-2.6.10pre.
>
> Unfortunately, I'm still seeing a problem -- almost surely because I'm
> using the latest svn copy of ACL2 and the books, and the so-called
> "GL" books pertaining to this example have changed a lot after the
> release of ACL2 Version 6.3 (which I'm guessing is what you're using).
>
> I just killed an attempt to certify books/centaur/gl/solutions.lisp
> (with the no-gcl restriction removed for the final form, "1f").
> It had been running on a reasonably fast machine for more than 4 1/2
> hours.  Allegro CL recently did the example in about 5.5 minutes, so
> the increase in time isn't solely due to either the CCL-specific
> optimizations in the "(h)" part of ACL2(h) or the fact that CCL
> compiles on the fly.  I don't know if hashing is a cause.
>
> You can play in this directory at UT CS if you like:
>
> /projects/acl2/test-nov9/
>
> See file README-camm in that directory for how to proceed
> interactively.  (If not interested, please let me know and I'll delete
> the directory.)
>
> I'll let the GL author know what's up in case he has any ideas.
>
> Thanks --
> -- Matt
>    From: Camm Maguire <address@hidden>
>    Cc: address@hidden
>    Date: Sat, 09 Nov 2013 08:24:37 -0500
>
>    Greetings!
>
>    Matt Kaufmann <address@hidden> writes:
>
>    > Hi, Camm --
>    >
>    > I don't seem to have access to that gcl:
>    >
>    >   sloth:~% ~/camm/git/gcl/gcl/bin/gcl
>    >   /u/kaufmann/camm/git/gcl/gcl/bin/gcl: Command not found.
>    >   sloth:~% 
>    >
>    > Perhaps you'd be willing to rebuild /p/bin/gcl-2.6.10pre at UT CS, to
>    > work as CLtL1 or (especially) ANSI -- then I'll just use that.  (I
>    > think Gordon Novak would appreciate it too.)
>    >
>
>    Great!  Done.
>
>    > That's great about the progress on hash tables.
>    >
>
>    We're still at ~3min and change, and ccl might still have an edge --
>    have not checked on the same machine.  It does appear that this job is
>    placing complex conses in compiled files.  We've put in a memoized
>    hash-equal for this purpose, but we flush the table on each
>    compile-file.  This flush might not be right, though I can't think of
>    anything better right now.  I was wondering if you could ask the authors
>    how other lisps might handle such things, in case they might know.
>
>    Take care,
>
>    > Thanks --
>    > -- Matt
>    >    From: Camm Maguire <address@hidden>
>    >    Cc: address@hidden
>    >    Date: Sat, 09 Nov 2013 00:04:03 -0500
>    >
>    >    Greetings!
>    >
>    >    Matt Kaufmann <address@hidden> writes:
>    >
>    >    > Hi, Camm --
>    >    >
>    >    > I'm glad you got a better time result.
>    >    >
>    >    > I notice that
>    >    > /v/filer4b/v11q001/acl2/camm-09-19/svn/acl2-devel/saved_acl2h was
>    >    > built on top of a GCL 2.6.10 ANSI dated Nov. 8.  I think my run was
>    >    > with one built Nov. 1.  Can you send me a path to your Nov. 8 build?
>    >    > Then I can try to re-create your result independently.  With luck,
>    >    > I'll get the same result and we can figure that you made some nice
>    >    > improvement during that week, or maybe some evil computer gnomes
>    >    > decided to stop messing with us!
>    >    >
>    >
>    >    saved_acl2h.gcl.ndbg was built off the nov 1 gcl installed as
>    >    /p/bin/gcl-2.6.10pre.  My debugging (and other experimental) gcls used
>    >    for the other tests is at ~/camm/git/gcl/gcl/bin/gcl.
>    >
>    >
>    >    > Regarding your question: I think ACL2(h) uses mostly EQL has tables
>    >    > but has EQ and EQUAL hash tables as well.  You could ask Jared to
>    >    > elaborate if you like (I'm not yet up to speed on the "(h)" part).
>    >
>    >    Yes, this I've since gathered.  Here is the key profiling section:
>    >
>    >    [2]     97.7 1456.60  162.36 240851473         gethash <cycle 2> [2]
>    >           159.25    0.00 2204624309/2216894685     eql1 [5]
>    >             3.04    0.00 498452497/498457020     hash_eql [22]
>    >             0.00    0.06   39822/45668       ihash_equal [136]
>    >             0.00    0.00   19527/3180596     equal1 [40]
>    >             0.00    0.00   19220/8213633     string_eq [118]
>    >
>    >
>    >    This suggested the gethash loop itself needed work, and perhaps that 
> the
>    >    keys weren't distributed optimally, with ~10 eql calls per gethash.
>    >    Backporting a few more ideas from master, I now get 
>    >
>    >    ; 259.47 seconds realtime,
>    >    ; 228.38 seconds runtime, 9.30 seconds child runtime,
>    >    ; 4.94 seconds systime, 3.42 seconds child systime.
>    >
>    >
>    >    with the bottleneck at
>    >
>    >    [4]     89.2  428.53  188.98 240857323         fShash_equal <cycle 2> 
> [4]
>    >           186.29    0.00 1393416127/1405686504     eql1 [5]
>    >             2.60    0.00 498452501/498457024     hash_eql [23]
>    >
>    >    I'll let you know if/when this gets pushed ...
>    >
>    >    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
>
>
>
>
>

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