gcl-devel
[Top][All Lists]
Advanced

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Gcl-devel] Re: GCL 2.7 bug in satisfies?


From: Camm Maguire
Subject: [Gcl-devel] Re: GCL 2.7 bug in satisfies?
Date: 13 Feb 2004 15:06:45 -0500
User-agent: Gnus/5.09 (Gnus v5.9.0) Emacs/21.2

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




reply via email to

[Prev in Thread] Current Thread [Next in Thread]