Hi --
I was able to reproduce the error after building ACL2 a new debug copy
of 64-bit gcl that the sysadmins built. Same instructions as before,
except for a slight change in the ACL2 executable directory. Quoting
from below, but updating the executable path (and fixing a misleading
comment):
Start up ACL2 built on GCL, as follows:
/projects/acl2/v3-4-linux-64/fast-linux-gcl-saved_acl2
Then issue these commands:
; Just to slow down the output from the thm form below:
(trace$ rewrite)
; ACL2 disables the debugger by default; this restores it:
(set-debugger-enable t)
; This goes pretty fast but you'll have time to interrupt it:
(thm (equal (append (append x x) x) (append x x x)))
[Now quickly interrupt with control-c, and then :q from the break.
If the form above completes, just try it again. Eventually I think
you'll see a Lisp "fatal error" or even a "Segmentation fault".]
It seems to take me about 3 to 5 THM calls to get the error, which
looks like this:
ACL2 !>(thm (equal (append (append x x) x) (append x x x)))
[SGC off]
Error: Caught fatal error [memory may be damaged]
Fast links are on: do (si::use-fast-links nil) for debugging
Error signalled by ACL2_*1*_ACL2::THM-FN.
Broken at COND. Type :H for Help.
ACL2[RAW LISP]>>
-- Matt
Date: Mon, 23 Feb 2009 17:12:04 -0600
From: "David A. Kotz" <dk...@cs.utexas.edu>
CC: c...@maguirefamily.org, gr...@cs.utexas.edu, gcl-devel@gnu.org
I've replaced both of our 64bit flavors and the 32bit with debug-enabled
versions. The 64s are in place now, and the 32 should rdist around
tonight. I want to keep all of them in sync, even if we're only
investigating a problem in one.
- dave
Matt Kaufmann wrote:
> Thanks, Dave! I really appreciate it.
>
> When I get the word from you, or when I see
> /lusr/opt/gcl-2.6.8pre/bin/gcl updated on lhug-0, I'll rebuild ACL2 on
> top of it and try to reproduce the problem.
>
> Thanks again --
> -- Matt
> Date: Mon, 23 Feb 2009 10:13:54 -0600
> From: "David A. Kotz" <dk...@cs.utexas.edu>
> CC: Matt Kaufmann <kaufm...@cs.utexas.edu>, gr...@cs.utexas.edu,
> gcl-devel@gnu.org
>
> I'll rebuild it with the debug flag.
>
> - dave
>
>
> Camm Maguire wrote:
> > Thanks! Please let me know if you run into troubles here.
> >
> > Take care,
> >
> > Matt Kaufmann <kaufm...@cs.utexas.edu> writes:
> >
> >> Howdy --
> >>
> >> Thanks for the reply.
> >>
> >> If gr...@cs is willing to do (1), or to send me the exact configure
> >> and make commands and source directory used so that I can do it
> >> myself, then I'll try to reproduce the error by building ACL2 on top
> >> of it. I'm assuming that --enable-debug is given to the configure
> >> command, not to make.
> >>
> >> Then if if I can't reproduce the problem, I'll let you and gr...@cs
> >> know and we can explore (2). In that case, if gr...@cs is willing to
> >> do it, great; then I'll try to reproduce the problem. But if I'm to
> >> do the build, I'd need explicit instructions on how to "make sure -g
> >> is included in the gcc calls"; maybe I need to do some setq in Lisp?
> >> Also I didn't understand the comment about makedefs. But I guess we
> >> can ignore (2) if (1) works.
> >>
> >> -- Matt
> >> Cc: gcl-devel@gnu.org, gr...@cs.utexas.edu
> >> From: Camm Maguire <c...@maguirefamily.org>
> >> Date: Fri, 20 Feb 2009 20:58:49 -0500
> >> X-SpamAssassin-Status: No, hits=-2.6 required=5.0
> >> X-UTCS-Spam-Status: No, hits=-282 required=165
> >>
> >> Greetings! I suspect a missing signal block around some code that
> >> needs protecting. I've reprodced under gdb, but there are no
> >> debugging symbols in the image. [ Question for list -- have
computers
> >> now become so fast that -g should be included by default in all
gcl
> >> images? It used to slow down the compiler, don't know about now.
It
> >> does make the image quite a bit bigger. ]
> >>
> >> Ideally, you or someone else at the site might be so kind as to
> >> rebuild atop
> >>
> >> 1) a gcl build with --enable-debug. If this does not reproduce,
then
> >> in addition
> >> 2) rebuild atop a standard gcl with the CFLAGS environment
variable
> >> set to -g before configure and make. Please make sure -g is
included
> >> in the gcc calls. Otherwise, makedefs can be modified after
configure
> >> and before make to include -g wherever one sees -O3 or -O
> >>
> >> Would this be too much trouble?
> >>
> >> Take care,
> >>
> >> Matt Kaufmann <kaufm...@cs.utexas.edu> writes:
> >>
> >> > Hi --
> >> >
> >> > The sysadmins here at UT CS have built GCL 2.6.8pre from CVS as
you
> >> > suggested. It's working great on 32-bit linux, but I've run
into an
> >> > issue for 64-bit linux.
> >> >
> >> > You can re-create the issue on a UT CS 64-bit linux machine as
> >> > follows.
> >> >
> >> > Start up ACL2 built on GCL, as follows:
> >> >
> >> > /projects/acl2/v3-4-linux/fast-linux-gcl-saved_acl2
> >> >
> >> > Then issue these commands:
> >> >
> >> > ; Just to slow down the output from the next form:
> >> > (trace$ rewrite)
> >> >
> >> > ; ACL2 disables the debugger by default; this restores it:
> >> > (set-debugger-enable t)
> >> >
> >> > ; This goes pretty fast but you'll have time to interrupt it:
> >> > (thm (equal (append (append x x) x) (append x x x)))
> >> >
> >> > [Now quickly interrupt with control-c, and then :q from the
break.
> >> > If the form above completes, just try it again. Eventually
I think
> >> > you'll see a Lisp "fatal error" or even a "Segmentation
fault".]
> >> >
> >> > By the way, I built /projects/acl2/v3-4-linux/fast-linux-gcl as
> >> > follows, on lhug-0 (a 64-bit linux machine):
> >> >
> >> > rm -f TAGS ; mv make-fast-gcl.log make-fast-gcl.old.log ; (time
nice make PREFIX=fast-linux-gcl- LISP=my-fast-gcl) >& make-fast-gcl.log&
> >> >
> >> > where "my-fast-gcl" is a script containing:
> >> >
> >> > #!/bin/sh
> >> > /lusr/opt/gcl-2.6.8pre/bin/gcl -eval "(defparameter
user::*fast-acl2-gcl-build* t)" $*
> >> >
> >> > Also by the way, if you instead run the following on a 32-bit
UT CS
> >> > linux machine
> >> >
> >> > /projects/acl2/v3-4-linux/gcl-saved_acl2
> >> >
> >> > then you won't see the interrupt problem described above (or at
least,
> >> > I didn't, and I tried).
> >> >
> >> > Thanks --
> >> > -- Matt
> >> >
> >> >
> >> >
> >> >
> >>
> >> --
> >> 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
