[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