####################################################################
#
#	$Id: rbj.mkf,v 1.107 2015/04/23 09:58:07 rbj Exp $
#
#	makefile for Roger's things
#
# This is an adaptation of Rob Arthan's maths_egs.mkf to work in my
# setup for those things I am now trying to do with ProofPower in
# his manner (rather than, say, in XML).
######################################################################

# suffixes known
.SUFFIXES: .db .doc .pdf .ldd .log .lot .sh .pp .tex .tch

# default make target.  displays a list of more useful targets

default:
	@echo "This is the make file for an assortment of experiments"
	@echo "with ProofPower, mostly philosophically motivated."
	@echo " "
	@echo "ProofPower version 2.7.3 or later is required."
	@echo "In addition we assume the existence of the database"
	@echo "maths_egs built from Rob Arthan's mathematics examples."
	@echo "in the RobArthan/pp-contrib github repo."
	@echo " "
	@echo "The following are useful for developers:"
	@echo " "
	@echo "make -f rbj.mkf doc      - makes a .pdf tar file (rbj.doc.tgz)"
	@echo "make -f rbj.mkf dist     - makes a source tar file (rbj.src.tgz)"
	@echo " "
	@echo "The following are the two most useful make commands for users:"
	@echo " "
	@echo "make -f rbj.mkf pdf      - build database; typeset documents as PDF files"
	@echo "make -f rbj.mkf bld      - just build database"
	@echo " "
	@echo "The make commands that build the database create a new ProofPower database"
	@echo "called rbjhol and load the documents into it, thus typechecking the"
	@echo "specifications and replaying the proofs."
#	@echo "You will need "." in your path to make pdf or doc."

vars:
	@echo HOLTEXS1: $(HOLTEXS1)
	@echo HOLMTEXS: $(HOLMTEXS)
	@echo HOLDBNAME: $(HOLDBNAME)
	@echo SPCDIR: $(SPCDIR)

######################################################################
#
#	Makefile Definitions
#
######################################################################

PPHOME=$(shell echo $${PPHOME:-/usr/local/pp})
SPCDIR=$(PPHOME)/src/hol
PPCHARSET=utf8
PPSVF=utf8svf
PRODNAME=rbj
SHORTNAME=rbj
PRODUCT=$(PRODNAME)
CWD=$(shell pwd)
HAVERCS=$(shell (test -d RCS && echo y ) || echo n)

USERDB=$(shell echo $$PPDB)
DBNAME=$(shell echo $${PPDB:-$(SHORTNAME)})

USERDB=$(shell echo $$PPDB)
DEFAULTHOLDBNAME=rbjhol
HOLDBNAME=$(shell echo $${PPDB:-$(DEFAULTHOLDBNAME)})

ZEDDBNAME=rbjzed
STARTHOLDBNAME=maths_egs
STARTZEDDBNAME=zed

RELDIR=release

# The documents

# Single file ppsvf cases

HOLPPS1= t000.pp \
	t002.pp t003.pp t004.pp t005.pp t006.pp t007.pp \
	t008.pp t009.pp t010.pp t011.pp t012.pp t013.pp t014.pp \
	t015.pp t016.pp t017.pp t018.pp t019.pp t020.pp t021.pp \
	t022.pp t023.pp t024.pp t025.pp t026.pp t027.pp t031.pp \
	t033.pp t034.pp t042.pp t043.pp t051.pp t052.pp t053.pp \
	t054.pp t056.pp t057.pp t058.pp \
	nt001.pp nt002.pp \
# nt004.pp \
	spc001.pp spc003.pp

# Three file ppsvf cases 

HOLPPS2= t001.pp t028.pp t029.pp t030.pp t032.pp t035.pp t037.pp t038.pp \
	  t039.pp t040.pp t041.pp t044.pp t045.pp t047.pp \
	  t048.pp t049.pp

# Three file min keyword ppsvf cases 

HOLPPS3= t046.pp t050.pp

# Single file min keyword no svf cases

HOLPPS4= t055.pp

HOLPPS=$(HOLPPS1) $(HOLPPS2) $(HOLPPS3) $(HOLPPS4)

HOLTEXS1=$(HOLPPS1:.pp=.tex)
HOLTEXS2=$(HOLPPS2:.pp=.tex)
HOLTEXS3=$(HOLPPS3:.pp=.tex)
HOLTEXS4=$(HOLPPS4:.pp=.tex)
HOLTEXS= $(HOLTEXS1) $(HOLTEXS2) $(HOLTEXS3) $(HOLTEXS4)
HOLMTEXS=$(HOLPPS2:.pp=m.tex) $(HOLPPS3:.pp=m.tex)

TTEX= \
        t001a.tex t002.tex t003.tex t004.tex t005.tex \
	t006.tex t007.tex t008.tex t009.tex t010.tex \
	t011.tex t012.tex t013.tex t014.tex t015.tex \
	t016.tex t017.tex t018.tex t019.tex t020.tex \
	t021.tex t022.tex t023.tex t024.tex t025.tex \
	t026.tex t027.tex t028a.tex t029a.tex t030a.tex \
	t031.tex t032a.tex t033.tex t034.tex \
	t037a.tex t038a.tex t039a.tex t040a.tex \
	t041a.tex t042.tex t043.tex t044a.tex t045a.tex \
	t046a.tex t047a.tex t048a.tex t049a.tex t050a.tex \
	t051.tex t052.tex t053.tex t054.tex t055.tex \
	t057.tex
# t056.tex t058.tex
	
NTEX= \
      nt001.tex nt002.tex \
# nt004.tex

ATEXS=$(HOLPPS2:.pp=a.tex) $(HOLPPS3:.pp=a.tex)
ZTEXS=$(HOLPPS2:.pp=z.tex) $(HOLPPS3:.pp=z.tex)
IPDFS=t028.pdf t040.pdf t041.pdf t045.pdf t046.pdf t047.pdf t048.pdf t049.pdf \
	       t050.pdf t055.pdf t057.pdf
ITEXS=$(IPDFS:.pdf=i.tex)

ZEDPPS=

SMLPPS=$(HOLPPS) $(ZEDPPS)

OTHERPPS=

HOLLDD=$(HOLPPS:.pp=.ldd)
ZEDLDD=$(ZEDPPS:.pp=.ldd)

# Variations on the documents
SMLFILES= $(SMLPPS:.pp=.sml)
LDDFILES= $(SMLPPS:.pp=.ldd) $(HOLDBNAME).ldd
PDFFILES1= $(HOLPPS1:.pp=.pdf) $(OTHERPPS:.pp=.pdf)
PDFFILES2= $(HOLPPS2:.pp=.pdf)
PDFFILES3= $(HOLPPS3:.pp=.pdf)
PDFFILES4= $(HOLPPS4:.pp=.pdf)
PDFFILES=$(PDFFILES1) $(PDFFILES2) $(PDFFILES3) $(PDFFILES4)

# The following sml files are included without the .sml since the top level .gitignore ignores .sml
SMLINCFILES=list_na.sml list_wa.sml
SMLINCBARE=$(SMLINCFILES:.sml=.bsml)

# packing list for a source release (target src)
PACKINGLIST= $(SMLPPS) $(ATEXS) $(ZTEXS) $(OTHERPPS) rbj.bib rbj2.bib rbj.mkf rbj.sty keywords \
	     rbjfmu.bst rbjpp.ist pppdf texpdf texindex2tex LICENSE $(SMLINCBARE)
# t000abs

$(SMLINCFILES): %.sml: %.bsml
	cp $*.bsml $*.sml

HOLSPCCPY=spc001.pp spc003.pp

$(HOLSPCCPY): %.pp : $(SPCDIR)/%.pp
	      cp $(SPCDIR)/$*.pp .

DISTPACKINGLIST=$(PACKINGLIST) README.txt

# Theories and Documents ##############################################
#
# This set of dependencies tells which theories are created by (and
# listed in) which documents, nd conversely, which tex files depend on
# module builds.
#
######################################################################

t000.pdf: t000abs.tex doc_theories.tex

t001.pdf: t001a.th.tex t001b.th.tex
t001a.th.pp t001b.th.pp: t001.ldd

t002.pdf: t002a.th.tex
t002a.th.pp: t002.ldd

t003.pdf: diffgeom.th.tex
diffgeom.th.pp: t003.ldd

t004.pdf: membership.th.tex fba.th.tex ba.th.tex bvi.th.tex memfunct.th.tex
membership.th.pp fba.th.pp ba.th.pp bvi.th.pp memfunct.th.pp: t004.ldd

t005.pdf: tc.th.tex memfunct.th.tex wfrel.th.tex wf_relp.th.tex wf_recp.th.tex
tc.th.pp memfunct.th.pp wfrel.th.pp wf_relp.th.pp wf_recp.th.pp: t005.ldd

t006.pdf: rbjmisc.th.tex
rbjmisc.th.pp: t006.ldd

t007.pdf: fixp.th.tex
fixp.th.pp: t007.ldd

t008.pdf: fixp-egs.th.tex
fixp-egs.th.pp: t008.ldd

t009.pdf: ordered_sets.th.tex U_orders.th.tex ordered_sets_i.th.tex
ordered_sets.th.pp U_orders.th.pp ordered_sets_i.th.pp: t009.ldd

t016.pdf: X-Logic-Auth.th.tex X-Logic-1.th.tex X-Logic-2.th.tex
X-Logic-Auth.th.pp X-Logic-1.th.pp X-Logic-2.th.pp: t016.ldd 

t017.pdf: cat.th.tex fcat.th.tex uacat.th.tex
cat.th.pp fcat.th.pp uacat.th.pp: t017.ldd

t018.pdf: pre_func.th.tex catfun.th.tex metapi.th.tex cfpi.th.tex metaci.th.tex
pre_func.th.pp catfun.th.pp metapi.th.pp cfpi.th.pp metaci.th.pp: t018.ldd 

t019.pdf: nf_h.th.tex nfu_s.th.tex nf_s.th.tex nfu_f.th.tex nff.th.tex 
nf_h.th.pp nfu_s.th.pp nf_s.th.pp nfu_f.th.pp nff.th.pp: t019.ldd

t020.pdf: poly-sets.th.tex
poly-sets.th.pp: t020.ldd

t021.pdf: ICsyn.th.tex ICsem.th.tex
ICsyn.th.pp ICsem.th.pp: t021.ldd

t022.pdf: GST.th.tex sra.th.tex src.th.tex sr.th.tex 
GST.th.pp sra.th.pp src.th.pp sr.th.pp: t022.ldd

t023.pdf: gst-ax.th.tex gst-fun.th.tex gst-ord.th.tex gst-nat.th.tex GS.th.tex 
gst-ax.th.pp gst-fun.th.pp gst-ord.th.pp gst-nat.th.pp GS.th.pp: t023.ldd

t024.pdf: ifol.th.tex misc1.th.tex
ifol.th.pp misc1.th.pp: t024.ldd

t025.pdf: misc1.th.tex misc2.th.tex
misc1.th.pp misc2.th.pp: t025.ldd

t026.pdf: ifos.th.tex sfp.th.tex 
ifos.th.pp sfp.th.pp: t026.ldd 

t027.pdf: infos.th.tex 
infos.th.pp: t027.ldd 

t028.pdf: aristotle.th.tex ariscat.th.tex syllog1.th.tex syllog2.th.tex syllog3.th.tex syllog4.th.tex syllog5.th.tex syllog6.th.tex  modsyllog.th.tex syllmetap.th.tex  gccon.th.tex 
aristotle.th.pp ariscat.th.pp syllog1.th.pp syllog2.th.pp syllog3.th.pp syllog4.th.pp syllog5.th.pp syllog6.th.pp modsyllog.th.pp syllmetap.th.pp gccon.th.pp: t028.ldd

t029.pdf: fmphil.th.tex
fmphil.th.pp: t029.ldd

t030.pdf: PM01.th.tex tract01.th.tex
PM01.th.pp tract01.th.pp: t030.ldd

t031.pdf: holw.th.tex
holw.th.pp: t031.ldd

t032.pdf: leibniz01.th.tex leibniz02.th.tex leibniz03.th.tex
leibniz01.th.pp leibniz02.th.pp leibniz03.th.pp: t032.ldd

t033.pdf: BRT.th.tex CC.th.tex 
BRT.th.pp CC.th.pp: t033.ldd

t034.pdf:

t037.pdf: grice.th.tex griceC.th.tex griceS.th.tex
grice.th.pp griceC.th.pp griceS.th.pp: t037.ldd

t039.pdf: equiv.th.tex unalg.th.tex lattice.th.tex latt2.th.tex 
equiv.th.pp unalg.th.pp lattice.th.pp latt2.th.pp: t039.ldd

t040.pdf: circuit.th.tex  alloy.th.tex 
circuit.th.pp alloy.th.pp: t040.ldd

t041.pdf: icomb.th.tex ilamb.th.tex
icomb.th.pp ilamb.th.pp: t041.ldd

t042.pdf: gsu-ax.th.tex gsu-fun.th.tex gsu-ord.th.tex gsu-nat.th.tex gsu-seq.th.tex GSU.th.tex 
gsu-ax.th.pp gsu-fun.th.pp gsu-ord.th.pp gsu-nat.th.pp gsu-seq.th.pp GSU.th.pp: t042.ldd

t043.pdf: misc3.th.tex
misc3.th.pp: t043.ldd

t044.pdf: unalgII.th.tex
unalgII.th.pp: t044.ldd

t045.pdf: t045.th.tex t045q.th.tex t045k.th.tex t045w.th.tex t045.thna.tex t045q.thna.tex t045k.thna.tex t045w.thna.tex
t045.th.pp t045q.th.pp t045k.th.pp t045w.th.pp  t045.thna.pp t045q.thna.pp t045k.thna.pp t045w.thna.pp: t045.ldd

t046.pdf: t046a.th.tex t046b.th.tex
t046a.th.pp t046b.th.pp: t046.ldd

t047.pdf: t047.th.tex
t047.th.pp: t047.ldd

t048.pdf: t048a.th.tex t048.stats.tex
t048a.th.pp t048.stats.tex: t048.ldd

t049.pdf: t049a.th.tex t049b.th.tex t049.stats.tex
t049a.th.pp t049b.th.pp t049.stats.tex: t049.ldd

t050.pdf: icl.th.tex
icl.th.pp: t050.ldd

t051.pdf: ordcard0.th.tex ordcard.th.tex
ordcard0.th.pp ordcard.th.pp: t051.ldd

# t053.pdf: t053h.th.tex t053z.th.tex
# t053h.th.pp t053z.th.pp: t053.ldd

t054.pdf: t054.th.tex
t054.th.pp: t054.ldd

t056.pdf: ordinals.th.tex inaccess.th.tex indatat.th.tex
ordinals.th.pp O.th.pp inaccess.th.pp idatat.th.pp: t056.ldd

t057.pdf: arch.th.tex
arch.th.pp: t057.ldd

t058.pdf: O.th.tex
O.th.pp: t058.ldd

nt004.pdf: spc003n.th.tex
spc003n.th.tex: nt004.ldd

$(IPDFS): %.pdf: %.sml

######################################################################
#
# Dependencies - determining the order of compilation
#
######################################################################

t038.ldd:
t010.ldd: $(HOLDBNAME).ldd
t011.ldd: $(HOLDBNAME).ldd
t006.ldd: t010.ldd
t045.ldd: t006.ldd
t012.ldd: t011.ldd
t003.ldd: t006.ldd
t005.ldd: t006.ldd
t009.ldd: t006.ldd
t016.ldd: t006.ldd
t039.ldd: t006.ldd
t029.ldd: t006.ldd
t037.ldd: t006.ldd
t002.ldd: t003.ldd
t004.ldd: t009.ldd
t017.ldd: t004.ldd t006.ldd t039.ldd
t023.ldd t042.ldd: t005.ldd t006.ldd t009.ldd
t021.ldd: t005.ldd t009.ldd t023.ldd
t007.ldd: t006.ldd t009.ldd t023.ldd
t008.ldd: t004.ldd t007.ldd
t019.ldd: t004.ldd t007.ldd
t018.ldd: t007.ldd t019.ldd
t025.ldd: t007.ldd t023.ldd
t040.ldd: t007.ldd t009.ldd t039.ldd
t043.ldd: t025.ldd t042.ldd
t044.ldd: t043.ldd t039.ldd
t045.ldd: t006.ldd
t046.ldd: t045.ldd
t047.ldd: t006.ldd
t048.ldd: t006.ldd
t049.ldd: t006.ldd
t024.ldd: t004.ldd t025.ldd
t001.ldd: t006.ldd t025.ldd
t022.ldd: t007.ldd t009.ldd t023.ldd
t020.ldd: t004.ldd t007.ldd t022.ldd
t026.ldd: t004.ldd t005.ldd t025.ldd
t027.ldd: t004.ldd t005.ldd t025.ldd
t028.ldd: t025.ldd
t030.ldd: t025.ldd
t031.ldd: t025.ldd
t032.ldd: t025.ldd t028.ldd
t033.ldd: t025.ldd
t041.ldd: t004.ldd t005.ldd t025.ldd t039.ldd t042.ldd t043.ldd
t050.ldd: t004.ldd t005.ldd t025.ldd t039.ldd t043.ldd
t051.ldd: t005.ldd t007.ldd t009.ldd t048.ldd
# t056 tramples over some names used by GSU so must be built after t044
t056.ldd: t009.ldd t044.ldd
t057.ldd: t009.ldd
t058.ldd: t056.ldd

spc001.ldd:
spc003.ldd:spc001.ldd

nt001.ldd:
nt004.ldd:spc003.ldd

# some variables and rules concerning document preparation

$(PDFFILES): rbj.bib rbj2.bib rbjfmu.bst rbjpp.ist rbj.sty pppdf texpdf

README.txt:

HTHSok= alloy.th ariscat.th aristotle.th \
      ba.th BRT.th bvi.th cat.th catfun.th CC.th cfpi.th circuit.th \
      diffgeom.th equiv.th fba.th fcat.th fixp.th fixp-egs.th fmphil.th \
      gccon.th grice.th griceC.th griceS.th \
      GS.th GST.th gst-ax.th gst-fun.th gst-nat.th gst-ord.th \
      GSU.th gsu-ax.th gsu-fun.th gsu-nat.th gsu-ord.th gsu-seq.th \
      holw.th icl.th ICsyn.th ICsem.th icomb.th ifol.th ifos.th \
      ilamb.th infos.th inaccess.th indatat.th\
      lattice.th latt2.th leibniz01.th leibniz02.th leibniz03.th \
      membership.th memfunct.th metaci.th metapi.th misc1.th misc2.th misc3.th modsyllog.th \
      nf_h.th nf_s.th nff.th nfu_s.th nfu_f.th \
      O.th ordcard0.th ordcard.th ordered_sets.th ordered_sets_i.th\
      ordinals.th PM01.th poly-sets.th pre_func.th rbjmisc.th \
      sfp.th sr.th sra.th src.th syllog1.th syllog2.th syllog3.th syllog4.th syllog5.th \
      syllog6.th syllmetap.th \
      t001a.th t001b.th t002a.th t045.th t045q.th t045k.th t045w.th t046a.th t046b.th \
      t047.th t048a.th t049a.th t049b.th t054.th tc.th tract01.th \
      U_orders.th uacat.th unalg.th unalgII.th wfrel.th wf_relp.th wf_recp.th \
      X-Logic-Auth.th X-Logic-1.th X-Logic-2.th \
      arch.th

ZTHS=ex2z.th t053h.th t053z.th

HTHSduff=
HTHS=$(HTHSok) $(HTHSduff)

HTHNAS=t045.thna t045q.thna t045k.thna t045w.thna

THEORIESok=$(HTHSok) # $(ZTHS)
THEORIES=$(THEORIESok) $(HTHSduff)

#HTHDOCS=$(HTHS:.th=.th.doc)
HTHPPS=$(HTHS:.th=.th.pp)
#HTHNADOCS=$(HTHNAS:.thna=.thna.doc)
HTHNAPPS=$(HTHNAS:.thna=.thna.pp)
#ZTHDOCS=$(ZTHS:.th=.th.pp)
ZTHPPS=$(ZTHS:.th=.th.pp)

THPPS=$(HTHPPS) $(ZTHPPS)
#THDOCS=$(HTHDOCS) $(ZTHDOCS)
THTEXSok=$(THEORIESok:.th=.th.tex)
THTEXS=$(THEORIES:.th=.th.tex)
THNATEXS=$(HTHNAS:.thna=.thna.tex)

$(THTEXS): %.tex: %.pp keywords
	   pptex -f $(PPSVF) -k keywords $*
	   @sed -i -e "/THE THEORY/s/THE THEORY/The Theory/" $*.tex
	   @sed -i -e "/underscoreoff/s/\([^_\]\)_/\1\\\\_/g" $*.tex
#	   @sed -i -e "/\\+\t/s/\t/       /g" $*.tex

$(THNATEXS): %.tex: %.pp
	   pptex -f $(PPSVF) -k keywords $*
	   @sed -i -e "/THE THEORY/s/THE THEORY\(.*\)/The Theory\1 (no aliases)/" $*.tex
	   @sed -i -e "/underscoreoff/s/\([^_\]\)_/\1\\\\_/g" $*.tex
#	   @sed -i -e "/\\+\t/s/\t/       /g" $*.tex

STATS=t046.stats t048.stats t049.stats
STATPPS=$(STATS:.stats=.stats.pp)
STATTEXS=$(STATS:.stats=.stats.tex)

$(STATTEXS): %.tex: %.doc
	   doctex $*

######################################################################
#
# Dependencies - describing which documents depend on which theory listings
#
######################################################################

######################################################################
#
#	Building the database
#
######################################################################

bld: t002.ldd t003.ldd t004.ldd t005.ldd t006.ldd t007.ldd \
     t008.ldd t009.ldd \
     t010.ldd t016.ldd t018.ldd t019.pp t020.ldd t021.ldd t022.ldd t023.ldd \
     t024.ldd t025.ldd t026.ldd t027.ldd t028.ldd t029.ldd t032.ldd t033.ldd t037.ldd \
     t038.ldd t039.ldd t040.ldd t041.ldd t042.ldd t043.ldd t044.ldd t045.ldd t046.ldd \
     t050.ldd t051.ldd t054.ldd
# t056.ldd t058.ldd

$(HOLDBNAME).ldd:
ifeq ($(USERDB),)
	pp_make_database -f -p $(STARTHOLDBNAME) $(HOLDBNAME)
endif
	touch $(HOLDBNAME).ldd

$(ZEDDBNAME).ldd:
	pp_make_database -f -p $(STARTZEDDBNAME) $(ZEDDBNAME)
	touch $(ZEDDBNAME).ldd

# useful target to print out the names of all the files in the source $(RELDIR)

packinglist:
	@echo $(PACKINGLIST)

######################################################################
#
#	Building the documents
#
######################################################################

t000abs.tex: $(TTEX) $(NTEX)
	./texindex2tex $(TTEX) $(NTEX) > t000abs.tex

doc_theories.tex: $(THTEXSok)
	cat $(THTEXSok) >| doc_theories.tex

pdf: $(PDFFILES)

######################################################################
#
#	Constructing source release directories
#
######################################################################

reldir:
	if [ "$${PPTARGETDIR:-}" = "" ]; \
	then \
		rm -rf $(RELDIR); \
	fi
	[ -d   $(RELDIR) ] || mkdir $(RELDIR)
	
srcdir:	reldir
	[ -d   $(RELDIR)/src ] || mkdir $(RELDIR)/src

docdir:	reldir
	[ -d   $(RELDIR)/doc ] || mkdir $(RELDIR)/doc

rcsrel:	srcdir
	[ -d   $(RELDIR)/src/RCS ] || mkdir $(RELDIR)/src/RCS
	@for f in $(PACKINGLIST); \
	do \
		cp RCS/$$f,v $(RELDIR)/src/RCS/$$f,v; \
	done
	chmod -R a-w $(RELDIR)
	chmod -R g-w $(RELDIR)
	chmod -R u+w $(RELDIR)

rcs:	rcsrel
	cd $(RELDIR) && tar cvf $(CWD)/$(PRODUCT).rcs.tar ./*
	cd $(CWD) && gzip $(PRODUCT).rcs.tar && \
	mv $(PRODUCT).rcs.tar.gz $(PRODUCT).rcs.tgz

srcrel: srcdir $(DISTPACKINGLIST)
	@for f in $(DISTPACKINGLIST); \
	do \
		cp $$f $(RELDIR)/src/$$f; \
	done
	chmod -R a-w $(RELDIR)
	chmod -R g-w $(RELDIR)
	chmod -R u+w $(RELDIR)

docrel: docdir $(PDFFILES)
	@for f in $(PDFFILES); \
	do \
		cp $$f $(RELDIR)/doc/$$f; \
	done
	chmod -R a-w $(RELDIR)
	chmod -R g-w $(RELDIR)
	chmod -R u+w $(RELDIR)

src:	srcrel
	cd $(RELDIR) && tar cvfz $(CWD)/$(PRODUCT).src.tgz ./*
	cd $(CWD)

dist:	src

doc:	docrel
	cd $(RELDIR) && tar cvfz $(CWD)/$(PRODUCT).pdf.tgz ./*
	cd $(CWD)

######################################################################
#
#	Tidying Up
#
######################################################################

clean:
	rm -f $(HOLTEXS) $(HOLMTEXS) $(ITEXS) $(SMLFILES) $(LDDFILES)
	rm -f *.aux *.bbl *.blg *.err *.idx *.log *.lot *.out *.sid *-e \
	*.thna.pp *.sml *.toc *.th.pp *.stats.doc *.stats.tex t000abs.tex \
	doc_theories.tex \\#*\\#

######################################################################
#
#	Generic Rules
#
######################################################################

$(HOLLDD): %.ldd: %.sml
	@rm -f $@ $*.err 2>/dev/null
	@echo "Compiling (code)" $<
	@PPCHARSET=utf8 pp -d $(HOLDBNAME) -f $< >$*.err
	@mv $*.err $@

$(ZEDLDD): %.ldd: %.sml
	@rm -f $@ $*.err 2>/dev/null
	@echo "Compiling (code)" $<
	@PPCHARSET=utf8 pp -d $(ZEDDBNAME) -f $< >$*.err
	@mv $*.err $@

$(HTHDOCS): %.th.doc: list_wa.sml
	@rm -f $@ $*.err 2>/dev/null
	@echo "Listing hol theory: " $*
	@pp_list -d $(HOLDBNAME) -i list_wa.sml $* >$*.err
	sed -e 's/val it = (): unit//' $*.err >$@

$(HTHPPS): %.th.pp: list_wa.sml
	@rm -f $@ $*.err 2>/dev/null
	@echo "Listing hol theory: " $*
	@pp_list -d $(HOLDBNAME) -i list_wa.sml $* >$*.err
	sed -e 's/val it = (): unit//' $*.err >$@

$(HTHNADOCS): %.thna.doc: list_na.sml
	@rm -f $@ $*.err 2>/dev/null
	@echo "Listing (without aliases) hol theory: " $*
	@pp_list -d $(HOLDBNAME) -i list_na.sml $* >$*.err
	sed -e 's/val it = (): unit//' $*.err >$@

$(HTHNAPPS): %.thna.pp: list_na.sml
	@rm -f $@ $*.err 2>/dev/null
	@echo "Listing (without aliases) hol theory: " $*
	@pp_list -d $(HOLDBNAME) -i list_na.sml $* >$*.err
	sed -e 's/val it = (): unit//' $*.err >$@

$(ZTHDOCS): %.th.doc:
	@rm -f $@ $*.err 2>/dev/null
	@echo "Listing zed theory: " $*
	@zed_list -d $(HOLDBNAME) $* >$*.err
	sed -e 's/val it = (): unit//' $*.err >$@

#%.sml: %.doc
#	docsml -f sieveview $*

%.sml: %.pp keywords
	ppsml -f $(PPSVF) -k keywords $*

# Single file ppsvf cases 

$(HOLTEXS1): %.tex: %.pp keywords
	pptex -f $(PPSVF) -k keywords $*

# Three file ppsvf cases 

$(HOLTEXS2): %.tex: %a.tex %.pp %z.tex keywords
	pptex -f $(PPSVF) -k keywords $*
	mv $*.tex $*m.tex
	cat $*a.tex $*m.tex $*z.tex > $*.tex

# Three file min keyword ppsvf cases 

$(HOLTEXS3): %.tex: %a.tex %.pp %z.tex
	pptex -f $(PPSVF) -K -k minkeys $*
	mv $*.tex $*m.tex
	cat $*a.tex $*m.tex $*z.tex > $*.tex

# Single file min keyword no svf! cases

$(HOLTEXS4): %.tex: %.pp
	pptex -K -k minkeys $*

%.dvi: %.tex
	TEXINPUTS=.:$(PPHOME)/tex: \
	BSTINPUTS=.:$(PPHOME)/tex: \
	BIBINPUTS=.:$(PPHOME)/tex: texdvi $*

$(PDFFILES1): %.pdf: %.pp
	TEXINPUTS=.:$(PPHOME)/tex: \
	BSTINPUTS=.:$(PPHOME)/tex: \
	BIBINPUTS=.:$(PPHOME)/tex: \
	PATH=.:$(PATH) pppdf -f $(PPSVF) $*

$(PDFFILES2): %.pdf: %.tex
	TEXINPUTS=.:$(PPHOME)/tex: \
	BSTINPUTS=.:$(PPHOME)/tex: \
	BIBINPUTS=.:$(PPHOME)/tex: \
	PATH=.:$(PATH) texpdf $*
	TEXINPUTS=.:$(PPHOME)/tex: \
	BSTINPUTS=.:$(PPHOME)/tex: \
	BIBINPUTS=.:$(PPHOME)/tex: bibtex $*
	TEXINPUTS=.:$(PPHOME)/tex: \
	BSTINPUTS=.:$(PPHOME)/tex: \
	BIBINPUTS=.:$(PPHOME)/tex: \
	PATH=.:$(PATH) texpdf $*

$(PDFFILES3): %.pdf: %.tex
	TEXINPUTS=.:$(PPHOME)/tex: \
	BSTINPUTS=.:$(PPHOME)/tex: \
	BIBINPUTS=.:$(PPHOME)/tex: \
	PATH=.:$(PATH) texpdf -p lualatex $*
	TEXINPUTS=.:$(PPHOME)/tex: \
	BSTINPUTS=.:$(PPHOME)/tex: \
	BIBINPUTS=.:$(PPHOME)/tex: bibtex $*
	TEXINPUTS=.:$(PPHOME)/tex: \
	BSTINPUTS=.:$(PPHOME)/tex: \
	BIBINPUTS=.:$(PPHOME)/tex: \
	PATH=.:$(PATH) texpdf -p lualatex $*

$(PDFFILES4): %.pdf: %.pp
	TEXINPUTS=.:$(PPHOME)/tex: \
	BSTINPUTS=.:$(PPHOME)/tex: \
	BIBINPUTS=.:$(PPHOME)/tex: \
	PATH=.:$(PATH) pppdf -p lualatex $*

#%.pdf: %.dvi
#	dvipdf -sPAPERSIZE=a4 $*