equal
deleted
inserted
replaced
2 ## targets |
2 ## targets |
3 |
3 |
4 default: tests |
4 default: tests |
5 images: |
5 images: |
6 |
6 |
7 all: tests paper pearl pearl-jv qpaper slides |
7 all: tests esop pearl pearl-jv qpaper slides |
8 |
8 |
9 |
9 |
10 ## global settings |
10 ## global settings |
11 |
11 |
12 SRC = $(ISABELLE_HOME)/src |
12 SRC = $(ISABELLE_HOME)/src |
21 tests: $(LOG)/HOL-Nominal2.gz |
21 tests: $(LOG)/HOL-Nominal2.gz |
22 |
22 |
23 $(LOG)/HOL-Nominal2.gz: Nominal/ROOT.ML Nominal/*.thy |
23 $(LOG)/HOL-Nominal2.gz: Nominal/ROOT.ML Nominal/*.thy |
24 @cd Nominal; $(USEDIR) -b -d "" HOL Nominal |
24 @cd Nominal; $(USEDIR) -b -d "" HOL Nominal |
25 |
25 |
26 ## Nominal2 Paper |
26 ## ESOP Paper |
27 |
27 |
28 paper: $(LOG)/HOL-Nominal2-Paper.gz |
28 esop: $(LOG)/HOL-ESOP-Paper.gz |
29 |
29 |
30 $(LOG)/HOL-Nominal2-Paper.gz: Paper/ROOT.ML Paper/document/root.* Paper/*.thy |
30 $(LOG)/HOL-ESOP-Paper.gz: ESOP-Paper/ROOT.ML ESOP-Paper/document/root.* ESOP-Paper/*.thy |
31 @$(USEDIR) -f ROOTa.ML -D generated HOL Paper |
31 @$(USEDIR) -f ROOT.ML -D generated HOL-Nominal2 ESOP-Paper |
32 @$(USEDIR) -D generated HOL Paper |
32 $(ISABELLE_TOOL) document -o pdf ESOP-Paper/generated |
33 $(ISABELLE_TOOL) document -o pdf Paper/generated |
33 @cp ESOP-Paper/document.pdf esop-paper.pdf |
34 @cp Paper/document.pdf paper.pdf |
|
35 |
34 |
36 ## Pearl Paper ITP |
35 ## Pearl Paper ITP |
37 |
36 |
38 pearl: $(LOG)/HOL-Pearl.gz |
37 pearl: $(LOG)/HOL-Pearl.gz |
39 |
38 |
105 rm -f Slides/generated4/*.aux # otherwise latex will fall over |
104 rm -f Slides/generated4/*.aux # otherwise latex will fall over |
106 cd Slides/generated4 ; $(ISABELLE_TOOL) latex -o pdf root.beamer.tex |
105 cd Slides/generated4 ; $(ISABELLE_TOOL) latex -o pdf root.beamer.tex |
107 cd Slides/generated4 ; $(ISABELLE_TOOL) latex -o pdf root.beamer.tex |
106 cd Slides/generated4 ; $(ISABELLE_TOOL) latex -o pdf root.beamer.tex |
108 cp Slides/generated4/root.beamer.pdf Slides/slides4.pdf |
107 cp Slides/generated4/root.beamer.pdf Slides/slides4.pdf |
109 |
108 |
110 slides: slides1 slides2 slides3 slides4 |
109 session5: Slides/ROOT5.ML \ |
|
110 Slides/document/root* \ |
|
111 Slides/Slides5.thy |
|
112 @$(USEDIR) -D generated5 -f ROOT5.ML HOL-Nominal Slides |
|
113 |
|
114 slides5: session5 |
|
115 rm -f Slides/generated5/*.aux # otherwise latex will fall over |
|
116 cd Slides/generated5 ; $(ISABELLE_TOOL) latex -o pdf root.beamer.tex |
|
117 cd Slides/generated5 ; $(ISABELLE_TOOL) latex -o pdf root.beamer.tex |
|
118 cp Slides/generated5/root.beamer.pdf Slides/slides5.pdf |
|
119 |
|
120 slides: slides1 slides2 slides3 slides4 slides5 |
111 |
121 |
112 |
122 |
113 |
123 |
114 |
124 |
115 ## clean |
125 ## clean |