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

[Matt Kaufmann]

Hi, Jens --

The issues you described are, I believe, all issues with the underlying GCL
and/or GCC rather than ACL2.  I'll leave it to the GCL experts to deal with
them.  Anyhow, I'm glad you're up and running now.

-- Matt
   From: "Jens Rickhoff" <address@hidden>
   Cc: "'Mike Thomas'" <address@hidden>,
           <address@hidden>
   Date: Tue, 9 Mar 2004 00:04:12 -0600
   Content-Type: text/plain;
           charset="us-ascii"
   X-Priority: 3 (Normal)
   X-MSMail-Priority: Normal
   Importance: Normal
   X-MimeOLE: Produced By Microsoft MimeOLE V6.00.2800.1165

   All,

   I think I found out what the problem was. Let's look at the gcc error
   message again:

   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.

   I investigated further, and strangly the problem did not occur in
   another directory(!), I was able to compile just fine:

   ACL2 !>(comp t)
   Compiling C:/acl2/bin/TMP.lisp.
   End of Pass 1.   
   End of Pass 2.   
   OPTIMIZE levels: Safety=0 (No runtime error checking), Space=0, Speed=3 
   Finished compiling C:/acl2/bin/TMP.lisp. Loading C:/acl2/bin/TMP.o
   start address -T 10f7d400 Finished loading C:/acl2/bin/TMP.o
   Compiling C:/acl2/bin/TMP1.lisp. 
   End of Pass 1.   
   End of Pass 2.   
   OPTIMIZE levels: 
   Safety=0 (No runtime error checking), Space=0, Speed=3 
   Finished compiling C:/acl2/bin/TMP1.lisp. Loading C:/acl2/bin/TMP1.o
   start address -T 10f7d624 Finished loading C:/acl2/bin/TMP1.o
    T
   ACL2 !>

   So I assume gcc complains about the space in the path "...Program
   Files..."
   and thinks it's the start of another option instead. The error message
   is just completely misleading. And gcc is not broken at all.

   Is there a way to change the gcc call from ACL2 so that it escapes
   spaces in the file name, or to put the entire file name in quotes before
   sending it off to gcc?


   Also, I noticed that (comp t) does not work from a root directory:

   ACL2 !>:comp t
   Compiling D://TMP.lisp.
   Error: Cannot create the file //TMP.data.
   Fast links are on: do (si::use-fast-links nil) for debugging
   Error signalled by LET.
   Broken at COND.  Type :H for Help.
   ACL2>>

   At first I thought that there is an easy solution to all these
   problems: use ACL2 under Linux, and not Windows ;-)
   But unfortunately, under Linux even the ACL2 start fails when it is
   called from a path that contains a space:

   jabberwock.cs.utexas.edu$ cd "my files"
   jabberwock.cs.utexas.edu$ ../acl2
   GCL (GNU Common Lisp)  Version(2.5.0) Tue Aug 27 18:02:58 CDT 2002
   Licensed under GNU Library General Public License
   ...
   Error: "/v/filer1a/v0q010/rickhoff/378/my files/" cannot be coerced to a
   pathname.
   Fast links are on: do (si::use-fast-links nil) for debugging
   Error signalled by LISP:LAMBDA-CLOSURE.
   Broken at COND.  Type :H for Help.
   ACL2>>


   Thanks for all your help,

   -- 
   Jens Rickhoff
   Computer Sciences Senior
   The University of Texas at Austin