IsaMakefile
author Christian Urban <urbanc@in.tum.de>
Sun, 22 Aug 2010 14:02:49 +0800
changeset 2430 a746d49b0240
parent 2351 842969a598f2
child 2440 0a36825b16c1
permissions -rw-r--r--
updated to new Isabelle
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
1261
853abc14c5c6 added IsaMakefile...but so far included only a test for the parser
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     1
853abc14c5c6 added IsaMakefile...but so far included only a test for the parser
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     2
## targets
853abc14c5c6 added IsaMakefile...but so far included only a test for the parser
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     3
853abc14c5c6 added IsaMakefile...but so far included only a test for the parser
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     4
default: Nominal2
853abc14c5c6 added IsaMakefile...but so far included only a test for the parser
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     5
images: 
853abc14c5c6 added IsaMakefile...but so far included only a test for the parser
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     6
1975
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents: 1785
diff changeset
     7
all: Nominal2 paper pearl pearl-jv qpaper
1261
853abc14c5c6 added IsaMakefile...but so far included only a test for the parser
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     8
853abc14c5c6 added IsaMakefile...but so far included only a test for the parser
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     9
853abc14c5c6 added IsaMakefile...but so far included only a test for the parser
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    10
## global settings
853abc14c5c6 added IsaMakefile...but so far included only a test for the parser
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    11
853abc14c5c6 added IsaMakefile...but so far included only a test for the parser
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    12
SRC = $(ISABELLE_HOME)/src
853abc14c5c6 added IsaMakefile...but so far included only a test for the parser
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    13
OUT = $(ISABELLE_OUTPUT)
853abc14c5c6 added IsaMakefile...but so far included only a test for the parser
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    14
LOG = $(OUT)/log
853abc14c5c6 added IsaMakefile...but so far included only a test for the parser
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    15
853abc14c5c6 added IsaMakefile...but so far included only a test for the parser
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    16
USEDIR = $(ISABELLE_TOOL) usedir -v true -t true ##-D generated
853abc14c5c6 added IsaMakefile...but so far included only a test for the parser
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    17
853abc14c5c6 added IsaMakefile...but so far included only a test for the parser
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    18
853abc14c5c6 added IsaMakefile...but so far included only a test for the parser
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    19
## Nominal2
853abc14c5c6 added IsaMakefile...but so far included only a test for the parser
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    20
853abc14c5c6 added IsaMakefile...but so far included only a test for the parser
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    21
Nominal2: $(LOG)/HOL-Nominal2.gz
853abc14c5c6 added IsaMakefile...but so far included only a test for the parser
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    22
853abc14c5c6 added IsaMakefile...but so far included only a test for the parser
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    23
$(LOG)/HOL-Nominal2.gz: Nominal/ROOT.ML Nominal/*.thy
1491
f970ca9b5bec paper uses now a heap file - does not compile so long anymore
Christian Urban <urbanc@in.tum.de>
parents: 1484
diff changeset
    24
	@cd Nominal; $(USEDIR) -b -d "" HOL Nominal
1261
853abc14c5c6 added IsaMakefile...but so far included only a test for the parser
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    25
1772
48c2eb84d5ce merged pearl paper with this repository; started litrature subdirectory
Christian Urban <urbanc@in.tum.de>
parents: 1491
diff changeset
    26
## Nominal2 Paper
48c2eb84d5ce merged pearl paper with this repository; started litrature subdirectory
Christian Urban <urbanc@in.tum.de>
parents: 1491
diff changeset
    27
1261
853abc14c5c6 added IsaMakefile...but so far included only a test for the parser
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    28
paper: $(LOG)/HOL-Nominal2-Paper.gz
853abc14c5c6 added IsaMakefile...but so far included only a test for the parser
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    29
1775
86122d793f32 typos in paper
Christian Urban <urbanc@in.tum.de>
parents: 1774
diff changeset
    30
$(LOG)/HOL-Nominal2-Paper.gz: Paper/ROOT.ML Paper/document/root.* Paper/*.thy
1491
f970ca9b5bec paper uses now a heap file - does not compile so long anymore
Christian Urban <urbanc@in.tum.de>
parents: 1484
diff changeset
    31
	@$(USEDIR) -D generated Nominal Paper
1484
dc7b049d9072 made paper to compile
Christian Urban <urbanc@in.tum.de>
parents: 1261
diff changeset
    32
	$(ISABELLE_TOOL) document -o pdf  Paper/generated
1261
853abc14c5c6 added IsaMakefile...but so far included only a test for the parser
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    33
	@cp Paper/document.pdf paper.pdf
853abc14c5c6 added IsaMakefile...but so far included only a test for the parser
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    34
1785
95df71c3df2f added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents: 1775
diff changeset
    35
## Pearl Paper ITP
1772
48c2eb84d5ce merged pearl paper with this repository; started litrature subdirectory
Christian Urban <urbanc@in.tum.de>
parents: 1491
diff changeset
    36
48c2eb84d5ce merged pearl paper with this repository; started litrature subdirectory
Christian Urban <urbanc@in.tum.de>
parents: 1491
diff changeset
    37
pearl: $(LOG)/HOL-Pearl.gz
48c2eb84d5ce merged pearl paper with this repository; started litrature subdirectory
Christian Urban <urbanc@in.tum.de>
parents: 1491
diff changeset
    38
1775
86122d793f32 typos in paper
Christian Urban <urbanc@in.tum.de>
parents: 1774
diff changeset
    39
$(LOG)/HOL-Pearl.gz: Pearl/ROOT.ML Pearl/document/root.* Pearl/*.thy
1772
48c2eb84d5ce merged pearl paper with this repository; started litrature subdirectory
Christian Urban <urbanc@in.tum.de>
parents: 1491
diff changeset
    40
	@$(USEDIR) -D generated HOL Pearl
48c2eb84d5ce merged pearl paper with this repository; started litrature subdirectory
Christian Urban <urbanc@in.tum.de>
parents: 1491
diff changeset
    41
	$(ISABELLE_TOOL) document -o pdf Pearl/generated
48c2eb84d5ce merged pearl paper with this repository; started litrature subdirectory
Christian Urban <urbanc@in.tum.de>
parents: 1491
diff changeset
    42
	@cp Pearl/document.pdf pearl.pdf
48c2eb84d5ce merged pearl paper with this repository; started litrature subdirectory
Christian Urban <urbanc@in.tum.de>
parents: 1491
diff changeset
    43
1785
95df71c3df2f added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents: 1775
diff changeset
    44
## Pearl Journal Paper 
95df71c3df2f added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents: 1775
diff changeset
    45
95df71c3df2f added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents: 1775
diff changeset
    46
pearl-jv: $(LOG)/HOL-Pearl-jv.gz
95df71c3df2f added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents: 1775
diff changeset
    47
95df71c3df2f added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents: 1775
diff changeset
    48
$(LOG)/HOL-Pearl-jv.gz: Pearl-jv/ROOT.ML Pearl-jv/document/root.* Pearl-jv/*.thy
95df71c3df2f added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents: 1775
diff changeset
    49
	@$(USEDIR) -D generated HOL Pearl-jv
95df71c3df2f added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents: 1775
diff changeset
    50
	$(ISABELLE_TOOL) document -o pdf Pearl-jv/generated
95df71c3df2f added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents: 1775
diff changeset
    51
	@cp Pearl-jv/document.pdf pearl-jv.pdf
95df71c3df2f added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents: 1775
diff changeset
    52
1772
48c2eb84d5ce merged pearl paper with this repository; started litrature subdirectory
Christian Urban <urbanc@in.tum.de>
parents: 1491
diff changeset
    53
1975
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents: 1785
diff changeset
    54
## Quotient Paper 
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents: 1785
diff changeset
    55
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents: 1785
diff changeset
    56
qpaper: $(LOG)/HOL-QPaper.gz
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents: 1785
diff changeset
    57
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents: 1785
diff changeset
    58
$(LOG)/HOL-QPaper.gz: Quotient-Paper/ROOT.ML Quotient-Paper/document/root.* Quotient-Paper/*.thy
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents: 1785
diff changeset
    59
	@$(USEDIR) -D generated HOL Quotient-Paper
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents: 1785
diff changeset
    60
	$(ISABELLE_TOOL) document -o pdf Quotient-Paper/generated
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents: 1785
diff changeset
    61
	@cp Quotient-Paper/document.pdf qpaper.pdf
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents: 1785
diff changeset
    62
2299
09bbed4f21d6 added slides
Christian Urban <urbanc@in.tum.de>
parents: 1975
diff changeset
    63
## Slides
09bbed4f21d6 added slides
Christian Urban <urbanc@in.tum.de>
parents: 1975
diff changeset
    64
2351
842969a598f2 added material for slides
Christian Urban <urbanc@in.tum.de>
parents: 2299
diff changeset
    65
session1: Slides/ROOT1.ML \
2299
09bbed4f21d6 added slides
Christian Urban <urbanc@in.tum.de>
parents: 1975
diff changeset
    66
         Slides/document/root* \
09bbed4f21d6 added slides
Christian Urban <urbanc@in.tum.de>
parents: 1975
diff changeset
    67
         Slides/Slides1.thy
2351
842969a598f2 added material for slides
Christian Urban <urbanc@in.tum.de>
parents: 2299
diff changeset
    68
	@$(USEDIR) -D generated1 -f ROOT1.ML HOL-Nominal Slides
2299
09bbed4f21d6 added slides
Christian Urban <urbanc@in.tum.de>
parents: 1975
diff changeset
    69
09bbed4f21d6 added slides
Christian Urban <urbanc@in.tum.de>
parents: 1975
diff changeset
    70
slides1: session1
09bbed4f21d6 added slides
Christian Urban <urbanc@in.tum.de>
parents: 1975
diff changeset
    71
	rm -f Slides/generated1/*.aux # otherwise latex will fall over
09bbed4f21d6 added slides
Christian Urban <urbanc@in.tum.de>
parents: 1975
diff changeset
    72
	cd Slides/generated1 ; $(ISABELLE_TOOL) latex -o pdf root.beamer.tex
09bbed4f21d6 added slides
Christian Urban <urbanc@in.tum.de>
parents: 1975
diff changeset
    73
	cd Slides/generated1 ; $(ISABELLE_TOOL) latex -o pdf root.beamer.tex
2351
842969a598f2 added material for slides
Christian Urban <urbanc@in.tum.de>
parents: 2299
diff changeset
    74
	cp Slides/generated1/root.beamer.pdf Slides/slides1.pdf     
842969a598f2 added material for slides
Christian Urban <urbanc@in.tum.de>
parents: 2299
diff changeset
    75
842969a598f2 added material for slides
Christian Urban <urbanc@in.tum.de>
parents: 2299
diff changeset
    76
session2: Slides/ROOT2.ML \
842969a598f2 added material for slides
Christian Urban <urbanc@in.tum.de>
parents: 2299
diff changeset
    77
         Slides/document/root* \
842969a598f2 added material for slides
Christian Urban <urbanc@in.tum.de>
parents: 2299
diff changeset
    78
         Slides/Slides2.thy
842969a598f2 added material for slides
Christian Urban <urbanc@in.tum.de>
parents: 2299
diff changeset
    79
	@$(USEDIR) -D generated2 -f ROOT2.ML HOL-Nominal Slides
842969a598f2 added material for slides
Christian Urban <urbanc@in.tum.de>
parents: 2299
diff changeset
    80
842969a598f2 added material for slides
Christian Urban <urbanc@in.tum.de>
parents: 2299
diff changeset
    81
slides2: session2
842969a598f2 added material for slides
Christian Urban <urbanc@in.tum.de>
parents: 2299
diff changeset
    82
	rm -f Slides/generated2/*.aux # otherwise latex will fall over
842969a598f2 added material for slides
Christian Urban <urbanc@in.tum.de>
parents: 2299
diff changeset
    83
	cd Slides/generated2 ; $(ISABELLE_TOOL) latex -o pdf root.beamer.tex
842969a598f2 added material for slides
Christian Urban <urbanc@in.tum.de>
parents: 2299
diff changeset
    84
	cd Slides/generated2 ; $(ISABELLE_TOOL) latex -o pdf root.beamer.tex
842969a598f2 added material for slides
Christian Urban <urbanc@in.tum.de>
parents: 2299
diff changeset
    85
	cp Slides/generated2/root.beamer.pdf Slides/slides2.pdf 
842969a598f2 added material for slides
Christian Urban <urbanc@in.tum.de>
parents: 2299
diff changeset
    86
842969a598f2 added material for slides
Christian Urban <urbanc@in.tum.de>
parents: 2299
diff changeset
    87
session3: Slides/ROOT3.ML \
842969a598f2 added material for slides
Christian Urban <urbanc@in.tum.de>
parents: 2299
diff changeset
    88
         Slides/document/root* \
842969a598f2 added material for slides
Christian Urban <urbanc@in.tum.de>
parents: 2299
diff changeset
    89
         Slides/Slides3.thy
842969a598f2 added material for slides
Christian Urban <urbanc@in.tum.de>
parents: 2299
diff changeset
    90
	@$(USEDIR) -D generated3 -f ROOT3.ML HOL-Nominal Slides
842969a598f2 added material for slides
Christian Urban <urbanc@in.tum.de>
parents: 2299
diff changeset
    91
842969a598f2 added material for slides
Christian Urban <urbanc@in.tum.de>
parents: 2299
diff changeset
    92
slides3: session3
842969a598f2 added material for slides
Christian Urban <urbanc@in.tum.de>
parents: 2299
diff changeset
    93
	rm -f Slides/generated3/*.aux # otherwise latex will fall over
842969a598f2 added material for slides
Christian Urban <urbanc@in.tum.de>
parents: 2299
diff changeset
    94
	cd Slides/generated3 ; $(ISABELLE_TOOL) latex -o pdf root.beamer.tex
842969a598f2 added material for slides
Christian Urban <urbanc@in.tum.de>
parents: 2299
diff changeset
    95
	cd Slides/generated3 ; $(ISABELLE_TOOL) latex -o pdf root.beamer.tex
842969a598f2 added material for slides
Christian Urban <urbanc@in.tum.de>
parents: 2299
diff changeset
    96
	cp Slides/generated3/root.beamer.pdf Slides/slides3.pdf 
2299
09bbed4f21d6 added slides
Christian Urban <urbanc@in.tum.de>
parents: 1975
diff changeset
    97
09bbed4f21d6 added slides
Christian Urban <urbanc@in.tum.de>
parents: 1975
diff changeset
    98
slides: slides1
09bbed4f21d6 added slides
Christian Urban <urbanc@in.tum.de>
parents: 1975
diff changeset
    99
09bbed4f21d6 added slides
Christian Urban <urbanc@in.tum.de>
parents: 1975
diff changeset
   100
09bbed4f21d6 added slides
Christian Urban <urbanc@in.tum.de>
parents: 1975
diff changeset
   101
1975
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents: 1785
diff changeset
   102
1261
853abc14c5c6 added IsaMakefile...but so far included only a test for the parser
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   103
## clean
853abc14c5c6 added IsaMakefile...but so far included only a test for the parser
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   104
853abc14c5c6 added IsaMakefile...but so far included only a test for the parser
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   105
clean:
1772
48c2eb84d5ce merged pearl paper with this repository; started litrature subdirectory
Christian Urban <urbanc@in.tum.de>
parents: 1491
diff changeset
   106
	@rm -f $(LOG)/HOL-Nominal2.gz $(LOG)/HOL-Pearl.gz