Greetings! Function proclaiming is indeed critical for GCL 2.6 and earlier. Without signature information at compile time, the function itself is compiled in the most generic fashion possible, as are calls to it. Typically systems compile themselves twice, collecting and generating proclaims in the first pass and then using them in the second. GCL 2.7 and later generate and incorporate the signature information (and the lisp source for the purposes of recompilation) for a given function as it is compiled. If the compiled function is loaded, all subsequently compiled calls to the function will also be optimal. Previously compiled calls will not, but will proceed correctly albeit slowly. There are several utilities which can iterate over the functions in an image and detect calls which need recompilation, optionally executing the same and even updating the original .o file presuming it is still available. By hand proclamations still work, but are only active when the named compiled function is not at hand.
I had a dream that each system would basically compile and load itself in order of dependency, with perhaps the utilities running at the end to catch a few exceptions, compiling programs in one step instead of two. The default build sequence of most programs using GCL, alas, do not follow this paradigm, resulting in the utilities having to recompile most files a second time anyway. If any of you have suggestions I am all ears. Please feel free to ask questions if unclear. Take care, Matt Kaufmann <matthew.j.kaufm...@gmail.com> writes: > Hi Bob, > > I agree that it might be worthwhile to investigate further use of > proclaiming by ACL2 (i.e., beyond GCL). Below are a couple of notes > that only hint at issues involved. I confess that it looks like a > potentially burdensome task that I'm not excited to take on, > especially now that my funding seems to have about dried up. But > maybe I'll get more interested after I complete the Version 8.6 > release, which has been somewhat time-consuming the last few days > (many, many steps that aren't widely known) but might be completed > this coming week. The first step might be as simple as to change the > value of *do-proclaims* to t. > > Here is a relevant passage from the comment to which I pointed you > (Essay on Proclaiming). > > ; At one time we proclaimed for CCL, but one profiling run of a > ; compute-intensive include-book form showed that this was costing us some 10% > ; of the time. After checking with Gary Byers we decided that there was > little > ; if any benefit in CCL for proclaiming functions, so we no longer do it. > ; Perhaps we should reconsider some time. See also comments below in > ; *do-proclaims*. > > Here is a relevant passage from :DOC note-3-0-1 (August, 2006). > > We have changed the automatic declaration of function types (still > done in GCL and OpenMCL only, for now). Our motivation was to > avoid the assumption that Common Lisp functions return one value > when ACL2 says that they do; thanks to Bob Boyer for bringing this > issue to our attention with the example of defining (foo x y) to be > (floor x y). ACL2 was saying that foo returns a single value, but > because floor returns two values in raw Lisp, so does foo. Other > changes to automatic declaration include comprehending [defund], > not just [defun]. > > Thanks, > Matt > > On Sat, Oct 5, 2024 at 9:51 PM Robert Boyer <robertstephenbo...@gmail.com> > wrote: > > Excellent! > > Forgive me for wondering whether CCL might benefit from the proclaims too. I > have used CCL a lot, but was never aware that it was doing proclaims. It > would never have occurred to me that SBCL was doing proclaims except that it > printed some mild warnings at > me when it disagreed! > > Bob > > On Sat, Oct 5, 2024 at 11:23 PM Matt Kaufmann <matthew.j.kaufm...@gmail.com> > wrote: > > Hi Bob, > > We definitely have code for this, not always used. Read below if > you want details. > > I think we proclaim (or declaim) function types only for GCL. If you > search for "Essay on Proclaiming" in source file acl2-fns.lisp, you'll > see a discussion about that, including documentation for the form > (defvar *do-proclaims* ...) just below the comment there. You'll see > that *do-proclaims* is nil except for GCL, and that > make-defun-declare-form is a no-op unless *do-proclaims* is non-nil. > I believe that make-defun-declare-form is what we call (in various > places) to declaim function types. > > I'll probably take a look at this stuff tomorrow, but I don't know > that I'd want to make any changes this close to the release. (I've > already spent many hours running all sorts of tests, which I prefer > not to re-run.) But thanks for the reminder about this issue. I > think that most who use ACL2 intensely fetch it from github, so > changes we make after the release (in github) would still have value. > > Thank you (via other emails) for all those additional typos! > > -- Matt > > On Sat, Oct 5, 2024 at 6:18 PM Robert Boyer <robertstephenbo...@gmail.com> > wrote: > > Dearest Matt and J, > > When you admit a new function with ACL2's 'defun', do you also 'proclaim' or > 'declaim' its signature in Lisp? Before calling the real 'defun'? > > I don't remember about that sort of thing. I bet you can check whether you > do in 60 seconds. I can remember lots of declaiming in Nqthm, but only for > the prover's functions. > > This is crucial because, for GCL and perhaps all other Lisps except SBCL, > this will speed up execution time by maybe 2x. > > Why? Because then a 'call' does not have to worry about 'optional' args or > multiple return values if it is not necessary to worry about them. Of > course, if the function does have optional args or multiple return values, > you must proclaim things properly. > > Fortunately, in ACL2 and SBCL, you can/could access the proclamations for > all called functions in a new function when inferring the proclamation for > the new function. SBCL whines if it runs into an undefined function. > > With Highest Regards, > > Bob > -- Camm Maguire c...@maguirefamily.org ========================================================================== "The earth is but one country, and mankind its citizens." -- Baha'u'llah
