|
1 # |
|
2 # IsaMakefile for Tutorial |
|
3 # |
|
4 |
|
5 ## targets |
|
6 |
|
7 default: HOL-ToyList HOL-Ifexpr HOL-CodeGen 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 |
|
23 ## HOL-Ifexpr |
|
24 |
|
25 HOL-Ifexpr: HOL $(LOG)/HOL-Ifexpr.gz |
|
26 |
|
27 Ifexpr/Ifexpr.thy: Ifexpr/prolog Ifexpr/boolex Ifexpr/value Ifexpr/ifex \ |
|
28 Ifexpr/valif Ifexpr/bool2if Ifexpr/normif Ifexpr/norm Ifexpr/normal \ |
|
29 Ifexpr/end |
|
30 @cd Ifexpr; \ |
|
31 cat prolog boolex value ifex valif bool2if normif norm normal \ |
|
32 end > Ifexpr.thy |
|
33 |
|
34 $(LOG)/HOL-Ifexpr.gz: $(OUT)/HOL Ifexpr/Ifexpr.thy Ifexpr/ROOT.ML |
|
35 @$(ISATOOL) usedir $(OUT)/HOL Ifexpr |
|
36 |
|
37 |
|
38 ## HOL-ToyList |
|
39 |
|
40 HOL-ToyList: HOL $(LOG)/HOL-ToyList.gz |
|
41 |
|
42 ToyList/ToyList.ML: ToyList/autotac ToyList/addsimps2 ToyList/inductxs \ |
|
43 ToyList/lemma1 ToyList/lemma2 ToyList/lemma3 \ |
|
44 ToyList/qed1 ToyList/qed2 ToyList/qed3 ToyList/thm ToyList/qed |
|
45 cd ToyList; \ |
|
46 cat lemma2 inductxs autotac qed2 addsimps2 lemma3 qed3 \ |
|
47 lemma1 inductxs autotac qed1 thm inductxs autotac qed > ToyList.ML |
|
48 |
|
49 $(LOG)/HOL-ToyList.gz: $(OUT)/HOL ToyList/ToyList.thy ToyList/ToyList.ML \ |
|
50 ToyList/ROOT.ML |
|
51 @$(ISATOOL) usedir $(OUT)/HOL ToyList |
|
52 |
|
53 ## HOL-CodeGen |
|
54 |
|
55 HOL-CodeGen: HOL $(LOG)/HOL-CodeGen.gz |
|
56 |
|
57 CodeGen/CodeGen.thy: CodeGen/prolog CodeGen/expr CodeGen/value \ |
|
58 CodeGen/instr CodeGen/exec CodeGen/comp CodeGen/end |
|
59 cd CodeGen; cat prolog expr value instr exec comp end > CodeGen.thy |
|
60 |
|
61 $(LOG)/HOL-CodeGen.gz: $(OUT)/HOL CodeGen/CodeGen.thy CodeGen/goal1.ML \ |
|
62 CodeGen/goal2.ML CodeGen/simpsplit.ML CodeGen/ROOT.ML |
|
63 @$(ISATOOL) usedir $(OUT)/HOL CodeGen |
|
64 |
|
65 |
|
66 ## HOL-Misc |
|
67 |
|
68 HOL-Misc: HOL $(LOG)/HOL-Misc.gz |
|
69 |
|
70 Misc/Tree.thy: Misc/treeprolog Misc/tree Misc/end |
|
71 cd Misc; cat treeprolog tree end > Tree.thy |
|
72 |
|
73 Misc/NatSum.thy: Misc/natsumprolog Misc/natsum Misc/end |
|
74 cd Misc; cat natsumprolog natsum end > NatSum.thy |
|
75 |
|
76 Misc/Types.thy: Misc/typesprolog Misc/types Misc/end |
|
77 cd Misc; cat typesprolog types end > Types.thy |
|
78 |
|
79 Misc/Defs.thy: Misc/defsprolog Misc/consts Misc/defs Misc/end |
|
80 cd Misc; cat defsprolog consts defs end > Defs.thy |
|
81 |
|
82 Misc/ConstDefs.thy: Misc/constdefsprolog Misc/constdefs Misc/end |
|
83 cd Misc; cat constdefsprolog constdefs end > ConstDefs.thy |
|
84 |
|
85 $(LOG)/HOL-Misc.gz: $(OUT)/HOL Misc/ROOT.ML Misc/exhaust.ML Misc/autotac.ML \ |
|
86 Misc/Tree.thy Misc/NatSum.thy Misc/NatSum.ML Misc/Types.thy \ |
|
87 Misc/Defs.thy Misc/ConstDefs.thy \ |
|
88 Misc/Exor.thy Misc/exorgoal.ML Misc/exorproof.ML \ |
|
89 Misc/splitif.ML Misc/splitlist.ML Misc/induct_auto.ML \ |
|
90 Misc/Itrev.thy Misc/itrev1.ML Misc/itrev2.ML Misc/itrev3.ML |
|
91 @$(ISATOOL) usedir $(OUT)/HOL Misc |
|
92 |
|
93 |
|
94 ## clean |
|
95 |
|
96 clean: |
|
97 @rm -f $(LOG)/HOL-Ifexpr.gz $(LOG)/HOL-Misc.gz |