src/ZF/Makefile
author clasohm
Sat Feb 10 19:04:21 1996 +0100 (1996-02-10)
changeset 1491 38a14548baad
parent 1361 90d615b599d9
child 1607 5c123831c4e2
permissions -rw-r--r--
make_html now only remains set if MAKE_HTML=true
     1 # $Id$
     2 #########################################################################
     3 #									#
     4 # 			Makefile for Isabelle (ZF)			#
     5 #									#
     6 #########################################################################
     7 
     8 #To make the system, cd to this directory and type
     9 #	make
    10 #To make the system and test it on standard examples, type 
    11 #	make test
    12 #To generate HTML files for every theory, set the environment variable
    13 #MAKE_HTML or add the parameter "MAKE_HTML=".
    14 
    15 #Environment variable ISABELLECOMP specifies the compiler.
    16 #Environment variable ISABELLEBIN specifies the destination directory.
    17 #For Poly/ML, ISABELLEBIN must begin with a /
    18 
    19 #Makes FOL if this file is ABSENT -- but not 
    20 #if it is out of date, since this Makefile does not know its dependencies!
    21 
    22 BIN = $(ISABELLEBIN)
    23 COMP = $(ISABELLECOMP)
    24 NAMES = ZF upair subset pair domrange \
    25 	func AC simpdata equalities Bool \
    26 	Sum QPair mono Fixedpt ind_syntax add_ind_def \
    27 	constructor intr_elim indrule Inductive Perm Rel EquivClass Trancl \
    28 	WF Order Ordinal Epsilon Arith Univ \
    29 	QUniv Datatype OrderArith OrderType \
    30 	Cardinal CardinalArith Cardinal_AC InfDatatype \
    31 	Zorn Nat Finite List 
    32 
    33 FILES = ROOT.ML thy_syntax.ML ../Pure/section_utils.ML \
    34  	$(NAMES:%=%.thy) $(NAMES:%=%.ML)
    35 
    36 #Uses cp rather than make_database because Poly/ML allows only 3 levels
    37 $(BIN)/ZF:   $(BIN)/FOL  $(FILES) 
    38 	case "$(COMP)" in \
    39 	poly*)	cp $(BIN)/FOL $(BIN)/ZF;\
    40                 if [ "$${MAKE_HTML}" = "true" ]; \
    41                 then echo 'open PolyML; make_html := true; exit_use_dir".";' \
    42                        | $(COMP) $(BIN)/ZF;\
    43 		elif [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
    44                 then echo 'open PolyML; make_html := true; exit_use_dir".";                               make_html := false;' | $(COMP) $(BIN)/ZF;\
    45                 else echo 'open PolyML; exit_use_dir".";' \
    46                        | $(COMP) $(BIN)/ZF;\
    47                 fi;;\
    48 	sml*)	if [ "$${MAKE_HTML}" = "true" ]; \
    49                 then echo 'make_html := true; exit_use_dir".";                                            xML"$(BIN)/ZF" banner;' | $(BIN)/FOL;\
    50                 elif [ "$${MAKE_HTML-undefined}" != "undefined" ];\
    51                 then echo 'make_html := true; exit_use_dir".";                                            make_html := false; xML"$(BIN)/ZF" banner;' \
    52                        | $(BIN)/FOL;\
    53                 else echo 'exit_use_dir"."; xML"$(BIN)/ZF" banner;' \
    54                        | $(BIN)/FOL;\
    55                 fi;;\
    56 	*)	echo Bad value for ISABELLECOMP: \
    57                 	$(COMP) is not poly or sml; exit 1;;\
    58 	esac
    59 
    60 $(BIN)/FOL:
    61 	cd ../FOL;  $(MAKE)
    62 
    63 #### Testing of ZF
    64 
    65 #A macro referring to the object-logic (depends on ML compiler)
    66 LOGIC:sh=case $ISABELLECOMP in \
    67 	poly*)	echo "$ISABELLECOMP $ISABELLEBIN/ZF" ;;\
    68 	sml*)	echo "$ISABELLEBIN/ZF" ;;\
    69 	*)	echo "echo Bad value for ISABELLECOMP: \
    70                 	$ISABELLEBIN is not poly or sml; exit 1" ;;\
    71 	esac
    72 
    73 ##IMP-semantics example
    74 IMP_NAMES = Com Denotation Equiv
    75 IMP_FILES = IMP/ROOT.ML $(IMP_NAMES:%=IMP/%.thy) $(IMP_NAMES:%=IMP/%.ML)
    76 
    77 IMP:   $(BIN)/ZF  $(IMP_FILES)
    78 	if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
    79         then echo 'make_html := true; exit_use_dir"IMP";quit();' | $(LOGIC); \
    80         else echo 'exit_use_dir"IMP";quit();' | $(LOGIC); \
    81         fi
    82 
    83 ##Coinduction example
    84 COIND_NAMES = ECR Language MT Map Static Types Values 
    85 
    86 COIND_FILES = Coind/ROOT.ML Coind/BCR.thy  Coind/Dynamic.thy \
    87               $(COIND_NAMES:%=Coind/%.thy) $(COIND_NAMES:%=Coind/%.ML)
    88 
    89 Coind:  $(BIN)/ZF  $(COIND_FILES)
    90 	if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
    91         then echo 'make_html := true; exit_use_dir"Coind";quit();' | $(LOGIC);\
    92         else echo 'exit_use_dir"Coind";quit();' | $(LOGIC); \
    93         fi
    94 
    95 ##AC examples
    96 AC_NAMES = AC_Equiv OrdQuant Transrec2 Cardinal_aux \
    97 	   AC15_WO6 AC16_WO4 AC16_lemmas AC17_AC1 AC18_AC19 AC1_WO2 \
    98            DC DC_lemmas HH Hartog WO1_AC \
    99            WO2_AC16 WO6_WO1 WO_AC first recfunAC16 rel_is_fun
   100 
   101 AC_FILES = AC/ROOT.ML AC/AC0_AC1.ML AC/AC10_AC15.ML AC/AC1_AC17.ML \
   102            AC/AC2_AC6.ML AC/AC7_AC9.ML \
   103            AC/WO1_WO6.ML AC/WO1_WO7.ML AC/WO1_WO8.ML \
   104            $(AC_NAMES:%=AC/%.thy) $(AC_NAMES:%=AC/%.ML)
   105 
   106 AC:  $(BIN)/ZF  $(AC_FILES)
   107 	if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
   108         then echo 'make_html := true; exit_use_dir"AC";quit();' | $(LOGIC); \
   109         else echo 'exit_use_dir"AC";quit();' | $(LOGIC); \
   110         fi
   111 
   112 ##Residuals example
   113 
   114 RESID_NAMES = Confluence Redex SubUnion Conversion Reduction Substitution \
   115               Cube Residuals Terms
   116 
   117 RESID_FILES = Resid/ROOT.ML $(RESID_NAMES:%=Resid/%.thy) \
   118                             $(RESID_NAMES:%=Resid/%.ML)
   119 
   120 Resid:  $(BIN)/ZF  $(RESID_FILES)
   121 	if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
   122         then echo 'make_html := true; exit_use_dir"Resid";quit();' | $(LOGIC);\
   123         else echo 'exit_use_dir"Resid";quit();' | $(LOGIC); \
   124         fi
   125 
   126 ##Miscellaneous examples
   127 EX_NAMES = Ramsey Limit Integ twos_compl Bin BT Term TF Ntree Brouwer \
   128            Data Enum Rmap PropLog ListN Acc Comb Primrec LList CoUnit 
   129 
   130 EX_FILES = ex/ROOT.ML ex/misc.ML $(EX_NAMES:%=ex/%.thy) $(EX_NAMES:%=ex/%.ML)
   131 
   132 #Test ZF by loading the examples in directory ex
   133 ex:     $(BIN)/ZF  $(EX_FILES)
   134 	if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
   135         then echo 'make_html := true; exit_use_dir"ex";quit();' | $(LOGIC); \
   136         else echo 'exit_use_dir"ex";quit();' | $(LOGIC); \
   137         fi
   138 
   139 #Full test.
   140 test:   $(BIN)/ZF IMP Coind AC Resid ex
   141 	echo 'Test examples ran successfully' > test
   142 
   143 .PRECIOUS:  $(BIN)/FOL $(BIN)/ZF