[Gcl-devel] Re: GCL on the Mac

[Camm Maguire]

Greetings!  Some other acl2 users had setup a mac account for me
sometime ago for the purpose of gcl work.  I just tried following the
login instructions and failed.  Will write separately regarding this
and try again.  Am also cc'ing Aurelien, a gcl developer who reported
success with acl2/gcl on the mac.  Aurelien, if you have any time to
try to reproduce this, I'd be most grateful.

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