src/Sequents/IsaMakefile
changeset 4518 74c01296e818
parent 4447 b7ee449eb345
child 6252 935f183bf406
     1.1 --- a/src/Sequents/IsaMakefile	Tue Jan 06 12:32:43 1998 +0100
     1.2 +++ b/src/Sequents/IsaMakefile	Wed Jan 07 13:53:42 1998 +0100
     1.3 @@ -4,32 +4,46 @@
     1.4  # IsaMakefile for Sequents
     1.5  #
     1.6  
     1.7 +## targets
     1.8 +
     1.9 +default: Sequents
    1.10 +images: Sequents
    1.11 +test: Sequents-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 -NAMES = ILL LK S4 S43 T
    1.22 -FILES = ROOT.ML Sequents.thy prover.ML $(NAMES:%=%.thy) $(NAMES:%=%.ML)
    1.23 +
    1.24 +## Sequents
    1.25 +
    1.26 +Sequents: Pure $(OUT)/Sequents
    1.27  
    1.28 -ILL_NAMES = ILL_predlog washing
    1.29 -EX_FILES = ex/ROOT.ML \
    1.30 -    ex/LK/ROOT.ML ex/LK/hardquant.ML ex/LK/prop.ML ex/LK/quant.ML \
    1.31 -    ex/Modal/ROOT.ML ex/Modal/S43thms.ML ex/Modal/S4thms.ML ex/Modal/Tthms.ML \
    1.32 -    ex/ILL/ILL_kleene_lemmas.ML \
    1.33 -    $(ILL_NAMES:%=ex/ILL/%.thy) $(ILL_NAMES:%=ex/ILL/%.ML)
    1.34 +Pure:
    1.35 +	@cd $(SRC)/Pure; $(ISATOOL) make Pure
    1.36  
    1.37 -$(OUT)/Sequents: $(OUT)/Pure $(FILES)
    1.38 +$(OUT)/Sequents: $(OUT)/Pure ILL.ML ILL.thy LK.ML LK.thy ROOT.ML S4.ML \
    1.39 +  S4.thy S43.ML S43.thy Sequents.thy T.ML T.thy prover.ML
    1.40  	@$(ISATOOL) usedir -b $(OUT)/Pure Sequents
    1.41  
    1.42 -$(OUT)/Pure:
    1.43 -	@cd ../Pure; $(ISATOOL) make
    1.44 +
    1.45 +## Sequents-ex
    1.46 +
    1.47 +Sequents-ex: Sequents $(LOG)/Sequents-ex.gz
    1.48  
    1.49 -$(LOG)/Sequents-ex.gz: $(OUT)/Sequents $(EX_FILES)
    1.50 +$(LOG)/Sequents-ex.gz: $(OUT)/Sequents ex/ILL/ILL_kleene_lemmas.ML \
    1.51 +  ex/ILL/ILL_predlog.ML ex/ILL/ILL_predlog.thy ex/ILL/washing.ML \
    1.52 +  ex/ILL/washing.thy ex/LK/ROOT.ML ex/LK/hardquant.ML ex/LK/prop.ML \
    1.53 +  ex/LK/quant.ML ex/Modal/ROOT.ML ex/Modal/S43thms.ML ex/Modal/S4thms.ML \
    1.54 +  ex/Modal/Tthms.ML ex/ROOT.ML
    1.55  	@$(ISATOOL) usedir $(OUT)/Sequents ex
    1.56  
    1.57 -test: $(OUT)/Sequents $(LOG)/Sequents-ex.gz
    1.58 +
    1.59 +## clean
    1.60  
    1.61  clean:
    1.62 -	@rm -f $(OUT)/Sequents $(LOG)/Sequents-ex.gz
    1.63 -
    1.64 -
    1.65 -.PRECIOUS: $(OUT)/Pure $(OUT)/Sequents
    1.66 +	@rm -f $(OUT)/Sequents $(LOG)/Sequents.gz $(LOG)/Sequents-ex.gz