src/FOL/Makefile
author oheimb
Thu May 15 15:51:09 1997 +0200 (1997-05-15 ago)
changeset 3206 a3de7f32728c
parent 2889 a86f3b5f3cc7
permissions -rw-r--r--
renamed addss to addSss, unsafe_addss to addss, extended auto_tac
     1 # $Id$
     2 #########################################################################
     3 #									#
     4 #			Makefile for Isabelle (FOL)			#
     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 pure Isabelle (Pure) 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 FILES =	ROOT.ML IFOL.thy IFOL.ML FOL.thy FOL.ML intprover.ML simpdata.ML \
    25 	thy_data.ML cladata.ML \
    26 	../Provers/hypsubst.ML ../Provers/classical.ML ../Provers/blast.ML \
    27 	../Provers/simplifier.ML ../Provers/splitter.ML ../Provers/ind.ML
    28 
    29 EX_NAMES = If List Nat Nat2 Prolog declIffOracle IffOracle
    30 EX_FILES = ex/ROOT.ML ex/cla.ML ex/foundn.ML  ex/int.ML ex/intro.ML\
    31 	   ex/prop.ML ex/quant.ML $(EX_NAMES:%=ex/%.thy) $(EX_NAMES:%=ex/%.ML)
    32 
    33 $(BIN)/FOL:   $(BIN)/Pure  $(FILES) 
    34 	@if [ -d $${ISABELLEBIN:?}/Pure ];\
    35 		then echo Bad value for ISABELLEBIN: \
    36 			$(BIN) is the Isabelle source directory; \
    37 			exit 1; \
    38 	fi
    39 	@case `basename "$(COMP)"` in \
    40 	poly*)	echo 'make_database"$(BIN)/FOL"; quit();' \
    41 		  | $(COMP) $(BIN)/Pure;\
    42 		if [ "$${MAKE_HTML}" = "true" ]; \
    43 		then echo 'open PolyML; make_html := true; exit_use_dir".";' \
    44 		       | $(COMP) $(BIN)/FOL;\
    45 		elif [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
    46 		then echo 'open PolyML; make_html := true; exit_use_dir".";				  make_html := false;' | $(COMP) $(BIN)/FOL;\
    47 		else echo 'open PolyML; exit_use_dir".";' \
    48 		       | $(COMP) $(BIN)/FOL;\
    49 		fi;\
    50 		discgarb -c $(BIN)/FOL;;\
    51 	sml*)	if [ "$${MAKE_HTML}" = "true" ]; \
    52 		then echo 'make_html := true; exit_use_dir".";						  xML"$(BIN)/FOL" banner;' | $(BIN)/Pure;\
    53 		elif [ "$${MAKE_HTML-undefined}" != "undefined" ];\
    54 		then echo 'make_html := true; exit_use_dir".";						  make_html := false; xML"$(BIN)/FOL" banner;' \
    55 		       | $(BIN)/Pure;\
    56 		else echo 'exit_use_dir"."; xML"$(BIN)/FOL" banner;' \
    57 		       | $(BIN)/Pure;\
    58 		fi;;\
    59 	*)	echo Bad value for ISABELLECOMP: \
    60 			\"$(COMP)\" is not poly or sml;;\
    61 	esac
    62 
    63 $(BIN)/Pure:
    64 	cd ../Pure;  $(MAKE)
    65 
    66 test:	ex/ROOT.ML  $(BIN)/FOL	$(EX_FILES) 
    67 	@case `basename "$(COMP)"` in \
    68 	poly*)	if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
    69 		then echo 'make_html := true; exit_use_dir"ex"; quit();' \
    70 		       | $(COMP) $(BIN)/FOL;\
    71 		else echo 'exit_use_dir"ex"; quit();' | $(COMP) $(BIN)/FOL;\
    72 		fi;;\
    73 	sml*)	if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
    74 		then echo 'make_html := true; exit_use_dir"ex";' \
    75 		       | $(BIN)/FOL;\
    76 		else echo 'exit_use_dir"ex";' | $(BIN)/FOL;\
    77 		fi;;\
    78 	*)	echo Bad value for ISABELLECOMP: \
    79 			\"$(COMP)\" is not poly or sml;;\
    80 	esac
    81 
    82 .PRECIOUS:   $(BIN)/Pure  $(BIN)/FOL