Greetings! Is it worth trying to see if the problem persists in 2.6.8pre? If not, how might we proceed? Is this error correlated to anything known at all? If memory serves, last I checked, merely compiling GCL with debugging symbols made the problem vanish.
The logical expectation is that there is an unprotected GC call somewhere in a plist manipulation routine. Is there anyway to exercise just the plist manipulation calls in ACL2 until hopefully the problem might rear its head? Take care, Matt Kaufmann <[EMAIL PROTECTED]> writes: > Hi, Dave and Camm -- > > Just FYI: > > This email is just to document an apparent issue with property lists > in GCL, which seems to hit from time to time, since I just ran across > it today. Unfortunately I've found this problem (assuming it's always > the same one as several times before) to be hard to reproduce reliably > -- in fact Camm, I think you tried once. > > So probably you should both ignore this email, except: > > - Camm, if this rings any bells and you happen to have an > easy-to-install GCL 2.6.7 patch lying around that could help, I'd be > interested in getting it and perhaps even distributing it to other > ACL2 users. > > - Dave, if you have anything to add, feel free -- and if you see weird > errors, it may come down to property lists, and by messing around > you might be able to eliminate them. > > The particular symptom in this case was the error string > > HARD ACL2 ERROR in RECORD-ERROR > > followed by ACL2 breaking because it couldn't actually complete the > error message. But the root cause seems to be a corruption of values > on the property list. ACL2 GETPROP (actually FGETPROP) does a Lisp > GET and then, in essence, an ASSOC. > > This is all in directory aamp7-separation/abstract/ of the Rockwell > books, which unfortunately I can't send to Camm. But I suspect that > the error is impossible to reproduce reliably anyhow... sigh. > > ============================================================ > > Failure (in a fresh ACL2 session): > > (include-book "../functional/fun-pkg") > (include-book "abstract-data") > (certify-book "abstract-fix" 2) > > Success (in a fresh ACL2 session): > > (include-book "mp-ip") > (u) ; undo the above include-book > ; Then execute the three forms above. > > By the way, the following also works in a fresh ACL2 session, which is > rather amazing since superficially it's very similar to the failure > case, since file abstract-fix.acl2 has exactly the three forms of the > failure case. > > (ld "abstract-fix.acl2") > > ============================================================ > > After failure (where the result seems to vary a lot over different > runs): > > ACL2 !>(getprop 'rational-listp > 'forward-chaining-rules > nil > 'current-acl2-world > (w state)) > MV-LET > ACL2 !> > > After success (this is much more what I'd expect): > > ACL2 !>(getprop 'rational-listp > 'forward-chaining-rules > nil > 'current-acl2-world > (w state)) > ((FORWARD-CHAINING-RULE ((:FORWARD-CHAINING RATIONALP-CAR-RATIONAL-LISTP) > . 5459) > (RATIONAL-LISTP X) > ((RATIONAL-LISTP X) X) > ((RATIONALP (CAR X)))) > (FORWARD-CHAINING-RULE > ((:FORWARD-CHAINING RATIONAL-LISTP-FORWARD-TO-TRUE-LISTP) > . 1026) > (RATIONAL-LISTP X) > ((RATIONAL-LISTP X)) > ((TRUE-LISTP X)))) > ACL2 !> > > ============================================================ > > Thanks -- > -- Matt > > > -- 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
