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 <[email protected]> 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 <[email protected]> > Cc: [email protected] > Date: Sat, 09 Nov 2013 08:24:37 -0500 > > Greetings! > > Matt Kaufmann <[email protected]> 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 <[email protected]> > > Cc: [email protected] > > Date: Sat, 09 Nov 2013 00:04:03 -0500 > > > > Greetings! > > > > Matt Kaufmann <[email protected]> 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 > [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 > > > > > -- 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
