16
+ − 1
+ − 2
## targets
+ − 3
24
+ − 4
default: paper
+ − 5
all: slides paper
16
+ − 6
+ − 7
## global settings
+ − 8
+ − 9
SRC = $(ISABELLE_HOME)/src
+ − 10
OUT = $(ISABELLE_OUTPUT)
+ − 11
LOG = $(OUT)/log
+ − 12
+ − 13
+ − 14
USEDIR = $(ISABELLE_TOOL) usedir -v true -t true
24
+ − 15
+ − 16
16
+ − 17
## Slides
+ − 18
24
+ − 19
session1: Slides/ROOT.ML \
16
+ − 20
Slides/document/root* \
24
+ − 21
Slides/Slides.thy
30
f5db9e08effc
Directory [tphols-2011] is added to host the commented version of [Myhill.thy]. Directory [pres] is created to host a build session for logical image [ListP] which is essentially [Main] extended with [List_prefix.thy].
zhang
diff
changeset
+ − 22
@$(USEDIR) -D generated -f ROOT.ML ListP tphols-2011
24
+ − 23
+ − 24
slides: session1
+ − 25
rm -f Slides/generated/*.aux # otherwise latex will fall over
+ − 26
cd Slides/generated ; $(ISABELLE_TOOL) latex -o pdf root.beamer.tex
+ − 27
cp Slides/generated/root.beamer.pdf Slides/slides.pdf
+ − 28
16
+ − 29
36
+ − 30
## long paper
16
+ − 31
30
f5db9e08effc
Directory [tphols-2011] is added to host the commented version of [Myhill.thy]. Directory [pres] is created to host a build session for logical image [ListP] which is essentially [Main] extended with [List_prefix.thy].
zhang
diff
changeset
+ − 32
session2: tphols-2011/ROOT.ML \
f5db9e08effc
Directory [tphols-2011] is added to host the commented version of [Myhill.thy]. Directory [pres] is created to host a build session for logical image [ListP] which is essentially [Main] extended with [List_prefix.thy].
zhang
diff
changeset
+ − 33
tphols-2011/document/root* \
31
b6815473ee2e
1. Myhill.thy is proved to correct some typos. 2. Some sections are added to the first direction. 3. The small theory of list difference is now separated into Prefix_subtract.thy and the ROOT.ML
zhang
diff
changeset
+ − 34
*.thy
55
+ − 35
@$(USEDIR) -D generated -f ROOT.ML ListP tphols-2011
24
+ − 36
+ − 37
paper: session2
30
f5db9e08effc
Directory [tphols-2011] is added to host the commented version of [Myhill.thy]. Directory [pres] is created to host a build session for logical image [ListP] which is essentially [Main] extended with [List_prefix.thy].
zhang
diff
changeset
+ − 38
rm -f tphols-2011/generated/*.aux # otherwise latex will fall over
f5db9e08effc
Directory [tphols-2011] is added to host the commented version of [Myhill.thy]. Directory [pres] is created to host a build session for logical image [ListP] which is essentially [Main] extended with [List_prefix.thy].
zhang
diff
changeset
+ − 39
cd tphols-2011/generated ; $(ISABELLE_TOOL) latex -o pdf root.tex
36
+ − 40
cd tphols-2011/generated ; $(ISABELLE_TOOL) latex -o pdf root.tex
30
f5db9e08effc
Directory [tphols-2011] is added to host the commented version of [Myhill.thy]. Directory [pres] is created to host a build session for logical image [ListP] which is essentially [Main] extended with [List_prefix.thy].
zhang
diff
changeset
+ − 41
cp tphols-2011/generated/root.pdf tphols-2011/myhill.pdf
16
+ − 42
72
+ − 43
## full paper
+ − 44
+ − 45
fullsession2: tphols-2011/ROOT.ML \
+ − 46
tphols-2011/document/root* \
+ − 47
*.thy
+ − 48
@$(USEDIR) -D generated -f ROOT.ML HOL tphols-2011
+ − 49
+ − 50
fullpaper: fullsession2
+ − 51
rm -f tphols-2011/generated/*.aux # otherwise latex will fall over
+ − 52
cd tphols-2011/generated ; $(ISABELLE_TOOL) latex -o pdf root.tex
+ − 53
cd tphols-2011/generated ; $(ISABELLE_TOOL) latex -o pdf root.tex
+ − 54
cp tphols-2011/generated/root.pdf tphols-2011/myhill.pdf
+ − 55
+ − 56
16
+ − 57
36
+ − 58
## ITP paper
+ − 59
+ − 60
session3: Paper/ROOT.ML \
+ − 61
Paper/document/root* \
+ − 62
Paper/*.thy
+ − 63
@$(USEDIR) -D generated -f ROOT.ML HOL Paper
+ − 64
+ − 65
itp: session3
+ − 66
rm -f Paper/generated/*.aux # otherwise latex will fall over
+ − 67
cd Paper/generated ; $(ISABELLE_TOOL) latex -o pdf root.tex
66
+ − 68
cd Paper/generated ; bibtex root
36
+ − 69
cd Paper/generated ; $(ISABELLE_TOOL) latex -o pdf root.tex
+ − 70
cp Paper/generated/root.pdf paper.pdf
+ − 71
162
+ − 72
## Journal Version
+ − 73
+ − 74
session4: Journal/ROOT.ML \
+ − 75
Journal/document/root* \
+ − 76
Journal/*.thy
+ − 77
@$(USEDIR) -D generated -f ROOT.ML HOL Journal
+ − 78
+ − 79
journal: session4
+ − 80
rm -f Journal/generated/*.aux # otherwise latex will fall over
+ − 81
cd Journal/generated ; $(ISABELLE_TOOL) latex -o pdf root.tex
+ − 82
cd Journal/generated ; bibtex root
+ − 83
cd Journal/generated ; $(ISABELLE_TOOL) latex -o pdf root.tex
+ − 84
cp Journal/generated/root.pdf journal.pdf
+ − 85
36
+ − 86
16
+ − 87
## clean
+ − 88
+ − 89
clean:
24
+ − 90
rm -rf Slides/generated/*
30
f5db9e08effc
Directory [tphols-2011] is added to host the commented version of [Myhill.thy]. Directory [pres] is created to host a build session for logical image [ListP] which is essentially [Main] extended with [List_prefix.thy].
zhang
diff
changeset
+ − 91
rm -rf tphols-2011/generated/*