equal
deleted
inserted
replaced
6 |
6 |
7 OUT = $(ISABELLE_OUTPUT_DIR) |
7 OUT = $(ISABELLE_OUTPUT_DIR) |
8 FILES = ROOT.ML Cube.thy Cube.ML |
8 FILES = ROOT.ML Cube.thy Cube.ML |
9 |
9 |
10 $(OUT)/Cube: $(OUT)/Pure $(FILES) |
10 $(OUT)/Cube: $(OUT)/Pure $(FILES) |
11 @$(ISABELLE) -e "make_html := $(ISABELLE_HTML);" -qu $(OUT)/Pure Cube |
11 @$(ISATOOL) usedir -b $(OUT)/Pure Cube |
12 @chmod -w $@ |
12 @chmod -w $@ |
13 |
13 |
14 $(OUT)/Pure: |
14 $(OUT)/Pure: |
15 @cd ../Pure; $(ISATOOL) make |
15 @cd ../Pure; $(ISATOOL) make |
16 |
16 |
17 test: ex.ML $(OUT)/Cube |
17 test: ex/ROOT.ML ex/ex.ML $(OUT)/Cube |
18 @$(ISABELLE) -e 'make_html := $(ISABELLE_HTML); use"ex.ML"; quit();' \ |
18 @$(ISATOOL) usedir $(OUT)/Cube ex |
19 -rq $(OUT)/Cube |
|
20 |
19 |
21 .PRECIOUS: $(OUT)/Pure $(OUT)/Cube |
20 .PRECIOUS: $(OUT)/Pure $(OUT)/Cube |