Greetings! OK, will do, but my result will be the same as yours on this class of machine.
It is conceivable we could get closer to 3 gb by relaxing the power of 2 constraint. Separately, did we not get a 1 billion cons acl2 image on some 64bit machine of yours? Lastly, while I know the Linux kernel has some recent work in this area, something special needs to be done at this level to get a 32bit kernel even to be able to address more than about 2.7 or 3gb, if memory serves. I'm testing a small patch now to 1) prevent recompilation in the final link, and 2) execute it with si::*optimize-maximum-pages* at nil. Image size is going down from ~15k pages to 4200. Take care, Robert Boyer <[EMAIL PROTECTED]> writes: > Just out of curiosity, can I ask you to spend a minute or > two to get into your biggest ACL2 Gnu-Linux GCL environment > and execute these two commands and send me the output? > > (room t) > > (loop for i from 1 collect (progn (print i) (make-list 1000000))) > > Here's what I get here in a big, static, ansi, GCL 2.7.0, > with some enlarged stacks, 32 bit, x86 Intel, > elgin.cs.utexas.edu, with an ACL2 saved image alone that is > now about 220 megabytes. The total number of conses limit > seems to be about 230 million conses, which seems > arithmetically about right at 8 bytes per cons, 1 gb for the > c control stack (where one might instead secret away another > 100 million conses), and 1 gb for the Gnu-Linux/os (and > immediate fixnums). I'd be most happy to send you my > cvs/build commands for these. > > ls -l /p/bin/xa > lrwxrwxrwx 1 boyer public 41 May 26 12:27 /p/bin/xa -> > /u/boyer/acl2/acl2-sources/saved_acl2.gcl > > > Bob > > ------------------------------------------------------------------------------- > > % xa > GCL (GNU Common Lisp) 2.7.0 ANSI Jun 19 2006 13:26:51 > Source License: LGPL(gcl,gmp,pargcl), GPL(unexec,bfd) > Binary License: GPL due to GPL'ed components: (BFD UNEXEC) > Modifications of this banner must retain notice of a compatible license > Dedicated to the memory of W. Schelter > > Use (help) to get some basic information on how to use GCL. > > Temporary directory for compiler files set to /tmp/ > > ACL2 Version 3.0 built June 19, 2006 14:05:21. > Copyright (C) 2006 University of Texas at Austin > ACL2 comes with ABSOLUTELY NO WARRANTY. This is free software and you > are welcome to redistribute it under certain conditions. For details, > see the GNU General Public License. > > Initialized with (INITIALIZE-ACL2 'INCLUDE-BOOK *ACL2-PASS-2-FILES*). > See the documentation topic note-3-0 for recent changes. > Note: We have modified the prompt in some underlying Lisps to further > distinguish it from the ACL2 prompt. > > NOTE!! Proof trees are disabled in ACL2. To enable them in emacs, > look under the ACL2 source directory in interface/emacs/README.doc; > and, to turn on proof trees, execute :START-PROOF-TREE in the ACL2 > command loop. Look in the ACL2 documentation under PROOF-TREE. > > ACL2 Version 3.0. Level 1. Cbd "/v/filer2/boyer/acl2/acl2-sources/". > > Type :help for help. > Type (good-bye) to quit completely out of ACL2. > > ACL2 !>:q > > Exiting the ACL2 read-eval-print loop. To re-enter, execute (LP). > ACL2>(room t) > > WS UP/MP FI% GC TYPES > > 2 10000/10000 53.8% CONS FIXNUM SHORT-FLOAT CHARACTER IFUN SPICE > 8 2448/2448 2.5% ARRAY PATHNAME BIT-VECTOR VECTOR HASH-TABLE > STREAM CCLOSURE CLOSURE > 4 1196/1196 7.1% STRUCTURE BIGNUM RATIONAL LONG-FLOAT COMPLEX > READTABLE CFUN > 10 600/600 58.9% SYMBOL > 14 1/2 52.1% PACKAGE > 6 1000/1000 25.0% SFUN STRING RANDOM-STATE GFUN VFUN AFUN CFDATA > > 20803/24690 contiguous (233 blocks) > 10000 hole > 2610 0.0% relocatable > > 15245 pages for cells > 48658 total pages > 450397 pages available > 25233 pages in heap but not gc'd + pages needed for gc marking > 524288 maximum pages > > > Key: > > WS: words per struct > UP: allocated pages > MP: maximum pages > FI: fraction of cells in use on allocated pages > GC: number of gc triggers allocating this type > > word size: 32 bits > page size: 4096 bytes > heap start: 0x8000000 > heap max : 0x88000000 > shared library start: 0x0 > cstack start: 0xc0000000 > cstack mark offset: 223 bytes > cstack direction: downward > cstack alignment: 16 bytes > cstack max: 934215679 bytes > immfix start: 0xc0000000 > immfix size: 536870912 fixnums > NIL > > ACL2>(loop for i from 1 collect (progn (print i) (make-list 1000000))) > > 1 [SGC for 465 CONS pages..(9378 writable)..(T=7).GC finished] > > 2 > 3 [SGC for 5465 CONS pages..(14378 writable)..(T=29).GC finished] > > 4 [SGC for 7167 CONS pages..(16080 writable)..(T=35).GC finished] > > 5 > 6 [SGC off][GC for 2610 RELOCATABLE-BLOCKS pages..(T=64).GC finished] > [GC for 2610 RELOCATABLE-BLOCKS pages..(T=64).GC finished] > [SGC on][SGC for 19970 CONS pages..(26240 writable)..(T=16).GC finished] > > 7 > 8 > 9 > 10 > 11 > ... much deleted > 216 > 217 > 218 > 219 > 220 > 221 > 222 > 223 [SGC for 66434 CONS pages..(72708 writable)..(T=369).GC finished] > [SGC for 66434 CONS pages..(72708 writable)..(T=370).GC finished] > [SGC for 66434 CONS pages..(72709 writable)..(T=371).GC finished] > [SGC for 66434 CONS pages..(72709 writable)..(T=279).GC finished] > > time to give up > > > -- 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
