[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: |
Camm Maguire |
|
Subject: |
Re: [Gcl-devel] Re: [Axiom-developer] Axiom May 2010 release |
|
Date: |
Mon, 27 Sep 2010 11:50:39 -0400 |
|
User-agent: |
Gnus/5.11 (Gnus v5.11) Emacs/22.2 (gnu/linux) |
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-helpers!
> .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