# Makefile for the SVRC prover: Ergo.
# ===================================
#
# The following pathnames will need to be set up for each system.

# QC should point to the Qu-Prolog compiler.
QC = /homes/qp/qp3.2/bin/qc

# ROOT should be the absolute path to the 'ergo' directory
#   which has subdirectories: prover, bin, thy, u1, userman etc.
ROOT = /homes/itp/ver4

#============ No changes should be needed beyond here ===========
#
# This must be the absolute path of the ergo_help script.
# (You should also check the path names within the ergo_help script).
HELP_PATH  = -H $(ROOT)/bin/ergo_help

# The absolute path of the default global.erg file.
# (the definitions below set up Ergo to use this path whenever there 
#  is no global.erg file in the current directory, so the prover will 
#  still be useable even if this path is not set correctly).
GLOBAL_FILE= $(ROOT)/thy/global.erg


# Warning: the only tabs in this file should be the ones before a
#          command to be executed, otherwise GNU make will complain.

# The development version.
# ------------------------
# This prover has no preloaded tactics and only looks for the 
# global.erg file in the current directory (though explicit -G arguments
# can be used to override this).

# Call it 'er', because it is a version of Ergo that may not 'go'  :-)
DEV_NAME   = er
DEV_GPATH  = -G global.erg

# Relative location of the development version of the tactics.
DEV_TACTICS = ../u1


# The release version.
# --------------------
REL_NAME   = ergo

# This specifies where to search for the global.erg file.
REL_GPATH  = -G global.erg -G $(GLOBAL_FILE)

# The relative (or absolute) location of the preloaded tactic files.
REL_TACTICS=../u1

# PRELOAD specifies which tactic files should be preloaded.
PRELOAD =  $(REL_TACTICS)/abbv.qo \
           $(REL_TACTICS)/commands1.qo \
           $(REL_TACTICS)/demo3.qo \
           $(REL_TACTICS)/it.qo \
           $(REL_TACTICS)/quick.qo \
           $(REL_TACTICS)/rerun.qo \
           $(REL_TACTICS)/show.qo \
           $(REL_TACTICS)/startup.qo \
           $(REL_TACTICS)/heur.qo \
           $(REL_TACTICS)/browse.qo \
           $(REL_TACTICS)/search.qo \
           $(REL_TACTICS)/rt.qo \
           $(REL_TACTICS)/exprabbr.qo \
           $(REL_TACTICS)/tools.qo

# This must be the same as PRELOAD, but without directories or extensions.
PRELOAD2 = abbv commands1 demo3 it quick rerun show startup tools \
           heur browse search rt exprabbr


# General Definitions
# ===================
.SUFFIXES: .ql .qo ,v

PR=prover
DB=dbms
LIB=lib

# A rule for extracting RCS files.
% :: %,v
	co $< $@

# A rule for compiling Qu-Prolog files.
.ql.qo: $(QC)
	$(QC) -c $*.ql


B1 =       $(LIB)/development.qo
B2 =       $(LIB)/release.qo

DBMS =     $(DB)/assert.qo \
           $(DB)/comprule.qo \
           $(DB)/fact_types.qo \
           $(DB)/main.qo \
           $(DB)/query.qo \
           $(DB)/save.qo \
           $(DB)/syntax1.qo \
           $(DB)/syntax2.qo \
           $(DB)/theory_dag.qo \
           $(DB)/theory_data.qo \
           $(DB)/unix.qo \
           $(DB)/win_rule.qo
         
         
PROVER =   $(PR)/hyps.qo \
           $(PR)/newvars.qo \
           $(PR)/prove.qo \
           $(PR)/trans.qo \
           $(PR)/window.qo	
         
TOOLS =    $(LIB)/arith.qo \
           $(LIB)/io.qo \
           $(LIB)/macros.qo \
           $(LIB)/tools.qo \
           $(LIB)/iu.qo

OBJ = $(DBMS) $(PROVER) $(TOOLS)
SRC = $(DB)/*.ql $(PR)/*.ql $(LIB)/*.ql $(DEV_TACTICS)/*.ql

# Targets
# -------

help:
	@echo "The possible make targets include:"
	@echo "  'development' makes " $(DEV_NAME)
	@echo "  'release' makes " $(REL_NAME)
	@echo "  'tags' makes vi and emacs tags files in this directory."

development: $(DEV_NAME)
release:     $(REL_NAME)

tags:   $(SRC)
	/homes/marku/bin/petags -e '^[$$a-z][$$a-zA-z0-9_]*' $(SRC)
	/homes/marku/bin/prologtags $(SRC)

$(DEV_NAME): $(OBJ) $(B1)
	-rm -f $(DEV_NAME)
	@echo "Shell PWD = $$PWD,  pwd gives:"
	@pwd
	$(QC) -o $(DEV_NAME) -h2800  -l128 -s96 $(OBJ) $(B1)
	read C <$(DEV_NAME); \
	    echo "$$C $(DEV_GPATH) $(HELP_PATH)" > $(DEV_NAME)
	chmod 775 $(DEV_NAME)

$(REL_NAME): $(OBJ) $(PRELOAD) $(B2)
	-rm -f $(REL_NAME)
	@echo "Shell PWD = $$PWD,  pwd gives:"
	@pwd
	$(QC) -o $(REL_NAME) -h2800  -l128 -s96 $(OBJ) $(PRELOAD) $(B2)
	read C <$(REL_NAME); \
	  echo "$$C -lib $(ROOT) -L $(PRELOAD2) $(REL_GPATH) $(HELP_PATH)" >$(REL_NAME)
	chmod 775 $(REL_NAME)


