[Top][All Lists]
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
[Gcl-devel] Re: P.S. address@hidden: Re: random mumblings]
From: |
Camm Maguire |
Subject: |
[Gcl-devel] Re: P.S. address@hidden: Re: random mumblings] |
Date: |
29 Jun 2006 17:20:17 -0400 |
User-agent: |
Gnus/5.09 (Gnus v5.9.0) Emacs/21.2 |
Greetings!
Matt Kaufmann <address@hidden> writes:
> Wow, seems tricky; thanks for doing this.
>
> Regarding:
>
> >> P.S. Looks like all or most of Matt's arg mismatches ran afoul of
> >> GCL's limit of 10 proclaimed arg types. This is to fit in the alloted
> >> number of bits in the sfun C struct.
>
> Should ACL2 inhibit automatic generation of a declaim form for a function when
> it has more than 10 arguments? I'm guessing it's harmless but simply won't
> give us optimally efficient code, but if it's not harmless, please let me
> know.
>
This is harmless, so pelase leave it in to flow with future
improvements.
Take care,
> Thanks --
> -- Matt
> Cc: address@hidden, address@hidden, address@hidden
> From: Camm Maguire <address@hidden>
> Date: 29 Jun 2006 11:51:52 -0400
> X-SpamAssassin-Status: No, hits=-1.8 required=5.0
> X-UTCS-Spam-Status: No, hits=-223 required=200
>
> Greetings! One quick idea here is to do one build, dump the gcl
> inferred proclaims as is given the command I posted earlier or
> equivalent, then load it at the beginning of a rebuild. This is
> essentially the same as the two pass .fn file based mechanism
> Dr. Schelter put in place -- all we are trying to do now is to do the
> same in one pass and automatically without user intervention.
>
> P.S. Looks like all or most of Matt's arg mismatches ran afoul of
> GCL's limit of 10 proclaimed arg types. This is to fit in the alloted
> number of bits in the sfun C struct.
>
> In general, there is quite a confusion in GCL between a variables type
> and its 'kind' or C storage type. In principle, we should be able to
> proagate the full type entirely apart from the kind, but in practice,
> there are many places where the code assumes that anything of type
> fixnum is also stored as a fixnum. More work ....
>
> Take care,
>
> Matt Kaufmann <address@hidden> writes:
>
> > P.S. In a build where GCL did type inference, the log
> >
> > /projects/hvg/ACL2/v3-0-hons-gcl-proclaim/save-acl2.log
> >
> > did show a lot of "Compiling /tmp/gazonk" and a lot of "recompiling".
> >
> > -- Matt
> > From: Matt Kaufmann <address@hidden>
> > Subject: Re: random mumblings
> > To: address@hidden
> > CC: address@hidden, address@hidden
> > Date: 29 Jun 2006 10:04:57 -0500
> >
> > Hi, Bob --
> >
> > There's a confusing array of ways to build ACL2 these days.
> > Can you point me to a log file with the compilation you mention and a
> build
> > script that was used to create it?
> >
> > For example, in directory
> >
> > /projects/hvg/ACL2/v3-0-hons-jun27/
> >
> > I executed /projects/hvg/ACL2/build-acl2.jun27, and if you look in
> > /projects/hvg/ACL2/v3-0-hons-jun27/save-acl2.log for "Compiling", you'll
> see
> > only compilation of a small file acl2-fns.lisp and then compilation of a
> > TMP*1.lisp file.
> >
> > Similarly, I executed (an alias for) this command in
> /projects/acl2/devel/
> >
> > mv make-fast-gcl.log make-fast-gcl.old.log ; (time nice make
> PREFIX=fast-linux-gcl- LISP=my-fast-gcl) >& make-fast-gcl.log&
> >
> > to create this log file:
> >
> > /projects/acl2/devel/make-fast-gcl.log
> >
> > If you search for the last occurrence of
> >
> > my-fast-gcl < workxxx
> >
> > in that log and then search from there for "Compiling", you'll see only
> > compilation of a small file acl2-fns.lisp and then compilation of a
> TMP*1.lisp
> > file.
> >
> > - -- Matt
> > Date: Thu, 29 Jun 2006 09:37:55 -0500
> > From: Robert Boyer <address@hidden>
> > Cc: address@hidden, address@hidden
> >
> > Let's see if I can revive a stalled conversation.
> >
> > 1. Camm says that it's best not to compile before saving in
> > a GCL 2.7.0 image if one wants the image to be of minimal
> > size.
> >
> > 2. Bob says he'll talk to Matt about how to avoid compiling
> > before saving.
> >
> > 3. Matt says something like "we only compile *1* functions
> > in the last pass of ACL2 building before saving."
> >
> > 4. Bob counts 556 occurrences of the string "compiling" in
> > the text of the last pass and shakes his head in a typical
> > (for him) stupor. Bob thinks that there could be a number
> > of explanations, e.g., nowadays in 2.7.0, compiling some *1*
> > functions sets off a cascade of the recompiling of a host of
> > its callers.
> >
> > Bob
> > ----------
> >
> >
> >
> >
>
> --
> 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