Re: acl2 autobuild
Greetings, and thanks!
OK, about 75% of the way through. There must be something very slow
I'm doing in gcl for m68k. In general, m68k beats arm in compile time
on all floating point and standard C lib packages of mine, but the
reverse is true for these lisp based packages. maxima goes through
quickly, but axiom and acl2 are very slow. Could it be a question of
swap?
Take care,
Wouter Verhelst <wouter@grep.be> writes:
> On Wed, Oct 06, 2004 at 05:00:23PM -0400, Camm Maguire wrote:
> > ... has been running for quite a while now -- is it stuck?
>
> It's still running on zot:
>
> wouter@zot:/var/lib/buildd/logs$ tail -n 22 acl2_2.8-5_20040918-0542
> (:REWRITE EXPT-MINUS)
> (:REWRITE UNICITY-OF-1)
> (:TYPE-PRESCRIPTION BITN-NONNEGATIVE-INTEGER))
> Warnings: None
> Time: 1.88 seconds (prove: 1.02, print: 0.00, other: 0.86)
> (:DEFTHMD BITN-NEGATIVE-BIT-OF-INTEGER)
>
> Summary
> Form: ( DEFTHM STICKY-21-8 ...)
> Rules: ((:DEFINITION =)
> (:DEFINITION NOT)
> (:DEFINITION SYNP)
> (:EXECUTABLE-COUNTERPART BINARY-+)
> (:EXECUTABLE-COUNTERPART EQUAL)
> (:EXECUTABLE-COUNTERPART UNARY--)
> (:FAKE-RUNE-FOR-TYPE-SET NIL)
> (:REWRITE BITN-NEGATIVE-BIT-OF-INTEGER)
> (:REWRITE BITS-WITH-INDICES-IN-THE-WRONG-ORDER)
> (:REWRITE COLLECT-CONSTANTS-IN-<-OF-SUMS))
> Warnings: None
> Time: 10.95 seconds (prove: 10.20, print: 0.00, other: 0.75)
> STICKY-21-8
> wouter@zot:/var/lib/buildd/logs$ date
> Thu Oct 7 17:09:47 CEST 2004
>
> Hope this helps. Note that the date and time the build started is
> embedded in the build log file name...
>
> --
> EARTH
> smog | bricks
> AIR -- mud -- FIRE
> soda water | tequila
> WATER
> -- with thanks to fortune
--
Camm Maguire camm@enhanced.com
==========================================================================
"The earth is but one country, and mankind its citizens." -- Baha'u'llah
Reply to: