[Top][All Lists]
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
[Gcl-devel] Re: address@hidden: RE: certifying M1]
|
From: |
Matt Kaufmann |
|
Subject: |
[Gcl-devel] Re: address@hidden: RE: certifying M1] |
|
Date: |
Sun, 21 Mar 2004 21:24:31 -0600 |
Thanks, Camm! That was quick! With your latest, the "sh: cd:" error from
before has also gone away. All looks good.
I've got an ACL2 user (Jared Davis) at UT who would like to build a Windows
version with this fix. Do you have one available (or, can he just copy your
source tree from /u/camm/debian/i386/gcl-2.6.1/)?
Also, do you mind if we distribute an ACL2 executable based on this GCL?
Thanks again --
-- Matt
cc: address@hidden
From: Camm Maguire <address@hidden>
Date: 21 Mar 2004 21:46:07 -0500
User-Agent: Gnus/5.09 (Gnus v5.9.0) Emacs/21.2
Content-Type: text/plain; charset=us-ascii
Greetings, Matt and thanks for your report as always! Think both this
and the time macro issue you wrote about separately are now fixed.
Please check it out. Am rebuilding the .deb at your site now.
Take care,
Matt Kaufmann <address@hidden> writes:
> Thanks, Camm. I think there is still a GCL problem. Below is a transcript
> using your executable, but I also unpacked the debian you pointed me to
and got
> essentially the same result
> (/projects/acl2/lisps/gcl/gcl_2.6.1-34_i386/usr/bin/mygcl). If instead I
first
> do (si::chdir "test one") and then (compile-file "abcd.lisp"), the problem
goes
> away.
>
> craigievar:~/temp/gcltest> /u/camm/debian/i386/gcl-2.6.1/bin/gcl
> GCL (GNU Common Lisp) 2.6.1 ANSI Mar 21 2004 06:38:14
> Source License: LGPL(gcl,gmp), GPL(unexec,bfd)
> Binary License: GPL due to GPL'ed components: (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 "test one/abcd.lisp")
>
> Compiling test one/abcd.lisp.
> End of Pass 1.
> End of Pass 2.
> sh: cd: test: No such file or directory
> gcc: abcd.c: No such file or directory
> gcc: No input files
> (SYSTEM "(cd test one/ ;gcc -c -Wall -DVOL=volatile -fsigned-char
-fwritable-strings -pipe -I/u/camm/debian/i386/gcl-2.6.1/unixport/../h -O3
-fomit-frame-pointer -c abcd.c -w)") returned a non-zero value 0.
>
> Fast links are on: do (use-fast-links nil) for debugging
> Broken at UNLESS. Type :H for Help.
> 1 (Continue) Continues anyway.
> 2 (Abort) Return to top level.
> dbl:>>
>
> Thanks --
> -- Matt
> From: Camm Maguire <address@hidden>
> Date: 21 Mar 2004 08:16:44 -0500
> User-Agent: Gnus/5.09 (Gnus v5.9.0) Emacs/21.2
> Content-Type: text/plain; charset=us-ascii
>
> Greetings! I've placed a .deb of the latest cut (-34) in my home dir
> under debian/i386. Please let me kow if you have problems with it.
>
> Take care,
>
> Matt Kaufmann <address@hidden> writes:
>
> > Hi, Camm --
> >
> > I would like to experiment with a recent gcl on linux i386 to better
understand
> > ACL2's part in the problem of spaces in pathnames. But I can't seem
to
> > complete the download from
> > ftp://ftp.debian.org/debian/pool/main/g/gcl/gcl_2.6.1-18_i386.deb (I
just got a
> > "failed to change directory" error message). I also tried
> > ftp://ftp.debian.org/debian/pool/main/g/gcl/gcl_2.6.1-33_i386.deb in
case that
> > was more appropriate, but without success. And my attempt to use "cvs
> > -d:pserver:address@hidden:/cvsroot/gcl login" never completed.
> >
> > Is there a better place I should try? Do you happen to have such a
GCL lying
> > around at UT CS?
> >
> > 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
> >
> >
> >
>
> --
> Camm Maguire address@hidden
>
==========================================================================
> "The earth is but one country, and mankind its citizens." --
Baha'u'llah
>
>
>
--
Camm Maguire address@hidden
==========================================================================
"The earth is but one country, and mankind its citizens." -- Baha'u'llah