regexp: prio/IsaMakefile@484c7b83f251 (annotated)

262 4190df6f4488 initial version of the PIP formalisation urbanc parents: diff changeset	1
4190df6f4488 initial version of the PIP formalisation urbanc parents: diff changeset	2	## targets
4190df6f4488 initial version of the PIP formalisation urbanc parents: diff changeset	3
265 993068ce745f changed abstract, intro and IsaMakefile urbanc parents: 264 diff changeset	4	default: itp
360 66e0ec8acedc added some slides for an informal talk about PIP urbanc parents: 282 diff changeset	5	all: session itp slides1
262 4190df6f4488 initial version of the PIP formalisation urbanc parents: diff changeset	6
4190df6f4488 initial version of the PIP formalisation urbanc parents: diff changeset	7	## global settings
4190df6f4488 initial version of the PIP formalisation urbanc parents: diff changeset	8
4190df6f4488 initial version of the PIP formalisation urbanc parents: diff changeset	9	SRC = $(ISABELLE_HOME)/src
4190df6f4488 initial version of the PIP formalisation urbanc parents: diff changeset	10	OUT = $(ISABELLE_OUTPUT)
4190df6f4488 initial version of the PIP formalisation urbanc parents: diff changeset	11	LOG = $(OUT)/log
4190df6f4488 initial version of the PIP formalisation urbanc parents: diff changeset	12
4190df6f4488 initial version of the PIP formalisation urbanc parents: diff changeset	13
4190df6f4488 initial version of the PIP formalisation urbanc parents: diff changeset	14	USEDIR = $(ISABELLE_TOOL) usedir -v true -t true
4190df6f4488 initial version of the PIP formalisation urbanc parents: diff changeset	15
4190df6f4488 initial version of the PIP formalisation urbanc parents: diff changeset	16
4190df6f4488 initial version of the PIP formalisation urbanc parents: diff changeset	17	## Slides
4190df6f4488 initial version of the PIP formalisation urbanc parents: diff changeset	18
360 66e0ec8acedc added some slides for an informal talk about PIP urbanc parents: 282 diff changeset	19	session1: Slides/ROOT1.ML \
66e0ec8acedc added some slides for an informal talk about PIP urbanc parents: 282 diff changeset	20	Slides/document/root* \
66e0ec8acedc added some slides for an informal talk about PIP urbanc parents: 282 diff changeset	21	Slides/Slides1.thy
66e0ec8acedc added some slides for an informal talk about PIP urbanc parents: 282 diff changeset	22	@$(USEDIR) -D generated -f ROOT1.ML HOL Slides
66e0ec8acedc added some slides for an informal talk about PIP urbanc parents: 282 diff changeset	23
66e0ec8acedc added some slides for an informal talk about PIP urbanc parents: 282 diff changeset	24	slides1: session1
66e0ec8acedc added some slides for an informal talk about PIP urbanc parents: 282 diff changeset	25	rm -f Slides/generated/*.aux # otherwise latex will fall over
66e0ec8acedc added some slides for an informal talk about PIP urbanc parents: 282 diff changeset	26	cd Slides/generated ; $(ISABELLE_TOOL) latex -o pdf root.beamer.tex
66e0ec8acedc added some slides for an informal talk about PIP urbanc parents: 282 diff changeset	27	cp Slides/generated/root.beamer.pdf Slides/slides.pdf
66e0ec8acedc added some slides for an informal talk about PIP urbanc parents: 282 diff changeset	28
66e0ec8acedc added some slides for an informal talk about PIP urbanc parents: 282 diff changeset	29	# main files
66e0ec8acedc added some slides for an informal talk about PIP urbanc parents: 282 diff changeset	30
262 4190df6f4488 initial version of the PIP formalisation urbanc parents: diff changeset	31	session: ./ROOT.ML ./*.thy
4190df6f4488 initial version of the PIP formalisation urbanc parents: diff changeset	32	@$(USEDIR) -b -D generated -f ROOT.ML HOL Prio
265 993068ce745f changed abstract, intro and IsaMakefile urbanc parents: 264 diff changeset	33
360 66e0ec8acedc added some slides for an informal talk about PIP urbanc parents: 282 diff changeset	34
66e0ec8acedc added some slides for an informal talk about PIP urbanc parents: 282 diff changeset	35	# itp paper
66e0ec8acedc added some slides for an informal talk about PIP urbanc parents: 282 diff changeset	36
265 993068ce745f changed abstract, intro and IsaMakefile urbanc parents: 264 diff changeset	37	itp: Paper/.thy Paper/.ML
262 4190df6f4488 initial version of the PIP formalisation urbanc parents: diff changeset	38	@$(USEDIR) -D generated -f ROOT.ML Prio Paper
4190df6f4488 initial version of the PIP formalisation urbanc parents: diff changeset	39	rm -f Paper/generated/*.aux # otherwise latex will fall over
4190df6f4488 initial version of the PIP formalisation urbanc parents: diff changeset	40	cd Paper/generated ; $(ISABELLE_TOOL) latex -o pdf root.tex
4190df6f4488 initial version of the PIP formalisation urbanc parents: diff changeset	41	cd Paper/generated ; bibtex root
4190df6f4488 initial version of the PIP formalisation urbanc parents: diff changeset	42	cd Paper/generated ; $(ISABELLE_TOOL) latex -o pdf root.tex
4190df6f4488 initial version of the PIP formalisation urbanc parents: diff changeset	43	cp Paper/generated/root.pdf paper.pdf
361 484c7b83f251 IsaMakefile modified zhang parents: 360 diff changeset	44
484c7b83f251 IsaMakefile modified zhang parents: 360 diff changeset	45
484c7b83f251 IsaMakefile modified zhang parents: 360 diff changeset	46	slides: Slides/ROOT1.ML Slides/*.thy
484c7b83f251 IsaMakefile modified zhang parents: 360 diff changeset	47	@$(USEDIR) -D generated -f ROOT1.ML Prio Slides
484c7b83f251 IsaMakefile modified zhang parents: 360 diff changeset	48	rm -f Slides/generated/*.aux # otherwise latex will fall over
484c7b83f251 IsaMakefile modified zhang parents: 360 diff changeset	49	cd Slides/generated ; $(ISABELLE_TOOL) latex -o pdf root.beamer.tex
484c7b83f251 IsaMakefile modified zhang parents: 360 diff changeset	50	cp Slides/generated/root.beamer.pdf Slides/slides.pdf
484c7b83f251 IsaMakefile modified zhang parents: 360 diff changeset	51

author	zhang
	Fri, 10 Aug 2012 13:54:21 +0000
changeset 361	484c7b83f251
parent 360	66e0ec8acedc
permissions	-rwxr-xr-x