[Top][All Lists]
[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
- Re: [Gcl-devel] Re: possible GCL/Windows compiler bug, (continued)
- Re: [Gcl-devel] Re: possible GCL/Windows compiler bug, Camm Maguire, 2004/10/15
- [Gcl-devel] workshop cert failure, Camm Maguire, 2004/10/29
- [Gcl-devel] Re: workshop cert failure, Matt Kaufmann, 2004/10/29
- [Gcl-devel] Re: workshop cert failure, Camm Maguire, 2004/10/29
- [Gcl-devel] Re: workshop cert failure, Matt Kaufmann, 2004/10/29
- Re: [Gcl-devel] Re: workshop cert failure, Camm Maguire, 2004/10/29
- Re: [Gcl-devel] Re: workshop cert failure,
Matt Kaufmann <=
RE: [Gcl-devel] Re: possible GCL/Windows compiler bug, Mike Thomas, 2004/10/12