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

[Camm Maguire]

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