[Gcl-devel] Re: GCL on the Mac

[Matt Kaufmann]

Camm --

Cool!  Just wondering -- do you know off the top of your head if it also would
work to use gcl out of the box, provided one edits ACL2's init.lsp file to do
(fmakunbound 'si::sgc-on) as the first step before building ACL2?

Thanks --
-- Matt
   Cc: address@hidden, address@hidden, address@hidden,
           address@hidden, Aurelien Chanudet <address@hidden>
   From: Camm Maguire <address@hidden>
   Date: 07 Dec 2004 21:38:45 -0500
   User-Agent: Gnus/5.09 (Gnus v5.9.0) Emacs/21.2
   Content-Type: text/plain; charset=us-ascii
   X-SpamAssassin-Status: No, hits=-2.6 required=5.0
   X-UTCS-Spam-Status: No, hits=-332 required=180

   Greetings!  OK, I've confirmed.  This is the same strange sgc/macosx
   issue which arose right after 2.6.5 was released.  I believe Aurelien
   has already written on this.  I've forgotten the details, but will dig
   them up.  I now have access to a macosx box and have confirmed this
   there, so perhaps I can help debug.

   In the meantime, there is a workaround.  Before building acl2, do

   gcl
   >(fmakunbound 'si::sgc-on)
   >(si::save-system "foo")

   then

   mv foo <path to your gcl unixport directory>/saved_gcl

   I will test this too and (hopefully) confirm that it resolves all
   problems.

   Take care,

   J Strother Moore <address@hidden> writes:

   > Hi Camm.  I recently installed GCL 2.6.5 on my new Mac G4 laptop.
   > I built ACL2 Version 2.9 from the sources on the ACL2 home page.
   > Then I tried to certify all the books, with
   > 
   > cd v2-9/acl2-sources
   > make certify-books
   > 
   > It ran a while and ultimately seemed to get into an infinite loop 
apparently
   > inside the GCL compiler.  The disk was rattling as though it was doing a 
lot
   > of I/O.  I let it rattle for about 30 minutes, way longer than the
   > compilation should have taken.
   > 
   > The book in question was
   > 
   > v2-9/acl2-sources/books/ordinals/ordinal-definitions.lisp
   > 
   > but you have to more or less run the entire make certify-books to 
   > certify the books it depends on.
   > 
   > Eventually the output looks like this:
   > 
   >    Compiling 
/v/filer3/v0q004/acl2/v2-9/acl2-sources/books/ordinals/ordinal-definitions.lisp.
   >    End of Pass 1.  
   >    [SGC for 5 SYMBOL pages..(23963 writable)..(T=6).GC finished]
   > 
   >    ;; Note: Tail-recursive call of LASTN was replaced by iteration.
   >    ;; Note: Tail-recursive call of OCMP-AUX was replaced by iteration.
   >    ;; Note: Tail-recursive call of NATPART was replaced by iteration.
   >    ;; Note: Tail-recursive call of O-LAST-EXPT was replaced by iteration.
   >    ;; Note: Tail-recursive call of O- was replaced by iteration.
   > 
   >    [at this point it just hangs forever]
   > 
   > I later tried to certify certain other books, and got this
   > error:
   > 
   >    Loading 
/v/filer3/v0q004/acl2/v2-9/acl2-sources/books/data-structures/list-defuns.o
   >    start address -T 0x2759000 Finished loading 
/v/filer3/v0q004/acl2/v2-9/acl2-sources/books/data-structures/list-defuns.o
   > 
   >    Summary
   >    Form:  ( INCLUDE-BOOK "list-defuns" ...)
   >    Rules: NIL
   >    Warnings:  None
   >    Time:  0.28 seconds (prove: 0.00, print: 0.00, other: 0.28)
   >    
"/v/filer3/v0q004/acl2/v2-9/acl2-sources/books/data-structures/list-defuns.lisp"
   >    [SGC for 5 SYMBOL pages..(22881 writable)..(T=3).GC finished]
   >    [SGC for 21 CFUN pages..(22914 writable)..(T=2).GC finished]
   >    [SGC for 452 CONS pages..(22951 writable)..(T=4).GC finished]
   >    Loading 
/v/filer3/v0q004/acl2/v2-9/acl2-sources/books/data-structures/utilities.o
   > 
   >    Error: The default dispatch macro signalled an error.
   >    Fast links are on: do (si::use-fast-links nil) for debugging
   >    Error signalled by ACL2::LOAD-COMPILED-FILE-IF-MORE-RECENT.
   >    Broken at COND.  Type :H for Help.
   > 
   > I don't have the Mac with me right now, so I cannot send you instructions
   > on how to reproduce the second error.  
   > 
   > I don't know if they're related.
   > 
   > GCL was installed on my Mac by Charles Sandel.  He can probably answer
   > questions about what he did.  I've cc'd him.
   > 
   > In the meantime, I'll use OpenMCL.  Sigh.  GCL is faster.
   > 
   > J
   > 
   > 
   > 
   > 

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