Greetings! Matt Kaufmann <[EMAIL PROTECTED]> 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: [EMAIL PROTECTED], [EMAIL PROTECTED], gcl-devel@gnu.org > From: Camm Maguire <[EMAIL PROTECTED]> > 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 <[EMAIL PROTECTED]> 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 <[EMAIL PROTECTED]> > > Subject: Re: random mumblings > > To: [EMAIL PROTECTED] > > CC: [EMAIL PROTECTED], [EMAIL PROTECTED] > > 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 <[EMAIL PROTECTED]> > > Cc: [EMAIL PROTECTED], [EMAIL PROTECTED] > > > > 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 [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
