Greetings! Matt Kaufmann <[EMAIL PROTECTED]> writes:
> Howdy -- > > >> Somewhere I think > >> you guys have some old timings using both regular and Schelter mv -- > >> are these comparable to gcl today with autoproclamations off (or also > >> hopefully on?) > > If I have such timings for a given GCL, I don't know where they are. But for > any given GCL, it's easy enough to come up with such timings. What's harder > for me is to compare two different GCLs. I don't build GCL very often; I tend > to use what's available. If you care to build two CLtL1 GCLs that you'd like > compared (2.6.7 vs. 2.7.0) with the same (or appropriately corresponding > parameters), then I could build and run stock ACL2 3.0 (with Schelter mv) on > top of each and also ordinary mv on top of each. > > Now I'll turn to today's results, which compare what I used to call #2 and #3 > on the HONS version of ACL2 3.0. It looks like ACL2-generated declaiming is > more efficient than what GCL generates, at least for these runs. > > With the usual ACL2-generated declaiming, from > /projects/hvg/ACL2/v3-0-hons-jun25/acl2-proclaims.lisp, and with: > (setq compiler::*compiler-auto-proclaim* nil si::*disable-recompile* t): > /projects/hvg/ACL2/v3-0-hons-jun25/make-regression.log: > 16925.205u 434.179s 4:55:01.49 98.0% 0+0k 0+0io 13pf+0w > > Turning off ACL2-generated declaiming, but with default values of > compiler::*compiler-auto-proclaim* (t) and > si::*disable-recompile* (nil): > /projects/hvg/ACL2/v3-0-hons-gcl-proclaim/make-regression.log: > 17808.712u 560.627s 5:09:51.50 98.8% 0+0k 0+0io 0pf+0w Thank you so much for this! This confirms my basic suspicions -- that we might be off 5 to 10% or so on the proclamations, but that the bulk of the issue lies elsewhere. I don't suppose you have gc time broken out. Next step for me is to compile a gprof image at some point and run under that. > Perhaps the difference is due to image sizes (about a factor of 4): > > sundance:~> ls -l /projects/hvg/ACL2/v3-0-hons-jun25/saved_acl2.gcl > -rwxrwxr-x 1 kaufmann hvg 204745243 Jun 25 09:23 > /projects/hvg/ACL2/v3-0-hons-jun25/saved_acl2.gcl > sundance:~> ls -l /projects/hvg/ACL2/v3-0-hons-gcl-proclaim/saved_acl2.gcl > -rwxrwxr-x 1 kaufmann hvg 208157211 Jun 25 15:03 > /projects/hvg/ACL2/v3-0-hons-gcl-proclaim/saved_acl2.gcl > sundance:~> ls -l /projects/acl2/v3-0-linux/gcl-saved_acl2.gcl > -r-xr-xr-x 1 kaufmann acl2 50606495 May 29 01:41 > /projects/acl2/v3-0-linux/gcl-saved_acl2.gcl > sundance:~> > I thought the image size was down to about 80Mb or so? This is also illustative in that keeping the function source around is on the order of 2% in size. I take it swap is not an issue (as indicated in your 0+0io above) I can't see why size per se would slow things down -- in general more space speeds things up. Take care, > -- Matt > Cc: [EMAIL PROTECTED] > From: Camm Maguire <[EMAIL PROTECTED]> > Date: 25 Jun 2006 20:35:14 -0400 > X-SpamAssassin-Status: No, hits=-2.5 required=5.0 > X-UTCS-Spam-Status: No, hits=-240 required=200 > > Greetings! > > Matt Kaufmann <[EMAIL PROTECTED]> writes: > > > Bob, Camm -- > > > > I can re-run any regressions you like. And, I'd like to build one > version that > > has as little new stuff as possible, and that we can leave in place for > awhile, > > so that UT students Sol, David, and Serita can comfortably use it (and > Warren > > and Bob too). > > > > Great! All I was after is some idea of whether the gcl > autoproclamations have slowed things down, and if so by how much. So > your #2 and #3 last time around are of most interest. > > I also know that there is some slowdown associated with regular mv. > What I'd like to know is whether there is any other slowdown that > cannot be accounted for either in mv or autoproclamation -- i.e. have > I done anything else recently to kill performance. Somewhere I think > you guys have some old timings using both regular and Schelter mv -- > are these comparable to gcl today with autoproclamations off (or also > hopefully on?) > > I get the rough idea that we're 50% slower than the fastest 2.7 we've > tested. I think its great to leave an xg around for a while in a semi > stable state. If you'd like, we can tag in cvs any state you find > particularly useful. It is just that at present we're in the middle > of this autoproclamation stuff, and things always get a little worse > right after something this new is introduced. As long as people > understand that I'm ok. > > So many little things to worry about -- e.g. currently we store > function comments in the function source, which is not compressed in > the fasd format -- I imagine this is quite big in acl2's case, and can > easily be ommitted. > > Finally, I think I have a plan now re: mv fast-linking and mutual > recursion. I won't commit for some considerable time, and will let > you know when its ready. If anyone is interested I can describe, but > I don't expect any takers! > > Take care, > > > So here's what I propose: > > > > A. (Like #3 in my email 23 Jun 2006 10:46:17) build in > > /projects/hvg/ACL2/v3-0-hons/, making full use of ACL2 proclaiming, but > with > > GCL auto-proclaim turned off. The only modification I'll make to the > ACL2 > > sources is this: > > > > (setq compiler::*compiler-auto-proclaim* nil si::*disable-recompile* > t) > > > > B. (Like #2 in my email 23 Jun 2006 10:46:17) I'll build in > > /projects/hvg/ACL2/v3-0-hons-gcl-proclaim/, relying on GCL to do its > > auto-proclaims (with no ACL2 proclaiming). > > > > C. Bob, it would be great if you'd keep /p/bin/xg unchanged till that's > > completed (at which time I'll send email). > > > > D. I'll delete or smash these at any time: > > > > /projects/hvg/ACL2/v3-0-hons-no-acl2-proclaim/ > > /projects/hvg/ACL2/v3-0-hons-no-gcl-proclaim/ > > /projects/hvg/ACL2/v3-0-hons-matt-backup/ > > > > (Camm, are you done with /v/filer3/v0q048/acl2/v3-0-debian/?) > > > > OK with you both? Should I do any of this with > si::*optimize-maximum-pages* > > on and avoid all explicit allocation?? If so, should I do so instead or > in > > addition to the existing approach of si::*optimize-maximum-pages* nil > with > > explicit allocation? > > > > Thanks -- > > --- Matt > > Date: Sat, 24 Jun 2006 19:25:07 -0500 > > From: Robert Boyer <[EMAIL PROTECTED]> > > Cc: [EMAIL PROTECTED] > > > > I have rebuilt /p/bin/xg and I have some evidence that you > > will be able to get further with the regression that you > > were last having trouble with, viz., I executed the text > > below with this new /p/bin/xg, and it no longer caused that > > weird error message in the compilation of axioms.lisp. > > However, I'm not sure I understood the bug or the fix. > > > > We now face some questions. 1. Should you now re-run all > > three of those regressions on your machine with the new > > /p/bin/xg to get more reliable data? 2. Should I leave the > > new xg as is until you are done with this? Please advise. > > No hurry. If there are further problems, please cc me and > > I'll try to work on them. > > > > Bob > > > > cd /u/boyer/acl2/acl2-sources > > xg > > (setq compiler::*default-c-file* t) > > (setq compiler::*compiler-auto-proclaim* nil) > > (setq si::*disable-recompile* t) > > (load "init.lisp") > > (in-package "ACL2") > > (load "axioms.lisp") > > (proclaim-file "axioms.lisp") > > (compile-file "axioms.lisp") > > > > > > > > > > -- > 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 Gcl-devel@gnu.org http://lists.gnu.org/mailman/listinfo/gcl-devel
