2 # $Id$ |
2 # $Id$ |
3 # |
3 # |
4 # IsaMakefile for FOLP |
4 # IsaMakefile for FOLP |
5 # |
5 # |
6 |
6 |
|
7 ## targets |
|
8 |
|
9 default: FOLP |
|
10 images: FOLP |
|
11 test: FOLP-ex |
|
12 all: images test |
|
13 |
|
14 |
|
15 ## global settings |
|
16 |
|
17 SRC = $(ISABELLE_HOME)/src |
7 OUT = $(ISABELLE_OUTPUT) |
18 OUT = $(ISABELLE_OUTPUT) |
8 LOG = $(OUT)/log |
19 LOG = $(OUT)/log |
9 |
20 |
10 FILES = ROOT.ML IFOLP.thy IFOLP.ML FOLP.thy FOLP.ML intprover.ML simpdata.ML \ |
|
11 hypsubst.ML classical.ML simp.ML |
|
12 |
21 |
13 EX_FILES = ex/ROOT.ML ex/cla.ML ex/foundn.ML ex/If.ML ex/If.thy ex/int.ML \ |
22 ## FOLP |
14 ex/intro.ML ex/Nat.ML ex/Nat.thy ex/Prolog.ML ex/Prolog.thy \ |
|
15 ex/prop.ML ex/quant.ML |
|
16 |
23 |
17 $(OUT)/FOLP: $(OUT)/Pure $(FILES) |
24 FOLP: Pure $(OUT)/FOLP |
|
25 |
|
26 Pure: |
|
27 @cd $(SRC)/Pure; $(ISATOOL) make Pure |
|
28 |
|
29 $(OUT)/FOLP: $(OUT)/Pure FOLP.ML FOLP.thy IFOLP.ML IFOLP.thy ROOT.ML \ |
|
30 classical.ML hypsubst.ML intprover.ML simp.ML simpdata.ML |
18 @$(ISATOOL) usedir -b $(OUT)/Pure FOLP |
31 @$(ISATOOL) usedir -b $(OUT)/Pure FOLP |
19 |
32 |
20 $(OUT)/Pure: |
|
21 @cd ../Pure; $(ISATOOL) make |
|
22 |
33 |
23 $(LOG)/FOLP-ex.gz: ex/ROOT.ML $(OUT)/FOLP $(EX_FILES) |
34 ## FOLP-ex |
|
35 |
|
36 FOLP-ex: FOLP $(LOG)/FOLP-ex.gz |
|
37 |
|
38 $(LOG)/FOLP-ex.gz: $(OUT)/FOLP ex/ROOT.ML ex/cla.ML ex/foundn.ML \ |
|
39 ex/If.ML ex/If.thy ex/int.ML ex/intro.ML ex/Nat.ML ex/Nat.thy \ |
|
40 ex/Prolog.ML ex/Prolog.thy ex/prop.ML ex/quant.ML |
24 @$(ISATOOL) usedir $(OUT)/FOLP ex |
41 @$(ISATOOL) usedir $(OUT)/FOLP ex |
25 |
42 |
26 test: $(OUT)/FOLP $(LOG)/FOLP-ex.gz |
43 |
|
44 ## clean |
27 |
45 |
28 clean: |
46 clean: |
29 @rm -f $(OUT)/FOLP $(LOG)/FOLP-ex.gz |
47 @rm -f $(OUT)/FOLP $(LOG)/FOLP.gz $(LOG)/FOLP-ex.gz |
30 |
|
31 |
|
32 .PRECIOUS: $(OUT)/Pure $(OUT)/FOLP |
|