pip: IsaMakefile@ed938e2246b9 (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
5 0f2d4b78f839 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 4 diff changeset	27	cp Slides/generated/root.beamer.pdf slides1.pdf
2 a04084de4946 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	28
4 9d667d545e32 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 2 diff changeset	29	## Slides
9d667d545e32 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 2 diff changeset	30
9d667d545e32 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 2 diff changeset	31	session2: Slides/ROOT2.ML \
9d667d545e32 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 2 diff changeset	32	Slides/document/root* \
9d667d545e32 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 2 diff changeset	33	Slides/Slides2.thy
9d667d545e32 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 2 diff changeset	34	@$(USEDIR) -D generated -f ROOT2.ML HOL Slides
9d667d545e32 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 2 diff changeset	35
9d667d545e32 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 2 diff changeset	36	slides2: session2
9d667d545e32 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 2 diff changeset	37	rm -f Slides/generated/*.aux # otherwise latex will fall over
9d667d545e32 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 2 diff changeset	38	cd Slides/generated ; $(ISABELLE_TOOL) latex -o pdf root.beamer.tex
5 0f2d4b78f839 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 4 diff changeset	39	cp Slides/generated/root.beamer.pdf slides2.pdf
4 9d667d545e32 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 2 diff changeset	40
9d667d545e32 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 2 diff changeset	41
2 a04084de4946 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	42	# main files
a04084de4946 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	43
a04084de4946 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	44	session: ./ROOT.ML ./*.thy
a04084de4946 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	45	@$(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	46
a04084de4946 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	47
a04084de4946 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	48	# itp paper
a04084de4946 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	49
a04084de4946 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	50	itp: Paper/.thy Paper/.ML
a04084de4946 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	51	@$(USEDIR) -D generated -f ROOT.ML Prio Paper
a04084de4946 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	52	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	53	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	54	cd Paper/generated ; bibtex root
a04084de4946 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	55	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	56	cp Paper/generated/root.pdf paper.pdf
a04084de4946 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	57
6 7f2493296c39 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 5 diff changeset	58	# C&L paper
7f2493296c39 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 5 diff changeset	59
7f2493296c39 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 5 diff changeset	60	jour: Journal/.thy Journal/.ML
7f2493296c39 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 5 diff changeset	61	@$(USEDIR) -D generated -f ROOT.ML Prio Journal
7f2493296c39 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 5 diff changeset	62	rm -f Journal/generated/*.aux # otherwise latex will fall over
7f2493296c39 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 5 diff changeset	63	cd Journal/generated ; $(ISABELLE_TOOL) latex -o pdf root.tex
7f2493296c39 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 5 diff changeset	64	cd Journal/generated ; bibtex root
7f2493296c39 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 5 diff changeset	65	cd Journal/generated ; $(ISABELLE_TOOL) latex -o pdf root.tex
7f2493296c39 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 5 diff changeset	66	cp Journal/generated/root.pdf journal.pdf
2 a04084de4946 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	67
a04084de4946 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	68
6 7f2493296c39 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 5 diff changeset	69

author	zhangx
	Thu, 28 Jan 2016 21:14:17 +0800
changeset 90	ed938e2246b9
parent 6	7f2493296c39
permissions	-rwxr-xr-x