Raymond Toy wrote:
"Raymond" == Raymond Toy <[EMAIL PROTECTED]> writes:Raymond> Jared C. Davis wrote: >> Hi, >> I'm having trouble reading in files which use a lot of >> structure-sharing abbreviations. For example, here is a typical file >> (490 KB) which has 18,000+ abbreviations. Unfortunately, reading this >> (with "read") takes about 13 minutes in CMUCL 19d on my test machine. >> http://www.cs.utexas.edu/users/jared/Milawa/Sources/ACL2/bootstrap/utilities/proofs/thm-equal-of-booleans-rewrite.proof Raymond> Jared has sent me a patch (for sbcl) which basically works on Raymond> cmucl. For the test case above, it is now read in about 2 sec on my Raymond> test machine. Raymond> Don't know if it's right or not, though. And I haven't tested the Raymond> speed of the reader using hash-tables instead of alists. I've made a few changes to the patch and reading "normal" stuff is as fast as before. Only when reading #1= stuff is there a difference. For the test file above, cmucl takes some 40 minutes to read it. With the patch, it takes 2.8 sec. That's a nice savings!
I'll be checking in these changes shortly. Ray
