Matt Kaufmann <[email protected]> writes: > Hi, Camm --
> That looks promising! >> I'm considering merging this into 2.6.10pre. > I didn't notice any mention of a downside, in which case I imagine > you'll do this. If you do, and you want me to test the result with > the development copy of ACL2 (and latest books), let me know. (Or you > can obtain all that here: http://acl2-devel.googlecode.com/) OK, this is pushed, so you can test if you'd like, but please don't go to unnecessary trouble unless interested. Separately, regarding our discussion on runtime vs realtime, your suspicion proved correct -- the gap between the two is larger for gcl. This may be due to calling the external gcc compiler, though I don't really know if your certifications compile stuff. My seafoam results, now showing both real and runtime, are at http://people.debian.org/~camm/acl2/r2.6.10prefi http://people.debian.org/~camm/acl2/rccl1 The fields for the gcl file are: run real #gc gc_time #sgc_off name and for the ccl file are: run real name Comparing runtimes with: join <(awk '{print $6,$1,$2,$3,$4,$5}' r10fi1|sort) \ <(awk '{print $3,$1,$2}' rccl1|sort) | \ awk '{print $2-$7,$0}' | sort -n we get -99.79 books/rtl/rel9/support/lib3.delta1/seed.cert.out 360.85 362.44 83 2083 2 460.64 461.73 -88.82 books/workshops/2013/greve-slind/defung/defung-stress.cert.out 469.07 471.89 48 1375 2 557.89 559.65 -82.63 books/tau/bounders/elementary-bounders.cert.out 863.85 873.20 94 6080 2 946.48 955.64 ... 21.84 books/models/jvm/guard-verified-m1/find-k!.cert.out 54.40 61.09 29 558 2 32.56 32.70 22.26 books/models/jvm/m1/find-k!.cert.out 54.38 60.86 29 557 2 32.12 32.54 32.05 books/centaur/vl/top.cert.out 136.66 162.17 162 4393 2 104.61 111.28 totaling -1603.11 seconds. Comparing realtimes with: join <(awk '{print $6,$1,$2,$3,$4,$5}' r10fi1|sort) \ <(awk '{print $3,$1,$2}' rccl1|sort) | \ awk '{print $3-$8,$0}' | sort -n we get -99.29 books/rtl/rel9/support/lib3.delta1/seed.cert.out 360.85 362.44 83 2083 2 460.64 461.73 -87.76 books/workshops/2013/greve-slind/defung/defung-stress.cert.out 469.07 471.89 48 1375 2 557.89 559.65 -82.44 books/tau/bounders/elementary-bounders.cert.out 863.85 873.20 94 6080 2 946.48 955.64 ... 28.39 books/models/jvm/guard-verified-m1/find-k!.cert.out 54.40 61.09 29 558 2 32.56 32.70 50.89 books/centaur/vl/top.cert.out 136.66 162.17 162 4393 2 104.61 111.28 123.41 books/workshops/2009/sumners/support/kas.cert.out 22.63 164.11 29 374 2 40.33 40.70 totaling 1460.11 seconds. The 'time' output for the whole regression was real 73m16.371s user 450m42.042s sys 16m21.313s for gcl and real 73m10.402s user 433m15.205s sys 9m8.050s for ccl. At least now 1460 ~ (450-433+16-9)*60. (But -1603.11 is not approximately (450-433)*60, as we earlier discussed.) gcl's runtime is via the 'times' system call, and returns the number of 'user' seconds in the calculation. My guess the rest is in 'system' seconds, but there are also times for children reported, though gcl does little forking. Perhaps books/workshops/2009/sumners/support/kas.cert.out might stand out in terms of compiling or other such computation? This is really nothing to fret about, but if I can believe -1603.11, I know I can confine my search to gcc integration and the like, but if (450-433)*60 is more accurate, further work can be done in gcl proper. Take care, -- 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
