# Makefile for the SPaDE ProofPower database

# This makes a composite SPaDE UTF8 ProofPower database contining the following:

# 1 The hol.polydb delivered by the ProofPower build
# 2 The maths_egs theories from ProofPower contrib repository (in maths_egs.polydb)
# 3. The formal specifications of ProofPower HOL in the spc???.pp series.
# 4. The rbj materials from the np directory.

# All of this, and ProofPower usage in general, is part of a bootstrap.
# The SPaDE system when operational will eventually eliminate dependence
# on ProofPower (while acknowledging the past contribution).

# The following variables are not used throughout, so changing the values
# probably won't work.

MATHEGPPDBNAME = maths_egs
BASEPPDBNAME = rbjhol
SPADEPPDBNAME = spade

PPDBNAMES = $(MATHEGPPDBNAME) $(BASEPPDBNAME) $(SPADEPPDBNAME)
PPDBLDDS = $(PPDBNAMES:=.ldd)

MATHEGPPDBPATH = $(PPDIR)/bld/db/maths_egs.polydb
BASEPPDBPATH = $(PPDIR)/bld/db/rbjhol.polydb
SPADEPPDBPATH = $(PPDIR)/bld/db/spade.polydb

PPDBS = $(MATHEGPPDBPATH) $(BASEPPDBPATH) $(SPADEPPDBPATH) 

clean:
	rm -f $(PPDBS) $(PPDBLDDS);cd ..; rm -rf $(PPDBLDDS); cd retro

# The maths_egs makefile creates a database called maths_egs.polydb

maths_egs.ldd:
	$(MAKE) -C maths_egs -f maths_egs.mkf clean load
	cp maths_egs/maths_egs.polydb $(PPDIR)/bld/db/
	touch maths_egs.ldd

# The PP HOL specs are then loaded to the maths_egs database

$(BASEPPDBNAME).ldd: maths_egs.ldd
	cd $(PPDIR)/src/hol && make -f hol.mkf spc001.sml spc002.sml spc003.sml spc004.sml spc005.sml && \
	echo "save_and_quit{};" | $(PPDIR)/bld/bin/pp -d maths_egs -f spc001 -f spc002 -f spc003 -f spc004 -f spc005 > $(BASEPPDBNAME).ldd
# The np/rbj.mkf makefile builds the rbjhol.poldb database on maths_egs.polydb.
# Some of the theories here (e.g. rbjmisc) will be used for early versions of the SPaDE specifications.
	$(MAKE) -C np -f rbj.mkf clean bld
	cp np/$(BASEPPDBNAME).polydb $(PPDIR)/bld/db/
	touch $(BASEPPDBNAME).ldd

# Then we make the spade.polydb database using rbjhol as parent.
# This freezes rbjhol. Task databases are further children of rbjhol,
# created in the task worktree (docs/admin/ampd004.md). They are not
# built here, and spade is not their parent.
# This remains pro-tem but is not expected to be used since spade.polydb is now to be placed in each worktree when the worktree is created.

$(SPADEPPDBNAME).ldd: $(BASEPPDBNAME).ldd
	pp_make_database -f -p $(BASEPPDBNAME) $(SPADEPPDBNAME)
	cp $(SPADEPPDBNAME).polydb $(PPDIR)/bld/db/
	touch $(SPADEPPDBNAME).ldd ../$(SPADEPPDBNAME).ldd