[Top][All Lists]

[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


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
> 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]