;; Adapted from the Nqthm-1992 file driver-header.lisp. #| This file `driver.lisp' is for running the standard Pc-Nqthm-1992 examples. See the warning near the top of the Nqthm-1992 file driver.lisp (which simply says, essentially, that you may need a lot of time and space -- that is somewhat true for the Pc-Nqthm-1992 examples, too). The various example files provided with Pc-Nqthm-1992 can each be run one at a time by invoking, say, (PROVE-FILE-OUT "ex") for each of the example files, say, `ex.events', in the order suggested below. But there are so many of these example files that we have organized them into subdirectories and coded this driver file to automate the process. The code in this file, `driver.lisp', does little more than support the necessary switching between subdirectories, before invoking PROVE-FILE-OUT. As indicated below, this switching is slightly operating system sensitive, unlike the rest of Pc-Nqthm-1992, which is one reason that we have separated the code for this driver from the code for Pc-Nqthm-1992 itself. Here are the instructions for running the Pc-Nqthm-1992 examples. 0. Cleanup. If any previous attempts have been made to run these examples at your site, consider deleting all files of the form *.proved in all the subdirectories of the Pc-Nqthm-1992 `examples' directory. If a file `ex.proved' exists on a subdirectory of the `examples' directory, that is taken as a sign, by this driver, that a file `ex.events' on the same subdirectory has been successfully checked, and so running `ex.events' will be skipped. For example, if you are running on a Unix, and if the `examples' subdirectory of Pc-Nqthm-1992 at your site happens to be named "/usr/smith/Pc-Nqthm-1992/examples/", then consider doing something like: cd /usr/smith/Pc-Nqthm-1992/examples/ rm examples/*/*.proved 1. Compile and load Pc-Nqthm-1992. To briefly review this matter, which is covered in further detail in the installation guide, we recall that the instructions are, when `connected' to the directory of the Pc-Nqthm sources, and after starting up Nqthm-1992 (which hence should already have been built): a. (LOAD "pc-nqthm.lisp") b. (IN-PACKAGE "USER") c. (COMPILE-PC-NQTHM) ; unnecessary if already compiled, of course. d. (LOAD-PC-NQTHM) 2. Directory identification. Set the variable *PC-NQTHM-EXAMPLES-DIR* to a string (not a pathname) that names the `examples' directory for Pc-Nqthm-1992 at your site. For example, on a Unix system, you might execute something like: (DEFPARAMETER *PC-NQTHM-EXAMPLES-DIR* "/home/smith/Pc-Nqthm-1992/examples/") It is important that the last character of the value of *PC-NQTHM-EXAMPLES-DIR* be the character that separates components of a pathname under your operating system. This file `driver.lisp' depends on it. On a Unix, for example, the character will be "/". On a Macintosh it will be ":". On a Symbolics it will be ">". If your operating system does not have such a simple, single-character convention for separating pathname components, this driver will not work for you. In that case, invent some other mechanism to invoke PROVE-FILE-OUT on each of the example files, in the order suggested below. 3. Running. LOAD this file. For example, evaluate something like: (LOAD "/home/smith/Pc-Nqthm-1992/examples/driver.lisp") This will result in the evaluation of all of the examples distributed with Pc-Nqthm-1992. That's all there is to do. But the computation takes quite a while! Hint. Because running this file may take such a long time, it may be a good idea to run it in the background, and `nicely'. Assume, for the moment, that we are running on a Unix, that the Unix command `Pc-Nqthm-1992' starts up a process containing a loaded Pc-Nqthm-1992, and that we are connected to the `examples' directory. Then one way to run this driver would be to put a command, such as the DEFPARAMETER above, for setting the directory variable, in a file, say `dir.lisp', and then to invoke, at the Unix shell level, the command: cat dir.lisp driver.lisp | nice Pc-Nqthm-1992 >& driver.log & For further information on resource problems and other issues, see the comments in the Nqthm-1992 file driver-header.lisp. |# (IN-PACKAGE "USER") (FORMAT *STANDARD-OUTPUT* "~%Loading driver.lisp.") (OR (AND (BOUNDP '*PC-NQTHM-EXAMPLES-DIR*) (STRINGP *PC-NQTHM-EXAMPLES-DIR*)) (ERROR "~% Before running this file, please set *PC-NQTHM-EXAMPLES-DIR* to a ~ string ~% that names the path to the Pc-Nqthm-1992 examples ~ directory at your~% site. For example, on a Unix, one might ~ execute something like~%~% (DEFPARAMETER *PC-NQTHM-EXAMPLES-DIR* ~ \"/usr/smith/Pc-Nqthm-1992/examples/\")~%~% It is important that the ~ string end in the character that separates ~% subdirectory ~ components, e.g., / on Unix, > on Symbolics, and : on Macintosh.~%" )) (FORMAT *STANDARD-OUTPUT* "~%We will assume that the Pc-Nqthm-1992 examples directory at this site ~ is: ~%~% ~a~%~%We will also assume that the single character ~a is ~ used to separate~%subdirectory components under this operating ~ system.~%~%Starting the Pc-Nqthm-1992 examples " *PC-NQTHM-EXAMPLES-DIR* (CHAR *PC-NQTHM-EXAMPLES-DIR* (1- (LENGTH *PC-NQTHM-EXAMPLES-DIR*)))) (PRINT-IDATE (IDATE) *STANDARD-OUTPUT*) (FORMAT *STANDARD-OUTPUT* ".") (DEFUN DRIVER-PROVE-FILE-OUT (DIR ROOT) ; DRIVER-PROVE-FILE-OUT runs PROVE-FILE-OUT on ROOT.events after `connecting' ; to subdirectory DIR, by rebinding *DEFAULT-NQTHM-PATH*. This `connecting' ; process involves operating system dependent code for dealing with the notion ; of subdirectory. The dependence is that we assume that that a single ; character is used, in a string for a pathname, to separate subdirectory ; components. e.g., / on Unix, > on Symbolics, and : on Macintosh. We rely ; upon the user to inform us, implicitly, what that character is by putting it ; at the end of the value of *PC-NQTHM-EXAMPLES-DIR*. (LET ((*DEFAULT-NQTHM-PATH* (FORMAT NIL "~A~A~A" *PC-NQTHM-EXAMPLES-DIR* DIR ; Yuk. Here we strip off the last character to use again: (CHAR *PC-NQTHM-EXAMPLES-DIR* (1- (LENGTH *PC-NQTHM-EXAMPLES-DIR*))))) VALUE) (COND ((PROBE-FILE (EXTEND-FILE-NAME ROOT FILE-EXTENSION-PROVED)) (FORMAT *STANDARD-OUTPUT* "~%Skipping ~a.~a because the file ~a.~a exists." ROOT FILE-EXTENSION-EVENTS ROOT FILE-EXTENSION-PROVED) "Skipped") (T (FORMAT *STANDARD-OUTPUT* "~%Trying ~a.~a." ROOT FILE-EXTENSION-EVENTS) (FORCE-OUTPUT *STANDARD-OUTPUT*) (COND ((SETQ VALUE (PROVE-FILE-OUT ROOT)) (FORMAT *STANDARD-OUTPUT* "~%Successfully finished ~a.~a." ROOT FILE-EXTENSION-EVENTS)) (T (ERROR "~%Failed on ~a.~a." ROOT FILE-EXTENSION-EVENTS))) (FORCE-OUTPUT *STANDARD-OUTPUT*) VALUE))))