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 <[EMAIL PROTECTED]> 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: [EMAIL PROTECTED], [EMAIL PROTECTED]
> From: Camm Maguire <[EMAIL PROTECTED]>
> 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 <[EMAIL PROTECTED]> 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 <[EMAIL PROTECTED]>
> > Subject: [EMAIL PROTECTED]: Re: benchmarking]
> > To: [EMAIL PROTECTED]
> > 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 <[EMAIL PROTECTED]>
> > To: [EMAIL PROTECTED]
> > CC: [EMAIL PROTECTED], [EMAIL PROTECTED]
> > In-reply-to: <[EMAIL PROTECTED]> (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 <[EMAIL PROTECTED]>
> > CC: [EMAIL PROTECTED], [EMAIL PROTECTED]
> >
> > > I will leave /p/bin/xg untouched until I hear you are done
> > > with it.
> >
> > Bob
> > - ------- End of forwarded message -------
> > ----------
> >
> >
> >
> >
>
> --
> Camm Maguire [EMAIL
> PROTECTED]
> ==========================================================================
> "The earth is but one country, and mankind its citizens." -- Baha'u'llah
>
>
>
--
Camm Maguire [EMAIL PROTECTED]
==========================================================================
"The earth is but one country, and mankind its citizens." -- Baha'u'llah
_______________________________________________
Gcl-devel mailing list
Gcl-devel@gnu.org
http://lists.gnu.org/mailman/listinfo/gcl-devel
