# Copyright (C) 1994 by Computational Logic, Inc.  All Rights Reserved.

# Copying of this file is authorized to those who have read and agreed with the
# terms in the "Pc-Nqthm-1992 GENERAL PUBLIC SOFTWARE LICENSE" at the beginning
# of the Pc-Nqthm file "basis-pc.lisp".

# Adapted from makefile for Nqthm-1992.

# This file is a Unix makefile for compiling Pc-Nqthm-1992, building a save
# image, and running some examples.  If this makefile does not work for you,
# you are advised not to use the `make' command to build Pc-Nqthm-1992, but
# instead to use the simple, manual instructions for Pc-Nqthm-1992 installation
# found in the `README-pc' file.  This file is not necessary for building
# Pc-Nqthm-1992, but is provided as a convenience to users who wish to build
# Pc-Nqthm-1992 under Unix.  NOTE:  If you have not already built a save image
# for Nqthm-1992, then there is no point in reading further in this file:  we
# assume henceforth that there is an Nqthm-1992 image available.

# To build an executable Pc-Nqthm-1992 image, invoke

#    % make NQTHM=xxx

# where xxx is the command for running your Nqthm-1992 image.  xxx
# defaults to `nqthm-1992'.  It is expected that this save-image-build
# process works for Nqthm-1992 images built using the Nqthm-1992
# makefile.  At the time of this writing, this includes Nqthm images
# built using the following Lisps:  AKCL, Lucid, Allegro, and CMU
# Lisp.  (For CMU Lisp, you should also provide your site's name for
# CMU Lisp, make NQTHM=nqthm-1992 CMULISP=cmulisp for example.)  For
# Lisps other than these four, it will be necessary to edit files in
# the ./make/ subdirectory, in particular to add the appropriate
# command to save an image, in the file ./make/save.lisp.

# As a result of this make, a very small, executable file named
# `pc-nqthm-1992' will be created on this directory.  This small file
# `points' to a large save file, which is also created by the make.
# After the make has completed, the file `pc-nqthm-1992' may
# optionally be copied with `cp' (not moved, with `mv') to a bin
# directory, e.g., with the command

#    % cp pc-nqthm-1992 /usr/local/bin

# The choice of bin directory varies a lot from site to site, and the
# copying may even require special privileges, so we do not try to
# automate it.  There is absolutely no necessity of copying the above file
# anywhere -- putting it on a bin path does nothing besides give users
# the convenience of not having to precede `pc-nqthm-1992' with some
# directory pathname to start it up.

# As a secondary result of the make command above, a very short little
# test will be run.  If a `looks ok' message gets printed at the end
# of the make, then the compilation and saving probably went ok.

# Once the first make has succeeded, a somewhat longer test can be invoked via

#    % make small-test

# which will run the file ./examples/defn-sk/csb.events, and if
# successful, create the files ./examples/defn-sk/csb.proofs and
# ./examples/defn-sk/csb.proved, and print out a message indicating
# that this small test worked.  You can monitor progress with `ls -lt
# examples/defn-sk/csb.proofs'.

# A large set of tests, generating megabytes of files, and probably requiring a
# substantial number of cpu hours to complete, can be invoked via

#    % make giant-test

# Before running this form, read the file `examples/README'.  You can
# monitor progress with the command `ls -lt examples/*/* | head'.

# The same set of tests can also be invoked via

#    % make giant-test-alt

# which differs from giant-test mainly in that each test is performed
# in a separate process.

# To build a TAGS file for use with Gnu Emacs, invoke

#   % make TAGS

# To remove files created by building under AKCL, Lucid, Allegro, and
# CMU Common Lisps, invoke

#    % make clean

# To remove files created by running the giant test, invoke

#    % make clean-giant-examples

# `make clean-giant-examples' should be executed before trying the
# giant examples afresh, if they have ever been tried before at your
# site; otherwise the make will resume where it was last aborted or
# failed.  This resumption feature is a real feature, not a bug:
# running the giant tests takes so long that there is a palpable
# chance that something external like a power failure or a network
# crash will occur during execution, so resumption is a common
# necessity.

NQTHM=nqthm-1992

CMULISP=cmulisp

SOURCES=defn-sk.lisp pc-nqthm.lisp nqthm-patches.lisp basis-pc.lisp\
  help.lisp utilities.lisp top.lisp top-nqthm.lisp macro-commands-aux.lisp\
  macro-commands.lisp

all: pc-nqthm-1992 make/tiny-test.lisp


make/compile-success: ${SOURCES}
	${NQTHM} < make/compile.lisp


pc-nqthm-1992 saved_pc-nqthm-1992: make/compile-success
# Here is a reasonable modification of what is in the nqthm-1992 makefile.
	echo '"'${CMULISP}'" "'`pwd`'"' > pc-nqthm-1992-tmp
	${NQTHM} < make/save.lisp
	mv pc-nqthm-1992-tmp pc-nqthm-1992
	chmod a+x pc-nqthm-1992


make/tiny-test.lisp: pc-nqthm-1992
	cd make; ../pc-nqthm-1992 < tiny-tester.lisp


small-test: pc-nqthm-1992
	cd examples/defn-sk; ../../pc-nqthm-1992 < ../../make/small-tester.lisp


giant-test: pc-nqthm-1992
	cd examples; cat dir.lisp driver.lisp | ../pc-nqthm-1992


giant-test-alt: pc-nqthm-1992
	cd examples; csh driver


TAGS: ${SOURCES}
	etags ${SOURCES}


clean:
	rm -f make/compile-success pc-nqthm-1992 TAGS
	rm -f *.o *.c *.h *.data *.sbin *.lbin *.fasl *.sparcf \
	 make/tiny-test.* *saved_pc-nqthm-1992 make/tmp.* *.log


clean-giant-examples:
	cd ./examples ; rm -f */*.lisp */*.lib */*.trans */*.err */*.log \
	  */*.proofs* */*.proved */*.STARTED */tmp.* */*.fail \
	  */*.o */*.fasl */*.lbin */*.sbin */*.sparcf \
	  */*.data */*.c */*.h */[0123456789]*