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

[Mike Thomas]

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.