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

[Matt Kaufmann]

Hi, Camm --

I am revisiting a problem pertaining to spaces in filenames, as I go through
issues before an ACL2 2.9 release that I think will happen within a couple of
weeks or maybe a month.  In your email below, you say:

>> I believe this is an issue with older gcl.  I'd appreciate
>> confirmation/refutation on windows.

Here are excerpts from an email Jared Davis sent me pretty recently about just
this issue, on Windows, with GCL 2.6.5.

>> However, the following fails:
>> 
>>    (defun f (x) (+ x 1))
>>    :comp t
>> 
>> For the failure cases, the output is the following:
>> 
>> Compiling C:/test dir/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 ... -O3 -c -w C:/test dir/TMP.c
>>            -o C:/test dir/TMP.o")
>> returned a non-zero value 1.
>> 
>> 
>> So, to me it looks like we just have a problem with not quoting the 
>> "C:/test dir/TMP.c" and "C:/test dir/TMP.o".
>> 
>> This is with GCL 2.6.5 using my current installer program.  I tried to 
>> replicate this problem on Linux (using GCL 2.6.3), but it seemed to 
>> handle everything fine.

Also: your original email (below) contains the following.

>> Compiling /tmp/foo bar/TMP1.lisp.
>> End of Pass 1.  
>> End of Pass 2.  
>> sh: line 1: cd: /tmp/foo: No such file or directory
>> OPTIMIZE levels: Safety=0 (No runtime error checking), Space=0, Speed=3
>> Finished compiling /tmp/foo bar/TMP1.lisp.

You said:

>> There are these issues with the shell, someone doing a (system "cd
>> ..."), but as far as I can tell this is not GCL.  Could it be acl2?

I don't see any (system "cd ...") in the ACL2 sources, and besides, it appears
above that the "sh" complaint is between "Compiling..." and "Finished
compiling...", which suggests to me that it's not related to anything ACL2 is
doing.  (That is, unless there is some sort of mixture of output to stdout and
stderr that makes it wrong for me to draw conclusions about the ordering of
output.)

Anyhow, I think that's all I know about the spaces issue, but I figured it was
time to pull it together in case you have time to look into this.  As Jared
pointed out to me (not included above), this isn't terribly critical for ACL2
since Windows users can avoid putting ACL2 in a path with spaces.

Thanks!
-- Matt
   Cc: address@hidden, address@hidden,
           address@hidden, address@hidden
   From: Camm Maguire <address@hidden>
   Date: 09 Mar 2004 18:33:50 -0500
   User-Agent: Gnus/5.09 (Gnus v5.9.0) Emacs/21.2
   Content-Type: text/plain; charset=us-ascii

   Greetings, and thanks for your diagnostics!

   I believe this is an issue with older gcl.  I'd appreciate
   confirmation/refutation on windows.  Here is my session with recent
   gcl (2.6.1)/acl2 on linux:

   >(pathname "/tmp/foo bar")

   #p"/tmp/foo bar"

   >(si::chdir (pathname "/tmp/foo bar"))

   #p"/tmp/foo bar"

   >(namestring (pathname "/tmp/foo bar"))

   "/tmp/foo bar"

   >(si::chdir (namestring (pathname "/tmp/foo bar")))

   "/tmp/foo bar"

   and

   $ mkdir /tmp/foo\ bar
   $ cd /tmp/foo\ bar
   $ acl2
   Licensed under GNU Library General Public License
   Modifications of this banner must retain notice of a compatible license
   Dedicated to the memory of W. Schelter

   Use (help) to get some basic information on how to use GCL.

    ACL2 Version 2.7 built February 16, 2004  00:38:53.
    Copyright (C) 2002  University of Texas at Austin
    ACL2 comes with ABSOLUTELY NO WARRANTY.  This is free software and you
    are welcome to redistribute it under certain conditions.  For details,
    see the GNU General Public License.

    Initialized with (INITIALIZE-ACL2 'INCLUDE-BOOK *ACL2-PASS-2-FILES* T).
    See the documentation topic note-2-7 for recent changes.

    NOTE!!  Proof trees are disabled in ACL2.  To enable them in emacs,
    look under the ACL2 source directory in interface/emacs/README.doc; 
    and, to turn on proof trees, execute :START-PROOF-TREE in the ACL2 
    command loop.   Look in the ACL2 documentation under PROOF-TREE.

    Contains corrections to the code in proof-checker.lisp made subsequent 
    to the official ACL2 2.7 release

   ACL2 Version 2.7.  Level 1.  Cbd "/tmp/foo bar/".
   Type :help for help.

   ACL2 !>(comp t)

   Compiling /tmp/foo bar/TMP.lisp.
   End of Pass 1.  
   End of Pass 2.  
   sh: line 1: cd: /tmp/foo: No such file or directory
   OPTIMIZE levels: Safety=0 (No runtime error checking), Space=0, Speed=3
   Finished compiling /tmp/foo bar/TMP.lisp.
   Loading /tmp/foo bar/TMP.o
   start address -T 0x864db90 Finished loading /tmp/foo bar/TMP.o
   Compiling /tmp/foo bar/TMP1.lisp.
   End of Pass 1.  
   End of Pass 2.  
   sh: line 1: cd: /tmp/foo: No such file or directory
   OPTIMIZE levels: Safety=0 (No runtime error checking), Space=0, Speed=3
   Finished compiling /tmp/foo bar/TMP1.lisp.
   Loading /tmp/foo bar/TMP1.o
   start address -T 0x864d890 Finished loading /tmp/foo bar/TMP1.o
    T
   ACL2 !>

   There are these issues with the shell, someone doing a (system "cd
   ..."), but as far as I can tell this is not GCL.  Could it be acl2?

   In the same directory:

   :/tmp/foo bar$ /usr/bin/gcl
   GCL (GNU Common Lisp)  2.6.1 CLtL1   Mar  9 2004 02:21:23
   Source License: LGPL(gcl,gmp), GPL(unexec,bfd)
   Binary License:  GPL due to GPL'ed components: (READLINE BFD UNEXEC)
   Modifications of this banner must retain notice of a compatible license
   Dedicated to the memory of W. Schelter

   Use (help) to get some basic information on how to use GCL.

   >(compile-file "TMP1.lisp")

   Compiling TMP1.lisp.
   End of Pass 1.  
   End of Pass 2.  
   OPTIMIZE levels: Safety=0 (No runtime error checking), Space=0, Speed=3
   Finished compiling TMP1.lisp.
   #p"TMP1.o"

   >(load "TMP1.o")

   Loading TMP1.o
   start address -T 0x83f8a00 Finished loading TMP1.o
   40

   >

   Take care,

   Matt Kaufmann <address@hidden> writes:

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

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