gcl-devel
[Top][All Lists]
Advanced

[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




reply via email to

[Prev in Thread] Current Thread [Next in Thread]