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
Jared has sent me a patch (for sbcl) which basically works on cmucl.
For the test case above, it is now read in about 2 sec on my test machine.
Don't know if it's right or not, though. And I haven't tested the speed
of the reader using hash-tables instead of alists.
Ray
