## targets
default: utm
images: utm
test:
all: images test
## global settings
SRC = $(ISABELLE_HOME)/src
OUT = $(ISABELLE_OUTPUT)
LOG = $(OUT)/log
USEDIR = $(ISABELLE_TOOL) usedir -v true -i false
## utm
utm: $(OUT)/utm
$(OUT)/utm: thys/*.thy ROOT.ML
@$(USEDIR) -f ROOT.ML -b HOL UTM
#paper: ROOT.ML \
# document/root* \
# *.thy
# rm -rf generated # otherwise latex will fall over
# @$(USEDIR) -f ROOT1.ML UTM .
# $(ISABELLE_TOOL) document -o pdf generated
# cp generated/root.pdf paper.pdf
## ITP itp
session_itp: Paper/ROOT.ML \
Paper/document/root* \
Paper/*.thy
@$(USEDIR) -D generated -f ROOT.ML UTM Paper
itp: session_itp
rm -f Paper/generated/*.aux # otherwise latex will fall over
cd Paper/generated ; $(ISABELLE_TOOL) latex -o pdf root.tex
cd Paper/generated ; bibtex root
cd Paper/generated ; $(ISABELLE_TOOL) latex -o pdf root.tex
cp Paper/generated/root.pdf paper.pdf
## clean
clean:
@rm -f $(OUT)/utm