src/FOLP/IsaMakefile
changeset 4518 74c01296e818
parent 4447 b7ee449eb345
child 17480 fd19f77dcf60
     1.1 --- a/src/FOLP/IsaMakefile	Tue Jan 06 12:32:43 1998 +0100
     1.2 +++ b/src/FOLP/IsaMakefile	Wed Jan 07 13:53:42 1998 +0100
     1.3 @@ -4,29 +4,44 @@
     1.4  # IsaMakefile for FOLP
     1.5  #
     1.6  
     1.7 +## targets
     1.8 +
     1.9 +default: FOLP
    1.10 +images: FOLP
    1.11 +test: FOLP-ex
    1.12 +all: images test
    1.13 +
    1.14 +
    1.15 +## global settings
    1.16 +
    1.17 +SRC = $(ISABELLE_HOME)/src
    1.18  OUT = $(ISABELLE_OUTPUT)
    1.19  LOG = $(OUT)/log
    1.20  
    1.21 -FILES =	ROOT.ML IFOLP.thy IFOLP.ML FOLP.thy FOLP.ML intprover.ML simpdata.ML \
    1.22 -	hypsubst.ML classical.ML simp.ML
    1.23 +
    1.24 +## FOLP
    1.25 +
    1.26 +FOLP: Pure $(OUT)/FOLP
    1.27  
    1.28 -EX_FILES = ex/ROOT.ML ex/cla.ML ex/foundn.ML ex/If.ML ex/If.thy ex/int.ML \
    1.29 -	   ex/intro.ML ex/Nat.ML ex/Nat.thy ex/Prolog.ML ex/Prolog.thy \
    1.30 -	   ex/prop.ML ex/quant.ML
    1.31 +Pure:
    1.32 +	@cd $(SRC)/Pure; $(ISATOOL) make Pure
    1.33  
    1.34 -$(OUT)/FOLP: $(OUT)/Pure $(FILES)
    1.35 +$(OUT)/FOLP: $(OUT)/Pure FOLP.ML FOLP.thy IFOLP.ML IFOLP.thy ROOT.ML \
    1.36 +  classical.ML hypsubst.ML intprover.ML simp.ML simpdata.ML
    1.37  	@$(ISATOOL) usedir -b $(OUT)/Pure FOLP
    1.38  
    1.39 -$(OUT)/Pure:
    1.40 -	@cd ../Pure; $(ISATOOL) make
    1.41 +
    1.42 +## FOLP-ex
    1.43  
    1.44 -$(LOG)/FOLP-ex.gz: ex/ROOT.ML $(OUT)/FOLP $(EX_FILES)
    1.45 +FOLP-ex: FOLP $(LOG)/FOLP-ex.gz
    1.46 +
    1.47 +$(LOG)/FOLP-ex.gz: $(OUT)/FOLP ex/ROOT.ML ex/cla.ML ex/foundn.ML \
    1.48 +  ex/If.ML ex/If.thy ex/int.ML ex/intro.ML ex/Nat.ML ex/Nat.thy \
    1.49 +  ex/Prolog.ML ex/Prolog.thy ex/prop.ML ex/quant.ML
    1.50  	@$(ISATOOL) usedir $(OUT)/FOLP ex
    1.51  
    1.52 -test: $(OUT)/FOLP $(LOG)/FOLP-ex.gz
    1.53 +
    1.54 +## clean
    1.55  
    1.56  clean:
    1.57 -	@rm -f $(OUT)/FOLP $(LOG)/FOLP-ex.gz
    1.58 -
    1.59 -
    1.60 -.PRECIOUS: $(OUT)/Pure $(OUT)/FOLP
    1.61 +	@rm -f $(OUT)/FOLP $(LOG)/FOLP.gz $(LOG)/FOLP-ex.gz