[Top][All Lists]
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
[Gcl-devel] Re: apparent property list issue with GCL 2.6.7
From: |
Camm Maguire |
Subject: |
[Gcl-devel] Re: apparent property list issue with GCL 2.6.7 |
Date: |
05 Nov 2007 16:42:41 -0500 |
User-agent: |
Gnus/5.09 (Gnus v5.9.0) Emacs/21.2 |
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
[Prev in Thread] |
Current Thread |
[Next in Thread] |
- [Gcl-devel] Re: apparent property list issue with GCL 2.6.7,
Camm Maguire <=