Your message dated Sat, 07 Oct 2006 16:37:10 -0400
with message-id <[EMAIL PROTECTED]>
and subject line Bug#381477: acl2: amd64 build succeeds with current gcl
(2.6.7-22)
has caused the attached Bug report to be marked as done.
This means that you claim that the problem has been dealt with.
If this is not the case it is now your responsibility to reopen the
Bug report if necessary, and/or fix the problem forthwith.
(NB: If you are a system administrator and have no idea what I am
talking about this indicates a serious mail system misconfiguration
somewhere. Please contact me immediately.)
Debian bug tracking system administrator
(administrator, Debian Bugs database)
--- Begin Message ---
Package: acl2
Version: 3.0.1-1
Severity: serious
Hi,
Your package is failing to build on amd64 with the following
error:
HARD ACL2 ERROR in RECORD-ERROR: An attempt was made to treat NIL
as a record of type REWRITE-RULE.
ACL2 Error in CERTIFY-BOOK: Evaluation aborted. See :DOC wet for
how you might be able to get an error backtrace.
Summary
Form: (CERTIFY-BOOK "arithmetic-theory" ...)
Rules: ((:COMPOUND-RECOGNIZER ZIP-COMPOUND-RECOGNIZER)
(:DEFINITION ARITH-COLLECT-*)
(:DEFINITION EVENP)
(:DEFINITION FIX)
(:DEFINITION NOT)
(:DEFINITION SYNP)
(:EXECUTABLE-COUNTERPART BINARY-*)
(:EXECUTABLE-COUNTERPART EQUAL)
(:EXECUTABLE-COUNTERPART EXPT)
(:EXECUTABLE-COUNTERPART INTEGERP)
(:EXECUTABLE-COUNTERPART NOT)
(:EXECUTABLE-COUNTERPART UNARY--)
(:EXECUTABLE-COUNTERPART UNARY-/)
(:FAKE-RUNE-FOR-TYPE-SET NIL)
(:REWRITE |(* x (if a b c))|)
(:REWRITE |(+ y x)|)
(:REWRITE |(- (if a b c))|)
(:REWRITE |(equal (- x) (- y))|)
(:REWRITE |(equal (- x) 0)|)
(:REWRITE |(equal (if a b c) x)|)
(:REWRITE |(expt (- x) n)|)
(:REWRITE DEFAULT-EXPT-1)
(:REWRITE DEFAULT-UNARY-MINUS)
(:REWRITE TEMP510)
(:REWRITE |arith (* x (- y))|)
(:REWRITE |arith (* y x)|)
(:REWRITE |arith (- (- x))|)
(:REWRITE |arith (expt 0 n)|)
(:REWRITE |arith (expt x (+ m n))|)
(:REWRITE |arith (expt x (- n))|)
(:REWRITE |arith (expt x 0)|))
Warnings: None
Time: 0.02 seconds (prove: 0.02, print: 0.00, other: 0.00)
******** FAILED ******** See :DOC failure ******** FAILED ********
ACL2 !>
Exiting the ACL2 read-eval-print loop. To re-enter, execute (LP).
ACL2>******************************************************************************
Build finished at 20060803-1733
FAILED [dpkg-buildpackage died]
Kurt
--- End Message ---
--- Begin Message ---
Kurt Roeckx requeued the package, which built this time around, so
this bug can be closed.
--
Aaron M. Ucko, KB1CJC (amu at alum.mit.edu, ucko at debian.org)
Finger [EMAIL PROTECTED] (NOT a valid e-mail address) for more info.
--- End Message ---
