Matt Kaufmann, ACL2 seminar, 8/4/04: Small vs. large images.

Large image advantages:  Verify-termination on system functions, :doc in loop.
Statistics below are for Debian Gnu Linux.
======================================================================
Allegro CL: Approximate 4.9% speedup, 59% image growth.

make-regression-jul31-04-allegro-small.log:
11931.590u 140.430s 3:29:24.01 96.0%	0+0k 0+0io 9718511pf+0w
make-regression-jul31-04-allegro-large.log:
11369.070u 141.610s 3:19:37.46 96.1%	0+0k 0+0io 8983236pf+0w

16867328 Jul 31 23:48 /projects/acl2/v2-9/allegro-saved_acl2.dxl
26861568 Jul 31 15:52 /projects/acl2/v2-9/allegro-large-saved_acl2.dxl
======================================================================
GCL 2.6.3 (no SGC): Approximate 3.6% slowdown, 12% image growth.

make-regression-jul31-04-gcl-small.log:
7683.820u 178.340s 2:17:06.54 95.5%	0+0k 0+0io 12734208pf+0w
make-regression-jul31-04-gcl-large.log:
7971.570u 173.370s 2:20:59.86 96.2%	0+0k 0+0io 13455763pf+0w

40596672 Aug  1 07:26 /projects/acl2/v2-9/linux-gcl-saved_acl2.gcl
45421760 Aug  1 11:57 /projects/acl2/v2-9/linux-gcl-large-saved_acl2.gcl
======================================================================
GCL 2.6.4pre (SGC): Approximate 1.4% slowdown, 26% image growth.

make-regression-jul31-04-gcl-2.6.4pre-small.log:
7750.700u 174.560s 2:17:20.00 96.1%	0+0k 0+0io 12742495pf+0w
make-regression-jul31-04-gcl-2.6.4pre-large.log:
7856.270u 182.790s 2:19:03.05 96.3%	0+0k 0+0io 14345776pf+0w

46234865 Aug  1 23:42 /projects/acl2/v2-9/linux-gcl-2.6.4pre-small-saved_acl2.gcl
58219761 Aug  1 20:18 /projects/acl2/v2-9/linux-gcl-2.6.4pre-large-saved_acl2.gcl
======================================================================
OpenMCL: Approximate 10.7% slowdown, 48% image growth.

make-regression.log:
real	511m9.531s
user	483m31.580s
sys	28m21.530s
make-regression-large.log:
....
real	568m46.501s
user	534m21.490s
sys	32m35.340s

17563424  6 Jun 17:42 saved_acl2.dppccl
26073312  2 Aug 11:43 large-saved_acl2.dppccl
======================================================================
CMUCL: Approximate 2.6% slowdown, 23% image growth.

make-regression-jul31-04-cmucl-small.log:
11081.210u 259.930s 3:25:37.99 91.9%	0+0k 0+0io 8840687pf+0w
make-regression-jul31-04-cmucl-large.log:
11372.140u 261.300s 3:29:01.75 92.7%	0+0k 0+0io 10121698pf+0w

37883904 Aug  2 11:49 /projects/acl2/v2-9/cmucl-saved_acl2.core
46608384 Aug  2 23:27 /projects/acl2/v2-9/cmucl-large-saved_acl2.core
======================================================================