## targets
default: itp
all: session itp slides1
## global settings
SRC = $(ISABELLE_HOME)/src
OUT = $(ISABELLE_OUTPUT)
LOG = $(OUT)/log
USEDIR = $(ISABELLE_TOOL) usedir -v true -t true
## Slides
session1: Slides/ROOT1.ML \
Slides/document/root* \
Slides/Slides1.thy
@$(USEDIR) -D generated -f ROOT1.ML HOL Slides
slides1: session1
rm -f Slides/generated/*.aux # otherwise latex will fall over
cd Slides/generated ; $(ISABELLE_TOOL) latex -o pdf root.beamer.tex
cp Slides/generated/root.beamer.pdf Slides/slides.pdf
# main files
session: ./ROOT.ML ./*.thy
@$(USEDIR) -b -D generated -f ROOT.ML HOL Prio
# itp paper
itp: Paper/*.thy Paper/*.ML
@$(USEDIR) -D generated -f ROOT.ML Prio Paper
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
slides: Slides/ROOT1.ML Slides/*.thy
@$(USEDIR) -D generated -f ROOT1.ML Prio Slides
rm -f Slides/generated/*.aux # otherwise latex will fall over
cd Slides/generated ; $(ISABELLE_TOOL) latex -o pdf root.beamer.tex
cp Slides/generated/root.beamer.pdf Slides/slides.pdf