[Gcl-devel] Re: P.S. address@hidden: Re: random mumblings]

[Camm Maguire]

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