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

[Matt Kaufmann]

Hi --

Just a comment you and Camm can use or ignore as you choose....

We maintain ACL2 in a manner such that the workshop books are all expected to
certify.  When I'm testing a local ACL2 build, I typically run the full
regression suite (including the workshop books) and I expect 100% to pass.

Perhaps the failure was just some weird Windows glitch, which would go away in
a re-run?

-- Matt
   From: "Mike Thomas" <address@hidden>
   Cc: <address@hidden>, "Matt Kaufmann" <address@hidden>
   Date: Tue, 15 Jun 2004 09:18:43 +1000
   Content-Type: text/plain;
           charset="US-ASCII"
   X-Priority: 3 (Normal)
   X-MSMail-Priority: Normal
   Importance: Normal
   X-MimeOLE: Produced By Microsoft MimeOLE V6.00.2800.1409
   X-SpamAssassin-Status: No, hits=-4.7 required=5.0
   X-UTCS-Spam-Status: No, hits=-304 required=180

   Hi Camm.

   | Greetings!  I'm a bit confused here -- do we post that mingw passes
   | the acl2 books certify test or not?  We just are using 'make
   | certify-books-fresh' for this purpose, i.e. no workshops.  Please
   | advise.

   Call it a pass as it is workshop code and Matt seems not to be too worried
   or, best of all, add a footnote if you can be bothered.

   Cheers

   Mike Thomas