[Gcl-devel] Re: address@hidden: Re: Initially Certifying books error]

[Camm Maguire]

Greetings!  There should have been a whole lot of error output before
the last line you reported.  Could you please post that?  What version
of GCL is this, and from what source?  Do you have reason to believe
there is a path problem?

Take care,

"Matt Kaufmann" <address@hidden> writes:

> Hi, Camm --
> 
> An ACL2 user had problems with compilation using GCL (I'm pretty sure) on
> Windows.  I tried to help, but you might be able to give a better answer.  If
> you can modify GCL to give a more informative error message when compilation
> breaks as shown below, that would be great.
> 
> I'm going out of town shortly.  If you care to reply, please send your reply
> directly to the "To" person below and address@hidden
> 
> Thanks!
> -- Matt
> From: Matt Kaufmann <address@hidden>
> Subject: Re: Initially Certifying books error
> To: address@hidden
> CC: address@hidden
> Date: 24 Nov 2003 17:35:48 -0600
> 
> That error message means that GCL (the underlying lisp) cannot compile.
> Perhaps someone on the acl2-help list has run into this and has some
> suggestions for how to deal with GCL here.
> 
> I *think* that you might be able to fix the problem by escaping to raw Lisp
> (with :q) and doing the following.  First, look at the value of compiler::*cc*
> as follows.
> 
> ACL2>compiler::*cc*
> 
> "gcc -c -Wall -DVOL=volatile -fsigned-char -fwritable-strings -pipe"
> 
> ACL2>
> 
> Then, replace gcc with a full path on your Windows machine to gcc:
> 
> ACL2>(setq compiler::*cc*
>       "C:/..../gcc -c -Wall -DVOL=volatile -fsigned-char -fwritable-strings 
> -pipe")
> 
> That's as far as my knowledge goes here.  If I learn any more, I'll let you
> know.
> 
> - -- Matt
>    From: address@hidden
>    Date: Mon, 24 Nov 2003 18:28:40 EST
>    Reply-to: address@hidden
>    Sender: address@hidden
>    X-Listprocessor-Version: 8.2.10/020311/17:52 -- ListProc(tm) by CREN
>    X-WSS-ID: 13DC4BD59735263-01-01
>    Content-Type: multipart/alternative;
>     boundary=-----------------------------1069716520
> 
>    when I run the command (ld "certify-numbers.lisp"), It runs for a while 
> and 
>    ends up giving me another error at the end:
> 
>    Error: (SYSTEM "gcc -c -Wall -fwritable-strings -DVOL= volatile 
> -fsigned-char 
>    -0 ............ C:/acl2/acl2-sources/books/arithmetic/mod-gcd.c -o  
> returned 
>    a 
>    non-zero value 1.
> 
>    I don't know what to do....
> ----------
> 
> 
> 
> 
> 

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