author | wenzelm |
Thu, 26 Jul 2012 17:16:02 +0200 | |
changeset 48519 | 5deda0549f97 |
parent 48506 | af1dabad14c0 |
child 48524 | 5af593945522 |
permissions | -rw-r--r-- |
8743 | 1 |
# |
2 |
# IsaMakefile for Tutorial |
|
3 |
# |
|
4 |
||
5 |
## targets |
|
6 |
||
48519 | 7 |
default: HOL-Tutorial HOL-ToyList2 |
9520 | 8 |
images: |
9 |
test: |
|
10 |
all: default |
|
8743 | 11 |
|
12 |
||
13 |
## global settings |
|
14 |
||
15 |
SRC = $(ISABELLE_HOME)/src |
|
16 |
OUT = $(ISABELLE_OUTPUT) |
|
17 |
LOG = $(OUT)/log |
|
32835
00c14c4a6b4f
enable slow-motion mode to accomodate unsynchronized refs within theory sources;
wenzelm
parents:
31676
diff
changeset
|
18 |
OPTIONS = -m brackets -i true -d "" -D document -M 1 |
48519 | 19 |
USEDIR = @$(ISABELLE_TOOL) usedir $(OPTIONS) |
11617 | 20 |
|
8743 | 21 |
|
22 |
## HOL |
|
23 |
||
24 |
HOL: |
|
28500 | 25 |
@cd $(SRC)/HOL; $(ISABELLE_TOOL) make HOL |
8743 | 26 |
|
27 |
||
48519 | 28 |
## HOL-Tutorial |
8743 | 29 |
|
48519 | 30 |
HOL-Tutorial: HOL $(LOG)/HOL-Tutorial.gz |
8743 | 31 |
|
48519 | 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/pairs.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 . |
|
8743 | 50 |
|
51 |
||
48519 | 52 |
## HOL-ToyList2 |
53 |
||
54 |
HOL-ToyList2: HOL $(LOG)/HOL-ToyList2.gz |
|
8743 | 55 |
|
56 |
ToyList2/ToyList.thy: ToyList2/ToyList1 ToyList2/ToyList2 |
|
57 |
cat ToyList2/ToyList1 ToyList2/ToyList2 > ToyList2/ToyList.thy |
|
58 |
||
48519 | 59 |
$(LOG)/HOL-ToyList2.gz: $(OUT)/HOL ToyList2/ROOT.ML |
60 |
$(USEDIR) $(OUT)/HOL ToyList2 |
|
10296 | 61 |
|
11647
0538cb0f7999
initial setup for chapter on document preparation;
wenzelm
parents:
11617
diff
changeset
|
62 |
|
8743 | 63 |
## clean |
64 |
||
65 |
clean: |
|
48519 | 66 |
@rm -f tutorial.dvi $(LOG)/HOL-Tutorial.gz $(LOG)/HOL-ToyList2.gz |