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

[Matt Kaufmann]

Hi, Mike --

Thanks for your email and for the points you raised.  I've made a note to look
into removing "nice" in all the workshop books' Makefiles (and perhaps
elsewhere) in favor of $(NICE), where NICE is set to nice in Makefile-generic
(which is included in the other Makefiles).

About .exe: The original extension of .gcl, ${LISPEXT}, is generated by some
ACL2 code.  I'm tempted simply to generate .gcl.exe on Windows as the
extension, so then no $(EXE) would be necessary.  Does that seem reasonable?
(Note that ${LISPEXT} is used in several places in Makefile in addition to the
one you pointed to.)

Thanks again --
-- Matt
   From: "Mike Thomas" <address@hidden>
   Cc: <address@hidden>
   Date: Mon, 28 Jun 2004 14:41:44 +1000
   Content-Type: text/plain;
           charset="iso-8859-1"
   X-Priority: 3 (Normal)
   X-MSMail-Priority: Normal
   X-MimeOLE: Produced By Microsoft MimeOLE V6.00.2800.1409
   Importance: Normal
   X-SpamAssassin-Status: No, hits=-4.9 required=5.0
   X-UTCS-Spam-Status: No, hits=-228 required=180

   Hi Matt.

   You wrote some time ago regarding a problem I had testing GCL 2.6.2 on
   Windows during ACL 2.8 workshop book certification:

   | | The current one can be
   | | obtained by way of
   | | the installation instructions from the ACL2 home page, or directly at:
   | |
   | | ftp://ftp.cs.utexas.edu:/pub/moore/acl2/v2-8/acl2-sources/books/wo
   | | rkshops.tar.gz
   |
   | | Testing the workshops books is icing on the cake, and may not add
   | | enough to be
   | | worth your trouble.  (But since there _was_ an error, I'm glad we
   | | tracked it
   | | down.)  Anyhow, I'm a little surprised actually that there
   | weren't massive
   | | failures using the old workshops/.


   I optimistically replied:

   | I'll let you know how it goes, perhaps this afternoon Australian time.


   Well, sometimes an afternoon almost takes a fortnight on the internet, for
   which my apologies; but here are the results (all clear on Windows including
   workshops):


   WINDOWS ACL 2.8 AND WORKSHOP BOOK BUILD AND CERTIFICATION RESULTS

   $ time make >make.log 2>&1

   real    5m11.125s
   user    0m1.571s
   sys     0m1.864s

   $ time make clean-books >certify-clean.log 2>&1; time make
   certify-books-short
   >certify-short.log 2>&1

   real    3m23.031s
   user    1m50.440s
   sys     1m35.414s

   real    7m12.078s
   user    0m31.466s
   sys     0m27.408s

   $ time make clean-books >certify-clean2.log 2>&1; time make certify-books
   >cert
   ify.log 2>&1

   real    2m57.015s
   user    1m50.546s
   sys     1m32.608s

   real    149m32.328s
   user    3m42.100s
   sys     3m5.417s

   The above certification ignores the workshops; the regression test below
   does not.

   $ time make clean-books >certify-clean2.log 2>&1; time make regression
   >regress
   ion.log 2>&1

   real    3m41.734s
   user    1m51.396s
   sys     1m41.985s

   real    297m30.188s
   user    6m42.119s
   sys     5m51.423s



   MINOR WINDOWS MODIFICATIONS TO ACL 2.8 MAKEFILES

   I modified the top level makefile to use the .exe file extension under MSYS:

   ===========================================================================
   ....
   LISP = gcl
   DIR = /tmp
   ACL2_VERSION = v2-8
   NONSTD =
   EXE= .exe
   ...
   ===========================================================================

   and

   ===========================================================================
   ...
   move-new:
           if [ -f nsaved_acl2.${LISPEXT}$(EXE) ]; then \
           mv -f nsaved_acl2.${LISPEXT}$(EXE) 
${PREFIXsaved_acl2}.${LISPEXT}$(EXE) ;
   fi
   ...
   ===========================================================================

   Before running the certifications I worked around what I believe is a bug in
   MSYS by modifying the paths in the build generated "saved_acl2" script from
   Windows to MSYS format ("/c/rumptdy/dumpty" rather than "c:/rumptdy/dumpty")

   I also used a NICE "books/Makefile-generic" macro to circumvent the lack of
   "nice" on Windows (probably not the best program to use when benchmarking
   GCL anyway):

   ===========================================================================
   NICE =
   #NICE = nice
   ACL2 = time $(NICE) ../../saved_acl2

   (and in the Workshop Makefiles I just deleted nice as there were so many I
   couldn't be bothered to do the full macro bit - perhaps for ACL 2.9 you
   could incorporate all these changes to smooth the ride?)
   ===========================================================================

   All this on a Windows XP 2.4 GHz P4 512 Mb machine, which was working on
   other, generally light but occasionally very heavy, work.

   Cheers

   Mike Thomas.