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

[Camm Maguire]

Greetings, and please excuse this followup to an old email.  Am going
through all that I saved as outstanding GCL issue emails in
preparation for 2.6.6.  

The windows-whitespace-pathname issue in compile-file has been fixed
in 2.6.6, at least as it appears in analogous testing in axiom.

Take care,

Matt Kaufmann <address@hidden> writes:

> 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
> 
> 
> _______________________________________________
> Gcl-devel mailing list
> address@hidden
> http://lists.gnu.org/mailman/listinfo/gcl-devel
> 
> 
> 

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