equal
deleted
inserted
replaced
3 # |
3 # |
4 # IsaMakefile for Cube |
4 # IsaMakefile for Cube |
5 # |
5 # |
6 |
6 |
7 OUT = $(ISABELLE_OUTPUT) |
7 OUT = $(ISABELLE_OUTPUT) |
|
8 LOG = $(OUT)/log |
|
9 |
8 FILES = ROOT.ML Cube.thy Cube.ML |
10 FILES = ROOT.ML Cube.thy Cube.ML |
9 |
11 |
10 $(OUT)/Cube: $(OUT)/Pure $(FILES) |
12 $(OUT)/Cube: $(OUT)/Pure $(FILES) |
11 @$(ISATOOL) usedir -b $(OUT)/Pure Cube |
13 @$(ISATOOL) usedir -b $(OUT)/Pure Cube |
12 |
14 |
13 $(OUT)/Pure: |
15 $(OUT)/Pure: |
14 @cd ../Pure; $(ISATOOL) make |
16 @cd ../Pure; $(ISATOOL) make |
15 |
17 |
16 test: ex/ROOT.ML ex/ex.ML $(OUT)/Cube |
18 $(LOG)/Cube-ex.gz: ex/ROOT.ML ex/ex.ML $(OUT)/Cube |
17 @$(ISATOOL) usedir $(OUT)/Cube ex |
19 @$(ISATOOL) usedir $(OUT)/Cube ex |
18 |
20 |
|
21 test: $(OUT)/Cube $(LOG)/Cube-ex.gz |
|
22 |
|
23 clean: |
|
24 @rm -f $(OUT)/Cube $(LOG)/Cube-ex.gz |
|
25 |
|
26 |
19 .PRECIOUS: $(OUT)/Pure $(OUT)/Cube |
27 .PRECIOUS: $(OUT)/Pure $(OUT)/Cube |