gcl-devel
[Top][All Lists]
Advanced

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: [Gcl-devel] Re: workshop cert failure


From: Matt Kaufmann
Subject: Re: [Gcl-devel] Re: workshop cert failure
Date: Fri, 29 Oct 2004 15:45:19 -0500

Excellent.  I forwarded your separate posting to Warren in case he wants to
rebuild GCL and then ACL2 on his 64-bit machines.

So as far as I know, there's nothing holding up the update you were going to
make (putting ACL2 2.9 in the stable Debian world, I believe).

Thanks --
-- Matt
   Cc: address@hidden, address@hidden
   From: Camm Maguire <address@hidden>
   Date: 29 Oct 2004 16:39:35 -0400
   User-Agent: Gnus/5.09 (Gnus v5.9.0) Emacs/21.2
   Content-Type: text/plain; charset=us-ascii
   X-SpamAssassin-Status: No, hits=-2.6 required=5.0
   X-UTCS-Spam-Status: No, hits=-332 required=180

   Thanks Matt!  Please see the separately posted fix.

   Take care,

   Matt Kaufmann <address@hidden> writes:

   > Hi --
   > 
   > Good news; I've isolated the problem.  As shown below, GCL and ACL2 on
   > hankypanky evaluate (+ -2147483648 -1) to -18446744071562067969, yet
   > (- -2147483648 1) evaluates correctly.
   > 
   > bash-2.05$ /home/camm/gcl-2.6.5/bin/gcl
   > GCL (GNU Common Lisp)  2.6.5 CLtL1    Oct 28 2004 14:27:33
   > Source License: LGPL(gcl,gmp), GPL(unexec,bfd)
   > Binary License:  GPL due to GPL'ed components: (READLINE UNEXEC)
   > Modifications of this banner must retain notice of a compatible license
   > Dedicated to the memory of W. Schelter
   > 
   > Use (help) to get some basic information on how to use GCL.
   > 
   > >(+ -2147483648 -1)
   > 
   > -18446744071562067969
   > 
   > >(- -2147483648 1)
   > 
   > -2147483649
   > 
   > >(bye)
   > bash-2.05$ /home/camm/acl2-2.9/saved_acl2
   > GCL (GNU Common Lisp)  2.6.5 CLtL1    Oct 28 2004 14:27:33
   > Source License: LGPL(gcl,gmp), GPL(unexec,bfd)
   > Binary License:  GPL due to GPL'ed components: (READLINE UNEXEC)
   > Modifications of this banner must retain notice of a compatible license
   > Dedicated to the memory of W. Schelter
   > 
   > Use (help) to get some basic information on how to use GCL.
   > 
   >  ACL2 Version 2.9 built October 28, 2004  15:03:41.
   >  Copyright (C) 2004  University of Texas at Austin
   >  ACL2 comes with ABSOLUTELY NO WARRANTY.  This is free software and you
   >  are welcome to redistribute it under certain conditions.  For details,
   >  see the GNU General Public License.
   > 
   >  Initialized with (INITIALIZE-ACL2 'INCLUDE-BOOK *ACL2-PASS-2-FILES*
   >                       /usr/share/acl2-2.9/).
   >  See the documentation topic note-2-9 for recent changes.
   > 
   >  NOTE!!  Proof trees are disabled in ACL2.  To enable them in emacs,
   >  look under the ACL2 source directory in interface/emacs/README.doc; 
   >  and, to turn on proof trees, execute :START-PROOF-TREE in the ACL2 
   >  command loop.   Look in the ACL2 documentation under PROOF-TREE.
   > 
   > ACL2 Version 2.9.  Level 1.  Cbd "/misc/home/kaufmann/".
   > Type :help for help.
   > Type (good-bye) to quit completely out of ACL2.
   > 
   > ACL2 !>:q
   > 
   > Exiting the ACL2 read-eval-print loop.  To re-enter, execute (LP).
   > ACL2>(+ -2147483648 -1)
   > 
   > -18446744071562067969
   > 
   > ACL2>(- -2147483648 1)
   > 
   > -2147483649
   > 
   > ACL2>
   > 
   > -- Matt
   >    Cc: address@hidden, address@hidden
   >    From: Camm Maguire <address@hidden>
   >    Date: 29 Oct 2004 11:17:22 -0400
   >    User-Agent: Gnus/5.09 (Gnus v5.9.0) Emacs/21.2
   >    Content-Type: text/plain; charset=us-ascii
   >    X-SpamAssassin-Status: No, hits=-2.6 required=5.0
   >    X-UTCS-Spam-Status: No, hits=-312 required=180
   > 
   >    Greetings!
   > 
   >    Matt Kaufmann <address@hidden> writes:
   > 
   >    > Great!  Thanks.  Warren Hunt says he hopes that my account on 
hankypanky will
   >    > be activated later today.  I believe that you'd find it most useful 
if I can
   >    > isolate a small function call that returns the wrong value; is that 
right?
   >    > 
   > 
   >    Yes!  Thanks!
   > 
   >    > -- Matt
   >    >    Cc: address@hidden
   >    >    From: Camm Maguire <address@hidden>
   >    >    Date: 29 Oct 2004 10:34:17 -0400
   >    >    User-Agent: Gnus/5.09 (Gnus v5.9.0) Emacs/21.2
   >    >    Content-Type: text/plain; charset=us-ascii
   >    >    X-SpamAssassin-Status: No, hits=-2.6 required=5.0
   >    >    X-UTCS-Spam-Status: No, hits=-272 required=180
   >    > 
   >    >    Greetings!  My suspicion is that we've uncovered a (hopefully)
   >    >    small 64bit issue in gcl.  I've reproduced on amd64, which builds 
via
   >    >    the conventional sequence, and on hankypanky.csres.utexas.edu 
(ia64,
   >    >    unconventional build sequence).  The files are in my home 
directory on
   >    >    that machine for your inspection.
   >    > 
   >    >    Please let me know.
   >    > 
   >    >    Take care,
   >    >    -- 
   >    >    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
   > 
   > 
   > _______________________________________________
   > 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




reply via email to

[Prev in Thread] Current Thread [Next in Thread]