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