1 # |
|
2 # IsaMakefile for Tutorial |
|
3 # |
|
4 |
|
5 ## targets |
|
6 |
|
7 default: HOL-Tutorial HOL-ToyList2 |
|
8 images: |
|
9 test: |
|
10 all: default |
|
11 |
|
12 |
|
13 ## global settings |
|
14 |
|
15 SRC = $(ISABELLE_HOME)/src |
|
16 OUT = $(ISABELLE_OUTPUT) |
|
17 LOG = $(OUT)/log |
|
18 OPTIONS = -m brackets -i true -d "" -D document -M 1 |
|
19 USEDIR = @$(ISABELLE_TOOL) usedir $(OPTIONS) |
|
20 |
|
21 |
|
22 ## HOL |
|
23 |
|
24 HOL: |
|
25 @cd $(SRC)/HOL; $(ISABELLE_TOOL) make HOL |
|
26 |
|
27 |
|
28 ## HOL-Tutorial |
|
29 |
|
30 HOL-Tutorial: HOL $(LOG)/HOL-Tutorial.gz |
|
31 |
|
32 $(LOG)/HOL-Tutorial.gz: $(OUT)/HOL ROOT.ML Ifexpr/Ifexpr.thy \ |
|
33 ToyList2/ToyList.thy CodeGen/CodeGen.thy Datatype/ABexpr.thy \ |
|
34 Datatype/Nested.thy Datatype/unfoldnested.thy Datatype/Fundata.thy \ |
|
35 Trie/Trie.thy Fun/fun0.thy Advanced/simp2.thy Rules/Basic.thy \ |
|
36 Rules/Blast.thy Rules/Force.thy Rules/Primes.thy Rules/Forward.thy \ |
|
37 Rules/Tacticals.thy Rules/find2.thy Sets/Examples.thy \ |
|
38 Sets/Functions.thy Sets/Recur.thy Sets/Relations.thy CTL/Base.thy \ |
|
39 CTL/PDL.thy CTL/CTL.thy CTL/CTLind.thy Inductive/Even.thy \ |
|
40 Inductive/Mutual.thy Inductive/Star.thy Inductive/AB.thy \ |
|
41 Inductive/Advanced.thy Types/Numbers.thy Types/Pairs.thy \ |
|
42 Types/Records.thy Types/Typedefs.thy Types/Overloading.thy \ |
|
43 Types/Axioms.thy Misc/Tree.thy Misc/Tree2.thy Misc/Plus.thy \ |
|
44 Misc/fakenat.thy Misc/natsum.thy Misc/pairs2.thy Misc/Option2.thy \ |
|
45 Misc/types.thy Misc/prime_def.thy Misc/case_exprs.thy Misc/simp.thy \ |
|
46 Misc/Itrev.thy Misc/AdvancedInd.thy Misc/appendix.thy \ |
|
47 Protocol/Message.thy Protocol/Event.thy Protocol/Public.thy \ |
|
48 Protocol/NS_Public.thy Documents/Documents.thy |
|
49 $(USEDIR) -s Tutorial $(OUT)/HOL . |
|
50 |
|
51 |
|
52 ## HOL-ToyList2 |
|
53 |
|
54 HOL-ToyList2: HOL $(LOG)/HOL-ToyList2.gz |
|
55 |
|
56 ToyList2/ToyList.thy: ToyList2/ToyList1 ToyList2/ToyList2 |
|
57 cat ToyList2/ToyList1 ToyList2/ToyList2 > ToyList2/ToyList.thy |
|
58 |
|
59 $(LOG)/HOL-ToyList2.gz: $(OUT)/HOL ToyList2/ROOT.ML |
|
60 $(USEDIR) $(OUT)/HOL ToyList2 |
|
61 |
|
62 |
|
63 ## clean |
|
64 |
|
65 clean: |
|
66 @rm -f tutorial.dvi $(LOG)/HOL-Tutorial.gz $(LOG)/HOL-ToyList2.gz |
|