[Adapted from the `README' file for the `examples' subdirectory of Nqthm-1992.]

This is the `README' file for the `examples' subdirectory of Pc-Nqthm-1992, a
collection of subdirectories of over one hundred event files, which together
contain thousands of theorems.

No file on this directory `examples', nor on any of its subdirectories, is
necessary for the compilation, installation, or execution of Pc-Nqthm-1992.

In the subdirectories such as basic, cowles, defn-sk, dmg, generalize,
mg, middle-gypsy, verkest, and wilding are the *.events files, the
actual example files.

There are a variety of ways to replay these examples.  Please note that to
replay all these examples is a data processing activity requiring SUBSTANTIAL
TIME AND SPACE RESOURCES -- well over 100 megabytes of disk space space,
substantial virtual memory, and possibly more cpu time than one would like to
apply to this activity.  See further warnings about resources in the Nqthm-1992
file driver-header.lisp.

Alternative 1.  From within a Common Lisp into which the compiled files for
Pc-Nqthm-1992 have been loaded, simply invoke, say, (prove-file-out "ex"), to
check an example file named, say, `ex.events'.  Before invoking prove-file-out,
one must indicate the directory of the file `ex.events', either (1) by using
some operating-system-specific or Common-Lisp-implementation-specific command
such as `cd' or (2) by setting *DEFAULT-NQTHM-PATH* to some suitable pathname
string, e.g. "/local/src/pc-nqthm-1992/examples/basic/".  Obviously, the choice of
the directory name depends upon where the Pc-Nqthm-1992 examples are located at
your site.  If the checking is successful, a file `ex.proved' will be created.
If unsuccessful, `ex.proved' will not be created, but a file `ex.proofs' may
contain an error message and, in all likelihood, files named `ex.STARTED' or
`ex.fail' will be created.  Because some example files start with instructions
to call `note-lib' to load information dumped after checking other example
files, the order in which examples are done is important.  An example file that
starts with a `boot-strap' does not depend on another file.  The drawback to
running the examples in this way, via explicit calls to prove-file-out, is that
it is tedious to do each by hand.  The remaining alternatives listed below
automate the invocation of prove-file on each of the examples.  However, these
other alternatives necessarily involve operating-system-specific and
Common-Lisp-implementation-specific code that will not work for some systems.

Alternative 2.  Load the file `driver.lisp' into a Common Lisp containing a
compiled Pc-Nqthm-1992.  See that file for further directions; in particular it is
necessary to set up certain directory variables; the file `dir.lisp' contains
typical example settings of variables that point to directories for use when
running `driver.lisp'.  There are two drawbacks to this `driver.lisp'
alternative.  First, because `driver.lisp' contains instructions for switching
between the various example directories, and because we know of no method to do
this in general in all Common Lisps, this method will fail for any operating
system in which subdirectory components of file names are not separated by a
single character, e.g., the character "/" in Unix.  If a single character is
not so used in your operating system, you will find it necessary to edit
suitably the definition of DRIVER-PROVE-FILE-OUT in the file `driver.lisp'.
Second, some of the examples are so large that they will not execute for want
of sufficient heap in the default configurations of some Common Lisps.

Alternative 3. Invoke either the command `make giant-test' or else the command
`make giant-test-alt' at the Unix csh level while connected to the directory
above this, i.e., pc-nqthm-1992.  Do this after successfully running the
command `make NQTHM=xxx', where xxx is the the command to run your Nqthm-1992.
This works for Nqthm-1992 built on top of AKCL, Allegro, CMU, and Lucid Common
Lisps.  The difference between giant-test and giant-test-alt is that the former
does all of the tests in a single Lisp process whereas the latter does each
test in a different process.


                   List of Files on this Directory

README                   Introduction
basic                    A Miscellany of Examples
cowles                   Solutions by John Cowles to a challenge of Knuth
defn-sk                  Some proofs involving quantification
dir.lisp                 Definition of some directory variables
dmg                      Proofs by David Goldschlag involving Mechanized UNITY
driver                   A Unix csh driver for running the examples
driver-header.lisp       A file used to help make the file driver.lisp
driver.lisp              For running the examples under any CL 
generalize               A proof by Matt Kaufmann of correctness of a
                         generalization algorithm
mg                       Bill Young's mechanically-verified code-generator for
                         micro-Gypsy
middle-gypsy             A mathematical definition (Siebert et al) of a subset
                         of Gypsy
verkest                  Diederik Verkest's events for ANRD division algorithm,
                         down to hardware
wilding                  Matt Wilding's proof of completeness of ground
                         resolution
