[Top][All Lists]
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
[Gcl-devel] Re: address@hidden: RE: certifying M1]
|
From: |
Camm Maguire |
|
Subject: |
[Gcl-devel] Re: address@hidden: RE: certifying M1] |
|
Date: |
22 Mar 2004 10:53:59 -0500 |
|
User-agent: |
Gnus/5.09 (Gnus v5.9.0) Emacs/21.2 |
Greetings!
Matt Kaufmann <address@hidden> writes:
> Thanks, Camm! That was quick! With your latest, the "sh: cd:" error from
> before has also gone away. All looks good.
>
Great!
> 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/)?
>
I'd copy the source tree or use cvs. I doubt the windows binary has
caught up yet as I just committed yesterday. The "space-filename" fix
was unix, not windows, specific. The time macro fix was generic.
> Also, do you mind if we distribute an ACL2 executable based on this GCL?
>
I feel the current state is very robust on Linux, FreeBSD, MacOSX, and
Solaris. We still have at least one Windows issue to chase down which
is a bit nasty. With this warning, I of course have no qualms about
you distributing ACL2 on this GCL.
Take care,
> 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
>
>
>
--
Camm Maguire address@hidden
==========================================================================
"The earth is but one country, and mankind its citizens." -- Baha'u'llah