#
# This file is adapted from the file examples/driver in the standard
# Nqthm-1992 distribution.

#                            PC-NQTHM-1992 EXAMPLES

#  This file, `examples/driver', contains Unix c-shell (csh) commands for
#  driving Pc-Nqthm-1992 to proof-check all of the example event files distributed
#  in the standard Pc-Nqthm-1992 distribution, which examples may all be found
#  under the `examples' subdirectory.  We describe below how to run this
#  checking process.  There are three very simple steps, SETUP, CLEANING (i.e.,
#  deleting residue from previous attempts, if any) and RUNNING.  Each step is
#  described in the section below of that name.  Needless to say, before
#  running this suite you must have compiled Pc-Nqthm-1992, for which action you
#  will find directions in the installation instructions.  Furthermore, to run
#  this set of examples you must arrange for some Unix command, perhaps
#  `pc-nqthm-1992', to start a Pc-Nqthm-1992 process running, perhaps by having
#  saved a binary image of your Common Lisp of choice, after loading into it
#  the compiled files, under the name pc-nqthm-1992.


#                            WARNINGS TO READ FIRST

#  Beware: in the process of running this file some csh variables whose names
#  begin with `nq' and `NQ' are set.  This should cause you no problem unless
#  you are knowingly using variables by those names for other purposes.  To see
#  what variables you currently have set, and their settings, execute the
#  c-shell command `set' with no arguments.

#  See the comments in the corresponding Nqthm-1992 driver file just above
#  the SETUP section if you are short of disk space or time, as they apply
#  pretty well for Pc-Nqthm also.  Other comments there describe what happens
#  when you use this makefile.


#                                     SETUP

#  The SETUP phase consists of examining, and perhaps editing, the three `set'
#  commands below.

#  1.  Make sure that the Unix command `pc-nqthm-1992' runs Pc-Nqthm-1992 at
#  your site, or else edit the `set NQRUN' line below appropriately.

set NQRUN="../../pc-nqthm-1992"


#  2.  To run this set of examples in a Common Lisp, such as CMU Common Lisp,
#  that does not terminate when reading end-of-file, you will need to edit the
#  `set NQQUIT' line below.  CMU Common Lisp is the only Lisp we know that
#  requires such an edit.  For CMU Common Lisp, use `set NQQUIT = "(quit)"'.
#  For certain other Lisps, it may be possible to set this variable to help
#  handle cases in which proofs fail due to some sort of stack overflow or
#  Nqthm-1992 bug.  For example, we use `:q' as the value of NQQUIT for AKCL so
#  that, if for some totally unexpected reason, a Lisp error arises and Lisp
#  goes into an error break, the `:q' will be read, rather than an eof, with
#  the result that AKCL will quit to the top level of Lisp, making an
#  Nqthm-1992 library on the way out, because of an `unwind-protect' in
#  `prove-file'.

set NQQUIT=" :q #+CMU (QUIT) #+Allegro (EXIT) "


#  3.  Because the proofs generated by these examples are very long, we
#  compress the *.proofs files right after they are successfully made, by
#  default.  To override this default, use 0 instead of 1 in the line below.
#  (Use the Unix command `uncompress' on any *.proofs.Z files that you wish to
#  examine.)

set NQCOMP = 1


#                                   CLEANING

#  If you have not previously attempted to run this set of examples on your
#  site, then you can skip the CLEANING phase, which is only concerned with
#  deleting files left by previous attempts.  Before beginning a complete round
#  of proofs, first clean house by executing: 
#
#     % make clean-giant-examples
#

#  while connected to the Pc-Nqthm-1992 directory.  This command gets rid of
#  compiled files created by a variety of Lisps during compiled make-libs.  You
#  may want to add to this list to delete files created by some other Lisp
#  compiler.  Please note that this deletes all files (in subdirectories of
#  `examples') that begin with a digit, so it is a terrible idea to have a file
#  named 20.events because it will be deleted.  Why do we act so rudely as to
#  delete all such files?  Because AKCL, when running with
#  compiler::*split-files* set, as we have it in order to do the goedel and
#  piton proofs, creates auxiliary *.o compiled files that begin with digits,
#  and such a file could possibly be confused with the compiled lib files
#  created in making a lib for an events file that began with a digit.

#  The following csh code will search for any file that is not of the form
#  *.events or README.  If any such file exists after cleaning, then perhaps a
#  new pattern should be added to the patterns above.

#  foreach v (*/*)
#    if !(${v:e} == "events" || ${v:t} == "README") then
#      echo "Warning: Suspicious file: ${v}"
#    endif
#  end


#                                    RUNNING

#  The final user step in running this set of examples is to execute the
#  following simple command while connected to the directory `examples':

#      % source driver

#  Or, as a reasonable alternative, execute this single command:

#      % nice csh < driver >& driver.log &

#  which runs the job in the background, sending a transcript to the file
#  `driver.log', while lowering the priority of the computation that takes
#  quite a while to complete.

#  Running this set of examples takes so long that completion may well fail in
#  a single run due to external causes, e.g., power failure.  If a crash or
#  other abort happens, then invoking the same command again will pick up
#  approximately where it left off, skipping those files whose proofs have been
#  done.  If and when successful completion occurs, the message ALL FILES
#  PROVED will be printed.  If a resumption is attempted, it may well be that
#  warnings will be printed about the presence of files of the form *.STARTED
#  or *.trans.  This is to be expected, since such files may have been created
#  in the processing of the *.events file where an interruption occurred.

#  Commands later in this file do several checks before printing the success
#  message.  We now describe three of those checks.  (1) To determine
#  successful completion, we check that for each event file x.events, there has
#  been created a file x.proved.  (2) We further check for the existence of the
#  file x.STARTED, the presence of which would indicate that checking x.events
#  was begun but did not finish properly.  This could be a sign of a proof
#  failure or merely of failure due an external cause, e.g., power failure or
#  user intervention.  In any case, the corresponding *.proofs file should be
#  investigated to determine the nature of the problem.  (3) We also check for
#  the existence of the file x.fail, an explicit sign of failure in the
#  checking of x.events.


#                                  THE FILES

#  An entry in the following list of files, nqfiles, must have the form
#  dir/name, where dir is a subdirectory of the directory `examples' and name
#  is the root name of a file name.events that can be found in dir.

#  Convention: when `PROVE-FILEing' one of these files, say
#  pascal/fermat.events, a new Pc-Nqthm-1992 process will be started only after
#  connecting to the directory of that file, e.g., pascal.  Thus, the form
#  (NOTE-LIB "euclid") in that file will, for the Lisps we know, refer to the
#  library named euclid on that subdirectory of events, pascal, rather than in
#  some other subdirectory.  We have ourselves avoided using any directory
#  names within the NOTE-LIBs of the event files we distribute so as not to tie
#  the events files to any operating system file syntax.  But we mention this
#  connectivity fact for the benefit of those who may wish to add to this set
#  of examples.

set nqfiles = (\
basic/subset\
basic/arith\
basic/mergesort\
basic/events1\
basic/transitive-closure\
basic/events2\
basic/pigeon-hole\
basic/hanoi\
basic/ramsey1\
basic/ramsey2\
basic/square\
basic/tsquare\
basic/symmetric-difference\
defn-sk/csb\
defn-sk/finite-state-machine-example\
defn-sk/koenig\
defn-sk/ramsey\
generalize/sets\
generalize/alists\
generalize/terms\
generalize/generalize\
mg/c1\
mg/c2\
mg/c3\
mg/c4\
mg/c5\
mg/c-signal\
mg/c-prog2\
mg/c-loop\
mg/c-if\
mg/c-begin\
mg/c-predefined1\
mg/c-predefined2\
mg/c-predefined3\
mg/c-predefined4\
mg/c-proc-call1\
mg/c-proc-call2\
mg/ca10\
middle-gypsy/r2\
middle-gypsy/gf\
middle-gypsy/gp\
wilding/ground-resolution\
dmg/bags\
dmg/naturals\
dmg/interpreter\
dmg/dining\
dmg/fifo\
dmg/me\
dmg/min\
verkest/Anrd\
cowles/bags\
cowles/naturals\
cowles/integers\
cowles/knuth-91\
cowles/knuth-91a\
)


#                         CHECK THAT THE FILES EXIST

#  This driver assumes that all event files are exactly one level deep, i.e.,
#  all event files can be listed by ls */*.events.

# for each of the above files v (head/tail)
foreach v ($nqfiles)
# if there does not exist a file named v.events
  if !(-e ${v}.events) then
# then report that fact and abort
  echo The file "${v}.events does not exist. Aborting."
  exit 0
  endif
end

# report any example event file that is not in nqfiles.
foreach v1 (*/*.events)
  set nqfound = 0
    foreach v2 ($nqfiles)
     if (${v1:r} == ${v2}) then
     set nqfound = 1
     endif
    end
    if ($nqfound == 0) then
     echo The file "${v1} is not scheduled to be checked."
    endif
end


# Flag set if any suspicious (non-event) files of the same root are
# seen before proving.
set nqoldfile = 0

#                        A LITTLE KNOWN FLAG

# Set this to 0 to cause the proofs to be skipped.  Useful, as far
# as we know, only for generating the file `driver.lisp' quickly.

set NQDOPROOFS = 1

#                          DO THE PROOFS

if ($NQDOPROOFS) then

# for each of the above files v, say, head/tail,
foreach v ($nqfiles)
# if there already exists a file named v.proved
   if (-e ${v}.proved) then
# then report that fact and go on to the next file
   echo "${v}.events already done."
  else
  echo -n $v.events "started ... "
# connect to the directory head
   cd ${v:h}
# Worry the user about the presence of extraneous files.
   foreach v2 (*${v:t}*)
    if (${v2} == ${v:t}.events) then
    else echo "\
     WARNING:  "\""${v:t}"\"" is a substring of "\""${v2}"\"", and the\
     file "\""${v2}"\"" exists in directory ${v:h}."
     set nqoldfile = 1
    endif
   end
# invoke Pc-Nqthm-1992 on (prove-file-out "tail") with output to
# the file tail.trans
  echo '(prove-file-out "'${v:t}'")'${NQQUIT} | ${NQRUN} >& ${v:t}.trans
# connect back to the superior directory
   cd ..
# check that the file head/tail.proved now exists
   if (!(-e ${v}.proved)) then
    echo $v.events failed.  Aborting.
# quit if it does not
    exit 0
# otherwise report that we are done with that file.
   else echo "done." 
# conditionally compress the proofs file.
     if (${NQCOMP}) then
       echo Compressing ${v}.proofs.
       compress ${v}.proofs
     endif
   endif
  endif
end
endif


#                               CHECK FOR SUCCESS

# Now we check that at this time, all files are proved and furthermore there
# are no .STARTED or .fail flag files left over.

if ($NQDOPROOFS) then

echo Checking that all files proved\.

if ($nqoldfile) echo "Beware of old file warnings reported above."

set nqwinning = 1
foreach v ($nqfiles)
  if (!(-e ${v}.proved)) then
  echo "ERROR:  ${v}.events was not successfully done:"
  echo "  ${v}.proved does not exist."
  set nqwinning = 0
  endif
end

foreach v ($nqfiles)
  if (-e ${v}.STARTED) then
  echo "ERROR:  ${v}.events was not successfully done:"
  echo "  ${v}.STARTED exists."
  set nqwinning = 0
  endif
end

foreach v ($nqfiles)
  if (-e ${v}.fail) then
  echo "ERROR:  ${v}.events was not successfully done:"
  echo "  ${v}.fail exists."
  set nqwinning = 0
  endif
end

if ($nqwinning) then
echo "ALL FILES PROVED"
endif

#  Below we print a cautionary note if any *.events file is `newer' than the
#  corresponding *.proved file, which probably indicates that the event file
#  was edited after the proofs were last done.  That this cautionary note is
#  not printed does not in itself provide much confidence or information.  This
#  driver file is not intended to (and does not) support `incremental' proving,
#  with correct tracking of inner dependencies, a la the Unix `make' program.
#  On the contrary, the only recommended procedure is to start with a massive
#  `clean up' as directed above, and then to run all of the files, with no
#  further editing of any of the events files, or any other user file editing,
#  creating, or deleting, once the run is started.

foreach v ($nqfiles)
  if (-e ${v}.proofs) then
    find ${v:h} -name ${v:t}.events -newer ${v}.proofs -exec \
      echo Warning\: ${v}.events has been written since proved\. \;
  endif
  if (-e ${v}.proofs.Z) then
    find ${v:h} -name ${v:t}.events -newer ${v}.proofs.Z -exec \
      echo Warning\: ${v}.events has been written since proved\. \;
  endif
end

#  Below we print a cautionary note if any *.lib file is `newer' than the
#  corresponding *.proved file, which probably indicates that the lib was made
#  after the proofs were done.  That this cautionary note is not printed does
#  not in itself provide much confidence or information.

foreach v ($nqfiles)
  if (-e ${v}.proved) then
    find ${v:h} -name ${v:t}.lib -newer ${v}.proved -exec \
      echo Warning\: ${v}.lib has been written since $v{}.events was proved\. \;
  endif
end

endif

#                        MAKE AN UP TO DATE driver.lisp

#  Although we sometimes check our examples in the fashion above, i.e., from a
#  Unix shell, it is perfectly reasonable to do it from within Lisp.  The
#  following code produces a Lisp file, driver.lisp, for checking our examples
#  from within Lisp.

cp driver-header.lisp driver.lisp

#  We package together all the commands for individual files into a PROGN so
#  that if an error arises in AKCL, there will be no more commands on the input
#  stream.

echo Creating the file driver\.lisp\.

echo '(TIME (PROGN' >> driver.lisp

foreach v ($nqfiles)
 echo '(DRIVER-PROVE-FILE-OUT "'${v:h}'" "'${v:t}'")' >> driver.lisp
end                                              

echo '(FORMAT T "~%~%All Pc-Nqthm-1992 tests completed successfully.~%~%")' >> driver.lisp

echo '))' >> driver.lisp
echo '(FORMAT *STANDARD-OUTPUT* "~%Finished loading driver.lisp.")' >> driver.lisp


#                  ADDING NEW ENTRIES TO THIS SET OF EXAMPLES

#  To add a new file, say, new.events, to this set of examples, proceed as follows.
#  1.  If appropriate, create a new subdirectory of examples, named perhaps
#      after the originator of the work.
#  2.  Put the file, named say new.events, in a subdirectory of examples, say dir.
#  3.  Add the entry dir/new to the definition of the variable `nqfiles' above.

#  A new events file must satisfy these rules:
#  1.  It must begin with a BOOT-STRAP or with a NOTE-LIB of a file given
#      explicitly by a string.
#  2.  It may contain only legal Pc-Nqthm-1992 event forms.  For example, we permit no
#      user defined macros, no setq's, no MAKE-LIBs except at the very end, no
#      boot-straps or NOTE-LIBs, except as the first form, and no uses of #, or
#      #.
#  3.  The file name may not begin with a digit or end with the three characters
#      "tmp".  Explanation:  We make the file tmp.lisp when executing
#      (COMPILE-UNCOMPILED-DEFNS "tmp"); AKCL names some *.o files with names
#      that begin with a digit when using the compiler:*split-files* feature.
#  4.  It may end with a MAKE-LIB, but the file-name argument to MAKE-LIB
#      must be the same as the root name of the events file in which it occurs.
#      That is, you may put (MAKE-LIB "euclid") at the end of euclid.events.
#  5.  The extension of the file name must be `events'.  Thus `euler.events' is
#      an ok name but `euler.ev' and `euler.lisp' are not.

#  Be sure, when adding a new event file to the list of nqfiles above, to put
#  file names in such an order that if file forms2.events does a (NOTE-LIB
#  "forms1"), then forms1 occurs before forms2 in the definition of the
#  variable `nqfiles'.  We check the files in the given order.


