November, 2003

To run Nqthm-1992 under Clisp, one may proceed as follows.

Connect, e.g., with "cd", to where the nqthm-1992 sources have been copied,
i.e., a directory containing the unzipped and untarred contents of
ftp://ftp.cs.utexas.edu/pub/boyer/nqthm/nqthm-2nd-edition.tar.gz.  Below we
assume the directory is /u/boyer/nqthm-2nd/nqthm-1992-test/, but any empty
directory to which reading and writing are permitted will do.  Then execute
the following commands.

clisp
(load "nqthm.lisp")
(in-package "USER")

; minor work-around number one: clisp defines a function named execute (in
; package LISP) and nqthm-1992 defines it in package USER.  clisp imports
; that definition into package USER.  We undo, roughly speaking, that
; importation with the following shadow command.  One can still execute the
; clisp execute function by calling lisp::execute.

(shadow 'execute)

; minor work-around number two: clisp uses the file extension "lib" for
; compilation.  We here tell nqthm-1992 to use another extension for its own
; compilations.

(setq FILE-EXTENSION-LIB "nlib")

(compile-nqthm)
(load-nqthm)

; at this point, the current clisp image contains a full nqthm. We save it
; for future use.

(saveinitmem "nqthm" :quiet t) 
(exit)

; and restart it.

clisp -M nqthm.mem
(in-package "USER")

; We now proceed to do the standard nqthm tests.

(setq *SUPPRESS-CHECK-REDEFINITION* t) ; just to avoid some warnings from Clisp
(proclaim '(optimize (speed 3) (safety 0) (space 0)))
(setq *thm-suppress-disclaimer-flg* t) ; for less noise from nqthm
(defparameter *nqthm-examples-dir* "/u/boyer/nqthm-2nd/nqthm-1992-test/examples/")
(defparameter *nqthm-source-dir* "/u/boyer/nqthm-2nd/nqthm-1992-test/")
(defparameter *nqthm-young-dir* "/u/boyer/nqthm-2nd/nqthm-1992-test/examples/young/")
(defparameter *nqthm-yu-dir*  "/u/boyer/nqthm-2nd/nqthm-1992-test/examples/yu/")
(load "/u/boyer/nqthm-2nd/nqthm-1992-test/examples/driver.lisp")
(load "/u/boyer/nqthm-2nd/nqthm-1992-test/examples/driver-sk.lisp")