isabelle: src/HOLCF/Makefile@17d7fad9c9a2 (annotated)

243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	1	############################################################################
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	2	# #
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	3	# Makefile for Isabelle (HOLCF) #
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	4	# #
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	5	############################################################################
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	6
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	7	#To make the system, cd to this directory and type
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	8	# make -f Makefile
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	9
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	10	#Environment variable ISABELLECOMP specifies the compiler.
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	11	#Environment variable ISABELLEBIN specifies the destination directory.
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	12	#For Poly/ML, ISABELLEBIN must begin with a /
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	13
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	14	#Makes HOL Isabelle if this file is ABSENT -- but not
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	15	#if it is out of date, since this Makefile does not know its dependencies!
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	16
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	17	BIN = $(ISABELLEBIN)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	18	COMP = $(ISABELLECOMP)
918 7ecdff86a5f0 Uses "suffix substitution" to shorten macro definitions. lcp parents: 752 diff changeset	19	THYS = Holcfb.thy Void.thy Porder.thy Pcpo.thy \
7ecdff86a5f0 Uses "suffix substitution" to shorten macro definitions. lcp parents: 752 diff changeset	20	Fun1.thy Fun2.thy Fun3.thy \
7ecdff86a5f0 Uses "suffix substitution" to shorten macro definitions. lcp parents: 752 diff changeset	21	Cfun1.thy Cfun2.thy Cfun3.thy Cont.thy \
7ecdff86a5f0 Uses "suffix substitution" to shorten macro definitions. lcp parents: 752 diff changeset	22	Cprod1.thy Cprod2.thy Cprod3.thy \
7ecdff86a5f0 Uses "suffix substitution" to shorten macro definitions. lcp parents: 752 diff changeset	23	Sprod0.thy Sprod1.thy Sprod2.thy Sprod3.thy \
7ecdff86a5f0 Uses "suffix substitution" to shorten macro definitions. lcp parents: 752 diff changeset	24	Ssum0.thy Ssum1.thy Ssum2.thy Ssum3.thy \
7ecdff86a5f0 Uses "suffix substitution" to shorten macro definitions. lcp parents: 752 diff changeset	25	Lift1.thy Lift2.thy Lift3.thy Fix.thy ccc1.thy One.thy \
7ecdff86a5f0 Uses "suffix substitution" to shorten macro definitions. lcp parents: 752 diff changeset	26	Tr1.thy Tr2.thy HOLCF.thy Dnat.thy Dnat2.thy \
7ecdff86a5f0 Uses "suffix substitution" to shorten macro definitions. lcp parents: 752 diff changeset	27	Stream.thy Stream2.thy Dlist.thy
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	28
918 7ecdff86a5f0 Uses "suffix substitution" to shorten macro definitions. lcp parents: 752 diff changeset	29	FILES = ROOT.ML Porder0.thy $(THYS) $(THYS:.thy=.ML)
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	30
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	31	$(BIN)/HOLCF: $(BIN)/HOL $(FILES)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	32	case "$(COMP)" in \
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	33	poly*) echo 'make_database"$(BIN)/HOLCF"; quit();' \
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	34	\| $(COMP) $(BIN)/HOL ;\
953 17d7fad9c9a2 Now calls exit_use instead of use, for prompt failure if errors are detected. lcp parents: 918 diff changeset	35	echo 'exit_use"ROOT";' \| $(COMP) $(BIN)/HOLCF ;;\
17d7fad9c9a2 Now calls exit_use instead of use, for prompt failure if errors are detected. lcp parents: 918 diff changeset	36	sml*) echo 'exit_use"ROOT.ML"; xML"$(BIN)/HOLCF" banner;' \| $(BIN)/HOL ;;\
468 3dd1dcb509ac Improved error checking lcp parents: 346 diff changeset	37	*) echo Bad value for ISABELLECOMP: \
3dd1dcb509ac Improved error checking lcp parents: 346 diff changeset	38	$(COMP) is not poly or sml;;\
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	39	esac
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	40
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	41	$(BIN)/HOL:
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	42	cd ../HOL; $(MAKE)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	43
918 7ecdff86a5f0 Uses "suffix substitution" to shorten macro definitions. lcp parents: 752 diff changeset	44	EX_THYS = ex/Coind.thy ex/Hoare.thy \
7ecdff86a5f0 Uses "suffix substitution" to shorten macro definitions. lcp parents: 752 diff changeset	45	ex/Loop.thy ex/Dagstuhl.thy
7ecdff86a5f0 Uses "suffix substitution" to shorten macro definitions. lcp parents: 752 diff changeset	46
7ecdff86a5f0 Uses "suffix substitution" to shorten macro definitions. lcp parents: 752 diff changeset	47	EX_FILES = ex/ROOT.ML ex/loeckx.ML $(EX_THYS) $(EX_THYS:.thy=.ML)
7ecdff86a5f0 Uses "suffix substitution" to shorten macro definitions. lcp parents: 752 diff changeset	48
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	49	test: ex/ROOT.ML $(BIN)/HOLCF $(EX_FILES)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	50	case "$(COMP)" in \
953 17d7fad9c9a2 Now calls exit_use instead of use, for prompt failure if errors are detected. lcp parents: 918 diff changeset	51	poly*) echo 'exit_use"ex/ROOT.ML"; quit();' \| $(COMP) $(BIN)/HOLCF ;;\
17d7fad9c9a2 Now calls exit_use instead of use, for prompt failure if errors are detected. lcp parents: 918 diff changeset	52	sml*) echo 'exit_use"ex/ROOT.ML"' \| $(BIN)/HOLCF;;\
468 3dd1dcb509ac Improved error checking lcp parents: 346 diff changeset	53	*) echo Bad value for ISABELLECOMP: \
3dd1dcb509ac Improved error checking lcp parents: 346 diff changeset	54	$(COMP) is not poly or sml;;\
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	55	esac
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	56
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	57	.PRECIOUS: $(BIN)/HOL $(BIN)/HOLCF
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	58

author	lcp
	Wed, 15 Mar 1995 10:34:47 +0100
changeset 953	17d7fad9c9a2
parent 918	7ecdff86a5f0
child 1274	ea0668a1c0ba
permissions	-rw-r--r--