Re: [Gcl-devel] 2.6.2.....

[Matt Kaufmann]

Hi --

I agree that the absence of a .cert file signifies that something is wrong
(perhaps I'm stating it more strongly than you are).  Something apparently
broke during the so-called "certification" of that file ("book" in ACL2
parlance).

-- Matt
   Cc: address@hidden, Matt Kaufmann <address@hidden>
   From: Camm Maguire <address@hidden>
   Date: 08 Jun 2004 16:03:33 -0400
   User-Agent: Gnus/5.09 (Gnus v5.9.0) Emacs/21.2
   Content-Type: text/plain; charset=us-ascii
   X-SpamAssassin-Status: No, hits=-3.7 required=5.0
   X-UTCS-Spam-Status: No, hits=-343 required=180

   Greetings!

   "Mike Thomas" <address@hidden> writes:

   > PS.  Further results on Windows ACL 2.8 overnight run
   > 
   > | ==================================================
   > | ACL 2.8 (timings not accurate as the machine worked hard on other stuff
   > | here)
   > | 
   > | time make mini-proveall
   > | Mini-proveall passed.
   > | 
   > | real    0m1.235s
   > | user    0m0.228s
   > | sys     0m0.123s
   > | 
   > | time make certify-books-short:
   > | ...
   > | Short test passed.
   > | make[1]: Leaving directory `/c/lang/source/gcl/acl2-sources-2.8/books'
   > | 
   > | real    6m31.938s
   > | user    0m30.579s
   > | sys     0m25.813s
   > | 
   > | Left the long version of book certification running overnight.
   > 
   > $ time make certify-books >make_cert.log 2>&1
   > 
   > real    74m36.766s
   > user    0m47.680s
   > sys     0m41.224s
   > 
   > This test included all the extra books (workshops etc) and gave one error:
   > 
   >   ACL2 Error in ( INCLUDE-BOOK "sets" ...):  There is no certificate
   >   ./books/workshops/1999/ivy/ivy-v2/ivy-sources/base.out
   > 

   While I wouldn't worry about this one too much, it is odd.
   Certificates should have .cert extensions.  Typically when one cannot
   be found, then there is a descriptive error in the .out file
   corresponding to the missing .cert.  Is it possible that some
   directory is not in place?

   It will be interesting to see at some post 2.6.2 point how this time
   changes when the SGC et.al. macros are added to config.h

   Take care,

   > 
   > 
   > 
   > _______________________________________________
   > Gcl-devel mailing list
   > address@hidden
   > http://lists.gnu.org/mailman/listinfo/gcl-devel
   > 
   > 
   > 

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