pip: IsaMakefile@a04084de4946 (annotated)

2 a04084de4946 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1
a04084de4946 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	2	## targets
a04084de4946 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	3
a04084de4946 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	4	default: itp
a04084de4946 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	5	all: session itp slides1
a04084de4946 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	6
a04084de4946 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	7	## global settings
a04084de4946 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	8
a04084de4946 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	9	SRC = $(ISABELLE_HOME)/src
a04084de4946 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	10	OUT = $(ISABELLE_OUTPUT)
a04084de4946 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	11	LOG = $(OUT)/log
a04084de4946 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	12
a04084de4946 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	13
a04084de4946 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	14	USEDIR = $(ISABELLE_TOOL) usedir -v true -t true
a04084de4946 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	15
a04084de4946 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	16
a04084de4946 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	17	## Slides
a04084de4946 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	18
a04084de4946 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	19	session1: Slides/ROOT1.ML \
a04084de4946 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	20	Slides/document/root* \
a04084de4946 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	21	Slides/Slides1.thy
a04084de4946 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	22	@$(USEDIR) -D generated -f ROOT1.ML HOL Slides
a04084de4946 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	23
a04084de4946 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	24	slides1: session1
a04084de4946 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	25	rm -f Slides/generated/*.aux # otherwise latex will fall over
a04084de4946 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	26	cd Slides/generated ; $(ISABELLE_TOOL) latex -o pdf root.beamer.tex
a04084de4946 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	27	cp Slides/generated/root.beamer.pdf Slides/slides.pdf
a04084de4946 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	28
a04084de4946 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	29	# main files
a04084de4946 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	30
a04084de4946 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	31	session: ./ROOT.ML ./*.thy
a04084de4946 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	32	@$(USEDIR) -b -D generated -f ROOT.ML HOL Prio
a04084de4946 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	33
a04084de4946 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	34
a04084de4946 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	35	# itp paper
a04084de4946 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	36
a04084de4946 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	37	itp: Paper/.thy Paper/.ML
a04084de4946 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	38	@$(USEDIR) -D generated -f ROOT.ML Prio Paper
a04084de4946 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	39	rm -f Paper/generated/*.aux # otherwise latex will fall over
a04084de4946 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	40	cd Paper/generated ; $(ISABELLE_TOOL) latex -o pdf root.tex
a04084de4946 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	41	cd Paper/generated ; bibtex root
a04084de4946 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	42	cd Paper/generated ; $(ISABELLE_TOOL) latex -o pdf root.tex
a04084de4946 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	43	cp Paper/generated/root.pdf paper.pdf
a04084de4946 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	44
a04084de4946 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	45
a04084de4946 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	46	slides: Slides/ROOT1.ML Slides/*.thy
a04084de4946 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	47	@$(USEDIR) -D generated -f ROOT1.ML Prio Slides
a04084de4946 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	48	rm -f Slides/generated/*.aux # otherwise latex will fall over
a04084de4946 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	49	cd Slides/generated ; $(ISABELLE_TOOL) latex -o pdf root.beamer.tex
a04084de4946 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	50	cp Slides/generated/root.beamer.pdf Slides/slides.pdf
a04084de4946 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	51

author	Christian Urban <christian dot urban at kcl dot ac dot uk>
	Thu, 06 Dec 2012 15:12:49 +0000
changeset 2	a04084de4946
child 4	9d667d545e32
permissions	-rwxr-xr-x