src/Pure/Makefile
changeset 0 a5a9c433f639
child 57 87e14d7f20dc
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/Pure/Makefile	Thu Sep 16 12:20:38 1993 +0200
     1.3 @@ -0,0 +1,50 @@
     1.4 +#########################################################################
     1.5 +#									#
     1.6 +# 			Makefile for Isabelle (Pure)			#
     1.7 +#									#
     1.8 +#########################################################################
     1.9 +
    1.10 +#The pure part is common to all systems.  
    1.11 +#Object-logics (like FOL) are loaded on top of it.
    1.12 +
    1.13 +#To make the system, cd to this directory and type  
    1.14 +#	make -f Makefile 
    1.15 +
    1.16 +#Environment variable ML_DBASE specifies the initial Poly/ML database, from
    1.17 +#  the Poly/ML distribution directory.
    1.18 +#WARNING: Poly/ML parent databases should not be moved!
    1.19 +
    1.20 +#Environment variable ISABELLECOMP specifies the compiler.
    1.21 +#Environment variable ISABELLEBIN specifies the destination directory.
    1.22 +#For Poly/ML, ISABELLEBIN must begin with a /
    1.23 +
    1.24 +BIN = $(ISABELLEBIN)
    1.25 +COMP = $(ISABELLECOMP)
    1.26 +FILES =	POLY.ML NJ.ML ROOT.ML library.ML term.ML symtab.ML type.ML sign.ML\
    1.27 +	sequence.ML envir.ML pattern.ML unify.ML logic.ML thm.ML net.ML\
    1.28 +	drule.ML tctical.ML tactic.ML goals.ML
    1.29 +
    1.30 +SYNTAX_FILES =  Syntax/ROOT.ML	Syntax/ast.ML		Syntax/xgram.ML\
    1.31 +	Syntax/extension.ML	Syntax/lexicon.ML	Syntax/parse_tree.ML\
    1.32 +	Syntax/earley0A.ML	Syntax/type_ext.ML	Syntax/sextension.ML\
    1.33 +	Syntax/pretty.ML	Syntax/printer.ML	Syntax/syntax.ML
    1.34 +
    1.35 +THY_FILES = Thy/ROOT.ML Thy/scan.ML Thy/parse.ML Thy/syntax.ML Thy/read.ML
    1.36 +
    1.37 +#Uses cp rather than make_database because Poly/ML allows only 3 levels
    1.38 +$(BIN)/Pure:   $(FILES)  $(SYNTAX_FILES)  $(THY_FILES)  $(ML_DBASE)
    1.39 +	case "$(COMP)" in \
    1.40 +	poly*)	echo database=$${ML_DBASE:?'No Poly/ML database specified'};\
    1.41 +		cp $(ML_DBASE) $(BIN)/Pure; chmod u+w $(BIN)/Pure;\
    1.42 +		echo 'PolyML.use"POLY";use"ROOT";' | $(COMP) $(BIN)/Pure;;\
    1.43 +	sml*)	if [ ! '(' -d $${ISABELLEBIN:?} -a -w $${ISABELLEBIN:?} ')' ];\
    1.44 +           	then echo Bad value for ISABELLEBIN : \
    1.45 +                	$(BIN) is not a writable directory; \
    1.46 +                	exit 1; \
    1.47 +           	fi;\
    1.48 +		echo 'use"NJ.ML"; use"ROOT.ML"; xML"$(BIN)/Pure" banner;'\
    1.49 +			  | $(COMP);;\
    1.50 +	*)	echo Bad value for ISABELLECOMP;;\
    1.51 +	esac
    1.52 +
    1.53 +.PRECIOUS:  $(BIN)/Pure