[Top][All Lists]
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: [Gcl-devel] Re: address@hidden: RE: certifying M1]
From: |
Camm Maguire |
Subject: |
Re: [Gcl-devel] Re: address@hidden: RE: certifying M1] |
Date: |
15 Jan 2005 18:01:06 -0500 |
User-agent: |
Gnus/5.09 (Gnus v5.9.0) Emacs/21.2 |
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
[Prev in Thread] |
Current Thread |
[Next in Thread] |
- Re: [Gcl-devel] Re: address@hidden: RE: certifying M1],
Camm Maguire <=