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: gcl-devel@gnu.org From: Camm Maguire <c...@maguirefamily.org> 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 <kaufm...@cs.utexas.edu> 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 <c...@maguirefamily.org> > 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? > > c...@localhost:~/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 <kaufm...@cs.utexas.edu> 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 <c...@maguirefamily.org> > > 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 <kaufm...@cs.utexas.edu> 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 <c...@maguirefamily.org> > > > 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 <kaufm...@cs.utexas.edu> 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: rk...@cs.utexas.edu, san...@cs.utexas.edu, h...@cs.utexas.edu > > > > From: Camm Maguire <c...@maguirefamily.org> > > > > 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 <kaufm...@cs.utexas.edu> 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 <c...@maguirefamily.org> > > > > > 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 <axiom-develo...@nongnu.org>, gcl-devel@gnu.org > > > > > Sender: gcl-devel-bounces+kaufmann=cs.utexas....@gnu.org > > > > > 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 c...@maguirefamily.org > > > > > ========================================================================== > > > > > "The earth is but one country, and mankind its citizens." -- Baha'u'llah > > > > > > > > > > _______________________________________________ > > > > > Gcl-devel mailing list > > > > > Gcl-devel@gnu.org > > > > > http://lists.gnu.org/mailman/listinfo/gcl-devel > > > > > > > > > > > > > > > > > > > > > > > -- > > > > Camm Maguire c...@maguirefamily.org > > > > ========================================================================== > > > > "The earth is but one country, and mankind its citizens." -- Baha'u'llah > > > > > > > > > > > > > > > > > > > > > > -- > > > Camm Maguire c...@maguirefamily.org > > > ========================================================================== > > > "The earth is but one country, and mankind its citizens." -- Baha'u'llah > > > > > > > > > > > > > > > > -- > > Camm Maguire c...@maguirefamily.org > > ========================================================================== > > "The earth is but one country, and mankind its citizens." -- Baha'u'llah > > > > > > > > > > -- > Camm Maguire c...@maguirefamily.org > ========================================================================== > "The earth is but one country, and mankind its citizens." -- Baha'u'llah > > > > -- Camm Maguire c...@maguirefamily.org ========================================================================== "The earth is but one country, and mankind its citizens." -- Baha'u'llah _______________________________________________ Gcl-devel mailing list Gcl-devel@gnu.org http://lists.gnu.org/mailman/listinfo/gcl-devel