IsaMakefile
author urbanc
Mon, 20 Feb 2012 11:02:50 +0000
changeset 333 813e7257c7c3
parent 258 1abf8586ee6b
child 334 d47c2143ab8a
permissions -rw-r--r--
some polishing of the repository
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
16
663816814e3e added initial slides for informal talk in Cambridge
urbanc
parents:
diff changeset
     1
663816814e3e added initial slides for informal talk in Cambridge
urbanc
parents:
diff changeset
     2
## targets
663816814e3e added initial slides for informal talk in Cambridge
urbanc
parents:
diff changeset
     3
24
f72c82bf59e5 added paper
urbanc
parents: 16
diff changeset
     4
default: paper
f72c82bf59e5 added paper
urbanc
parents: 16
diff changeset
     5
all: slides paper
16
663816814e3e added initial slides for informal talk in Cambridge
urbanc
parents:
diff changeset
     6
663816814e3e added initial slides for informal talk in Cambridge
urbanc
parents:
diff changeset
     7
## global settings
663816814e3e added initial slides for informal talk in Cambridge
urbanc
parents:
diff changeset
     8
663816814e3e added initial slides for informal talk in Cambridge
urbanc
parents:
diff changeset
     9
SRC = $(ISABELLE_HOME)/src
663816814e3e added initial slides for informal talk in Cambridge
urbanc
parents:
diff changeset
    10
OUT = $(ISABELLE_OUTPUT)
663816814e3e added initial slides for informal talk in Cambridge
urbanc
parents:
diff changeset
    11
LOG = $(OUT)/log
663816814e3e added initial slides for informal talk in Cambridge
urbanc
parents:
diff changeset
    12
663816814e3e added initial slides for informal talk in Cambridge
urbanc
parents:
diff changeset
    13
663816814e3e added initial slides for informal talk in Cambridge
urbanc
parents:
diff changeset
    14
USEDIR = $(ISABELLE_TOOL) usedir -v true -t true 
24
f72c82bf59e5 added paper
urbanc
parents: 16
diff changeset
    15
f72c82bf59e5 added paper
urbanc
parents: 16
diff changeset
    16
333
813e7257c7c3 some polishing of the repository
urbanc
parents: 258
diff changeset
    17
## Slides 1
16
663816814e3e added initial slides for informal talk in Cambridge
urbanc
parents:
diff changeset
    18
24
f72c82bf59e5 added paper
urbanc
parents: 16
diff changeset
    19
session1: Slides/ROOT.ML \
16
663816814e3e added initial slides for informal talk in Cambridge
urbanc
parents:
diff changeset
    20
         Slides/document/root* \
24
f72c82bf59e5 added paper
urbanc
parents: 16
diff changeset
    21
         Slides/Slides.thy
203
5d724fe0e096 changes according to afp-submission
urbanc
parents: 162
diff changeset
    22
	@$(USEDIR) -D generated -f ROOT.ML HOL Slides
24
f72c82bf59e5 added paper
urbanc
parents: 16
diff changeset
    23
333
813e7257c7c3 some polishing of the repository
urbanc
parents: 258
diff changeset
    24
slides1: session1 
24
f72c82bf59e5 added paper
urbanc
parents: 16
diff changeset
    25
	rm -f Slides/generated/*.aux # otherwise latex will fall over
f72c82bf59e5 added paper
urbanc
parents: 16
diff changeset
    26
	cd Slides/generated ; $(ISABELLE_TOOL) latex -o pdf root.beamer.tex 
f72c82bf59e5 added paper
urbanc
parents: 16
diff changeset
    27
	cp Slides/generated/root.beamer.pdf Slides/slides.pdf     
f72c82bf59e5 added paper
urbanc
parents: 16
diff changeset
    28
333
813e7257c7c3 some polishing of the repository
urbanc
parents: 258
diff changeset
    29
## Slides 2
203
5d724fe0e096 changes according to afp-submission
urbanc
parents: 162
diff changeset
    30
333
813e7257c7c3 some polishing of the repository
urbanc
parents: 258
diff changeset
    31
session2: Slides/ROOT.ML \
203
5d724fe0e096 changes according to afp-submission
urbanc
parents: 162
diff changeset
    32
         Slides/document/root* \
5d724fe0e096 changes according to afp-submission
urbanc
parents: 162
diff changeset
    33
         Slides/Slides1.thy
5d724fe0e096 changes according to afp-submission
urbanc
parents: 162
diff changeset
    34
	@$(USEDIR) -D generated -f ROOT1.ML HOL Slides
5d724fe0e096 changes according to afp-submission
urbanc
parents: 162
diff changeset
    35
333
813e7257c7c3 some polishing of the repository
urbanc
parents: 258
diff changeset
    36
slides2: session2 
203
5d724fe0e096 changes according to afp-submission
urbanc
parents: 162
diff changeset
    37
	rm -f Slides/generated/*.aux # otherwise latex will fall over
5d724fe0e096 changes according to afp-submission
urbanc
parents: 162
diff changeset
    38
	cd Slides/generated ; $(ISABELLE_TOOL) latex -o pdf root.beamer.tex 
5d724fe0e096 changes according to afp-submission
urbanc
parents: 162
diff changeset
    39
	cp Slides/generated/root.beamer.pdf Slides/slides1.pdf   
5d724fe0e096 changes according to afp-submission
urbanc
parents: 162
diff changeset
    40
333
813e7257c7c3 some polishing of the repository
urbanc
parents: 258
diff changeset
    41
## Slides 3
258
1abf8586ee6b added slides for a talk in St Andrews
urbanc
parents: 203
diff changeset
    42
333
813e7257c7c3 some polishing of the repository
urbanc
parents: 258
diff changeset
    43
session3: Slides/ROOT.ML \
258
1abf8586ee6b added slides for a talk in St Andrews
urbanc
parents: 203
diff changeset
    44
         Slides/document/root* \
1abf8586ee6b added slides for a talk in St Andrews
urbanc
parents: 203
diff changeset
    45
         Slides/Slides2.thy
1abf8586ee6b added slides for a talk in St Andrews
urbanc
parents: 203
diff changeset
    46
	@$(USEDIR) -D generated -f ROOT2.ML HOL Slides
1abf8586ee6b added slides for a talk in St Andrews
urbanc
parents: 203
diff changeset
    47
333
813e7257c7c3 some polishing of the repository
urbanc
parents: 258
diff changeset
    48
slides3: session3 
258
1abf8586ee6b added slides for a talk in St Andrews
urbanc
parents: 203
diff changeset
    49
	rm -f Slides/generated/*.aux # otherwise latex will fall over
1abf8586ee6b added slides for a talk in St Andrews
urbanc
parents: 203
diff changeset
    50
	cd Slides/generated ; $(ISABELLE_TOOL) latex -o pdf root.beamer.tex 
1abf8586ee6b added slides for a talk in St Andrews
urbanc
parents: 203
diff changeset
    51
	cp Slides/generated/root.beamer.pdf Slides/slides2.pdf   
16
663816814e3e added initial slides for informal talk in Cambridge
urbanc
parents:
diff changeset
    52
663816814e3e added initial slides for informal talk in Cambridge
urbanc
parents:
diff changeset
    53
333
813e7257c7c3 some polishing of the repository
urbanc
parents: 258
diff changeset
    54
slides: slides1 slides2 slides3
72
e5116c2e6187 added an option fullpaper to IsaMakefile
urbanc
parents: 66
diff changeset
    55
16
663816814e3e added initial slides for informal talk in Cambridge
urbanc
parents:
diff changeset
    56
36
f5cc33a0ba99 added an itp entry to IsaMakefile; fixed problem with eqref; have not used heap file ListP
wu
parents: 31
diff changeset
    57
## ITP paper
f5cc33a0ba99 added an itp entry to IsaMakefile; fixed problem with eqref; have not used heap file ListP
wu
parents: 31
diff changeset
    58
333
813e7257c7c3 some polishing of the repository
urbanc
parents: 258
diff changeset
    59
session_itp: Paper/ROOT.ML \
36
f5cc33a0ba99 added an itp entry to IsaMakefile; fixed problem with eqref; have not used heap file ListP
wu
parents: 31
diff changeset
    60
	Paper/document/root* \
f5cc33a0ba99 added an itp entry to IsaMakefile; fixed problem with eqref; have not used heap file ListP
wu
parents: 31
diff changeset
    61
	Paper/*.thy
f5cc33a0ba99 added an itp entry to IsaMakefile; fixed problem with eqref; have not used heap file ListP
wu
parents: 31
diff changeset
    62
	@$(USEDIR) -D generated -f ROOT.ML HOL Paper
f5cc33a0ba99 added an itp entry to IsaMakefile; fixed problem with eqref; have not used heap file ListP
wu
parents: 31
diff changeset
    63
333
813e7257c7c3 some polishing of the repository
urbanc
parents: 258
diff changeset
    64
itp: session_itp
36
f5cc33a0ba99 added an itp entry to IsaMakefile; fixed problem with eqref; have not used heap file ListP
wu
parents: 31
diff changeset
    65
	rm -f Paper/generated/*.aux # otherwise latex will fall over      
f5cc33a0ba99 added an itp entry to IsaMakefile; fixed problem with eqref; have not used heap file ListP
wu
parents: 31
diff changeset
    66
	cd Paper/generated ; $(ISABELLE_TOOL) latex -o pdf root.tex 
66
828ea293b61f more on the introduction
urbanc
parents: 62
diff changeset
    67
	cd Paper/generated ; bibtex root
36
f5cc33a0ba99 added an itp entry to IsaMakefile; fixed problem with eqref; have not used heap file ListP
wu
parents: 31
diff changeset
    68
	cd Paper/generated ; $(ISABELLE_TOOL) latex -o pdf root.tex
f5cc33a0ba99 added an itp entry to IsaMakefile; fixed problem with eqref; have not used heap file ListP
wu
parents: 31
diff changeset
    69
	cp Paper/generated/root.pdf paper.pdf     
f5cc33a0ba99 added an itp entry to IsaMakefile; fixed problem with eqref; have not used heap file ListP
wu
parents: 31
diff changeset
    70
162
e93760534354 added directory for journal version; took uptodate version of the theory files
urbanc
parents: 72
diff changeset
    71
## Journal Version
e93760534354 added directory for journal version; took uptodate version of the theory files
urbanc
parents: 72
diff changeset
    72
333
813e7257c7c3 some polishing of the repository
urbanc
parents: 258
diff changeset
    73
session_journal: Journal/ROOT.ML \
162
e93760534354 added directory for journal version; took uptodate version of the theory files
urbanc
parents: 72
diff changeset
    74
	Journal/document/root* \
e93760534354 added directory for journal version; took uptodate version of the theory files
urbanc
parents: 72
diff changeset
    75
	Journal/*.thy
e93760534354 added directory for journal version; took uptodate version of the theory files
urbanc
parents: 72
diff changeset
    76
	@$(USEDIR) -D generated -f ROOT.ML HOL Journal
e93760534354 added directory for journal version; took uptodate version of the theory files
urbanc
parents: 72
diff changeset
    77
333
813e7257c7c3 some polishing of the repository
urbanc
parents: 258
diff changeset
    78
journal: session_journal
162
e93760534354 added directory for journal version; took uptodate version of the theory files
urbanc
parents: 72
diff changeset
    79
	rm -f Journal/generated/*.aux # otherwise latex will fall over       
e93760534354 added directory for journal version; took uptodate version of the theory files
urbanc
parents: 72
diff changeset
    80
	cd Journal/generated ; $(ISABELLE_TOOL) latex -o pdf root.tex 
e93760534354 added directory for journal version; took uptodate version of the theory files
urbanc
parents: 72
diff changeset
    81
	cd Journal/generated ; bibtex root
e93760534354 added directory for journal version; took uptodate version of the theory files
urbanc
parents: 72
diff changeset
    82
	cd Journal/generated ; $(ISABELLE_TOOL) latex -o pdf root.tex
e93760534354 added directory for journal version; took uptodate version of the theory files
urbanc
parents: 72
diff changeset
    83
	cp Journal/generated/root.pdf journal.pdf     
e93760534354 added directory for journal version; took uptodate version of the theory files
urbanc
parents: 72
diff changeset
    84
36
f5cc33a0ba99 added an itp entry to IsaMakefile; fixed problem with eqref; have not used heap file ListP
wu
parents: 31
diff changeset
    85
16
663816814e3e added initial slides for informal talk in Cambridge
urbanc
parents:
diff changeset
    86
## clean
663816814e3e added initial slides for informal talk in Cambridge
urbanc
parents:
diff changeset
    87
663816814e3e added initial slides for informal talk in Cambridge
urbanc
parents:
diff changeset
    88
clean:
333
813e7257c7c3 some polishing of the repository
urbanc
parents: 258
diff changeset
    89
	rm -rf Slides/generated*
813e7257c7c3 some polishing of the repository
urbanc
parents: 258
diff changeset
    90
	rm -rf Paper/generated*
813e7257c7c3 some polishing of the repository
urbanc
parents: 258
diff changeset
    91
	rm -rf Journal/generated*