|
8743
|
1 |
#
|
|
|
2 |
# IsaMakefile for Tutorial
|
|
|
3 |
#
|
|
|
4 |
|
|
|
5 |
## targets
|
|
|
6 |
|
|
|
7 |
default: styles HOL-ToyList HOL-Ifexpr HOL-CodeGen HOL-Trie HOL-Datatype HOL-Recdef HOL-Misc
|
|
|
8 |
|
|
|
9 |
|
|
|
10 |
## global settings
|
|
|
11 |
|
|
|
12 |
SRC = $(ISABELLE_HOME)/src
|
|
|
13 |
OUT = $(ISABELLE_OUTPUT)
|
|
|
14 |
LOG = $(OUT)/log
|
|
|
15 |
|
|
|
16 |
|
|
|
17 |
## HOL
|
|
|
18 |
|
|
|
19 |
HOL:
|
|
|
20 |
@cd $(SRC)/HOL; $(ISATOOL) make HOL
|
|
|
21 |
|
|
|
22 |
styles: isabelle.sty isabellesym.sty pdfsetup.sty
|
|
|
23 |
|
|
|
24 |
isabelle.sty: $(ISABELLE_HOME)/lib/texinputs/isabelle.sty
|
|
|
25 |
cp $(ISABELLE_HOME)/lib/texinputs/isabelle.sty .
|
|
|
26 |
|
|
|
27 |
isabellesym.sty: $(ISABELLE_HOME)/lib/texinputs/isabellesym.sty
|
|
|
28 |
cp $(ISABELLE_HOME)/lib/texinputs/isabellesym.sty .
|
|
|
29 |
|
|
|
30 |
pdfsetup.sty: $(ISABELLE_HOME)/lib/texinputs/pdfsetup.sty
|
|
|
31 |
cp $(ISABELLE_HOME)/lib/texinputs/pdfsetup.sty .
|
|
|
32 |
|
|
|
33 |
|
|
|
34 |
## HOL-Ifexpr
|
|
|
35 |
|
|
|
36 |
HOL-Ifexpr: HOL $(LOG)/HOL-Ifexpr.gz
|
|
|
37 |
|
|
|
38 |
$(LOG)/HOL-Ifexpr.gz: $(OUT)/HOL Ifexpr/Ifexpr.thy Ifexpr/ROOT.ML
|
|
|
39 |
@$(ISATOOL) usedir -i true -d dvi -D document $(OUT)/HOL Ifexpr
|
|
|
40 |
|
|
|
41 |
|
|
|
42 |
## HOL-ToyList
|
|
|
43 |
|
|
|
44 |
HOL-ToyList: HOL $(LOG)/HOL-ToyList.gz $(LOG)/HOL-ToyList2.gz
|
|
|
45 |
|
|
|
46 |
ToyList2/ToyList.thy: ToyList2/ToyList1 ToyList2/ToyList2
|
|
|
47 |
cat ToyList2/ToyList1 ToyList2/ToyList2 > ToyList2/ToyList.thy
|
|
|
48 |
|
|
|
49 |
$(LOG)/HOL-ToyList2.gz: $(OUT)/HOL ToyList2/ToyList.thy ToyList2/ROOT.ML
|
|
|
50 |
@$(ISATOOL) usedir -i true -d dvi -D document $(OUT)/HOL ToyList2
|
|
|
51 |
|
|
|
52 |
$(LOG)/HOL-ToyList.gz: $(OUT)/HOL ToyList/ToyList.thy ToyList/ROOT.ML
|
|
|
53 |
@$(ISATOOL) usedir -i true -d dvi -D document $(OUT)/HOL ToyList
|
|
|
54 |
|
|
|
55 |
## HOL-CodeGen
|
|
|
56 |
|
|
|
57 |
HOL-CodeGen: HOL $(LOG)/HOL-CodeGen.gz
|
|
|
58 |
|
|
|
59 |
$(LOG)/HOL-CodeGen.gz: $(OUT)/HOL CodeGen/CodeGen.thy
|
|
|
60 |
@$(ISATOOL) usedir -i true -d dvi -D document $(OUT)/HOL CodeGen
|
|
|
61 |
|
|
|
62 |
|
|
|
63 |
## HOL-Datatype
|
|
|
64 |
|
|
|
65 |
HOL-Datatype: HOL $(LOG)/HOL-Datatype.gz
|
|
|
66 |
|
|
8751
|
67 |
$(LOG)/HOL-Datatype.gz: $(OUT)/HOL Datatype/ROOT.ML Datatype/ABexpr.thy \
|
|
|
68 |
Datatype/Nested.thy Datatype/unfoldnested.thy Datatype/Fundata.thy
|
|
8743
|
69 |
@$(ISATOOL) usedir -i true -d dvi -D document $(OUT)/HOL Datatype
|
|
|
70 |
|
|
|
71 |
|
|
|
72 |
## HOL-Trie
|
|
|
73 |
|
|
|
74 |
HOL-Trie: HOL $(LOG)/HOL-Trie.gz
|
|
|
75 |
|
|
|
76 |
$(LOG)/HOL-Trie.gz: $(OUT)/HOL Trie/Option2.thy Trie/Trie.thy
|
|
|
77 |
@$(ISATOOL) usedir -i true -d dvi -D document $(OUT)/HOL Trie
|
|
|
78 |
|
|
|
79 |
|
|
|
80 |
## HOL-Recdef
|
|
|
81 |
|
|
|
82 |
HOL-Recdef: HOL $(LOG)/HOL-Recdef.gz
|
|
|
83 |
|
|
|
84 |
$(LOG)/HOL-Recdef.gz: $(OUT)/HOL Recdef/examples.thy Recdef/termination.thy \
|
|
|
85 |
Recdef/simplification.thy Recdef/Induction.thy
|
|
|
86 |
@$(ISATOOL) usedir -i true -d dvi -D document $(OUT)/HOL Recdef
|
|
|
87 |
|
|
|
88 |
|
|
|
89 |
## HOL-Misc
|
|
|
90 |
|
|
|
91 |
HOL-Misc: HOL $(LOG)/HOL-Misc.gz
|
|
|
92 |
|
|
|
93 |
$(LOG)/HOL-Misc.gz: $(OUT)/HOL Misc/ROOT.ML Misc/Tree.thy Misc/cases.thy \
|
|
|
94 |
Misc/fakenat.thy Misc/natsum.thy Misc/pairs.thy Misc/types.thy Misc/prime_def.thy \
|
|
|
95 |
Misc/arith1.thy Misc/arith2.thy Misc/arith3.thy Misc/arith4.thy \
|
|
|
96 |
Misc/def_rewr.thy Misc/let_rewr.thy Misc/cond_rewr.thy Misc/case_splits.thy \
|
|
|
97 |
Misc/trace_simp.thy Misc/Itrev.thy Misc/asm_simp.thy
|
|
|
98 |
@$(ISATOOL) usedir -i true -d dvi -D document $(OUT)/HOL Misc
|
|
|
99 |
|
|
|
100 |
|
|
|
101 |
## clean
|
|
|
102 |
|
|
|
103 |
clean:
|
|
|
104 |
@rm -f $(LOG)/HOL-Ifexpr.gz $(LOG)/HOL-CodeGen.gz $(LOG)/HOL-Misc.gz $(LOG)/HOL-ToyList.gz $(LOG)/HOL-ToyList2.gz $(LOG)/HOL-Trie.gz $(LOG)/HOL-Datatype.gz $(LOG)/HOL-Recdef.gz
|