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

[Camm Maguire]

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