| author | wenzelm | 
| Thu, 01 Mar 2012 15:42:44 +0100 | |
| changeset 46749 | 042c546d2bac | 
| parent 45860 | 93eda35a8377 | 
| permissions | -rw-r--r-- | 
| 2489 | 1  | 
#  | 
2  | 
# IsaMakefile for CCL  | 
|
3  | 
#  | 
|
4  | 
||
| 4518 | 5  | 
## targets  | 
6  | 
||
7  | 
default: CCL  | 
|
8  | 
images: CCL  | 
|
9  | 
test: CCL-ex  | 
|
10  | 
all: images test  | 
|
| 45860 | 11  | 
full: all  | 
| 
42138
 
e54a985daa61
added make target 'smlnj' to refer to what can/should be tested using smlnj -- allows the use of "isabelle makeall smlnj";
 
krauss 
parents: 
36862 
diff
changeset
 | 
12  | 
smlnj: all  | 
| 4518 | 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:  | 
| 28500 | 27  | 
@cd $(SRC)/FOL; $(ISABELLE_TOOL) make FOL  | 
| 2489 | 28  | 
|
| 13300 | 29  | 
$(OUT)/FOL: FOL  | 
30  | 
||
| 20140 | 31  | 
$(OUT)/CCL: $(OUT)/FOL CCL.thy Fix.thy Gfp.thy Hered.thy Lfp.thy ROOT.ML \  | 
32  | 
Set.thy Term.thy Trancl.thy Type.thy Wfd.thy  | 
|
| 28500 | 33  | 
@$(ISABELLE_TOOL) usedir -b -r $(OUT)/FOL CCL  | 
| 2489 | 34  | 
|
| 4518 | 35  | 
|
36  | 
## CCL-ex  | 
|
| 2489 | 37  | 
|
| 4518 | 38  | 
CCL-ex: CCL $(LOG)/CCL-ex.gz  | 
39  | 
||
| 20140 | 40  | 
$(LOG)/CCL-ex.gz: $(OUT)/CCL ex/Flag.thy ex/List.thy ex/Nat.thy ex/ROOT.ML \  | 
41  | 
ex/Stream.thy  | 
|
| 28500 | 42  | 
@$(ISABELLE_TOOL) usedir $(OUT)/CCL ex  | 
| 2489 | 43  | 
|
| 4518 | 44  | 
|
45  | 
## clean  | 
|
| 4447 | 46  | 
|
47  | 
clean:  | 
|
| 4518 | 48  | 
@rm -f $(OUT)/CCL $(LOG)/CCL.gz $(LOG)/CCL-ex.gz  |