prio/IsaMakefile
author urbanc
Fri, 20 Apr 2012 14:15:36 +0000
changeset 349 dae7501b26ac
parent 282 a3b4eed091d2
child 360 66e0ec8acedc
permissions -rwxr-xr-x
changes to get the files through for CU
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
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
282
a3b4eed091d2 moved unused theories to Attic
urbanc
parents: 265
diff changeset
     5
all: session itp
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
4190df6f4488 initial version of the PIP formalisation
urbanc
parents:
diff changeset
    19
session: ./ROOT.ML ./*.thy
4190df6f4488 initial version of the PIP formalisation
urbanc
parents:
diff changeset
    20
	@$(USEDIR) -b -D generated -f ROOT.ML HOL Prio
265
993068ce745f changed abstract, intro and IsaMakefile
urbanc
parents: 264
diff changeset
    21
993068ce745f changed abstract, intro and IsaMakefile
urbanc
parents: 264
diff changeset
    22
itp: Paper/*.thy Paper/*.ML 
262
4190df6f4488 initial version of the PIP formalisation
urbanc
parents:
diff changeset
    23
	@$(USEDIR) -D generated -f ROOT.ML Prio Paper
4190df6f4488 initial version of the PIP formalisation
urbanc
parents:
diff changeset
    24
	rm -f Paper/generated/*.aux # otherwise latex will fall over  
4190df6f4488 initial version of the PIP formalisation
urbanc
parents:
diff changeset
    25
	cd Paper/generated ; $(ISABELLE_TOOL) latex -o pdf root.tex 
4190df6f4488 initial version of the PIP formalisation
urbanc
parents:
diff changeset
    26
	cd Paper/generated ; bibtex root
4190df6f4488 initial version of the PIP formalisation
urbanc
parents:
diff changeset
    27
	cd Paper/generated ; $(ISABELLE_TOOL) latex -o pdf root.tex
4190df6f4488 initial version of the PIP formalisation
urbanc
parents:
diff changeset
    28
	cp Paper/generated/root.pdf paper.pdf