[Gcl-devel] Re: address@hidden: RE: certifying M1]

[Camm Maguire]

Greetings!

The -c definitely has to be there.  And as the poster said, there is
no -S, so I suspect a bad gcc.  You can just make a dummy test file:

int
main() {
return 0;
}

and try to run the gcc command as specified in *cc* to confirm.  

BTW, there are newer and more robust windows gcl builds available at

http://www.cs.utexas.edu/users/boyer/gcl

Take care,

Matt Kaufmann <address@hidden> writes:

> Hi, Jens --
> 
> [I'm keeping Camm Maguire in the loop in case he's interested or has anything
> to suggest.]
> 
> Hmmm.... From the error message, I wonder if -c shouldn't be there either in
> your environment.  Maybe then try this:
> 
> [start up ACL2]
> :q
> (setq compiler::*cc* "gcc -Wall -fwritable-strings -DVOL=volatile 
> -fsigned-char -march=i386 ")
> (lp)
> (defun foo (x) x)
> :comp t
> 
> Let me know, OK?
> 
> Thanks --
> -- Matt
>    From: "Jens Rickhoff" <address@hidden>
>    Date: Mon, 8 Mar 2004 09:29:20 -0600
>    Content-Type: text/plain;
>          charset="us-ascii"
>    X-Priority: 3 (Normal)
>    X-MSMail-Priority: Normal
>    X-MIMEOLE: Produced By Microsoft MimeOLE V6.00.2800.1165
>    Importance: Normal
> 
>    Hi Matt,
> 
>    thanks for your fast reply.
>    This is weird -- there is no -S in the gcc string:
> 
>    ACL2>compiler::*cc*
>     "gcc -c -Wall -fwritable-strings -DVOL=volatile -fsigned-char
>    -march=i386 "
>    ACL2>
> 
>    Jens
> 
>    > -----Original Message-----
>    > From: Matt Kaufmann [mailto:address@hidden 
>    > Sent: Monday, March 08, 2004 8:11 AM
>    > To: address@hidden
>    > Cc: address@hidden; address@hidden
>    > Subject: Re: address@hidden: RE: certifying M1]
>    > 
>    > 
>    > [Camm, I'm CCing you on this reply in case you're interested 
>    > in a possible
>    > problem with GCL on Windows with its setting of compiler::*cc*.]
>    > 
>    > Jens --
>    > 
>    > It does look like a GCC issue.  I notice the following error 
>    > in your log:
>    > 
>    > gcc: cannot specify -o with -c or -S and multiple compilations
>    > 
>    > Here's what might work.  After starting ACL2, you can go into 
>    > raw Lisp (:q from
>    > ACL2) and evaluate:
>    > 
>    > compiler::*cc*
>    > 
>    > Then try removing -S from the resulting string -- say the 
>    > resulting string is
>    > STR -- and execute:
>    > 
>    > (setq compiler::*cc* STR)
>    > 
>    > I'm hoping this will fix the compiler call, so that you can 
>    > go back into the
>    > ACL2 loop (with (LP)) and execute :COMP T.
>    > 
>    > If this works, you can probably just create a file init.lsp 
>    > in the current
>    > directory that contains the above form (setq compiler::*cc* 
>    > STR), which will
>    > then get evaluated automatically when you start up ACL2 in 
>    > that directory.
>    > 
>    > By the way, here's why I think -S is what needs to be 
>    > removed.  First, here's
>    > the value of compiler:*cc* on the local machine, which has -c 
>    > but not -S:
>    > 
>    >   ACL2>compiler::*cc*
>    > 
>    >   "gcc -c -I../h -Wall -DVOL=volatile 
>    > -I/p/src/gcl-2.5.0-linuxP3/o -fsigned-char -fwritable-strings 
>    > -pipe -O6 -fomit-frame-pointer"
>    > 
>    >   ACL2>
>    > 
>    > Second, the gcc man page seems to suggest that -c and -S 
>    > should not both be
>    > supplied.
>    > 
>    > -- Matt
>    >    Date: Sun, 7 Mar 2004 22:59:45 -0600
>    >    From: J Strother Moore <address@hidden>
>    >    cc: address@hidden
>    >    X-Virus-Scanned: clamd / ClamAV version 0.67, 
>    > clamav-milter version 0.66n
>    > 
>    >    Hi Matt.  One of my students is having a problem compiling.
>    >    Jens, I don't know much about the system level support for Lisp]
>    >    these days, but Matt Kaufmann, the co-author of ACL2, may 
>    > see something.
>    > 
>    >    J
>    >    ------- Start of forwarded message -------
>    >    From: "Jens Rickhoff" <address@hidden>
>    >    To: "'J Strother Moore'" <address@hidden>
>    >    Subject: RE: certifying M1
>    >    Date: Sun, 7 Mar 2004 22:49:21 -0600
>    >    Content-Type: text/plain;
>    >     charset="us-ascii"
>    >    X-Priority: 3 (Normal)
>    >    X-MSMail-Priority: Normal
>    >    In-reply-to: <address@hidden>
>    >    Importance: Normal
>    >    X-MimeOLE: Produced By Microsoft MimeOLE V6.00.2800.1165
>    > 
>    >    Actually, the error occurs when I just try to compile my functions
>    >    with (comp t). ACL2 has certified M1, so it's not a certification
>    >    error as I assumed at first and has nothing to do with M1.
>    > 
>    >    I think it is rather a problem with the gcc version that 
>    > came with the
>    >    distribution of mingw (gcc (GCC) 3.2.3 (mingw special 20030504-1)).
>    >    The good thing is, I was able to finish problem set 5 without the
>    >    (comp t) line, and with a lot of garbage collecting :-).
>    > 
>    >    Here's a transcript:
>    > 
>    >    ACL2 Version 2.7.  Level 1.  Cbd "c:/Program 
>    > Files/emacs-20.7/bin/".
>    >    Type :help for help.
>    > 
>    >    ACL2 !>(comp t)
>    > 
>    >    Compiling c:/Program Files/emacs-20.7/bin/TMP.lisp. 
>    >    End of Pass 1.   
>    >    End of Pass 2.   
>    >    gcc: cannot specify -o with -c or -S and multiple compilations
>    > 
>    >    Error: (SYSTEM "gcc -c -Wall -fwritable-strings -DVOL=volatile
>    >    - -fsigned-char -march=i386   -O2 -fomit-frame-pointer -c 
>    > -w /Program
>    >    Files/emacs-20.7/bin/TMP.c -o /Program Files/emacs-20.7/bin/TMP.o")
>    >    returned a non-zero value 1. 
>    >    Fast links are on: do (si::use-fast-links nil) for debugging
>    >    Error signalled by UNLESS. 
>    >    Broken at COND.  Type :H for Help. 
>    >    ACL2>>
>    > 
>    > 
>    > 
>    >    Jens
>    > 
>    >    > -----Original Message-----
>    >    > From: J Strother Moore [mailto:address@hidden 
>    >    > Sent: Sunday, March 07, 2004 10:35 PM
>    >    > To: address@hidden
>    >    > Cc: address@hidden
>    >    > Subject: Re: certifying M1
>    >    > 
>    >    > 
>    >    > Hi Jens.  You'll have to tell me more.  Is your file 
>    > named M1.lisp
>    >    > or m1.lisp?  Show me 
>    >    > 
>    >    >  % pwd
>    >    > and
>    >    >  % ls -l m1.*
>    >    > 
>    >    > and then send me a transcript of the ACL2 session from the 
>    >    > time you started
>    >    > ACL2 to the error.
>    >    > 
>    >    > J
>    >    > 
>    >    > 
>    >    ------- End of forwarded message -------
>    > 
>    > 
> 
> 
> 

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