[Gcl-devel] Re: address@hidden: ACL2 on GCL on a MAC]

[Camm Maguire]

Greetings!  The issue appears to be that on some (as yet undetermined
subclass of) systems, SGC is not working.  A known workaround is to
echo '(fmakunbound 'si::sgc-on)(si::save-system "foo")' | saved_gcl &&
mv foo saved_gcl, though this is obviously not optimal from a
performance standpoint.  John and Aurelien are reportedly exchanging
working and broken images in an attempt to get to the bottom of this.

Take care,

Matt Kaufmann <address@hidden> writes:

> P.S. I've heard back from Robert that this isn't a pressing issue for him.  So
> unless I hear from John or Camm, I'll probably let this one go until/unless I
> get another such complaint, in which case Robert has given me access to his
> machine so I could perhaps look into it.
> 
> From: Matt Kaufmann <address@hidden>
> Subject: ACL2 on GCL on a MAC
> To: address@hidden, rkrug, address@hidden
> CC: hunt
> Date: 28 May 2004 15:16:08 -0500
> 
> Hi --
> 
> I've had two reports of problems building ACL2 on GCL on a Mac.  Today I got
> this from Robert Krug:
> 
> >> I just tried compiling ACL2 with GCL on my Mac, but GCL
> >> hung after the main build but before saving the image.
> >> I followed the instructions on the web page and GCL itself
> >> seems OK, so I have no idea what to try next.
> 
> About a week ago John Matthews sent the email included below, I think to the
> same effect (it never made it to acl2-help because of a mail server glitch),
> but I replied that he might want to contact Camm.
> 
> Anyhow, I don't yet have a clue about what's going on.  The solution might be
> for Robert to get me access to his Mac (actually I think I already have that
> access).  But I wanted to get us all in the loop in case John has already
> solved the problem, or Camm is already aware of it, etc.
> 
> Camm and John, do you have any thoughts about this?  Camm, could it be a
> problem with si::save-system?
> 
> One solution might be to get a binary (perhaps selecting 2.8.3 from
> ftp://ftp.debian.org/debian/pool/main/a/acl2/), but it would still be good to
> get to the bottom of this.
> 
> Thanks --
> - -- Matt
> >    Received: from galois.com (galoisconnections.com [206.103.62.46])
> >        by iceman.cc.utexas.edu (8.9.3p2/8.9.3/cc-lists.mc-1.30) with  
> > ESMTP id UAA09709
> >        for <address@hidden>; Wed, 19 May 2004 20:03:38  
> > -0500 (CDT)
> >    Received: from [192.168.50.52] (209-162-200-41.dv0sn.easystreet.com  
> > [209.162.200.41])
> >        (authenticated bits=0)
> >        by galois.com (8.12.8/8.12.8) with ESMTP id i4K13bl1018537
> >        (version=TLSv1/SSLv3 cipher=RC4-SHA bits=128 verify=NO);
> >        Wed, 19 May 2004 18:03:38 -0700
> >    Mime-Version: 1.0 (Apple Message framework v613)
> >    Content-Type: text/plain; charset=US-ASCII; delsp=yes; format=flowed
> >    Message-Id: <address@hidden>
> >    Content-Transfer-Encoding: 7bit
> >    Cc: address@hidden
> >    From: John Matthews <address@hidden>
> >    Subject: Can't build ACL2 using GCL under Mac OS X 3.3
> >    Date: Wed, 19 May 2004 18:03:36 -0700
> >    To: address@hidden
> >    X-Mailer: Apple Mail (2.613)
> >
> >    GCL seems to be hanging when executing a "check and save" phase of
> >    ACL2's build.
> >
> >    I have a 1.5 GHz Mac Powerbook G4, running Mac OS X 10.3.3 (Build  
> > 7G43).
> >
> >    I've installed the Mac developer tools, and used fink to install GNU
> >    sed. My gcc version is
> >    3.3 20030304 (Apple Computer, Inc. build 1495).
> >
> >    I used this cvs command to check out the latest GCL files:
> >
> >       export CVS_RSH=ssh
> >       cvs -z3 -d :ext:address@hidden:/cvsroot/gcl co gcl
> >
> >    I then set the following environment variables:
> >
> >        ulimit -s 8192
> >        export PATH=/sw/bin:/sw/sbin:/usr/local/bin:$PATH
> >        export MACOSX_DEPLOYMENT_TARGET=10.2
> >        export LIBRARY_PATH=/sw/lib
> >        export C_INCLUDE_PATH=/sw/include
> >        export CPPFLAGS="-no-cpp-precomp"
> >
> >    I then called configure, make, and make install within the GCL
> >    directory, which were all successful.
> >    gcl was installed into /usr/local/bin.
> >
> >    I downloaded ACL2 2.8, and typed
> >
> >       make large
> >
> >    One of the "check and save" phases seems to have hung.
> >    Here are the last few pages of output:
> >
> >    -------------
> >
> >    Finished loading
> >    '((IN-PACKAGE "ACL2")
> >       (DEFCONST *COMMON-LISP-SYMBOLS-FROM-MAIN-LISP-PACKAGE*
> >             '(&ALLOW-OTHER-KEYS *PRINT-MISER-WIDTH*
> >                                 &AUX *PRINT-PPRINT-DISPATCH*
> >                                 &BODY *PRINT-PRETTY* &ENVIRONMENT ...))
> >       (DEFCONST *ACL2-VERSION* "ACL2 Version 2.8")
> >       (DEFCONST
> >        *ACL2-FILES*
> >        '("axioms" "basis" "translate" "type-set-a"
> >               "linear-a" "type-set-b" "linear-b" ...)
> >        "*acl2-files* is the list of all the files necessary to build
> >    ACL2 from scratch.")
> >       (DEFCONST *COMMON-LISP-SPECIALS-AND-CONSTANTS*
> >             '(* ** *** *BREAK-ON-SIGNALS*
> >                 *COMPILE-FILE-PATHNAME*
> >                 *COMPILE-FILE-TRUENAME*
> >                 *COMPILE-PRINT* ...))
> >       (DEFCONST *STOBJ-INLINE-DECLARE* '(DECLARE #))
> >       (DEFMACRO MAKE-PACKAGE-ENTRY
> >             (&KEY NAME IMPORTS
> >                   HIDDEN-P BOOK-PATH DEFPKG-EVENT-INFO)
> >             (CONS 'LIST* (CONS NAME #)))
> >       ...).
> >
> >
> >    ACL2 loading '((COMP-FN :EXEC NIL STATE)).
> >    Compiling /Applications/acl2/acl2-sources/TMP1.lisp.
> >    [GC for 224 ARRAY pages..(T=31).GC finished]
> >    [GC for 224 ARRAY pages..(T=30).GC finished]
> >    [GC for 224 ARRAY pages..(T=32).GC finished]
> >    End of Pass 1.
> >    End of Pass 2.
> >    OPTIMIZE levels: Safety=0 (No runtime error checking), Space=0,  
> > Speed=3
> >    Finished compiling /Applications/acl2/acl2-sources/TMP1.lisp.
> >    Loading TMP1.o
> >    [GC for 2098 CONTIGUOUS-BLOCKS pages..(T=34).GC finished]
> >    [GC for 2098 CONTIGUOUS-BLOCKS pages..(T=38).GC finished]
> >    [GC for 2098 CONTIGUOUS-BLOCKS pages..(T=37).GC finished]
> >    [GC for 2098 CONTIGUOUS-BLOCKS pages..(T=36).GC finished]
> >    [GC for 2098 CONTIGUOUS-BLOCKS pages..(T=37).GC finished]
> >    [GC for 2098 CONTIGUOUS-BLOCKS pages..(T=37).GC finished]
> >    [GC for 2098 CONTIGUOUS-BLOCKS pages..(T=36).GC finished]
> >    [GC for 2098 CONTIGUOUS-BLOCKS pages..(T=35).GC finished]
> >    start address -T 0xf66000 Finished loading TMP1.o
> >      T
> >
> >    Finished loading '((COMP-FN :EXEC NIL STATE)).
> >
> >     
> > *********************************************************************** 
> > *
> >    ******
> >           Initialization complete, beginning the check and save.
> >     
> > *********************************************************************** 
> > *
> >    ******
> >    Loading akcl-acl2-trace.lisp
> >    Warning: TRACE is being redefined.
> >    Warning: UNTRACE is being redefined.
> >    Finished loading akcl-acl2-trace.lisp
> >    [GC for 7543 CONS pages..(T=27).GC finished]
> >    [SGC on]
> >    Finished loading
> >    '((IN-PACKAGE "ACL2")
> >       (DEFCONST *COMMON-LISP-SYMBOLS-FROM-MAIN-LISP-PACKAGE*
> >             '(&ALLOW-OTHER-KEYS *PRINT-MISER-WIDTH*
> >                                 &AUX *PRINT-PPRINT-DISPATCH*
> >                                 &BODY *PRINT-PRETTY* &ENVIRONMENT ...))
> >       (DEFCONST *ACL2-VERSION* "ACL2 Version 2.8")
> >       (DEFCONST
> >        *ACL2-FILES*
> >        '("axioms" "basis" "translate" "type-set-a"
> >               "linear-a" "type-set-b" "linear-b" ...)
> >        "*acl2-files* is the list of all the files necessary to build
> >    ACL2 from scratch.")
> >       (DEFCONST *COMMON-LISP-SPECIALS-AND-CONSTANTS*
> >             '(* ** *** *BREAK-ON-SIGNALS*
> >                 *COMPILE-FILE-PATHNAME*
> >                 *COMPILE-FILE-TRUENAME*
> >                 *COMPILE-PRINT* ...))
> >       (DEFCONST *STOBJ-INLINE-DECLARE* '(DECLARE #))
> >       (DEFMACRO MAKE-PACKAGE-ENTRY
> >             (&KEY NAME IMPORTS
> >                   HIDDEN-P BOOK-PATH DEFPKG-EVENT-INFO)
> >             (CONS 'LIST* (CONS NAME #)))
> >       ...).
> >
> >
> >    ACL2 loading '((COMP-FN :EXEC NIL STATE)).
> >    Compiling /Applications/acl2/acl2-sources/TMP1.lisp.
> >    [GC for 224 ARRAY pages..(T=31).GC finished]
> >    [GC for 224 ARRAY pages..(T=30).GC finished]
> >    [GC for 224 ARRAY pages..(T=32).GC finished]
> >    End of Pass 1.
> >    End of Pass 2.
> >    OPTIMIZE levels: Safety=0 (No runtime error checking), Space=0,  
> > Speed=3
> >    Finished compiling /Applications/acl2/acl2-sources/TMP1.lisp.
> >    Loading TMP1.o
> >    [GC for 2098 CONTIGUOUS-BLOCKS pages..(T=34).GC finished]
> >    [GC for 2098 CONTIGUOUS-BLOCKS pages..(T=38).GC finished]
> >    [GC for 2098 CONTIGUOUS-BLOCKS pages..(T=37).GC finished]
> >    [GC for 2098 CONTIGUOUS-BLOCKS pages..(T=36).GC finished]
> >    [GC for 2098 CONTIGUOUS-BLOCKS pages..(T=37).GC finished]
> >    [GC for 2098 CONTIGUOUS-BLOCKS pages..(T=37).GC finished]
> >    [GC for 2098 CONTIGUOUS-BLOCKS pages..(T=36).GC finished]
> >    [GC for 2098 CONTIGUOUS-BLOCKS pages..(T=35).GC finished]
> >    start address -T 0xf66000 Finished loading TMP1.o
> >      T
> >
> >    Finished loading '((COMP-FN :EXEC NIL STATE)).
> >
> >     
> > *********************************************************************** 
> > *
> >    ******
> >           Initialization complete, beginning the check and save.
> >     
> > *********************************************************************** 
> > *
> >    ******
> >    Loading akcl-acl2-trace.lisp
> >    Warning: TRACE is being redefined.
> >    Warning: UNTRACE is being redefined.
> >    Finished loading akcl-acl2-trace.lisp
> >    [GC for 7543 CONS pages..(T=27).GC finished]
> >    [SGC on]
> >
> >    --------
> >
> >    The GCL process continues to take up nearly 50% of the CPU cycles,
> >    although almost none of that time is in user mode. The GCL process  
> > has
> >    been running for over 20 minutes now.
> >
> >    Does anyone have any ideas? I've been building from source because I
> >    don't know where to download a binary version of either GCL or ACL2
> >    that runs on Mac OS X.
> >
> >    Thanks,
> >
> >    -john
> >
> >
> >    John Matthews
> >    Sr. Technical Staff                              Assistant  
> > Professor,
> >    CSE Dept.
> >    Galois Connections, Inc.                   Oregon Graduate  
> > Institute at
> >    OHSU
> >    http://www.galois.com                         
> > http://cse.ogi.edu/~johnm
> >    (503) 626-6616, ext. 121
> ----------
> 
> 
> 
> 

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