[Top][All Lists]
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
[Gcl-devel] Re: GCL 2.7 bug in satisfies?
From: |
Matt Kaufmann |
Subject: |
[Gcl-devel] Re: GCL 2.7 bug in satisfies? |
Date: |
Fri, 13 Feb 2004 14:30:51 -0600 |
Thanks, Camm. I hope to look at your latest acl2 debs soon. I've got
out-of-town guests this weekend, so it may be another week or two; let me know
if I should push to get to it sooner than that.
-- Matt
Cc: address@hidden, address@hidden, address@hidden
From: Camm Maguire <address@hidden>
Date: 13 Feb 2004 15:06:45 -0500
User-Agent: Gnus/5.09 (Gnus v5.9.0) Emacs/21.2
Content-Type: text/plain; charset=us-ascii
Greetings!
The change supporing this was put into stable and HEAD cvs on
1/16/04. You can get this if you'd like at
export CVS_RSH=ssh
export CVSROOT=:ext:address@hidden:/cvsroot/gcl
cvs -z9 -q co -d gcl-2.6.1 -r Version_2_6_1 gcl
(stable)
or
cvs -z9 -q co -d gcl-2.6.1 -r Version_2_6_1 gcl
(development)
Regarding the new Debian acl2 packages, I've passed them through the
autobuilders to flush out any potential problems in advance of your
feedback. In short, its looking pretty good. There is a recent libc
on alpha which is interfering with the SGC garbage collection which
the libc people should be fixing soon. And there is an issue which
I've been unable to reproduce on m68k, but think I've fixed anyway.
We'll know for sure in a few days. When I get your comments, I hope
to be able to finalize the package and rebuild once more against the
latest GCL.
The latest acl2 debs can be retrieved at
http://ftp.debian.org/debian/pool/main/a/acl2/
Here is what I get with this build:
=============================================================================
GCL (GNU Common Lisp) (2.6.1) Tue Jan 27 20:46:38 UTC 2004
Licensed under GNU Library General Public 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 5, 2004 17:41:09.
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 "/".
Type :help for help.
ACL2 !>(defstobj mystobj
(outgoingFrame :type (satisfies true-listp) :initially nil))
Summary
Form: ( DEFSTOBJ MYSTOBJ ...)
Rules: NIL
Warnings: None
Time: 0.01 seconds (prove: 0.00, print: 0.01, other: 0.00)
MYSTOBJ
ACL2 !>
=============================================================================
Please let me know if further assistance is needed.
Take care,
Matt Kaufmann <address@hidden> writes:
> Hi, Camm --
>
> An ACL2 user (who I am CCing) has told me that he is using GCL 2.7 with
ACL2
> 2.7, and he got this error:
>
> ACL2 !>
> (defstobj mystobj
> (outgoingFrame :type (satisfies true-listp) :initially nil))
>
>
> Error: Cannot process type (SATISFIES TRUE-LISTP)
>
> Apparently GCL 2.7 cannot handle SATISFIES type declarations. Anyhow, I
> directed him to:
>
> http://people.debian.org/~camm/acl2_2.7-8_i386.deb
> http://people.debian.org/~camm/acl2-doc_2.7-8_all.deb
>
> But if he wants to build ACL2 himself, is there a suitable GCL version? He
> says he can't do the build on his laptop using GCL 2.5.
>
> Thanks --
> -- Matt
>
>
--
Camm Maguire address@hidden
==========================================================================
"The earth is but one country, and mankind its citizens." -- Baha'u'llah