[Gcl-devel] Re: address@hidden: gcl news and issues]

[Camm Maguire]

Greetings, and please excuse my delayed reply!

OK, first build a fresh gcl configured with --enable-debug and make
sure it is in your path.

Then reproduce the error below.

Then make sure the workxxx file has the contents as indicated in the
trace below:

> \\> \\> \\echo '(load "init.lsp")' > workxxx
> \\> \\> \\echo '(acl2::compile-acl2)' >> workxxx
> \\> \\> \\echo '(acl2::exit-lisp)' >> workxxx


Then
gdb gcl
(gdb) r
>(si::use-fast-links nil)
>(si:;sgc-on nil)
>(load "workxxx")
(gdb) bt
(gdb) c
Error:: Caught...
>>:bt

And send me the output.  In case the error goes away, it is an sgc
problem on this machine and I can provide further instructions.

Take care,


Sandip Ray <address@hidden> writes:

> Hi Camm,
> 
> I am not sure I can provide you a remote ssh access to my machine.
> However, please let me know how to generate a gdb backtrace; I'll do that
> and send it.
> 
> Thanks a lot,
> 
> Sandip.
> 
> On Tue, 4 Jan 2005, Camm Maguire wrote:
> 
> \\Greetings!  OK, from here I can either instruct you in producing a gdb
> \\backtrace of the error, or perhaps you might be able to provide me
> \\remote ssh access.
> \\
> \\Take care,
> \\
> \\Sandip Ray <address@hidden> writes:
> \\
> \\> Hello Camm,
> \\>
> \\> The attached file compile.txt shows the entire configure and make output
> \\> on my system. At the end of the file is also the attempt to try to compile
> \\> ACL2, which gave me the error.
> \\>
> \\> Thanks a lot,
> \\>
> \\> Sandip.
> \\>
> \\> On Tue, 4 Jan 2005, Camm Maguire wrote:
> \\>
> \\> \\Greetings!  Could you please send me the full gcl configure and make
> \\> \\output?
> \\> \\
> \\> \\Take care,
> \\> \\
> \\> \\Sandip Ray <address@hidden> writes:
> \\> \\
> \\> \\> Hi Matt and Camm,
> \\> \\>
> \\> \\> I was trying to compile acl2 version 2.9.1, but after this email I 
> tried
> \\> \\> 2.9 and saw the same error. Evidently there is something trivial I am
> \\> \\> missing. Sorry for bothering you all with this,
> \\> \\>
> \\> \\> Sandip.
> \\> \\>
> \\> \\> On Mon, 3 Jan 2005, Matt Kaufmann wrote:
> \\> \\>
> \\> \\> \\Hi again, Camm --
> \\> \\> \\
> \\> \\> \\I forwarded you an email earlier today from Sandip.  Here is a 
> later one, with
> \\> \\> \\an error under GCL 2.6.5:
> \\> \\> \\
> \\> \\> \\Error: Caught fatal error [memory may be damaged]
> \\> \\> \\Fast links are on: do (si::use-fast-links nil) for debugging
> \\> \\> \\
> \\> \\> \\I'd appreciate it if you can help Sandip with this.  (I'm ignorant 
> about such
> \\> \\> \\matters, but I'm assuming this is a GCL problem.)
> \\> \\> \\
> \\> \\> \\Sandip, are you compiling ACL2 2.9 or ACL2 2.9.1?
> \\> \\> \\
> \\> \\> \\-- Matt
> \\> \\> \\------- Start of forwarded message -------
> \\> \\> \\Date: Mon, 3 Jan 2005 21:59:39 -0600 (CST)
> \\> \\> \\From: Sandip Ray <address@hidden>
> \\> \\> \\To: Matt Kaufmann <address@hidden>
> \\> \\> \\Subject: gcl news and issues
> \\> \\> \\In-Reply-To: <address@hidden>
> \\> \\> \\Content-Type: TEXT/PLAIN; charset=US-ASCII
> \\> \\> \\
> \\> \\> \\Hi Matt,
> \\> \\> \\
> \\> \\> \\I did get gcl2-2.6.5 compiled by making binutils using the following
> \\> \\> \\option (suggested by Camm)
> \\> \\> \\
> \\> \\> \\./configure  --disable-statsysbfd --enable-locbfd.
> \\> \\> \\
> \\> \\> \\Now when I get to compile ACL2  using this gcl,  I get the following
> \\> \\> \\error:
> \\> \\> \\
> \\> \\> \\===================================================================
> \\> \\> address@hidden acl2-sources]# make -f GNUmakefile
> \\> \\> \\rm -f acl2-fns.o
> \\> \\> \\if [ "" = "r" ] ; then \
> \\> \\> \\echo '(or (member :non-standard-analysis *features*) (push
> \\> \\> \\:non-standard-analysis *features*))' > acl2r.lisp ;\
> \\> \\> \\elif [ "" = "" ] ; then \
> \\> \\> \\echo ';(or (member :non-standard-analysis *features*) (push
> \\> \\> \\:non-standard-analysis *features*))' > acl2r.lisp ;\
> \\> \\> \\else \
> \\> \\> \\echo 'Please supply either r or the empty string for make variable 
> NONSTD,
> \\> \\> \\not  .' ;\
> \\> \\> \\exit 1 ;\
> \\> \\> \\fi
> \\> \\> \\date
> \\> \\> \\Mon Jan  3 21:40:58 CST 2005
> \\> \\> \\rm -f workxxx
> \\> \\> \\echo '(load "init.lsp")' > workxxx
> \\> \\> \\echo '(acl2::check-suitability-for-acl2)' >> workxxx
> \\> \\> \\echo '(acl2::exit-lisp)' >> workxxx
> \\> \\> \\gcl < workxxx
> \\> \\> \\GCL (GNU Common Lisp)  2.6.5 CLtL1    Jan  3 2005 21:16:59
> \\> \\> \\Source License: LGPL(gcl,gmp), GPL(unexec,bfd)
> \\> \\> \\Binary License:  GPL due to GPL'ed components: (READLINE BFD 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.
> \\> \\> \\Loading init.lsp
> \\> \\> \\Loading acl2r.lisp
> \\> \\> \\Finished loading acl2r.lisp
> \\> \\> \\Loading acl2-init.lisp
> \\> \\> \\Loading acl2.lisp
> \\> \\> \\Loading acl2-fns.lisp
> \\> \\> \\Finished loading acl2-fns.lisp
> \\> \\> \\Compiling acl2-fns.lisp.
> \\> \\> \\End of Pass 1.
> \\> \\> \\
> \\> \\> \\;; Note: Tail-recursive call of GET-TYPE-FROM-DCLS was replaced by
> \\> \\> \\iteration.
> \\> \\> \\;; Note: Tail-recursive call of COLLECT-TYPES was replaced by 
> iteration.
> \\> \\> \\;; Note: Tail-recursive call of OUTPUT-TYPE-FOR-DECLARE-FORM-REC was
> \\> \\> \\replaced by iteration.
> \\> \\> \\;; Note: Tail-recursive call of REV1@ was replaced by iteration.
> \\> \\> \\;; Note: Tail-recursive call of ACL2-READ-CHARACTER-STRING was 
> replaced by
> \\> \\> \\iteration.[GC for 211 CONS pages..(T=1).GC finished]
> \\> \\> \\
> \\> \\> \\End of Pass 2.
> \\> \\> \\OPTIMIZE levels: Safety=0 (No runtime error checking), Space=0, 
> Speed=3
> \\> \\> \\Finished compiling acl2-fns.lisp.
> \\> \\> \\Loading acl2-fns.o
> \\> \\> \\start address -T 0x8428860 Finished loading acl2-fns.o
> \\> \\> \\Finished loading acl2.lisp
> \\> \\> \\Finished loading acl2-init.lisp
> \\> \\> \\Loading enable-eval.lisp
> \\> \\> \\Disabling evaluation inside breaks.
> \\> \\> \\Finished loading enable-eval.lisp
> \\> \\> \\Finished loading init.lsp
> \\> \\> \\
> \\> \\> \\>
> \\> \\> \\Loading init.lsp
> \\> \\> \\Finished loading init.lsp
> \\> \\> \\T
> \\> \\> \\
> \\> \\> \\>
> \\> \\> \\Loading acl2-check.lisp
> \\> \\> \\[GC for 211 CONS pages..(T=0).GC finished]
> \\> \\> \\Check completed.
> \\> \\> \\Finished loading acl2-check.lisp
> \\> \\> \\T
> \\> \\> \\
> \\> \\> \\>rm -f workxxx
> \\> \\> \\rm -f workxxx
> \\> \\> \\rm -f acl2-fns.o acl2-fns.lbin acl2-fns.sbin acl2-fns.fasl 
> acl2-fns.wfasl
> \\> \\> \\\
> \\> \\> \\  acl2-fns.fas acl2-fns.lib acl2-fns.sparcf acl2-fns.ufsl 
> acl2-fns.x86f \
> \\> \\> \\          acl2-fns.dfsl
> \\> \\> \\echo '(load "init.lsp")' > workxxx
> \\> \\> \\echo '(acl2::compile-acl2)' >> workxxx
> \\> \\> \\echo '(acl2::exit-lisp)' >> workxxx
> \\> \\> \\gcl < workxxx
> \\> \\> \\GCL (GNU Common Lisp)  2.6.5 CLtL1    Jan  3 2005 21:16:59
> \\> \\> \\Source License: LGPL(gcl,gmp), GPL(unexec,bfd)
> \\> \\> \\Binary License:  GPL due to GPL'ed components: (READLINE BFD 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.
> \\> \\> \\Loading init.lsp
> \\> \\> \\Loading acl2r.lisp
> \\> \\> \\Finished loading acl2r.lisp
> \\> \\> \\Loading acl2-init.lisp
> \\> \\> \\Loading acl2.lisp
> \\> \\> \\Loading acl2-fns.lisp
> \\> \\> \\Finished loading acl2-fns.lisp
> \\> \\> \\Compiling acl2-fns.lisp.
> \\> \\> \\End of Pass 1.
> \\> \\> \\
> \\> \\> \\;; Note: Tail-recursive call of GET-TYPE-FROM-DCLS was replaced by
> \\> \\> \\iteration.
> \\> \\> \\;; Note: Tail-recursive call of COLLECT-TYPES was replaced by 
> iteration.
> \\> \\> \\;; Note: Tail-recursive call of OUTPUT-TYPE-FOR-DECLARE-FORM-REC was
> \\> \\> \\replaced by iteration.
> \\> \\> \\;; Note: Tail-recursive call of REV1@ was replaced by iteration.
> \\> \\> \\;; Note: Tail-recursive call of ACL2-READ-CHARACTER-STRING was 
> replaced by
> \\> \\> \\iteration.[GC for 211 CONS pages..(T=0).GC finished]
> \\> \\> \\
> \\> \\> \\End of Pass 2.
> \\> \\> \\OPTIMIZE levels: Safety=0 (No runtime error checking), Space=0, 
> Speed=3
> \\> \\> \\Finished compiling acl2-fns.lisp.
> \\> \\> \\Loading acl2-fns.o
> \\> \\> \\start address -T 0x8428860 Finished loading acl2-fns.o
> \\> \\> \\Finished loading acl2.lisp
> \\> \\> \\Finished loading acl2-init.lisp
> \\> \\> \\Loading enable-eval.lisp
> \\> \\> \\Disabling evaluation inside breaks.
> \\> \\> \\Finished loading enable-eval.lisp
> \\> \\> \\Finished loading init.lsp
> \\> \\> \\
> \\> \\> \\>
> \\> \\> \\Loading init.lsp
> \\> \\> \\Finished loading init.lsp
> \\> \\> \\T
> \\> \\> \\
> \\> \\> \\>
> \\> \\> \\Loading axioms.lisp
> \\> \\> \\[GC for 211 CONS pages..(T=0).GC finished]
> \\> \\> \\[GC for 49 SYMBOL pages..(T=0).GC finished]
> \\> \\> \\Finished loading axioms.lisp
> \\> \\> \\Compiling axioms.lisp.
> \\> \\> \\[GC for 1030 CONS pages..(T=1).GC finished]
> \\> \\> \\[GC for 38 ARRAY pages..(T=1).GC finished]
> \\> \\> \\[GC for 57 ARRAY pages..(T=1).GC finished]
> \\> \\> \\[GC for 32 STRING pages..(T=1).GC finished]
> \\> \\> \\End of Pass 1.
> \\> \\> \\[GC for 32 STRING pages..(T=2).GC finished]
> \\> \\> \\[GC for 73 SYMBOL pages..(T=2).GC finished]
> \\> \\> \\End of Pass 2.
> \\> \\> \\OPTIMIZE levels: Safety=0 (No runtime error checking), Space=0, 
> Speed=3
> \\> \\> \\Finished compiling axioms.lisp.
> \\> \\> \\Loading axioms.o
> \\> \\> \\
> \\> \\> \\Error: Caught fatal error [memory may be damaged]
> \\> \\> \\Fast links are on: do (si::use-fast-links nil) for debugging
> \\> \\> \\Error signalled by PROGN.
> \\> \\> \\Broken at COND.  Type :H for Help.
> \\> \\> \\ACL2>>
> \\> \\> \\Sorry, execution of top-level forms is disabled inside breaks.
> \\> \\> \\Execute :enable-eval T if you want such evaluation enabled.
> \\> \\> \\NIL
> \\> \\> \\ACL2>>rm -f workxxx
> \\> \\> \\rm -f workxxx
> \\> \\> \\rm -f worklispext
> \\> \\> \\echo -n "" >> osaved_acl2
> \\> \\> \\rm -f osaved_acl2
> \\> \\> \\echo '(load "init.lsp")' > workxxx
> \\> \\> \\echo '(in-package "ACL2")' >> workxxx
> \\> \\> \\echo '(save-acl2 (quote (initialize-acl2 (quote include-book)
> \\> \\> \\acl2::*acl2-pass-2-files* nil)) "saved_acl2")' >> workxxx
> \\> \\> \\echo '(exit-lisp)' >> workxxx
> \\> \\> \\gcl < workxxx
> \\> \\> \\GCL (GNU Common Lisp)  2.6.5 CLtL1    Jan  3 2005 21:16:59
> \\> \\> \\Source License: LGPL(gcl,gmp), GPL(unexec,bfd)
> \\> \\> \\Binary License:  GPL due to GPL'ed components: (READLINE BFD 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.
> \\> \\> \\Loading init.lsp
> \\> \\> \\Loading acl2r.lisp
> \\> \\> \\Finished loading acl2r.lisp
> \\> \\> \\Loading acl2-init.lisp
> \\> \\> \\Loading acl2.lisp
> \\> \\> \\Loading acl2-fns.lisp
> \\> \\> \\Finished loading acl2-fns.lisp
> \\> \\> \\Compiling acl2-fns.lisp.
> \\> \\> \\End of Pass 1.
> \\> \\> \\
> \\> \\> \\;; Note: Tail-recursive call of GET-TYPE-FROM-DCLS was replaced by
> \\> \\> \\iteration.
> \\> \\> \\;; Note: Tail-recursive call of COLLECT-TYPES was replaced by 
> iteration.
> \\> \\> \\;; Note: Tail-recursive call of OUTPUT-TYPE-FOR-DECLARE-FORM-REC was
> \\> \\> \\replaced by iteration.
> \\> \\> \\;; Note: Tail-recursive call of REV1@ was replaced by iteration.
> \\> \\> \\;; Note: Tail-recursive call of ACL2-READ-CHARACTER-STRING was 
> replaced by
> \\> \\> \\iteration.[GC for 211 CONS pages..(T=1).GC finished]
> \\> \\> \\
> \\> \\> \\End of Pass 2.
> \\> \\> \\OPTIMIZE levels: Safety=0 (No runtime error checking), Space=0, 
> Speed=3
> \\> \\> \\Finished compiling acl2-fns.lisp.
> \\> \\> \\Loading acl2-fns.o
> \\> \\> \\start address -T 0x8428860 Finished loading acl2-fns.o
> \\> \\> \\Finished loading acl2.lisp
> \\> \\> \\Finished loading acl2-init.lisp
> \\> \\> \\Loading enable-eval.lisp
> \\> \\> \\Disabling evaluation inside breaks.
> \\> \\> \\Finished loading enable-eval.lisp
> \\> \\> \\Finished loading init.lsp
> \\> \\> \\
> \\> \\> \\>
> \\> \\> \\Loading init.lsp
> \\> \\> \\Finished loading init.lsp
> \\> \\> \\T
> \\> \\> \\
> \\> \\> \\>
> \\> \\> \\#<"ACL2" package>
> \\> \\> \\
> \\> \\> \\ACL2>
> \\> \\> \\Error: Please compile ACL2 using (COMPILE-ACL2) or
> \\> \\> \\       (QUICK-COMPILE-ACL2 T), which will write the
> \\> \\> \\       token :compiled to the file acl2-status.txt.
> \\> \\> \\Fast links are on: do (si::use-fast-links nil) for debugging
> \\> \\> \\Error signalled by COND.
> \\> \\> \\Broken at COND.  Type :H for Help.
> \\> \\> \\ACL2>>
> \\> \\> \\Sorry, execution of top-level forms is disabled inside breaks.
> \\> \\> \\Execute :enable-eval T if you want such evaluation enabled.
> \\> \\> \\NIL
> \\> \\> \\ACL2>>if [ -f worklispext ]; then make move-to-old LISPEXT=`cat
> \\> \\> \\worklispext` ;\
> \\> \\> \\elif [ -f saved_acl2 ]; then \
> \\> \\> \\mv -f saved_acl2 osaved_acl2 ;\
> \\> \\> \\else \
> \\> \\> \\touch saved_acl2 ;\
> \\> \\> \\mv -f saved_acl2 osaved_acl2 ;\
> \\> \\> \\fi
> \\> \\> \\mv -f nsaved_acl2 saved_acl2
> \\> \\> \\mv: cannot stat `nsaved_acl2': No such file or directory
> \\> \\> \\make: *** [init] Error 1
> \\> \\> address@hidden acl2-sources]#
> \\> \\> \\====================================================================
> \\> \\> \\
> \\> \\> \\The same thing happens of course if I start up gcl and go to the 
> step
> \\> \\> \\(compile-acl2).
> \\> \\> \\
> \\> \\> \\I think I had seen the error (memory might be damaged) above 
> before, and I
> \\> \\> \\had known how to fix it, but I dont seem to remember any more. Is 
> this a
> \\> \\> \\quick thing to answer?
> \\> \\> \\
> \\> \\> \\I am sorry to bother you with these newbie questions; but I had not 
> done
> \\> \\> \\much of acl2-compiling myself other than at UT, and there make had 
> always
> \\> \\> \\just worked, so I never had to figure out all this. Sorry for 
> bothering
> \\> \\> \\you.
> \\> \\> \\
> \\> \\> \\Sandip.
> \\> \\> \\------- End of forwarded message -------
> \\> \\> \\
> \\> \\>
> \\> \\>
> \\> \\>
> \\> \\
> \\> \\
> \\>
> \\
> \\
> 
> 
> 

-- 
Camm Maguire                                            address@hidden
==========================================================================
"The earth is but one country, and mankind its citizens."  --  Baha'u'llah