[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 |
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
- [Gcl-devel] Re: apparent GCL/Windows issue,
Camm Maguire <=