# /bin/csh
#
set nqthmsources="ftp://ftp.cs.utexas.edu/pub/boyer/nqthm/nqthm-2nd-edition.tar.gz"
#
# The standard cvs command, which gets the latest 2.7.0, is one command:
# set cvsgcl = "cvs -z3 -Q -d:pserver:anonymous@cvs.sv.gnu.org:/sources/gcl checkout gcl"
#
# To use CVS to get an older version seems to require two commands: 
# setenv CVSROOT :pserver:anonymous@cvs.sv.gnu.org:/sources/gcl
# set cvsgcl = "cvs -z9 -q co -d gcl -D 20051214 gcl"
#
# For now, we just want the latest 2.7.0:
set cvsgcl = "cvs -z3 -Q -d:pserver:anonymous@cvs.sv.gnu.org:/sources/gcl checkout gcl"
#
set mailto="boyer@cs.utexas.edu"
set tmpdir=`pwd`/$$tmp
date
echo "\
Trying to time test Nqthm-1992 in Gnu Common Lisp 2.7.0 (aka cvs head).\
This may take a couple of hours, in 2006 anyway.\
Output will be written to the file ${tmpdir}/time-nqthm.text.\
At the conclusion, summary mail will be sent to ${mailto}.\
We now delete the directory ${tmpdir}, if it exists, and then recreate it.\
Look at the end of the file ${tmpdir}/time-nqthm.text for the string\
          All Nqthm-1992 tests completed successfully.\
That text precedes the sought timing results for doing the Nqthm proofs.\
GCL will be built in ${tmpdir}/gcl\
Nqthm will be built in ${tmpdir}/nqthm-1992\
To later run this GCL execute ${tmpdir}/gcl/bin/gcl\
To later run the Nqthm execute ${tmpdir}/nqthm-1992/nqthm-1992\
To flush all files created do rm -rf ${tmpdir}"
rm -rf ${tmpdir}
mkdir ${tmpdir}
cd ${tmpdir}
#
echo '(in-package "USER") (load "nqthm.lisp") (compile-nqthm) (load-nqthm)\
      (setq si::*multiply-stacks* 4) \
      (si::chdir "examples") \
      (load "dir.lisp") \
      (load "driver.lisp")' > time-nqthm-helper.text
#
echo "Trying to fetch Nqthm."
echo "Trying to time test Nqthm-1992 in Gnu Common Lisp 2.7.0 (aka cvs head)." >& time-nqthm.text
echo "Nqthm-1992 sources fetched from ${nqthmsources}." >>& time-nqthm.text
echo "GCL sources fetched from ${cvsgcl}." >>& time-nqthm.text
cat /proc/cpuinfo >>& time-nqthm.text
echo "One may wish to tail -f ${tmpdir}/time-nqthm.text to watch the progress."
cat /proc/meminfo >>& time-nqthm.text
wget ${nqthmsources} >>& time-nqthm.text
echo "Got Nqthm."
#
tar vzxf nqthm-2nd-edition.tar.gz >>& time-nqthm.text
#
echo "Trying to fetch GCL."
${cvsgcl} >>& time-nqthm.text
echo "Got GCL."
cd gcl
echo "Building GCL."
time nice ./configure --quiet --silent --enable-ansi  \
	    --disable-statsysbfd --enable-locbfd \
            >>&  ../time-nqthm.text
echo "That was GCL configure time."
echo "Making GCL."
time nice make >>&  ../time-nqthm.text
echo "That was GCL make time."
cd ../nqthm-1992
echo "Trying to build and run Nqthm-1992."
time nice ../gcl/bin/gcl < ../time-nqthm-helper.text >>&  ../time-nqthm.text
echo "That was Nqthm-1992 building and proving time."
cd ..
head -100 time-nqthm.text > mailtmp
tail -20 time-nqthm.text >> mailtmp
sendmail -i boyer@cs.utexas.edu < mailtmp
echo "Mail sent."
date