IsaMakefile
author urbanc
Thu, 03 May 2012 08:52:03 +0000
changeset 354 677364c67cc8
parent 334 d47c2143ab8a
child 367 79401279ba21
permissions -rw-r--r--
some small editing
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
334
d47c2143ab8a partially updated conference paper; slightly tuned journal paper
urbanc
parents: 333
diff changeset
     4
default: slides4
d47c2143ab8a partially updated conference paper; slightly tuned journal paper
urbanc
parents: 333
diff changeset
     5
all: slides itp
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
334
d47c2143ab8a partially updated conference paper; slightly tuned journal paper
urbanc
parents: 333
diff changeset
    53
## Slides 4
16
663816814e3e added initial slides for informal talk in Cambridge
urbanc
parents:
diff changeset
    54
334
d47c2143ab8a partially updated conference paper; slightly tuned journal paper
urbanc
parents: 333
diff changeset
    55
session4: Slides/ROOT.ML \
d47c2143ab8a partially updated conference paper; slightly tuned journal paper
urbanc
parents: 333
diff changeset
    56
         Slides/document/root* \
d47c2143ab8a partially updated conference paper; slightly tuned journal paper
urbanc
parents: 333
diff changeset
    57
         Slides/Slides2.thy
d47c2143ab8a partially updated conference paper; slightly tuned journal paper
urbanc
parents: 333
diff changeset
    58
	@$(USEDIR) -D generated -f ROOT4.ML HOL Slides
d47c2143ab8a partially updated conference paper; slightly tuned journal paper
urbanc
parents: 333
diff changeset
    59
d47c2143ab8a partially updated conference paper; slightly tuned journal paper
urbanc
parents: 333
diff changeset
    60
slides4: session4 
d47c2143ab8a partially updated conference paper; slightly tuned journal paper
urbanc
parents: 333
diff changeset
    61
	rm -f Slides/generated/*.aux # otherwise latex will fall over
d47c2143ab8a partially updated conference paper; slightly tuned journal paper
urbanc
parents: 333
diff changeset
    62
	cd Slides/generated ; $(ISABELLE_TOOL) latex -o pdf root.beamer.tex 
d47c2143ab8a partially updated conference paper; slightly tuned journal paper
urbanc
parents: 333
diff changeset
    63
	cp Slides/generated/root.beamer.pdf Slides/slides4.pdf  
72
e5116c2e6187 added an option fullpaper to IsaMakefile
urbanc
parents: 66
diff changeset
    64
16
663816814e3e added initial slides for informal talk in Cambridge
urbanc
parents:
diff changeset
    65
334
d47c2143ab8a partially updated conference paper; slightly tuned journal paper
urbanc
parents: 333
diff changeset
    66
slides: slides1 slides2 slides3 slides4
d47c2143ab8a partially updated conference paper; slightly tuned journal paper
urbanc
parents: 333
diff changeset
    67
d47c2143ab8a partially updated conference paper; slightly tuned journal paper
urbanc
parents: 333
diff changeset
    68
d47c2143ab8a partially updated conference paper; slightly tuned journal paper
urbanc
parents: 333
diff changeset
    69
## ITP itp
36
f5cc33a0ba99 added an itp entry to IsaMakefile; fixed problem with eqref; have not used heap file ListP
wu
parents: 31
diff changeset
    70
333
813e7257c7c3 some polishing of the repository
urbanc
parents: 258
diff changeset
    71
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
    72
	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
    73
	Paper/*.thy
f5cc33a0ba99 added an itp entry to IsaMakefile; fixed problem with eqref; have not used heap file ListP
wu
parents: 31
diff changeset
    74
	@$(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
    75
333
813e7257c7c3 some polishing of the repository
urbanc
parents: 258
diff changeset
    76
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
    77
	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
    78
	cd Paper/generated ; $(ISABELLE_TOOL) latex -o pdf root.tex 
66
828ea293b61f more on the introduction
urbanc
parents: 62
diff changeset
    79
	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
    80
	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
    81
	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
    82
162
e93760534354 added directory for journal version; took uptodate version of the theory files
urbanc
parents: 72
diff changeset
    83
## Journal Version
e93760534354 added directory for journal version; took uptodate version of the theory files
urbanc
parents: 72
diff changeset
    84
333
813e7257c7c3 some polishing of the repository
urbanc
parents: 258
diff changeset
    85
session_journal: Journal/ROOT.ML \
162
e93760534354 added directory for journal version; took uptodate version of the theory files
urbanc
parents: 72
diff changeset
    86
	Journal/document/root* \
e93760534354 added directory for journal version; took uptodate version of the theory files
urbanc
parents: 72
diff changeset
    87
	Journal/*.thy
e93760534354 added directory for journal version; took uptodate version of the theory files
urbanc
parents: 72
diff changeset
    88
	@$(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
    89
333
813e7257c7c3 some polishing of the repository
urbanc
parents: 258
diff changeset
    90
journal: session_journal
162
e93760534354 added directory for journal version; took uptodate version of the theory files
urbanc
parents: 72
diff changeset
    91
	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
    92
	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
    93
	cd Journal/generated ; bibtex root
e93760534354 added directory for journal version; took uptodate version of the theory files
urbanc
parents: 72
diff changeset
    94
	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
    95
	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
    96
36
f5cc33a0ba99 added an itp entry to IsaMakefile; fixed problem with eqref; have not used heap file ListP
wu
parents: 31
diff changeset
    97
16
663816814e3e added initial slides for informal talk in Cambridge
urbanc
parents:
diff changeset
    98
## clean
663816814e3e added initial slides for informal talk in Cambridge
urbanc
parents:
diff changeset
    99
663816814e3e added initial slides for informal talk in Cambridge
urbanc
parents:
diff changeset
   100
clean:
333
813e7257c7c3 some polishing of the repository
urbanc
parents: 258
diff changeset
   101
	rm -rf Slides/generated*
813e7257c7c3 some polishing of the repository
urbanc
parents: 258
diff changeset
   102
	rm -rf Paper/generated*
813e7257c7c3 some polishing of the repository
urbanc
parents: 258
diff changeset
   103
	rm -rf Journal/generated*