[Top][All Lists]
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: [Gcl-devel] Re: [Axiom-developer] Axiom May 2010 release
|
From: |
Matt Kaufmann |
|
Subject: |
Re: [Gcl-devel] Re: [Axiom-developer] Axiom May 2010 release |
|
Date: |
Mon, 27 Sep 2010 15:37:54 -0500 |
Hi, Camm --
I just did a quick check, and I didn't notice any "bad plist" sort of
error in the 7 GCL-based ACL2 regression logs I looked at that
occurred since installing that new ACL2 thingamobob in, I think, late
March. That's not a lot of runs runs, so I'm not sure what kind of
proof we have here, but I'm happy to go with the assumption that the
problem is history!
Thanks again --
-- Matt
Cc: address@hidden
From: Camm Maguire <address@hidden>
Date: Mon, 27 Sep 2010 11:50:39 -0400
X-SpamAssassin-Status: No, hits=3.7 required=5.0
X-UTCS-Spam-Status: No, hits=-3 required=165
Greetings!
Matt Kaufmann <address@hidden> writes:
> That's really great news! This "Bad plist" error may have been the
> only unreliable aspect of GCL that I've encountered in many years, and
> it was frustrating at times.
>
Good to hear this may be of value.
>>> If you happen to
>>> have any old binary test case lying around, try running it without
>>> fast-links set, and then with (si::use-fast-links
>>> nil)(si::use-fast-links t).
>
> Sadly, I don't. But even if I did, I'm not sure it would do any good
> -- my sense was that the errors were stored in already-miscompiled
> files, and that a new GCL image would probably solve any particular
> instance of the problem even if the bug were still there.
>
>>> I'll push this fix to ut in a bit if you are interested.
>
> Absolutely! Feel free to overwrite what you recently installed at UT
> CS.
>
OK, this is done for 32bit and 64bit via the /p/bin/gcl-2.6.8pre-big
link. I did not update the /p/bin/gcl-2.6.8pre-small (32bit only) and
was thinking of removing it. This is the official Debian/Ubuntu
package, and only differs from the big in having 1/4 the number of
maxpages. But my sense is that this is not particularly important to
you, true? Please let me know if I should wipe this or update it.
> By the way, several months ago we changed how ACL2 loaded compiled
> files (released in early July with ACL2 4.0), in such a manner as to
> make it much less common that we would smash the definition of a
> function. In essence, a load first arranges to save old
> symbol-functions, which are then restored after the file is loaded.
> Maybe that explains why I don't recall seeing this error so much in
> recent months.
If you can correlate these two, that would definitely be indicative of
the bug just fixed. I.e. there was nothing plist specific in this
change, only that gcl erroneously ended up changing pointers in memory
previously used by code but subsequently gc'ed and used by something
else, at the time when the code pointed to by said pointer was also
modified. Only when fast-links were on. This made me think of this
error as the corruption appeared random when I looked at it last,
i.e. not traceable by any defineable function call path, as it would
if this were the case.
>
> Thanks again -- wow.
>
My pleasure. Take care,
> -- Matt
> cc: address@hidden
> From: Camm Maguire <address@hidden>
> Date: Fri, 24 Sep 2010 16:39:46 -0400
> X-SpamAssassin-Status: No, hits=4.7 required=5.0
> X-UTCS-Spam-Status: No, hits=-85 required=165
>
> Greetings!
>
> Regarding this old issue which has suffered from exacerbating
> irreproducibility -- I think I might have fixed it. If you happen to
> have any old binary test case lying around, try running it without
> fast-links set, and then with (si::use-fast-links
> nil)(si::use-fast-links t). If this clears the issue, I'd be most
> pleased to hear it.
>
> I've just found and fixed a long standing bug regarding fast-linking
> and gc of old loaded .o files (subsequently replaced with newer
> functions of the same name elsewhere). There was a possibility that
> an old file containing a live fast link could be reset when its target
> was redefined, even if the file had already been gc'ed and used for
> other data.
>
> Here's a form showing the error:
>
> (dotimes (i 100) (dolist (l '(cmptype cmpeval cmpvar cmpwt cmpif cmplet
cmptag cmpinline cmpenv cmplam cmptop
> cmpbind cmpblock cmpcall cmpcatch cmpflet cmpfun
cmplabel cmploc cmpmap
> cmpmulti cmpspecial cmputil cmpvs cmpmain))
> (time (load (compile-file
> (concatenate 'string "../cmpnew/gcl_" (string-downcase
(string l)) ".lsp")
> :c-file t :h-file t :data-file t :system-p t)))))
>
> I'll push this fix to ut in a bit if you are interested.
>
> Take care,
>
> Matt Kaufmann <address@hidden> writes:
>
> > Hi, Camm --
> >
> > The "Bad plist" error is something we've had emails about over the
> > years, and sigh, I think we both gave up. It seems horribly difficult
> > to reproduce, and I'm pretty sure that it's usually the result of some
> > corruption of a previously compiled file (from an earlier book
> > certification). My guess is that if you change something --
> > e.g. build GCL with a different max_pages -- and then try again from
> > scratch (i.e., after "make clean-books" or using "make
> > regression-fresh"), then that error will disappear, though maybe
> > you'll get a "Bad plist" somewhere else.
> >
> > I think I've tried various things, such as compiling with safety 2,
> > but to no avail. Actually, you could try that and see (but again,
> > you'll have to get rid of existing compiled files from certified
> > books, which I think contain at least one that is already corrupted).
> > Safety 3 probably won't work because we need tail recursion
> > elimination.
> >
> > I wish I could be more helpful! But this "Bad plist" problem has
> > seemed intractable to me! Maybe you'll have some idea. At least you
> > can reproduce it!
> >
> > Gotta run -- my wife will be here to pick me up shortly....
> >
> > -- Matt
> > From: Camm Maguire <address@hidden>
> > Date: Sun, 06 Jun 2010 19:24:35 -0400
> > X-MagicMail-UUID: b5682c3c-71c2-11df-9b4b-000c29c6406d
> > X-SpamAssassin-Status: No, hits=-0.7 required=5.0
> > X-UTCS-Spam-Status: No, hits=-146 required=165
> >
> > Greetings!
> >
> > Argh, 3.6.1 issue below -- any ideas? Do I have insufficient
memory
> > of a sudden?
> >
> > address@hidden:~/debian/acl2/acl2-3.6.1/books/rtl/rel8/support$
make
> > make[1]: Entering directory
`/home/camm/debian/acl2/acl2-3.6.1/books/rtl/rel8/support/support'
> > Using ACL2=../../../../../saved_acl2
> > make -s -f Makefile mod4.cert add3-proofs.cert add3.cert
all-ones.cert ash.cert bias-proofs.cert bias.cert bitn.cert
bitn-proofs.cert bits.cert bits-proofs.cert bvecp-proofs.cert bvecp.cert
bvecp-helpers.cert bvecp-lemmas.cert ocat.cert lnot-proofs.cert lnot.cert
decode-proofs.cert decode.cert encode.cert fast-and.cert ground-zero.cert
ireps.cert log-proofs.cert log.cert land0-proofs.cert land0.cert
lextra-proofs.cert lextra0.cert lextra.cert cat-proofs.cert cat.cert
cat-def.cert lior0-proofs.cert lior0.cert logand.cert logand-proofs.cert
logeqv.cert logior-proofs.cert logior.cert logior1-proofs.cert logior1.cert
lognot.cert logorc1.cert logs.cert logxor.cert lop1-proofs.cert lop1.cert
lop2-proofs.cert lop2.cert lop3-proofs.cert lop3.cert lxor0-proofs.cert
lxor0.cert float.cert sumbits.cert merge.cert model-helpers.cert
badguys.cert mulcat-proofs.cert mulcat.cert rewrite-theory.cert rnd.cert
rom-he!
lpers!
> .cert!
> > rtl.cert rtlarr.cert setbits-proofs.cert setbits.cert
setbitn-proofs.cert setbitn.cert shft.cert sgn.cert
simple-loop-helpers.cert sticky-proofs.cert sticky.cert trunc-proofs.cert
trunc.cert bits-trunc-proofs.cert bits-trunc.cert away-proofs.cert
away.cert near-proofs.cert near.cert near+-proofs.cert near+.cert
oddr-proofs.cert oddr.cert rnd.cert util.cert log-equal.cert lop1.cert
lop2.cert lop3.cert ereps-proofs.cert ereps.cert ireps.cert
stick-proofs.cert stick.cert drnd-original.cert merge2.cert fadd.cert
clocks.cert openers.cert package-defs.cert simplify-model-helpers.cert
top1.cert land.cert lior.cert lxor.cert guards.cert fadd-extra.cert
fadd-extra0.cert float-extra.cert round-extra.cert top.cert
INHIBIT='(set-inhibit-output-lst (list (quote prove) (quote proof-tree) (quote
warning) (quote observation) (quote event) (quote expansion)))'
ACL2='../../../../../saved_acl2'
> > make[2]: Entering directory
`/home/camm/debian/acl2/acl2-3.6.1/books/rtl/rel8/support/support'
> > Making
/home/camm/debian/acl2/acl2-3.6.1/books/rtl/rel8/support/support/lextra.cert on
Sun Jun 6 23:19:17 UTC 2010
> > ls: cannot access lextra.cert: No such file or directory
> > **CERTIFICATION FAILED** for
/home/camm/debian/acl2/acl2-3.6.1/books/rtl/rel8/support/support/lextra.lisp
> >
> > | Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
> > | BVECP-TAU
> > |
> > | Summary
> > | Form: ( DEFTHM TOP-THM-2 ...)
> > | Rules: ((:COMPOUND-RECOGNIZER NATP-COMPOUND-RECOGNIZER)
> > | (:DEFINITION NATP)
> > | (:DEFINITION NOT)
> > | (:FAKE-RUNE-FOR-TYPE-SET NIL)
> > | (:REWRITE LIOR-IS-LIOR0)
> > | (:REWRITE LXOR-IS-LXOR0))
> > | Warnings: None
> > | Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
> > | TOP-THM-2
> > |
> > | Summary
> > | Form: ( DEFTHM TOP-THM-3 ...)
> > | Rules: ((:COMPOUND-RECOGNIZER NATP-COMPOUND-RECOGNIZER)
> > | (:DEFINITION NATP)
> > | (:DEFINITION NOT)
> > | (:FAKE-RUNE-FOR-TYPE-SET NIL)
> > | (:REWRITE LAND-IS-LAND0)
> > | (:REWRITE LXOR-IS-LXOR0))
> > | Warnings: None
> > | Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
> > | TOP-THM-3
> > |
> > | Summary
> > | Form: ( DEFTHM LOP-THM-1 ...)
> > | Rules: ((:DEFINITION =)
> > | (:DEFINITION NOT)
> > | (:REWRITE A2)
> > | (:REWRITE LIOR-IS-LIOR0))
> > | Warnings: None
> > | Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
> > | LOP-THM-1
> > |
> > | Summary
> > | Form: ( DEFUN LAMT ...)
> > | Rules: ((:TYPE-PRESCRIPTION LXOR-NONNEGATIVE-INTEGER-TYPE))
> > | Warnings: None
> > | Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
> > | LAMT
> > |
> > | Summary
> > | Form: ( DEFUN LAMG ...)
> > | Rules: ((:TYPE-PRESCRIPTION LAND-NONNEGATIVE-INTEGER-TYPE))
> > | Warnings: None
> > | Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
> > | LAMG
> > |
> > | Summary
> > | Form: ( DEFUN LAMZ ...)
> > | Rules: ((:TYPE-PRESCRIPTION LNOT))
> > | Warnings: None
> > | Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
> > | LAMZ
> > |
> > | Summary
> > | Form: ( DEFUN LAM1 ...)
> > | Rules: ((:TYPE-PRESCRIPTION LAND-NONNEGATIVE-INTEGER-TYPE))
> > | Warnings: None
> > | Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
> > | LAM1
> > |
> > | Summary
> > | Form: ( DEFUN LAM2 ...)
> > | Rules: ((:TYPE-PRESCRIPTION LAND-NONNEGATIVE-INTEGER-TYPE))
> > | Warnings: None
> > | Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
> > | LAM2
> > |
> > | Summary
> > | Form: ( DEFUN LAM3 ...)
> > | Rules: ((:TYPE-PRESCRIPTION LAND-NONNEGATIVE-INTEGER-TYPE))
> > | Warnings: None
> > | Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
> > | LAM3
> > |
> > | Summary
> > | Form: ( DEFUN LAM4 ...)
> > | Rules: ((:TYPE-PRESCRIPTION LAND-NONNEGATIVE-INTEGER-TYPE))
> > | Warnings: None
> > | Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
> > | LAM4
> > |
> > | Summary
> > | Form: ( DEFUN LAM0 ...)
> > | Rules: ((:TYPE-PRESCRIPTION LIOR-NONNEGATIVE-INTEGER-TYPE))
> > | Warnings: None
> > | Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
> > | LAM0
> > |
> > | Summary
> > | Form: ( DEFUN LAMB ...)
> > | Rules: ((:FAKE-RUNE-FOR-TYPE-SET NIL)
> > | (:TYPE-PRESCRIPTION INTEGERP-PROD)
> > | (:TYPE-PRESCRIPTION LAM0)
> > | (:TYPE-PRESCRIPTION LNOT))
> > | Warnings: None
> > | Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
> > | LAMB
> > | [SGC for 12105 CONS pages..(19920 writable)..(T=6).GC
finished]
> > | [SGC for 12105 CONS pages..(19933 writable)..(T=6).GC
finished]
> > | [SGC for 12105 CONS pages..(19933 writable)..(T=7).GC
finished]
> > | [SGC for 17096 CONS pages..(24975 writable)..(T=9).GC
finished]
> > |
> > | Summary
> > | Form: ( DEFTHM LOP-THM-2 ...)
> > | Rules: ((:COMPOUND-RECOGNIZER NATP-COMPOUND-RECOGNIZER)
> > | (:COMPOUND-RECOGNIZER ZIP-COMPOUND-RECOGNIZER)
> > | (:DEFINITION =)
> > | (:DEFINITION ABS)
> > | (:DEFINITION EXPT)
> > | (:DEFINITION FIX)
> > | (:DEFINITION LAM0)
> > | (:DEFINITION LAM0-0)
> > | (:DEFINITION LAM1)
> > | (:DEFINITION LAM1-0)
> > | (:DEFINITION LAM2)
> > | (:DEFINITION LAM2-0)
> > | (:DEFINITION LAM3)
> > | (:DEFINITION LAM3-0)
> > | (:DEFINITION LAM4)
> > | (:DEFINITION LAM4-0)
> > | (:DEFINITION LAMB)
> > | (:DEFINITION LAMB-0)
> > | (:DEFINITION LAMG)
> > | (:DEFINITION LAMG-0)
> > | (:DEFINITION LAMT)
> > | (:DEFINITION LAMT-0)
> > | (:DEFINITION LAMZ)
> > | (:DEFINITION LAMZ-0)
> > | (:DEFINITION MIN)
> > | (:DEFINITION NOT)
> > | (:DEFINITION SYNP)
> > | (:EXECUTABLE-COUNTERPART BINARY-*)
> > | (:EXECUTABLE-COUNTERPART BINARY-+)
> > | (:EXECUTABLE-COUNTERPART BINARY-LAND0)
> > | (:EXECUTABLE-COUNTERPART BINARY-LIOR0)
> > | (:EXECUTABLE-COUNTERPART BINARY-LXOR0)
> > | (:EXECUTABLE-COUNTERPART EQUAL)
> > | (:EXECUTABLE-COUNTERPART EXPT-EXECUTE)
> > | (:EXECUTABLE-COUNTERPART FIX)
> > | (:EXECUTABLE-COUNTERPART FL)
> > | (:EXECUTABLE-COUNTERPART LNOT)
> > | (:EXECUTABLE-COUNTERPART NOT)
> > | (:EXECUTABLE-COUNTERPART UNARY--)
> > | (:FAKE-RUNE-FOR-TYPE-SET NIL)
> > | (:META CANCEL_PLUS-EQUAL-CORRECT)
> > | (:REWRITE A2)
> > | (:REWRITE A4)
> > | (:REWRITE A5)
> > | (:REWRITE BITN-LXOR0)
> > | (:REWRITE BITS-LAND0)
> > | (:REWRITE BITS-LIOR0)
> > | (:REWRITE BITS-LNOT)
> > | (:REWRITE BITS-LXOR0)
> > | (:REWRITE BITS-WITH-INDICES-IN-THE-WRONG-ORDER)
> > | (:REWRITE COLLECT-CONSTANTS-IN-<-OF-SUMS)
> > | (:REWRITE COLLECT-CONSTANTS-IN-<-OF-SUMS-2)
> > | (:REWRITE COMMUTATIVITY-OF-+)
> > | (:REWRITE DUMB)
> > | (:REWRITE EXPO-BOUND-ERIC)
> > | (:REWRITE EXPO-COMPARISON-REWRITE-TO-BOUND)
> > | (:REWRITE EXPO-COMPARISON-REWRITE-TO-BOUND-2)
> > | (:REWRITE EXPT-EXECUTE-REWRITE)
> > | (:REWRITE INTEGERP-<-NON-INTEGERP)
> > | (:REWRITE LAND-COMMUTATIVE)
> > | (:REWRITE LAND-IS-LAND0)
> > | (:REWRITE LAND0-0)
> > | (:REWRITE LAND0-ASSOCIATIVE)
> > | (:REWRITE LAND0-COMMUTATIVE)
> > | (:REWRITE LAND0-COMMUTATIVE-2)
> > | (:REWRITE LAND0-X-Y-0)
> > | (:REWRITE LIOR-IS-LIOR0)
> > | (:REWRITE LIOR0-COMMUTATIVE)
> > | (:REWRITE LIOR0-COMMUTATIVE-2)
> > | (:REWRITE LXOR-IS-LXOR0)
> > | (:REWRITE MOVE-NEGATIVE-CONSTANT-1)
> > | (:REWRITE UNICITY-OF-0)
> > | (:REWRITE ZIP-OPEN)
> > | (:TYPE-PRESCRIPTION A14 . 2)
> > | (:TYPE-PRESCRIPTION EXPO-INTEGER-TYPE)
> > | (:TYPE-PRESCRIPTION EXPO-OF-INTEGER-TYPE)
> > | (:TYPE-PRESCRIPTION INTEGERP-PROD)
> > | (:TYPE-PRESCRIPTION LNOT)
> > | (:TYPE-PRESCRIPTION NONNEG-+-TYPE)
> > | (:TYPE-PRESCRIPTION RATIONALP-EXPT-TYPE-PRESCRIPTION))
> > | Warnings: None
> > | Time: 9.60 seconds (prove: 9.59, print: 0.01, other: 0.00)
> > | LOP-THM-2
> > |
> > | Summary
> > | Form: ( DEFTHM LAND-GEN-0-COR ...)
> > | Rules: ((:DEFINITION =)
> > | (:DEFINITION NOT)
> > | (:REWRITE LAND-IS-LAND0))
> > | Warnings: None
> > | Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
> > | LAND-GEN-0-COR
> > |
> > | Summary
> > | Form: ( IN-THEORY (E/D ...))
> > | Rules: NIL
> > | Warnings: None
> > | Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
> > | 3072
> > | [SGC for 17096 CONS pages..(25142 writable)..(T=9).GC
finished]
> > | [SGC for 451 CFUN pages..(25246 writable)..(T=6).GC finished]
> > | [SGC for 451 CFUN pages..(25246 writable)..(T=7).GC finished]
> > |
> > | Summary
> > | Form: ( DEFTHM LXOR-IS-LIOR ...)
> > | Rules: ((:COMPOUND-RECOGNIZER ZP-COMPOUND-RECOGNIZER)
> > | (:DEFINITION BINARY-LAND)
> > | (:DEFINITION BINARY-LIOR)
> > | (:DEFINITION BINARY-LXOR)
> > | (:DEFINITION FIX)
> > | (:DEFINITION IFF)
> > | (:DEFINITION MOD)
> > | (:DEFINITION NOT)
> > | (:DEFINITION SYNP)
> > | (:EXECUTABLE-COUNTERPART BINARY-*)
> > | (:EXECUTABLE-COUNTERPART BINARY-LAND)
> > | (:EXECUTABLE-COUNTERPART EQUAL)
> > | (:EXECUTABLE-COUNTERPART EXPT-EXECUTE)
> > | (:EXECUTABLE-COUNTERPART IFF)
> > | (:EXECUTABLE-COUNTERPART NOT)
> > | (:EXECUTABLE-COUNTERPART UNARY-/)
> > | (:EXECUTABLE-COUNTERPART ZP)
> > | (:FAKE-RUNE-FOR-LINEAR NIL)
> > | (:FAKE-RUNE-FOR-TYPE-SET NIL)
> > | (:INDUCTION BINARY-LAND)
> > | (:INDUCTION BINARY-LIOR)
> > | (:INDUCTION BINARY-LXOR)
> > | (:LINEAR LAND-BND)
> > | (:LINEAR LAND-UPPER-BOUND)
> > | (:LINEAR LIOR-BND)
> > | (:LINEAR LXOR-BND)
> > | (:META CANCEL_PLUS-EQUAL-CORRECT)
> > | (:REWRITE A2)
> > | (:REWRITE A5)
> > | (:REWRITE CANCEL-COMMON-FACTORS-IN-EQUAL)
> > | (:REWRITE COLLECT-CONSTANTS-WITH-DIVISION)
> > | (:REWRITE COMMUTATIVITY-2-OF-*)
> > | (:REWRITE COMMUTATIVITY-OF-*)
> > | (:REWRITE COMMUTATIVITY-OF-+)
> > | (:REWRITE EXPT-EXECUTE-REWRITE)
> > | (:REWRITE FLOOR-FL)
> > | (:REWRITE INVERSE-OF-*-2)
> > | (:REWRITE LAND-0)
> > | (:REWRITE LAND-FL-1)
> > | (:REWRITE LAND-FL-2-ERIC)
> > | (:REWRITE LAND-OF-SINGLE-BITS-EQUAL-1)
> > | (:REWRITE LAND-WITH-N-NOT-A-NATP)
> > | (:REWRITE LIOR-0)
> > | (:REWRITE LIOR-FL-1)
> > | (:REWRITE LIOR-FL-2-ERIC)
> > | (:REWRITE LIOR-WITH-N-NOT-A-NATP)
> > | (:REWRITE LXOR-0)
> > | (:REWRITE LXOR-FL-1)
> > | (:REWRITE LXOR-FL-2-ERIC)
> > | (:REWRITE LXOR-WITH-N-NOT-A-NATP)
> > | (:REWRITE UNICITY-OF-0)
> > | (:TYPE-PRESCRIPTION INTEGERP-PROD)
> > | (:TYPE-PRESCRIPTION LAND-NONNEGATIVE-INTEGER-TYPE)
> > | (:TYPE-PRESCRIPTION LIOR-NONNEGATIVE-INTEGER-TYPE)
> > | (:TYPE-PRESCRIPTION LXOR-NONNEGATIVE-INTEGER-TYPE)
> > | (:TYPE-PRESCRIPTION NONNEG-+-TYPE))
> > | Warnings: None
> > | Time: 3.06 seconds (prove: 3.06, print: 0.00, other: 0.00)
> > | LXOR-IS-LIOR
> > |
> > |
> > | HARD ACL2 ERROR in FIND-MAPPING-PAIRS-TAIL: We have
exhausted the
> > | mapping-pairs of the basic symbol of
> > | Error: Bad plist (((< # #) 192) ((BINARY-* # Y) 63 (LEMMA
FAKE-RUNE-FOR-TYPE-SET NIL)) ((INTEGERP #) 192) ...)
> > | Fast links are on: do (si::use-fast-links nil) for debugging
> > | Error signalled by DEFTHM-FN.
> > | Backtrace: funcall > system:top-level > eval > lp >
acl2_*1*_acl2::certify-book-fn > certify-book-fn > acl2_*1*_acl2::progn-fn >
progn-fn > acl2_*1*_acl2::defthm-fn > defthm-fn > error-fms >
system:universal-error-handler > system::break-level-for-acl2 > let* > UNLESS
> > | Here is the current pstack [see :DOC pstack]:
> > | (WATERFALL)
> > |
> > | Error: Bad plist (((< # #) 192) ((BINARY-* # Y) 63 (LEMMA
FAKE-RUNE-FOR-TYPE-SET NIL)) ((INTEGERP #) 192) ...)
> > | Fast links are on: do (si::use-fast-links nil) for debugging
> > | Error signalled by LP.
> > | Backtrace: funcall > system:top-level > eval > lp >
retract-world1 > system:universal-error-handler > system::break-level-for-acl2
> let* > UNLESS
> > |
> > | ***NOTE***: An interrupt or error has occurred in the process
of cleaning
> > | up from an earlier interrupt or error. This is likely to
leave you
> > | at the raw Lisp prompt after you abort to the top level. If
so, then
> > | execute (LP) to re-enter the ACL2 read-eval-print loop.
> > |
> > |
> > | Top level.
> > | ACL2>
> > | NIL
> > |
> > | ACL2>
> >
> > **CERTIFICATION FAILED** for
/home/camm/debian/acl2/acl2-3.6.1/books/rtl/rel8/support/support/lextra.lisp
> >
> > Take care,
> >
> > Matt Kaufmann <address@hidden> writes:
> >
> > > Hi, Camm --
> > >
> > > The ACL2 user community isn't all that huge, I think -- the acl2
> > > mailing list had well under 200 people on it last time I checked
(as I
> > > recall). And I think the ACL2(r) community -- those who use the
> > > non-std stuff -- is probably under 10 people. So perhaps it's
not
> > > worth the trouble packaging the workshops or non-std stuff.
> > >
> > > There's kind of a big change coming in Version 4.0, by the way,
in how
> > > compilation interacts with book certification. If you want me
to send
> > > you a pre-release to play with, let me know.
> > >
> > > Thanks --
> > > -- Matt
> > > From: Camm Maguire <address@hidden>
> > > Date: Sun, 06 Jun 2010 16:12:48 -0400
> > > X-MagicMail-UUID: e5195c00-71a7-11df-a74c-000c29c6406d
> > > X-SpamAssassin-Status: No, hits=0.2 required=5.0
> > > X-UTCS-Spam-Status: No, hits=-210 required=165
> > >
> > > Greetings!
> > >
> > > Matt Kaufmann <address@hidden> writes:
> > >
> > > > Hi, Camm --
> > > >
> > > > Thanks for looking into GCL for Intel Macs. It will be
great to have
> > > > it!
> > > >
> > >
> > > Indeed. The issue (don't know if I mentioned) now lies with
gmp, not
> > > gcl proper, so I hope I will be able to adequately address it.
> > >
> > > > Oh my -- I don't know how I forgot to establish that link,
but it
> > > > appears that I did! Sorry about that. ACL2 3.6.1 was
released last
> > > > September. I don't expect to make that mistake again --
I've left
> > > > myself clear instructions to do this step with any ACL2
release.
> > > >
> > > > ACL2 4.0 will probably be out within a couple of weeks or
so (maybe
> > > > even sooner). Should I copying over that 3.6.1 link, or
not?
> > > > Whatever you prefer is fine with me -- copying it will take
only a few
> > > > seconds.
> > > >
> > >
> > > No problem. Am building 3.6.1 now for upload into Debian
shortly. It
> > > appears there will be enough time, and in case there are any
troubles
> > > with 4.0 that cannot be esolved before Debian finalizes, this
is
> > > probably worth doing.
> > >
> > > At some point, it might be nice to package acl2-workshops and
> > > acl2-non-std source as well. I'm not really sure how many
> > > Debian/Ubuntu users there are in any case -- perhaps you have
some
> > > feedback?
> > >
> > > Take care,
> > >
> > > > -- Matt
> > > > From: Camm Maguire <address@hidden>
> > > > Date: Sat, 05 Jun 2010 14:39:20 -0400
> > > > X-SpamAssassin-Status: No, hits=0.2 required=5.0
> > > > X-UTCS-Spam-Status: No, hits=-180 required=165
> > > >
> > > > Greetings!
> > > >
> > > > Matt Kaufmann <address@hidden> writes:
> > > >
> > > > > Hi, Camm --
> > > > >
> > > > > Thanks for letting us know. If that changes, feel
free to ask again.
> > > > >
> > > > > If you can get ACL2 3.6.1 to build and run on a Mac,
that would be
> > > > > great. I'm hoping to start final testing for ACL2 4.0
in about a week
> > > > > or so, and it would be great to test it using GCL on
an Intel Mac.
> > > > >
> > > >
> > > > OK, will let you know. The problem appears with gmp,
not gcl -- am
> > > > investigating.
> > > >
> > > > BTW, is ACL2 3.6.1 out? Debian tells me the current 3.6
is up to
> > > > date. Is that link for this purpose we set up some time
ago still
> > > > operative?
> > > >
> > > > Take care,
> > > >
> > > > > -- Matt
> > > > > Cc: address@hidden, address@hidden, address@hidden
> > > > > From: Camm Maguire <address@hidden>
> > > > > Date: Wed, 02 Jun 2010 12:02:45 -0400
> > > > > X-SpamAssassin-Status: No, hits=-2.6 required=5.0
> > > > > X-UTCS-Spam-Status: No, hits=-252 required=165
> > > > >
> > > > > Hi Matt!
> > > > >
> > > > > I've got an axiom mac I'm checking out now. No
need for further
> > > > > efforts on your part, yet at least. Thank you so
much!
> > > > >
> > > > > Take care,
> > > > >
> > > > > Matt Kaufmann <address@hidden> writes:
> > > > >
> > > > > > Hi, Camm --
> > > > > >
> > > > > > I've just learned that we do indeed have a couple
of Intel Macs in our
> > > > > > group. One is suitable and its "owner" is happy
to give you access,
> > > > > > but it's had some virus issues so that might (or
might not) take
> > > > > > awhile. The other might be OK but I don't know
if it has enough
> > > > > > "oomph".
> > > > > >
> > > > > > Sorry it's taken awhile. If the axiom people or
anyone else manages
> > > > > > to get you that access, please let us know and
we'll stop the process
> > > > > > here.
> > > > > >
> > > > > > Thanks --
> > > > > > -- Matt
> > > > > > From: Camm Maguire <address@hidden>
> > > > > > Date: Tue, 01 Jun 2010 12:01:27 -0400
> > > > > > X-detected-operating-system: by eggs.gnu.org:
GNU/Linux 2.6 (newer, 2)
> > > > > > Cc: Axiom-Developer <address@hidden>,
address@hidden
> > > > > > Sender: address@hidden
> > > > > > X-SpamAssassin-Status: No, hits=-3.6
required=5.0
> > > > > > X-UTCS-Spam-Status: No, hits=-326 required=165
> > > > > >
> > > > > > Greetings! Tim, do you have a publicly
accessible intel mac osx
> > > > > > machine I can use for gcl porting?
> > > > > >
> > > > > > Thanks!
> > > > > > --
> > > > > > Camm Maguire
address@hidden
> > > > > >
==========================================================================
> > > > > > "The earth is but one country, and mankind its
citizens." -- Baha'u'llah
> > > > > >
> > > > > > _______________________________________________
> > > > > > Gcl-devel mailing list
> > > > > > address@hidden
> > > > > > http://lists.gnu.org/mailman/listinfo/gcl-devel
> > > > > >
> > > > > >
> > > > > >
> > > > >
> > > > > --
> > > > > Camm Maguire
address@hidden
> > > > >
==========================================================================
> > > > > "The earth is but one country, and mankind its
citizens." -- Baha'u'llah
> > > > >
> > > > >
> > > > >
> > > > >
> > > >
> > > > --
> > > > Camm Maguire
address@hidden
> > > >
==========================================================================
> > > > "The earth is but one country, and mankind its
citizens." -- Baha'u'llah
> > > >
> > > >
> > > >
> > > >
> > >
> > > --
> > > Camm Maguire
address@hidden
> > >
==========================================================================
> > > "The earth is but one country, and mankind its citizens." --
Baha'u'llah
> > >
> > >
> > >
> > >
> >
> > --
> > Camm Maguire
address@hidden
> >
==========================================================================
> > "The earth is but one country, and mankind its citizens." --
Baha'u'llah
> >
> >
> >
> >
>
> --
> Camm Maguire address@hidden
>
==========================================================================
> "The earth is but one country, and mankind its citizens." --
Baha'u'llah
>
>
>
>
>
--
Camm Maguire address@hidden
==========================================================================
"The earth is but one country, and mankind its citizens." -- Baha'u'llah