Re: [Gcl-devel] Re: Chasing down a compiler bug

[Matt Kaufmann]

Hi, Camm --

You're welcome, and sorry about the defect in my reply; I was imagining that
you would replace the definition in raw Lisp.  The problem is that ACL2 doesn't
know about the FORMAT function and insists that it know about all functions
used in its source code (with some exceptions but never mind that....).  The
following should work:

(defun remove-after-last-directory-separator (p)
  (let* ((p-rev (reverse p))
         (posn (position *directory-separator* p-rev)))
    (if posn
        (subseq p 0 (1- (- (length p) posn)))
      (er hard 'remove-after-last-directory-separator
          "foo Implementation error!  Unable to handle a directory string.~x0 
~x1 ~x2~%"
          p p-rev *directory-separator*))))

-- Matt
   Cc: address@hidden, address@hidden
   From: Camm Maguire <address@hidden>
   Date: 24 Feb 2004 17:56:01 -0500
   User-Agent: Gnus/5.09 (Gnus v5.9.0) Emacs/21.2
   Content-Type: text/plain; charset=us-ascii

   Hi Matt!  Thanks for the quick reply!

   The below looks great, its just that when I try to compile a test acl2
   with a patched remove-after-last-directory-separator calling format, I
   get

   ACL2 Error in ( DEFUN REMOVE-AFTER-LAST-DIRECTORY-SEPARATOR ...): 
   The symbol FORMAT (in package "COMMON-LISP") has neither a function
   nor macro definition in ACL2.  Please define it.

   I did it like this, though:

   (defun remove-after-last-directory-separator (p)
     (let* ((p-rev (reverse p))
            (posn (position *directory-separator* p-rev)))
       (if posn
           (subseq p 0 (1- (- (length p) posn)))
         (er hard 'remove-after-last-directory-separator
             (format nil "foo Implementation error!  Unable to handle a 
directory string.~S ~S ~S~%" p p-rev *directory-separator*)))))


   Perhaps the problem is that I'm trying to use the return value of
   format?  

   Take care,

   Matt Kaufmann <address@hidden> writes:

   > Hi, Camm --
   > 
   > I have a feeling that what I'm about to suggest already occurred to you (or
   > maybe something simpler did), and you've already ruled it out.  That said:
   > 
   > I wonder if you could just print every call, like this:
   > 
   > (defun remove-after-last-directory-separator (p)
   >   (format t "(remove-after-last-directory-separator ~s)~%" p)
   >   (let* ((p-rev (reverse p))
   >          (posn (position *directory-separator* p-rev)))
   >     (if posn
   >         (subseq p 0 (1- (- (length p) posn)))
   >       (er hard 'remove-after-last-directory-separator
   >           "Implementation error!  Unable to handle a directory string."))))
   > 
   > The last such format issued before an error would at least lead to the
   > offending call.
   > 
   > Sorry if I missed your point though (as I suspect I did).  Feel free to try
   > asking again.
   > 
   > Here's an alternate idea that is superseded by my suggestion above, but 
since
   > it's what I first thought of I figure I might as well mention it:
   > 
   > (defvar *my-stream* (open "xxx" :direction :input))
   > 
   > (defun my-assert (x)
   >   (or (eval x)
   >       (error "Assertion failed, ~s" x)))
   > 
   > Then at the end of the run:
   > 
   > (load "xxx")
   > 
   > An error would at least show that it's not GCL's fault.
   > 
   > (defun remove-after-last-directory-separator (p)
   >   (let* ((p-rev (reverse p))
   >          (posn (progn (format t
   >                               "(my-assert (equal '~s (reverse '~s)))~%"
   >                               p-rev p)
   >                       (position *directory-separator* p-rev))))
   >     (format t
   >             "(my-assert (equal '~s (position *directory-separator* 
'~s)))~%"
   >             posn p-rev)
   >     (if posn
   >         (subseq p 0 (1- (- (length p) posn)))
   >       (er hard 'remove-after-last-directory-separator
   >           "Implementation error!  Unable to handle a directory string."))))
   > 
   > -- Matt
   >    Cc: address@hidden, address@hidden
   >    From: Camm Maguire <address@hidden>
   >    Date: 24 Feb 2004 17:14:04 -0500
   >    User-Agent: Gnus/5.09 (Gnus v5.9.0) Emacs/21.2
   >    Content-Type: text/plain; charset=us-ascii
   > 
   >    Greetings!  There is what in all likelihood appears to be a gcc
   >    optimization bug on hppa which is erratically causing the acl2 full
   >    test to fail when any optimization at all is enabled.  Some runs of
   >    the book certifier pass, others fail, but when they fail, it is in
   >    precisely the same point:
   > 
   >    (defun remove-after-last-directory-separator (p)
   >      (let* ((p-rev (reverse p))
   >        (posn (position *directory-separator* p-rev)))
   >        (if posn
   >       (subseq p 0 (1- (- (length p) posn)))
   >     (er hard 'remove-after-last-directory-separator
   >         "Implementation error!  Unable to handle a directory string."))))
   > 
   >    Evidently posn is nil at times when it shouldn't be.
   > 
   >    I want to make sure this is not gcl's fault, preferably before
   >    release. 
   > 
   >    In any case, acl2 is so well isolated from the underlying lisp that I
   >    am hard pressed to simply set a gdb break point at this failure.  I
   >    can't use format, error, anything I can trap.  Do you have any advice? 
   > 
   >    Take care,
   >    -- 
   >    Camm Maguire                                            address@hidden
   >    
==========================================================================
   >    "The earth is but one country, and mankind its citizens."  --  
Baha'u'llah
   > 
   > 
   > _______________________________________________
   > 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