|
2489
|
1 |
#
|
|
|
2 |
# $Id$
|
|
|
3 |
#
|
|
|
4 |
# IsaMakefile for CCL
|
|
|
5 |
#
|
|
|
6 |
|
|
4518
|
7 |
## targets
|
|
|
8 |
|
|
|
9 |
default: CCL
|
|
|
10 |
images: CCL
|
|
|
11 |
test: CCL-ex
|
|
|
12 |
all: images test
|
|
|
13 |
|
|
|
14 |
|
|
|
15 |
## global settings
|
|
|
16 |
|
|
|
17 |
SRC = $(ISABELLE_HOME)/src
|
|
3118
|
18 |
OUT = $(ISABELLE_OUTPUT)
|
|
4447
|
19 |
LOG = $(OUT)/log
|
|
2489
|
20 |
|
|
4518
|
21 |
|
|
|
22 |
## CCL
|
|
|
23 |
|
|
|
24 |
CCL: FOL $(OUT)/CCL
|
|
2489
|
25 |
|
|
4518
|
26 |
FOL:
|
|
|
27 |
@cd $(SRC)/FOL; $(ISATOOL) make FOL
|
|
2489
|
28 |
|
|
4518
|
29 |
$(OUT)/CCL: $(OUT)/FOL CCL.ML CCL.thy Fix.ML Fix.thy Gfp.ML Gfp.thy \
|
|
|
30 |
Hered.ML Hered.thy Lfp.ML Lfp.thy ROOT.ML Set.ML Set.thy Term.ML \
|
|
|
31 |
Term.thy Trancl.ML Trancl.thy Type.ML Type.thy Wfd.ML Wfd.thy \
|
|
|
32 |
coinduction.ML equalities.ML eval.ML genrec.ML mono.ML subset.ML \
|
|
|
33 |
typecheck.ML
|
|
3057
|
34 |
@$(ISATOOL) usedir -b $(OUT)/FOL CCL
|
|
2489
|
35 |
|
|
4518
|
36 |
|
|
|
37 |
## CCL-ex
|
|
2489
|
38 |
|
|
4518
|
39 |
CCL-ex: CCL $(LOG)/CCL-ex.gz
|
|
|
40 |
|
|
|
41 |
$(LOG)/CCL-ex.gz: $(OUT)/CCL ex/Flag.ML ex/Flag.thy ex/List.ML \
|
|
|
42 |
ex/List.thy ex/Nat.ML ex/Nat.thy ex/ROOT.ML ex/Stream.ML ex/Stream.thy
|
|
2821
|
43 |
@$(ISATOOL) usedir $(OUT)/CCL ex
|
|
2489
|
44 |
|
|
4518
|
45 |
|
|
|
46 |
## clean
|
|
4447
|
47 |
|
|
|
48 |
clean:
|
|
4518
|
49 |
@rm -f $(OUT)/CCL $(LOG)/CCL.gz $(LOG)/CCL-ex.gz
|