IsaMakefile
author Christian Urban <christian dot urban at kcl dot ac dot uk>
Wed, 26 Dec 2012 14:52:14 +0000
changeset 1 4b9aa15ff713
parent 0 aa8656a8dbef
child 2 26b17f2d583e
permissions -rw-r--r--
added
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
0
aa8656a8dbef initial setup
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
     1
aa8656a8dbef initial setup
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
     2
## targets
aa8656a8dbef initial setup
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
     3
aa8656a8dbef initial setup
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
     4
default: utm
aa8656a8dbef initial setup
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
     5
images: utm
aa8656a8dbef initial setup
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
     6
test: 
aa8656a8dbef initial setup
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
     7
aa8656a8dbef initial setup
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
     8
all: images test
aa8656a8dbef initial setup
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
     9
aa8656a8dbef initial setup
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    10
aa8656a8dbef initial setup
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    11
## global settings
aa8656a8dbef initial setup
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    12
aa8656a8dbef initial setup
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    13
SRC = $(ISABELLE_HOME)/src
aa8656a8dbef initial setup
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    14
OUT = $(ISABELLE_OUTPUT)
aa8656a8dbef initial setup
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    15
LOG = $(OUT)/log
aa8656a8dbef initial setup
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    16
1
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 0
diff changeset
    17
USEDIR = $(ISABELLE_TOOL) usedir -v true -i false -d pdf  ## -D generated
0
aa8656a8dbef initial setup
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    18
aa8656a8dbef initial setup
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    19
aa8656a8dbef initial setup
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    20
## utm
aa8656a8dbef initial setup
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    21
aa8656a8dbef initial setup
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    22
utm: $(OUT)/utm
aa8656a8dbef initial setup
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    23
1
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 0
diff changeset
    24
$(OUT)/utm: *.thy
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 0
diff changeset
    25
	@$(USEDIR) -b HOL UTM
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 0
diff changeset
    26
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 0
diff changeset
    27
session:  ROOT.ML \
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 0
diff changeset
    28
	document/root* \
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 0
diff changeset
    29
	*.thy
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 0
diff changeset
    30
	@$(USEDIR) -D generated -f ROOT.ML UTM .
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 0
diff changeset
    31
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 0
diff changeset
    32
paper: utm
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 0
diff changeset
    33
	rm -f generated/*.aux # otherwise latex will fall over       
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 0
diff changeset
    34
	cd generated ; $(ISABELLE_TOOL) latex -o pdf root.tex 
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 0
diff changeset
    35
#	cd generated ; bibtex root
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 0
diff changeset
    36
#	cd generated ; $(ISABELLE_TOOL) latex -o pdf root.tex
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 0
diff changeset
    37
	cp generated/root.pdf paper.pdf  
0
aa8656a8dbef initial setup
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    38
aa8656a8dbef initial setup
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    39
aa8656a8dbef initial setup
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    40
## clean
aa8656a8dbef initial setup
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    41
aa8656a8dbef initial setup
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    42
clean:
aa8656a8dbef initial setup
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    43
	@rm -f $(OUT)/utm