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

[Mike Thomas]

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