Greetings!
OK, the compile problem is now fixed -- still looking at the extranous
values returned by compile-file with C optimization on.
Take care,
Robert Boyer <[EMAIL PROTECTED]> writes:
> Here's a rather pointless message.
>
> As you suggested, I rebuilt with enable-debug and ran under gdb and got an
> error at the same place in ACL2 compilation, though this time called
> 'segmentation violation' rather than 'stack overflow'. Below is a partial
> transcript, and then a couple of comments.
>
> Bob
>
> ;; Compiling interface-raw.lisp.
> ; (DEFUN ACL2-GENTEMP ...) is being compiled.
> ;; Warning: ret type mismatch in auto-proclamation T(NIL) -> (VALUES T
> T)
>
> ; (DEFUN CHECK-ACL2-WORLD-INVARIANT ...) is being compiled.
> ;; Warning: ret type mismatch in auto-proclamation T(NIL) -> *
>
> ; (DEFUN CHK-VIRGIN2 ...) is being compiled.
> ;; Warning: ret type mismatch in auto-proclamation T(NIL) -> *
>
> ; (DEFUN CHK-PACKAGE-REINCARNATION-IMPORT-RESTRICTIONS2 ...) is being
> compiled.
> ;; Warning: ret type mismatch in auto-proclamation T(NIL) -> *
>
> ; (DEFUN CHECK-BUILT-IN-CONSTANTS ...) is being compiled.
> ;; Warning: ret type mismatch in auto-proclamation T(NIL) -> *
>
> ; (DEFUN STOBJ-PRINT-SYMBOL ...) is being compiled.
> ;; Warning: ret type mismatch in auto-proclamation T(NIL) -> (VALUES T
> T)
>
> ; (DEFUN SAVED-BUILD-DATE-STRING ...) is being compiled.
> ;; Warning: ret type mismatch in auto-proclamation T(NIL) -> *
>
> ;; End of Pass 1.
>
> Program received signal SIGSEGV, Segmentation fault.
> 0x083bed22 in LI157 (V4812=0x349e76b8, V4813=0x24b27b60, V4814=0x9ebe7d8,
> V4815=0xb5fa8c8) at gcl_recompile.c:27809
> 27809 V4863= make_cons(CMPcadr(CMPcar((V4862))),Cnil);
> (gdb) (gdb)
>
>
> -rwxr-xr-x 1 boyer prof 3724 Jul 12 22:04 gcl_profile.lsp
> -rw-r--r-- 1 boyer prof 156 Jul 12 22:04 gcl_recompile.c
> -rw-r--r-- 1 boyer prof 112 Jul 12 22:04 gcl_recompile.data
> -rw-r--r-- 1 boyer prof 66 Jul 12 22:04 gcl_recompile.h
> -rw-r--r-- 1 boyer prof 0 Jul 12 22:04 gcl_recompile.lsp
> -rw-r--r-- 1 boyer prof 29148 Jul 12 22:04 gcl_recompile.o
>
> which is strange to me because gcl_recompile.lsp is an empty file and
> gcl_recompile.c does not have very many lines, certainly not 27809.
>
> #include "cmpinclude.h"
> #include "gcl_recompile.h"
> void init_gcl_recompile(){do_init((void *)VV);}
>
> #ifdef SYSTEM_SPECIAL_INIT
> SYSTEM_SPECIAL_INIT
> #endif
>
>
>
>
--
Camm Maguire [EMAIL PROTECTED]
==========================================================================
"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
