12 |
12 |
13 |
13 |
14 USEDIR = $(ISABELLE_TOOL) usedir -v true -t true |
14 USEDIR = $(ISABELLE_TOOL) usedir -v true -t true |
15 |
15 |
16 |
16 |
17 ## Slides |
17 ## Slides 1 |
18 |
18 |
19 session1: Slides/ROOT.ML \ |
19 session1: Slides/ROOT.ML \ |
20 Slides/document/root* \ |
20 Slides/document/root* \ |
21 Slides/Slides.thy |
21 Slides/Slides.thy |
22 @$(USEDIR) -D generated -f ROOT.ML HOL Slides |
22 @$(USEDIR) -D generated -f ROOT.ML HOL Slides |
23 |
23 |
24 slides: session1 |
24 slides1: session1 |
25 rm -f Slides/generated/*.aux # otherwise latex will fall over |
25 rm -f Slides/generated/*.aux # otherwise latex will fall over |
26 cd Slides/generated ; $(ISABELLE_TOOL) latex -o pdf root.beamer.tex |
26 cd Slides/generated ; $(ISABELLE_TOOL) latex -o pdf root.beamer.tex |
27 cp Slides/generated/root.beamer.pdf Slides/slides.pdf |
27 cp Slides/generated/root.beamer.pdf Slides/slides.pdf |
28 |
28 |
29 ## Slides 1 |
29 ## Slides 2 |
30 |
30 |
31 session11: Slides/ROOT.ML \ |
31 session2: Slides/ROOT.ML \ |
32 Slides/document/root* \ |
32 Slides/document/root* \ |
33 Slides/Slides1.thy |
33 Slides/Slides1.thy |
34 @$(USEDIR) -D generated -f ROOT1.ML HOL Slides |
34 @$(USEDIR) -D generated -f ROOT1.ML HOL Slides |
35 |
35 |
36 slides1: session11 |
36 slides2: session2 |
37 rm -f Slides/generated/*.aux # otherwise latex will fall over |
37 rm -f Slides/generated/*.aux # otherwise latex will fall over |
38 cd Slides/generated ; $(ISABELLE_TOOL) latex -o pdf root.beamer.tex |
38 cd Slides/generated ; $(ISABELLE_TOOL) latex -o pdf root.beamer.tex |
39 cp Slides/generated/root.beamer.pdf Slides/slides1.pdf |
39 cp Slides/generated/root.beamer.pdf Slides/slides1.pdf |
40 |
40 |
41 ## Slides 2 |
41 ## Slides 3 |
42 |
42 |
43 session22: Slides/ROOT.ML \ |
43 session3: Slides/ROOT.ML \ |
44 Slides/document/root* \ |
44 Slides/document/root* \ |
45 Slides/Slides2.thy |
45 Slides/Slides2.thy |
46 @$(USEDIR) -D generated -f ROOT2.ML HOL Slides |
46 @$(USEDIR) -D generated -f ROOT2.ML HOL Slides |
47 |
47 |
48 slides2: session22 |
48 slides3: session3 |
49 rm -f Slides/generated/*.aux # otherwise latex will fall over |
49 rm -f Slides/generated/*.aux # otherwise latex will fall over |
50 cd Slides/generated ; $(ISABELLE_TOOL) latex -o pdf root.beamer.tex |
50 cd Slides/generated ; $(ISABELLE_TOOL) latex -o pdf root.beamer.tex |
51 cp Slides/generated/root.beamer.pdf Slides/slides2.pdf |
51 cp Slides/generated/root.beamer.pdf Slides/slides2.pdf |
52 |
52 |
53 ## long paper |
|
54 |
53 |
55 session2: tphols-2011/ROOT.ML \ |
54 slides: slides1 slides2 slides3 |
56 tphols-2011/document/root* \ |
|
57 *.thy |
|
58 @$(USEDIR) -D generated -f ROOT.ML ListP tphols-2011 |
|
59 |
|
60 paper: session2 |
|
61 rm -f tphols-2011/generated/*.aux # otherwise latex will fall over |
|
62 cd tphols-2011/generated ; $(ISABELLE_TOOL) latex -o pdf root.tex |
|
63 cd tphols-2011/generated ; $(ISABELLE_TOOL) latex -o pdf root.tex |
|
64 cp tphols-2011/generated/root.pdf tphols-2011/myhill.pdf |
|
65 |
|
66 ## full paper |
|
67 |
|
68 fullsession2: tphols-2011/ROOT.ML \ |
|
69 tphols-2011/document/root* \ |
|
70 *.thy |
|
71 @$(USEDIR) -D generated -f ROOT.ML HOL tphols-2011 |
|
72 |
|
73 fullpaper: fullsession2 |
|
74 rm -f tphols-2011/generated/*.aux # otherwise latex will fall over |
|
75 cd tphols-2011/generated ; $(ISABELLE_TOOL) latex -o pdf root.tex |
|
76 cd tphols-2011/generated ; $(ISABELLE_TOOL) latex -o pdf root.tex |
|
77 cp tphols-2011/generated/root.pdf tphols-2011/myhill.pdf |
|
78 |
|
79 |
55 |
80 |
56 |
81 ## ITP paper |
57 ## ITP paper |
82 |
58 |
83 session3: Paper/ROOT.ML \ |
59 session_itp: Paper/ROOT.ML \ |
84 Paper/document/root* \ |
60 Paper/document/root* \ |
85 Paper/*.thy |
61 Paper/*.thy |
86 @$(USEDIR) -D generated -f ROOT.ML HOL Paper |
62 @$(USEDIR) -D generated -f ROOT.ML HOL Paper |
87 |
63 |
88 itp: session3 |
64 itp: session_itp |
89 rm -f Paper/generated/*.aux # otherwise latex will fall over |
65 rm -f Paper/generated/*.aux # otherwise latex will fall over |
90 cd Paper/generated ; $(ISABELLE_TOOL) latex -o pdf root.tex |
66 cd Paper/generated ; $(ISABELLE_TOOL) latex -o pdf root.tex |
91 cd Paper/generated ; bibtex root |
67 cd Paper/generated ; bibtex root |
92 cd Paper/generated ; $(ISABELLE_TOOL) latex -o pdf root.tex |
68 cd Paper/generated ; $(ISABELLE_TOOL) latex -o pdf root.tex |
93 cp Paper/generated/root.pdf paper.pdf |
69 cp Paper/generated/root.pdf paper.pdf |
94 |
70 |
95 ## Journal Version |
71 ## Journal Version |
96 |
72 |
97 session4: Journal/ROOT.ML \ |
73 session_journal: Journal/ROOT.ML \ |
98 Journal/document/root* \ |
74 Journal/document/root* \ |
99 Journal/*.thy |
75 Journal/*.thy |
100 @$(USEDIR) -D generated -f ROOT.ML HOL Journal |
76 @$(USEDIR) -D generated -f ROOT.ML HOL Journal |
101 |
77 |
102 journal: session4 |
78 journal: session_journal |
103 rm -f Journal/generated/*.aux # otherwise latex will fall over |
79 rm -f Journal/generated/*.aux # otherwise latex will fall over |
104 cd Journal/generated ; $(ISABELLE_TOOL) latex -o pdf root.tex |
80 cd Journal/generated ; $(ISABELLE_TOOL) latex -o pdf root.tex |
105 cd Journal/generated ; bibtex root |
81 cd Journal/generated ; bibtex root |
106 cd Journal/generated ; $(ISABELLE_TOOL) latex -o pdf root.tex |
82 cd Journal/generated ; $(ISABELLE_TOOL) latex -o pdf root.tex |
107 cp Journal/generated/root.pdf journal.pdf |
83 cp Journal/generated/root.pdf journal.pdf |
108 |
84 |
109 |
85 |
110 ## clean |
86 ## clean |
111 |
87 |
112 clean: |
88 clean: |
113 rm -rf Slides/generated/* |
89 rm -rf Slides/generated* |
114 rm -rf tphols-2011/generated/* |
90 rm -rf Paper/generated* |
|
91 rm -rf Journal/generated* |