gcl-devel
[Top][All Lists]
Advanced

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Gcl-devel] Re: apparent GCL/Windows issue


From: Camm Maguire
Subject: [Gcl-devel] Re: apparent GCL/Windows issue
Date: 11 Aug 2003 12:21:44 -0400
User-agent: Gnus/5.09 (Gnus v5.9.0) Emacs/21.2

Greetings!

Matt Kaufmann <address@hidden> writes:

> Hi, Camm --
> 
> An ACL2 user, Jared Davis, is having problems with ACL2 on Windows/GCL, as
> reported below.  It appears that the crash was in the middle of a GC, so I
> suspect it's a GCL issue.  The ACL2 binary he is using was built on a GCL
> obtained quite awhile ago, from:
> 
> ftp://ftp.gnu.org/gnu/gcl/cvs/gcl-cvs-20021014-mingw32.zip
> 

Mike, can you comment on whether diffs between then and now might be relevant?

> Perhaps we need to build ACL2 on a more up-to-date Windows/GCL.  But I went to
> both ftp://ftp.gnu.org/pub/gnu/gcl/ and ftp://ftp.gnu.org/pub/gnu/gcl/cvs/ and
> there isn't any GCL 2.5.x to be found.  Any suggestions?
> 

The ftp site at gnu.org was apparently compromised.  They are trying
to restore files asap.  Mike, if you could upload your latest tarball
again, I think it should appear within 24 hours at the site.

> Thanks --
> -- Matt
> From: Jared C Davis <address@hidden>
> Subject: Problem certifying arithmetic-2 library
> To: address@hidden
> Date: Fri, 8 Aug 2003 19:23:34 -0500
> Reply-To: address@hidden
> 
> 
> 
> 
> 
> My VSSP is done and I need to make it work on Windows for some other people
> who won't be very familiar with ACL2.  I am trying to put together a sort
> of package deal for them, but I'm having some trouble getting the
> arithmetic-2 books to certify.
> 
> I have Cygwin installed and the appropriate tools (gcc, make, etc), and am
> trying to use the binary Windows image for ACL2.  I also downloaded the
> source tarball for ACL 2.7 to get the actual books from.
> 

Currently, GCL only supports MinGW32 as opposed to cygwin.
Personally, I'd like to see both eventually supported, but our Windows
expert vouches highly for the superiority of the former, and I defer
to his judgement.  Mike, could the presence of the cygwin libs cause
problems here?


> I can certify the arithmetic book without a problem, but "make
> cancel-terms-meta.cert" fails with:
> 
>    make[2]: *** [cancel-terms-meta.cert] Error 128
> 
> Looking at the cancel-terms-meta.out file, I see pages of "[GC for 100
> FIXNUM pages..[GC for 100 FIXNUM pages..[GC for 100 FIXNUM pages.."
> immediately following the following:
> 

Mike, could this possibly be due to the following patch, committed
shortly after the build they are using was cut?

(sid)address@hidden:/fix/t1/camm/gcl-2.5.4/o$ cvs log unixtime.c

...
revision 1.15
date: 2002/11/19 03:05:59;  author: mjthomas;  state: Exp;  lines: +34 -11
make_fixnum() called GBC(t_fixnum) called runtime() called make_fixnum...
----------------------------


Take care,


> Summary
> Form:  ( DEFUN PREFER-POSITIVE-FACTORS-SCATTER-EXPONENTS-<-FN ...)
> Rules: ((:TYPE-PRESCRIPTION GOOD-ARG))
> Warnings:  None
> Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
> [GC for 3917 CONS pages..(T=233368).GC finished]
> 
> I don't really know how to debug this.  I don't get an overflow message,
> but it seems like some sort of overflow/loop.  Any ideas?
> 
> Thanks,
>     Jared
> ----------
> 
> 
> 
> 

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




reply via email to

[Prev in Thread] Current Thread [Next in Thread]