Greetings, and thanks! OK, this is fixed now in branch 2.6.8pre of cvs, and will be in cvs head soon. Please let me know if you need a reminder about how to get 2.6.8pre.
Take care, Matt Kaufmann <kaufm...@cs.utexas.edu> writes: > 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 > > >> > > >> > > >> > > >> > > > > > > > -- 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
