[Axiom-developer] Re: gcl inlining policy

[Matt Kaufmann]

Hi, Camm --

That's exciting that GCL, which is already the fastest Lisp I know of
for running ACL2, may become even faster!  Thank you.

I don't have any opinions about defaults or heuristics, but:

It might be *very* useful to have a user-settable special variable
that controls inlining.  I'm imagining that by default, ACL2 would
inline all built-in and user-defined function calls that GCL allows,
but that when one wants to trace, then it would be nice to be able to
rebuild with inlining turned down or off.

Thanks --
-- Matt
   cc: address@hidden, Matt Kaufmann <address@hidden>,
           address@hidden, address@hidden,
           "Robert Dodier" <address@hidden>,
           Maxima mailing list <address@hidden>
   From: Camm Maguire <address@hidden>
   Date: Fri, 06 Jul 2007 12:58:02 -0400
   X-SpamAssassin-Status: No, hits=-2.5 required=5.0
   X-UTCS-Spam-Status: No, hits=-280 required=200

   Greetings!  If you would be so kind, I'd appreciate some direction on
   the desired inlining policy fro gcl 2.7.0.

   GCL has always inlined certain functions, e.g. mapcar, member, etc.
   Without this, performance would be noticeably worse.

   Traditionally, this has been accomplished though ad-hoc 'c1 functions
   in the compiler, or C-snippet inline attributes in cmpopt.lsp.  Thus
   one had not only to write the function, but its inline support in the
   compiler as well.  Support for these remain, but thanks to Boyer's
   suggestion to carry the original source around in the image, automatic
   inlining is now possible.  Support for this is in place in 2.7 with
   notable improvements in performance.

   The question is, what functions should be inlined by default?
   Currently, symbols external to the lisp package are automatically
   considered. Explicitly declared or declaimed functions are also.
   inlining may decline if the inline is too large, using a heuristic
   function using the *space* setting as input, though in many cases,
   inlined code is smaller.  The real cost of inlining is compiler speed,
   and tracing support.

   Boyer recently posted a benchmark which would benefit greatly from
   automatic inlining of user functions.

   Separately, should inlining be allowed at safety 3?

   Take care, 
   -- 
   Camm Maguire                                         address@hidden
   ==========================================================================
   "The earth is but one country, and mankind its citizens."  --  Baha'u'llah