| author | Cezary Kaliszyk <kaliszyk@in.tum.de> |
| Thu, 06 May 2010 14:14:30 +0200 | |
| changeset 2076 | 6cb1a4639521 |
| parent 1975 | b1281a0051ae |
| child 2299 | 09bbed4f21d6 |
| permissions | -rw-r--r-- |
|
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 | 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 | 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 | 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 |
|
|
b1281a0051ae
added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
1785
diff
changeset
|
63 |
|
|
1261
853abc14c5c6
added IsaMakefile...but so far included only a test for the parser
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
64 |
## clean |
|
853abc14c5c6
added IsaMakefile...but so far included only a test for the parser
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
65 |
|
|
853abc14c5c6
added IsaMakefile...but so far included only a test for the parser
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
66 |
clean: |
|
1772
48c2eb84d5ce
merged pearl paper with this repository; started litrature subdirectory
Christian Urban <urbanc@in.tum.de>
parents:
1491
diff
changeset
|
67 |
@rm -f $(LOG)/HOL-Nominal2.gz $(LOG)/HOL-Pearl.gz |