[Gcl-devel] Re: apparent property list issue with GCL 2.6.7

[Camm Maguire]

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 <address@hidden> 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                                            address@hidden
==========================================================================
"The earth is but one country, and mankind its citizens."  --  Baha'u'llah