src/HOLCF/Makefile
author oheimb
Mon Feb 24 16:12:24 1997 +0100 (1997-02-24)
changeset 2679 3eac428cdd1b
parent 2640 ee4dfce170a0
child 3028 45204c79ad1d
permissions -rw-r--r--
removed explicit_domains/, which is now covered by ex/
     1 # $Id$
     2 ############################################################################
     3 #									   #
     4 #		    Makefile for Isabelle (HOLCF)			   #
     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 HOL Isabelle 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 THYS = Porder.thy Porder0.thy Pcpo.thy \
    25        Fun1.thy Fun2.thy Fun3.thy \
    26        Cfun1.thy Cfun2.thy Cfun3.thy Cont.thy \
    27        Cprod1.thy Cprod2.thy Cprod3.thy \
    28        Sprod0.thy Sprod1.thy Sprod2.thy Sprod3.thy \
    29        Ssum0.thy Ssum1.thy Ssum2.thy Ssum3.thy \
    30        Up1.thy Up2.thy Up3.thy Fix.thy ccc1.thy \
    31        One.thy Tr.thy \
    32        Lift1.thy Lift2.thy Lift3.thy HOLCF.thy 
    33 
    34 ONLYTHYS = Lift.thy
    35 
    36 FILES = ROOT.ML $(THYS) $(ONLYTHYS) $(THYS:.thy=.ML)
    37 
    38 #Uses cp rather than make_database because Poly/ML allows only 3 levels
    39 $(BIN)/HOLCF:	$(BIN)/HOL  $(FILES) 
    40 	@case `basename "$(COMP)"` in \
    41 	poly*)	cp $(BIN)/HOL $(BIN)/HOLCF; chmod u+w $(BIN)/HOLCF;\
    42 		if [ "$${MAKE_HTML}" = "true" ]; \
    43 		then echo 'open PolyML; make_html := true; exit_use_dir".";' \
    44 		       | $(COMP) $(BIN)/HOLCF;\
    45 		elif [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
    46 		then echo 'open PolyML; make_html := true; exit_use_dir".";				  make_html := false;' | $(COMP) $(BIN)/HOLCF;\
    47 		else echo 'open PolyML; exit_use_dir".";' \
    48 		       | $(COMP) $(BIN)/HOLCF;\
    49 		fi;\
    50 		discgarb -c $(BIN)/HOLCF;;\
    51 	sml*)	if [ "$${MAKE_HTML}" = "true" ]; \
    52 		then echo 'make_html := true; exit_use_dir".";						  xML"$(BIN)/HOLCF" banner;' | $(BIN)/HOL;\
    53 		elif [ "$${MAKE_HTML-undefined}" != "undefined" ];\
    54 		then echo 'make_html := true; exit_use_dir".";						  make_html := false; xML"$(BIN)/HOLCF" banner;' \
    55 		       | $(BIN)/HOL;\
    56 		else echo 'exit_use_dir"."; xML"$(BIN)/HOLCF" banner;' \
    57 		       | $(BIN)/HOL;\
    58 		fi;;\
    59 	*)	echo Bad value for ISABELLECOMP: \
    60 			\"$(COMP)\" is not poly or sml;;\
    61 	esac
    62 
    63 $(BIN)/HOL:
    64 	cd ../HOL;  $(MAKE)
    65 
    66 EX_THYS = ex/Classlib.thy ex/Witness.thy\
    67 	  ex/Dnat.thy ex/Dlist.thy ex/Stream.thy\
    68 	  ex/Dagstuhl.thy ex/Focus_ex.thy ex/Fix2.thy\
    69 	  ex/Hoare.thy ex/Loop.thy
    70 
    71 EX_FILES = ex/ROOT.ML ex/loeckx.ML $(EX_THYS) $(EX_THYS:.thy=.ML)
    72 
    73 test:	ex/ROOT.ML  $(BIN)/HOLCF  $(EX_FILES) 
    74 	@case `basename "$(COMP)"` in \
    75 	poly*)	if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
    76 		then echo 'make_html := true; exit_use_dir"ex"; quit();' \
    77 		       | $(COMP) $(BIN)/HOLCF;\
    78 		else echo 'exit_use_dir"ex"; quit();' | $(COMP) $(BIN)/HOLCF;\
    79 		fi;;\
    80 	sml*)	if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
    81 		then echo 'make_html := true; exit_use_dir"ex";' \
    82 		       | $(BIN)/HOLCF;\
    83 		else echo 'exit_use_dir"ex";' | $(BIN)/HOLCF;\
    84 		fi;;\
    85 	*)	echo Bad value for ISABELLECOMP: \
    86 			\"$(COMP)\" is not poly or sml;;\
    87 	esac
    88 
    89 .PRECIOUS:  $(BIN)/HOL	$(BIN)/HOLCF 
    90