Re: [Gcl-devel] Windows issues - reversion

[Matt Kaufmann]

Hi, Camm --

>> Anyone have 'showstoppers' that need fixing in 2.6.1?  Seems
>> to work great for me with itself, maxima, acl2 and axiom.

Dave Greve reported a 2.6.1 bug (Linux) yesterday that is a bit of a
show-stopper for certain uses of ACL2:

  (proclaim
   '(ftype (function
                 ((satisfies integerp))
                 t)
                foo))

  results in the error:

  Error: (satisfies integerp) is not of type STRING.

I'd be happy to re-send his email if you like.

-- Matt
   Cc: Mike Thomas <address@hidden>, address@hidden,
           Matt Kaufmann <address@hidden>
   From: Camm Maguire <address@hidden>
   Date: 19 Sep 2003 11:24:45 -0400
   User-Agent: Gnus/5.09 (Gnus v5.9.0) Emacs/21.2
   Content-Type: text/plain; charset=us-ascii

   Greetings, and thanks for your feedback!

   Jacques Mequin <address@hidden> writes:

   > I am new, and yet unexperimented, ACL2 user
   > 
   > Originally I have pulled the already built ACL2 image from the
   > ACL2 ftp
   > 
   > The problem is that this image was built with an old GCL 2.5.0
   > release that had a nasty "fixnum" garbage collector bug making
   > sometime the ACL2 user to lose its entire session
   > 
   > Matt, knowing that the bug was fixed, has suggested me to build
   > myself an ACL2 image starting from a recent win32 cvs GCL image
   > 
   > In fact, maybe GCL 2.5.1, or 2.5.2 would have been enough for me
   > but the only available binary on the "cvs" is that 2.5.3 that,
   > like any "cvs", may be unstable
   > 
   > I suggest you to also keep, on line, a stable image of the previous
   > official release

   Not a bad idea.  Binary or source?  What do other binary package
   providers think?

   > 
   > Its is a pain, but to resume my ACL2 work, I have tried to compile
   > an official GCL release for the source tar files
   > Unfortunatly, with cygwin, but for mingw, I have ran into trouble
   > during compilation and I have not yet succeeded to complete a GCL
   > image
   > 
   > Yes, even with the current "cvs" 5.2.3 image the later building of
   > ACL2 can be performed without error
   > The "garbage collector" bug is gone and that solves the issue that
   > was at the origin of all of this
   > But that goes wrong, now, is the fact to (console) interrupt an ACL2
   > long (or looping) proof by a "control-c" no longer returns (as it
   > used to do on 2.5.0) to common lisp top level but directly abort the
   > whole session with an error message
   > This makes ACL2 very painful to use
   > 

   OK, I think we need to finalize 2.6.1, and all build the *same* tree
   and place on the website.  We might call this 2.6.2 if people like,
   and then proceed to work on 2.7.0 pending critical bugs that may
   appear.  Anyone have 'showstoppers' that need fixing in 2.6.1?  Seems
   to work great for me with itself, maxima, acl2 and axiom.

   Take care,

   > Regards,
   >    Jacque
   > 
   > 
   > _______________________________________________
   > Gcl-devel mailing list
   > address@hidden
   > http://mail.gnu.org/mailman/listinfo/gcl-devel
   > 
   > 
   > 

   -- 
   Camm Maguire                                         address@hidden
   ==========================================================================
   "The earth is but one country, and mankind its citizens."  --  Baha'u'llah