[Gcl-devel] Re: address@hidden: address@hidden: Re: benchmarking]]

[Camm Maguire]

Greetings, and thanks!

This should be fixed now.  add-hash is protected everywhere by a check
against *compiler-auto-proclaim*, and user proclamations are "eq-type"
normalized before processing just as autogenerated ones are.

I'll be committing some related minor cleanups of the same
synchronization nature in a little bit which should not affect
anything. 

1) what is compiler::proclamation for?  It doesn't appear to be called
   by anything, and is not in the spec.

2) Do any of you use defentry?  I am considering an unrelated commit
   for xgcl which is slightly backward incompatible.  Namely, the
   defentry asserts C proclamations for its functions -- if the user
   had
        a) put in a static definition or proclamation by hand using
           clines 
        b) included c headers with conflicting proclamations, or
        c) entered as C function name a string with an explicit cast,
           e.g. "(object)my_c_fun"
   this will result in C compile failure.  I've cleaned up the few
   such instances in gcl itself, just wondering what else might be out
   there.   In any case, some C proclamation is needed for correct
   usage on certain machines which pass arguments on other than word
   sized boundaries, e.g. amd64.

Take care,

Matt Kaufmann <address@hidden> writes:

> Good morning --
> 
> Thank you for looking into this.
> 
> I agree with Bob's answer:
> 
> >> I think that you should regard any xargs declaration as
> >> nothing more than a comment to be ignored.
> 
> But just in case you're simply looking for some intuition about this (and 
> since
> I've written most of this reply already!), I'll send this along in case you
> find it useful.  (Feel free to ignore it!)
> 
> Roughly speaking, the (declare (xargs :guard form)) syntax asserts that ACL2
> expects form to be true whenever the function is called.  More precisely, ACL2
> is set up so that only when the above assertion is suitably proved, will ACL2
> invoke Common Lisp to evaluate calls of the function whose arguments satisfy
> the guard.
> 
> However, Common Lisp itself will ignore such declare forms (that's Bob's 
> point,
> I think).
> 
> In the case of aset1, the guard does imply that we have an (unsigned-byte 31).
> Maybe that's what you were asking.  The rest of this email justifies that
> claim, but please don't feel obligated to read it, of course!
> 
> In the definition of aset1 we find:
> 
>   #+acl2-loop-only
>   (declare (xargs :guard (and (array1p name l)
>                               (integerp n)
>                               (>= n 0)
>                               (< n (car (dimensions name l))))))
> 
> But the definition of array1p implies that (car (dimensions name l)) is less
> than 2^31; hence from the above, so is n.  Here are the relevant snippets of
> code.
> 
> (defun array1p (name l)
> ....
>        (let ((header-keyword-list (cdr (assoc-eq :header l))))
> .....
>               (let ((dimensions (cadr (assoc-keyword :dimensions 
> header-keyword-list)))
> .....
>                 (and
> .....
>                      (integerp (car dimensions))
>                      (integerp maximum-length)
>                      (< 0 (car dimensions))
>                      (< (car dimensions) maximum-length)
>                      (<= maximum-length *maximum-positive-32-bit-integer*)
> ....
> 
> where:
> 
> (defconst *maximum-positive-32-bit-integer*
>   (1- (expt 2 31)))
> 
> (defun dimensions (name l)
> .....
>   (cadr (assoc-keyword :dimensions
>                        (cdr (header name l)))))
> 
> (defun header (name l)
> .....
>           (assoc-eq :header l))
> .....
> 
> -- Matt
>    Cc: address@hidden, address@hidden
>    From: Camm Maguire <address@hidden>
>    Date: 24 Jun 2006 10:45:50 -0400
>    X-SpamAssassin-Status: No, hits=-1.9 required=5.0
>    X-UTCS-Spam-Status: No, hits=-225 required=200
> 
>    Greetings, and thanks!  Am looking nto this but had one question.  I
>    don't understand the (declare (xargs :guard ...)) syntax.  Though
>    aset1 in axioms.lisp is declaimed with an (unsigned-byte 31) arg, this
>    declaration appears to be asserting an integer type.  If you had any
>    illumination to spare, it would be most appreciated.
> 
>    Take care,
> 
>    Matt Kaufmann <address@hidden> writes:
> 
>    > P.S. I forgot to mention that in
>    > 
>    > /projects/hvg/ACL2/v3-0-hons-no-gcl-proclaim/
>    > 
>    > I did the build with:
>    > 
>    > ../build-acl2.jun23
>    > 
>    > -- Matt
>    > From: Matt Kaufmann <address@hidden>
>    > Subject: address@hidden: Re: benchmarking]
>    > To: address@hidden
>    > CC: boyer, hunt
>    > Date: 23 Jun 2006 23:59:28 -0500
>    > 
>    > Hi, Camm --
>    > 
>    > I think that you asked for a comparison of runs using different proclaim
>    > approaches.  The results are below.  The third one didn't work, but I'll 
> leave
>    > that directory around for now:
>    > 
>    > /projects/hvg/ACL2/v3-0-hons-no-gcl-proclaim/
>    > 
>    > You're welcome to do what you will with it.  Please let me know when I 
> can
>    > delete it.
>    > 
>    > ============================================================
>    > 
>    > Using some sort of hybrid of ACL2 and GCL proclaims:
>    > /projects/hvg/ACL2/v3-0-hons/make-regression.log,
>    > 17438.565u 493.162s 5:02:49.31 98.6%     0+0k 0+0io 3pf+0w
>    > [Minor point: I think about 30 seconds of the above was from cleaning 
> books,
>    > not necessary and hence skipped below.]
>    > 
>    > ============================================================
>    > 
>    > Using GCL proclaims only:
>    > /projects/hvg/ACL2/v3-0-hons-no-acl2-proclaim/make-regression.log,
>    > 17939.093u 560.419s 5:16:23.49 97.4%     0+0k 0+0io 0pf+0w
>    > 
>    > ============================================================
>    > 
>    > Using ACL2 proclaims only, with
>    > (setq compiler::*compiler-auto-proclaim* nil si::*disable-recompile* t):
>    > Build failed.
>    > 
>    > Here's the first error I noticed in the log file,
>    > /projects/hvg/ACL2/v3-0-hons-no-gcl-proclaim/compile-acl2.log:
>    > 
>    > .....
>    > 
>    > Finished loading axioms.lisp
>    > ;; Compiling axioms.lisp.
>    > ;; End of Pass 1.  
>    > ;; End of Pass 2.  
>    > axioms.c: In function `LI268':
>    > axioms.c:19663: warning: initialization from incompatible pointer type
>    > axioms.c:19720: warning: assignment from incompatible pointer type
>    > axioms.c:19720: warning: passing arg 1 of `make_cons1' from incompatible 
> pointer type
>    > axioms.c:19723: warning: initialization from incompatible pointer type
>    > axioms.c:19734: warning: assignment from incompatible pointer type
>    > axioms.c:19734: warning: passing arg 1 of `make_cons1' from incompatible 
> pointer type
>    > axioms.c: In function `LI428':
>    > axioms.c:28102: warning: initialization from incompatible pointer type
>    > axioms.c: In function `L459':
>    > axioms.c:30000: warning: comparison is always true due to limited range 
> of data type
>    > ;; OPTIMIZE levels: Safety=0 (No runtime error checking), Space=0, 
> Speed=3, (Debug quality ignored)
>    > ;; Finished compiling axioms.o.
>    > Loading axioms.o
>    > 
>    > .....
>    > 
>    > Then later (as mentioned in earlier email):
>    > 
>    > .....
>    > 
>    > Loading type-set-b.lisp
>    > 
>    > Raw Lisp Break.
>    > Error in LET [or a callee]: Arg or result mismatch in call to  
> TYPE-SET-BINARY-+-ALIST-ENTRY
>    > 
>    > .....
>    > 
>    > I don't really know how to investigate this further, so I don't plan to 
> do
>    > anything further here.
>    > 
>    > - -- Matt
>    > - ------- Start of forwarded message -------
>    > Date: 23 Jun 2006 22:48:13 -0500
>    > From: Matt Kaufmann <address@hidden>
>    > To: address@hidden
>    > CC: address@hidden, address@hidden
>    > In-reply-to: <address@hidden> (message from
>    >  Robert Boyer on Fri, 23 Jun 2006 12:59:55 -0500)
>    > Subject: Re: benchmarking
>    > 
>    > [Sorry if you all get this twice; I can't tell if it was sent.]
>    > 
>    > Hi, Bob --
>    > 
>    > I completed the run shown here
>    > /projects/hvg/ACL2/v3-0-hons-no-acl2-proclaim/make-regression.log
>    > but I failed in the build as shown here
>    > /projects/hvg/ACL2/v3-0-hons-no-gcl-proclaim/compile-acl2.log
>    > where you'll see:
>    > 
>    > Raw Lisp Break.
>    > Error in LET [or a callee]: Arg or result mismatch in call to  
> TYPE-SET-BINARY-+-ALIST-ENTRY
>    > 
>    > The latter was a run where I started with this change to the sources 
> copied
>    > from /projects/hvg/ACL2/v3-0-hons/:
>    > 
>    > ;;; #+GCL (setq si::*disable-recompile* t)
>    > ;;; Even more than the above:
>    > (setq compiler::*compiler-auto-proclaim* nil si::*disable-recompile* t)
>    > 
>    > I have no idea what's wrong; maybe I'll take a look tomorrow.
>    > 
>    > - - -- Matt
>    >    Date: Fri, 23 Jun 2006 12:59:55 -0500
>    >    From: Robert Boyer <address@hidden>
>    >    CC: address@hidden, address@hidden
>    > 
>    >    > I will leave /p/bin/xg untouched until I hear you are done
>    >    > with it.
>    > 
>    >    Bob
>    > - ------- End of forwarded message -------
>    > ----------
>    > 
>    > 
>    > 
>    > 
> 
>    -- 
>    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