src/ZF/IsaMakefile
author wenzelm
Fri Dec 19 10:18:58 1997 +0100 (1997-12-19)
changeset 4447 b7ee449eb345
parent 3505 1cb4ea47d967
child 4518 74c01296e818
permissions -rw-r--r--
log files;
'clean' target;
     1 #
     2 # $Id$
     3 #
     4 # IsaMakefile for ZF
     5 #
     6 
     7 #### Base system
     8 
     9 OUT = $(ISABELLE_OUTPUT)
    10 LOG = $(OUT)/log
    11 
    12 NAMES = ZF upair subset pair domrange \
    13 	func AC equalities Bool \
    14 	Sum QPair mono Fixedpt ind_syntax cartprod add_ind_def \
    15 	constructor intr_elim indrule Inductive Perm Rel EquivClass Trancl \
    16 	WF Order Ordinal Epsilon Arith Univ \
    17 	QUniv Datatype OrderArith OrderType \
    18 	Cardinal CardinalArith Cardinal_AC InfDatatype \
    19 	Zorn Nat Finite List
    20 
    21 FILES = ROOT.ML thy_syntax.ML ../Pure/section_utils.ML simpdata.ML typechk.ML \
    22 	$(NAMES:%=%.thy) $(NAMES:%=%.ML)
    23 
    24 $(OUT)/ZF: $(OUT)/FOL $(FILES)
    25 	@$(ISATOOL) usedir -b $(OUT)/FOL ZF
    26 
    27 $(OUT)/FOL:
    28 	@cd ../FOL; $(ISATOOL) make
    29 
    30 
    31 
    32 #### Tests and examples
    33 
    34 ## IMP-semantics example
    35 
    36 IMP_NAMES = Com Denotation Equiv
    37 IMP_FILES = IMP/ROOT.ML $(IMP_NAMES:%=IMP/%.thy) $(IMP_NAMES:%=IMP/%.ML)
    38 
    39 $(LOG)/ZF-IMP.gz: $(OUT)/ZF $(IMP_FILES)
    40 	@$(ISATOOL) usedir $(OUT)/ZF IMP
    41 
    42 
    43 ## Coinduction example
    44 
    45 COIND_NAMES = ECR MT Map Static Types Values
    46 
    47 COIND_FILES = Coind/ROOT.ML Coind/Language.thy Coind/BCR.thy Coind/Dynamic.thy \
    48 	      $(COIND_NAMES:%=Coind/%.thy) $(COIND_NAMES:%=Coind/%.ML)
    49 
    50 $(LOG)/ZF-Coind.gz: $(OUT)/ZF $(COIND_FILES)
    51 	@$(ISATOOL) usedir $(OUT)/ZF Coind
    52 
    53 
    54 ## AC examples
    55 
    56 AC_NAMES = AC_Equiv Cardinal_aux \
    57 	   AC15_WO6 AC16_WO4 AC16_lemmas AC17_AC1 AC18_AC19 AC1_WO2 \
    58 	   DC DC_lemmas HH Hartog WO1_AC \
    59 	   WO2_AC16 WO6_WO1 WO_AC recfunAC16 rel_is_fun
    60 
    61 AC_FILES = AC/ROOT.ML AC/AC0_AC1.ML AC/AC10_AC15.ML AC/AC1_AC17.ML \
    62 	   AC/AC2_AC6.ML AC/AC7_AC9.ML \
    63 	   AC/WO1_WO6.ML AC/WO1_WO7.ML AC/WO1_WO8.ML \
    64 	   $(AC_NAMES:%=AC/%.thy) $(AC_NAMES:%=AC/%.ML)
    65 
    66 $(LOG)/ZF-AC.gz: $(OUT)/ZF $(AC_FILES)
    67 	@$(ISATOOL) usedir $(OUT)/ZF AC
    68 
    69 
    70 ## Residuals example
    71 
    72 RESID_NAMES = Confluence Redex SubUnion Conversion Reduction Substitution \
    73 	      Cube Residuals Terms
    74 
    75 RESID_FILES = Resid/ROOT.ML $(RESID_NAMES:%=Resid/%.thy) $(RESID_NAMES:%=Resid/%.ML)
    76 
    77 $(LOG)/ZF-Resid.gz: $(OUT)/ZF $(RESID_FILES)
    78 	@$(ISATOOL) usedir $(OUT)/ZF Resid
    79 
    80 
    81 ## Miscellaneous examples
    82 
    83 EX_NAMES = Primes Ramsey Limit Integ twos_compl Bin BT Term TF Ntree Brouwer \
    84 	   Data Enum Rmap Mutil PropLog ListN Acc Comb Primrec LList CoUnit
    85 
    86 EX_FILES = ex/ROOT.ML ex/misc.ML $(EX_NAMES:%=ex/%.thy) $(EX_NAMES:%=ex/%.ML)
    87 
    88 $(LOG)/ZF-ex.gz: $(OUT)/ZF $(EX_FILES)
    89 	@$(ISATOOL) usedir $(OUT)/ZF ex
    90 
    91 
    92 ## Full test
    93 
    94 ALL_TARGETS = $(OUT)/ZF $(LOG)/ZF-IMP.gz $(LOG)/ZF-Coind.gz \
    95   $(LOG)/ZF-AC.gz $(LOG)/ZF-Resid.gz $(LOG)/ZF-ex.gz
    96 
    97 test: $(ALL_TARGETS)
    98 
    99 clean:
   100 	@rm -f $(ALL_TARGETS)
   101 
   102 
   103 .PRECIOUS: $(OUT)/FOL $(OUT)/ZF