[Gcl-devel] Re: fast ACL2 build

[Camm Maguire]

Greetings!

Robert Boyer <address@hidden> writes:

> Getting the ACL2 build time down to 3 minutes and 44 seconds real time in GCL
> 2.7.0 is great!  (elgin.cs.utexas.edu)
> 
>  Trying to build ACL2 in /v/filer2/boyer/acl2/acl2-sources at Thu Mar 23 
> 06:33:05 CST 2006
>  end date                                                     Thu Mar 23 
> 06:36:49 CST 2006
> 

Great!  Separately, just committed:

1) compiler macros for intersection, union, set-difference,
   set-exclusive-or, and subsetp.  The idea behind these is to catch
   inlinable :key and :test arguments.  We might consider declining
   the inline when no such arguments are present.  Cleaned up the
   function versions too so that the no :key/:test case is optimally
   fast.  About to maroon the si::member1 hack, but still needed for
   adjoin.  Those interested might enjoy benchmarking a compiled
   version of (lambda (x y) (intersection x y :key 1+ :test (lambda (x
   y) (= (* 2 x y) y)))) for example.

2) Better nthcdr handling, capturing finite first arg cases and
   relying on new type inferencing in c1if.

3) rotatef fix, car propagator, si::seqindp predicate

4) Hopefully fix package handling at load time.  defpackage and
   make-package only are duplicated at the top of the load file --
   likely make-package should be a move rather than a copy.  The
   package must exist to read the data symbols in the data vector,
   which must be in place before executing the init forms, which
   typically would contain the package ops.... At least this allows
   maxima compilation without intervention.  If some kind soul would
   like to narrow down the test suite failures with cvs head, I'd be
   most grateful.

The expander code needs centralization, as does certain inferencing
code (two-tp-inf/num-bounds, all code involving *restore-vars*).
Also, would like to eventually move to an eq type hashing strategy,
but don't see how this would be a win, and to dump a startup hash
table into the final saved image containing all the self compilation
relationships. 

safety 3 has come up recently.  This mode is actually slower than
running interpreted in many cases.  Briefly, safety 1 means check
arguments and types, safety 2 means prevent unsafe inlines, and safety
3 means "push events", which means that all function calls go on the
ihs stack and proceed through funcall_with_catcher.  Several of the
ansi tests would be remarkably faster if the auxiliary code under
ansi-tests was compiled at anything less than 3.  Alternately, we
could dispose with this mode or otherwise prevent it in ansi-tests.
Advice/suggestions here most appreciated.

The *compile-tests* switch has been great at testing the inliners --
my previous request to Paul for more random-compiler tests for certain
sequence functions appears less important now.  

Just checked the last ansi run -- there may be a temporary performance
issue. 

Take care,

> Bob
> 
> 
> 

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