[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: |
Fri, 24 Sep 2010 16:37:40 -0500 |
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.
>> 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.
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.
Thanks again -- wow.
-- 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