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

[Camm Maguire]

P.S. just a note in passing as before stated, it certainly appears
that gcl and acl2 are both implementing very similar type inferencing
logic.  It would be great some day to consolidate.

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