isabelle: src/Tools/Metis/Makefile@70f1994988d4 (annotated)

39433 3e41c9d29769 make "metis.ML" building process slightly more robust by eliminating the need for "FILES"; blanchet parents: diff changeset	1	###############################################################################
3e41c9d29769 make "metis.ML" building process slightly more robust by eliminating the need for "FILES"; blanchet parents: diff changeset	2	# METIS MAKEFILE
39444 beabb8443ee4 MIT license -> BSD License blanchet parents: 39443 diff changeset	3	# Copyright (c) 2001 Joe Hurd, distributed under the BSD License
39433 3e41c9d29769 make "metis.ML" building process slightly more robust by eliminating the need for "FILES"; blanchet parents: diff changeset	4	###############################################################################
3e41c9d29769 make "metis.ML" building process slightly more robust by eliminating the need for "FILES"; blanchet parents: diff changeset	5
3e41c9d29769 make "metis.ML" building process slightly more robust by eliminating the need for "FILES"; blanchet parents: diff changeset	6	.SUFFIXES:
3e41c9d29769 make "metis.ML" building process slightly more robust by eliminating the need for "FILES"; blanchet parents: diff changeset	7
3e41c9d29769 make "metis.ML" building process slightly more robust by eliminating the need for "FILES"; blanchet parents: diff changeset	8	###############################################################################
3e41c9d29769 make "metis.ML" building process slightly more robust by eliminating the need for "FILES"; blanchet parents: diff changeset	9	# The default action.
3e41c9d29769 make "metis.ML" building process slightly more robust by eliminating the need for "FILES"; blanchet parents: diff changeset	10	###############################################################################
3e41c9d29769 make "metis.ML" building process slightly more robust by eliminating the need for "FILES"; blanchet parents: diff changeset	11
3e41c9d29769 make "metis.ML" building process slightly more robust by eliminating the need for "FILES"; blanchet parents: diff changeset	12	.PHONY: default
3e41c9d29769 make "metis.ML" building process slightly more robust by eliminating the need for "FILES"; blanchet parents: diff changeset	13	default: mosml
3e41c9d29769 make "metis.ML" building process slightly more robust by eliminating the need for "FILES"; blanchet parents: diff changeset	14
3e41c9d29769 make "metis.ML" building process slightly more robust by eliminating the need for "FILES"; blanchet parents: diff changeset	15	###############################################################################
3e41c9d29769 make "metis.ML" building process slightly more robust by eliminating the need for "FILES"; blanchet parents: diff changeset	16	# Cleaning temporary files.
3e41c9d29769 make "metis.ML" building process slightly more robust by eliminating the need for "FILES"; blanchet parents: diff changeset	17	###############################################################################
3e41c9d29769 make "metis.ML" building process slightly more robust by eliminating the need for "FILES"; blanchet parents: diff changeset	18
3e41c9d29769 make "metis.ML" building process slightly more robust by eliminating the need for "FILES"; blanchet parents: diff changeset	19	TEMP = \
3e41c9d29769 make "metis.ML" building process slightly more robust by eliminating the need for "FILES"; blanchet parents: diff changeset	20	$(MOSML_TARGETS) \
3e41c9d29769 make "metis.ML" building process slightly more robust by eliminating the need for "FILES"; blanchet parents: diff changeset	21	bin/mosml/.sml bin/mosml/.ui bin/mosml/*.uo bin/mosml/a.out \
3e41c9d29769 make "metis.ML" building process slightly more robust by eliminating the need for "FILES"; blanchet parents: diff changeset	22	$(MLTON_TARGETS) \
3e41c9d29769 make "metis.ML" building process slightly more robust by eliminating the need for "FILES"; blanchet parents: diff changeset	23	bin/mlton/.sml bin/mlton/.mlb \
3e41c9d29769 make "metis.ML" building process slightly more robust by eliminating the need for "FILES"; blanchet parents: diff changeset	24	$(POLYML_TARGETS) \
43269 3535f16d9714 new Metis version blanchet parents: 42102 diff changeset	25	bin/polyml/.sml bin/polyml/.log bin/polyml/*.o
39433 3e41c9d29769 make "metis.ML" building process slightly more robust by eliminating the need for "FILES"; blanchet parents: diff changeset	26
3e41c9d29769 make "metis.ML" building process slightly more robust by eliminating the need for "FILES"; blanchet parents: diff changeset	27	.PHONY: clean
3e41c9d29769 make "metis.ML" building process slightly more robust by eliminating the need for "FILES"; blanchet parents: diff changeset	28	clean:
3e41c9d29769 make "metis.ML" building process slightly more robust by eliminating the need for "FILES"; blanchet parents: diff changeset	29	@echo
3e41c9d29769 make "metis.ML" building process slightly more robust by eliminating the need for "FILES"; blanchet parents: diff changeset	30	@echo '********************'
3e41c9d29769 make "metis.ML" building process slightly more robust by eliminating the need for "FILES"; blanchet parents: diff changeset	31	@echo '* Clean everything *'
3e41c9d29769 make "metis.ML" building process slightly more robust by eliminating the need for "FILES"; blanchet parents: diff changeset	32	@echo '********************'
3e41c9d29769 make "metis.ML" building process slightly more robust by eliminating the need for "FILES"; blanchet parents: diff changeset	33	@echo
3e41c9d29769 make "metis.ML" building process slightly more robust by eliminating the need for "FILES"; blanchet parents: diff changeset	34	rm -f $(TEMP)
3e41c9d29769 make "metis.ML" building process slightly more robust by eliminating the need for "FILES"; blanchet parents: diff changeset	35	$(MAKE) -C test $@
3e41c9d29769 make "metis.ML" building process slightly more robust by eliminating the need for "FILES"; blanchet parents: diff changeset	36
3e41c9d29769 make "metis.ML" building process slightly more robust by eliminating the need for "FILES"; blanchet parents: diff changeset	37	###############################################################################
3e41c9d29769 make "metis.ML" building process slightly more robust by eliminating the need for "FILES"; blanchet parents: diff changeset	38	# Testing.
3e41c9d29769 make "metis.ML" building process slightly more robust by eliminating the need for "FILES"; blanchet parents: diff changeset	39	###############################################################################
3e41c9d29769 make "metis.ML" building process slightly more robust by eliminating the need for "FILES"; blanchet parents: diff changeset	40
3e41c9d29769 make "metis.ML" building process slightly more robust by eliminating the need for "FILES"; blanchet parents: diff changeset	41	.PHONY: test
3e41c9d29769 make "metis.ML" building process slightly more robust by eliminating the need for "FILES"; blanchet parents: diff changeset	42	test:
3e41c9d29769 make "metis.ML" building process slightly more robust by eliminating the need for "FILES"; blanchet parents: diff changeset	43	$(MAKE) -C test
3e41c9d29769 make "metis.ML" building process slightly more robust by eliminating the need for "FILES"; blanchet parents: diff changeset	44
3e41c9d29769 make "metis.ML" building process slightly more robust by eliminating the need for "FILES"; blanchet parents: diff changeset	45	###############################################################################
3e41c9d29769 make "metis.ML" building process slightly more robust by eliminating the need for "FILES"; blanchet parents: diff changeset	46	# Source files.
3e41c9d29769 make "metis.ML" building process slightly more robust by eliminating the need for "FILES"; blanchet parents: diff changeset	47	###############################################################################
3e41c9d29769 make "metis.ML" building process slightly more robust by eliminating the need for "FILES"; blanchet parents: diff changeset	48
3e41c9d29769 make "metis.ML" building process slightly more robust by eliminating the need for "FILES"; blanchet parents: diff changeset	49	SRC = \
3e41c9d29769 make "metis.ML" building process slightly more robust by eliminating the need for "FILES"; blanchet parents: diff changeset	50	src/Useful.sig src/Useful.sml \
3e41c9d29769 make "metis.ML" building process slightly more robust by eliminating the need for "FILES"; blanchet parents: diff changeset	51	src/Lazy.sig src/Lazy.sml \
3e41c9d29769 make "metis.ML" building process slightly more robust by eliminating the need for "FILES"; blanchet parents: diff changeset	52	src/Ordered.sig src/Ordered.sml \
3e41c9d29769 make "metis.ML" building process slightly more robust by eliminating the need for "FILES"; blanchet parents: diff changeset	53	src/Map.sig src/Map.sml \
3e41c9d29769 make "metis.ML" building process slightly more robust by eliminating the need for "FILES"; blanchet parents: diff changeset	54	src/KeyMap.sig src/KeyMap.sml \
3e41c9d29769 make "metis.ML" building process slightly more robust by eliminating the need for "FILES"; blanchet parents: diff changeset	55	src/Set.sig src/Set.sml \
3e41c9d29769 make "metis.ML" building process slightly more robust by eliminating the need for "FILES"; blanchet parents: diff changeset	56	src/ElementSet.sig src/ElementSet.sml \
3e41c9d29769 make "metis.ML" building process slightly more robust by eliminating the need for "FILES"; blanchet parents: diff changeset	57	src/Sharing.sig src/Sharing.sml \
3e41c9d29769 make "metis.ML" building process slightly more robust by eliminating the need for "FILES"; blanchet parents: diff changeset	58	src/Stream.sig src/Stream.sml \
3e41c9d29769 make "metis.ML" building process slightly more robust by eliminating the need for "FILES"; blanchet parents: diff changeset	59	src/Heap.sig src/Heap.sml \
3e41c9d29769 make "metis.ML" building process slightly more robust by eliminating the need for "FILES"; blanchet parents: diff changeset	60	src/Print.sig src/Print.sml \
3e41c9d29769 make "metis.ML" building process slightly more robust by eliminating the need for "FILES"; blanchet parents: diff changeset	61	src/Parse.sig src/Parse.sml \
3e41c9d29769 make "metis.ML" building process slightly more robust by eliminating the need for "FILES"; blanchet parents: diff changeset	62	src/Name.sig src/Name.sml \
3e41c9d29769 make "metis.ML" building process slightly more robust by eliminating the need for "FILES"; blanchet parents: diff changeset	63	src/NameArity.sig src/NameArity.sml \
3e41c9d29769 make "metis.ML" building process slightly more robust by eliminating the need for "FILES"; blanchet parents: diff changeset	64	src/Term.sig src/Term.sml \
3e41c9d29769 make "metis.ML" building process slightly more robust by eliminating the need for "FILES"; blanchet parents: diff changeset	65	src/Subst.sig src/Subst.sml \
3e41c9d29769 make "metis.ML" building process slightly more robust by eliminating the need for "FILES"; blanchet parents: diff changeset	66	src/Atom.sig src/Atom.sml \
3e41c9d29769 make "metis.ML" building process slightly more robust by eliminating the need for "FILES"; blanchet parents: diff changeset	67	src/Formula.sig src/Formula.sml \
3e41c9d29769 make "metis.ML" building process slightly more robust by eliminating the need for "FILES"; blanchet parents: diff changeset	68	src/Literal.sig src/Literal.sml \
3e41c9d29769 make "metis.ML" building process slightly more robust by eliminating the need for "FILES"; blanchet parents: diff changeset	69	src/Thm.sig src/Thm.sml \
3e41c9d29769 make "metis.ML" building process slightly more robust by eliminating the need for "FILES"; blanchet parents: diff changeset	70	src/Proof.sig src/Proof.sml \
3e41c9d29769 make "metis.ML" building process slightly more robust by eliminating the need for "FILES"; blanchet parents: diff changeset	71	src/Rule.sig src/Rule.sml \
3e41c9d29769 make "metis.ML" building process slightly more robust by eliminating the need for "FILES"; blanchet parents: diff changeset	72	src/Normalize.sig src/Normalize.sml \
3e41c9d29769 make "metis.ML" building process slightly more robust by eliminating the need for "FILES"; blanchet parents: diff changeset	73	src/Model.sig src/Model.sml \
3e41c9d29769 make "metis.ML" building process slightly more robust by eliminating the need for "FILES"; blanchet parents: diff changeset	74	src/Problem.sig src/Problem.sml \
3e41c9d29769 make "metis.ML" building process slightly more robust by eliminating the need for "FILES"; blanchet parents: diff changeset	75	src/TermNet.sig src/TermNet.sml \
3e41c9d29769 make "metis.ML" building process slightly more robust by eliminating the need for "FILES"; blanchet parents: diff changeset	76	src/AtomNet.sig src/AtomNet.sml \
3e41c9d29769 make "metis.ML" building process slightly more robust by eliminating the need for "FILES"; blanchet parents: diff changeset	77	src/LiteralNet.sig src/LiteralNet.sml \
3e41c9d29769 make "metis.ML" building process slightly more robust by eliminating the need for "FILES"; blanchet parents: diff changeset	78	src/Subsume.sig src/Subsume.sml \
3e41c9d29769 make "metis.ML" building process slightly more robust by eliminating the need for "FILES"; blanchet parents: diff changeset	79	src/KnuthBendixOrder.sig src/KnuthBendixOrder.sml \
3e41c9d29769 make "metis.ML" building process slightly more robust by eliminating the need for "FILES"; blanchet parents: diff changeset	80	src/Rewrite.sig src/Rewrite.sml \
3e41c9d29769 make "metis.ML" building process slightly more robust by eliminating the need for "FILES"; blanchet parents: diff changeset	81	src/Units.sig src/Units.sml \
3e41c9d29769 make "metis.ML" building process slightly more robust by eliminating the need for "FILES"; blanchet parents: diff changeset	82	src/Clause.sig src/Clause.sml \
3e41c9d29769 make "metis.ML" building process slightly more robust by eliminating the need for "FILES"; blanchet parents: diff changeset	83	src/Active.sig src/Active.sml \
3e41c9d29769 make "metis.ML" building process slightly more robust by eliminating the need for "FILES"; blanchet parents: diff changeset	84	src/Waiting.sig src/Waiting.sml \
3e41c9d29769 make "metis.ML" building process slightly more robust by eliminating the need for "FILES"; blanchet parents: diff changeset	85	src/Resolution.sig src/Resolution.sml \
3e41c9d29769 make "metis.ML" building process slightly more robust by eliminating the need for "FILES"; blanchet parents: diff changeset	86	src/Tptp.sig src/Tptp.sml \
3e41c9d29769 make "metis.ML" building process slightly more robust by eliminating the need for "FILES"; blanchet parents: diff changeset	87	src/Options.sig src/Options.sml
3e41c9d29769 make "metis.ML" building process slightly more robust by eliminating the need for "FILES"; blanchet parents: diff changeset	88
3e41c9d29769 make "metis.ML" building process slightly more robust by eliminating the need for "FILES"; blanchet parents: diff changeset	89	EXTRA_SRC = \
3e41c9d29769 make "metis.ML" building process slightly more robust by eliminating the need for "FILES"; blanchet parents: diff changeset	90	src/problems.sml
3e41c9d29769 make "metis.ML" building process slightly more robust by eliminating the need for "FILES"; blanchet parents: diff changeset	91
3e41c9d29769 make "metis.ML" building process slightly more robust by eliminating the need for "FILES"; blanchet parents: diff changeset	92	###############################################################################
3e41c9d29769 make "metis.ML" building process slightly more robust by eliminating the need for "FILES"; blanchet parents: diff changeset	93	# The ML preprocessor.
3e41c9d29769 make "metis.ML" building process slightly more robust by eliminating the need for "FILES"; blanchet parents: diff changeset	94	###############################################################################
3e41c9d29769 make "metis.ML" building process slightly more robust by eliminating the need for "FILES"; blanchet parents: diff changeset	95
3e41c9d29769 make "metis.ML" building process slightly more robust by eliminating the need for "FILES"; blanchet parents: diff changeset	96	MLPP = scripts/mlpp
3e41c9d29769 make "metis.ML" building process slightly more robust by eliminating the need for "FILES"; blanchet parents: diff changeset	97
3e41c9d29769 make "metis.ML" building process slightly more robust by eliminating the need for "FILES"; blanchet parents: diff changeset	98	MLPP_OPTS =
3e41c9d29769 make "metis.ML" building process slightly more robust by eliminating the need for "FILES"; blanchet parents: diff changeset	99
3e41c9d29769 make "metis.ML" building process slightly more robust by eliminating the need for "FILES"; blanchet parents: diff changeset	100	###############################################################################
3e41c9d29769 make "metis.ML" building process slightly more robust by eliminating the need for "FILES"; blanchet parents: diff changeset	101	# Building using Moscow ML.
3e41c9d29769 make "metis.ML" building process slightly more robust by eliminating the need for "FILES"; blanchet parents: diff changeset	102	###############################################################################
3e41c9d29769 make "metis.ML" building process slightly more robust by eliminating the need for "FILES"; blanchet parents: diff changeset	103
3e41c9d29769 make "metis.ML" building process slightly more robust by eliminating the need for "FILES"; blanchet parents: diff changeset	104	MOSMLC = mosmlc -toplevel -q
3e41c9d29769 make "metis.ML" building process slightly more robust by eliminating the need for "FILES"; blanchet parents: diff changeset	105
3e41c9d29769 make "metis.ML" building process slightly more robust by eliminating the need for "FILES"; blanchet parents: diff changeset	106	MOSML_SRC = \
3e41c9d29769 make "metis.ML" building process slightly more robust by eliminating the need for "FILES"; blanchet parents: diff changeset	107	src/Portable.sig src/PortableMosml.sml \
3e41c9d29769 make "metis.ML" building process slightly more robust by eliminating the need for "FILES"; blanchet parents: diff changeset	108	$(SRC)
3e41c9d29769 make "metis.ML" building process slightly more robust by eliminating the need for "FILES"; blanchet parents: diff changeset	109
3e41c9d29769 make "metis.ML" building process slightly more robust by eliminating the need for "FILES"; blanchet parents: diff changeset	110	MOSML_TARGETS = \
3e41c9d29769 make "metis.ML" building process slightly more robust by eliminating the need for "FILES"; blanchet parents: diff changeset	111	bin/mosml/problems2tptp \
3e41c9d29769 make "metis.ML" building process slightly more robust by eliminating the need for "FILES"; blanchet parents: diff changeset	112	bin/mosml/metis
3e41c9d29769 make "metis.ML" building process slightly more robust by eliminating the need for "FILES"; blanchet parents: diff changeset	113
3e41c9d29769 make "metis.ML" building process slightly more robust by eliminating the need for "FILES"; blanchet parents: diff changeset	114	include bin/mosml/Makefile.src
3e41c9d29769 make "metis.ML" building process slightly more robust by eliminating the need for "FILES"; blanchet parents: diff changeset	115
3e41c9d29769 make "metis.ML" building process slightly more robust by eliminating the need for "FILES"; blanchet parents: diff changeset	116	.PHONY: mosml-info
3e41c9d29769 make "metis.ML" building process slightly more robust by eliminating the need for "FILES"; blanchet parents: diff changeset	117	mosml-info:
3e41c9d29769 make "metis.ML" building process slightly more robust by eliminating the need for "FILES"; blanchet parents: diff changeset	118	@echo
3e41c9d29769 make "metis.ML" building process slightly more robust by eliminating the need for "FILES"; blanchet parents: diff changeset	119	@echo '*****************************************'
3e41c9d29769 make "metis.ML" building process slightly more robust by eliminating the need for "FILES"; blanchet parents: diff changeset	120	@echo '* Build and test the Moscow ML programs *'
3e41c9d29769 make "metis.ML" building process slightly more robust by eliminating the need for "FILES"; blanchet parents: diff changeset	121	@echo '*****************************************'
3e41c9d29769 make "metis.ML" building process slightly more robust by eliminating the need for "FILES"; blanchet parents: diff changeset	122	@echo
3e41c9d29769 make "metis.ML" building process slightly more robust by eliminating the need for "FILES"; blanchet parents: diff changeset	123
3e41c9d29769 make "metis.ML" building process slightly more robust by eliminating the need for "FILES"; blanchet parents: diff changeset	124	.PHONY: mosml
3e41c9d29769 make "metis.ML" building process slightly more robust by eliminating the need for "FILES"; blanchet parents: diff changeset	125	mosml: mosml-info $(MOSML_OBJ) $(MOSML_TARGETS) test
3e41c9d29769 make "metis.ML" building process slightly more robust by eliminating the need for "FILES"; blanchet parents: diff changeset	126
3e41c9d29769 make "metis.ML" building process slightly more robust by eliminating the need for "FILES"; blanchet parents: diff changeset	127	###############################################################################
3e41c9d29769 make "metis.ML" building process slightly more robust by eliminating the need for "FILES"; blanchet parents: diff changeset	128	# Building using MLton.
3e41c9d29769 make "metis.ML" building process slightly more robust by eliminating the need for "FILES"; blanchet parents: diff changeset	129	###############################################################################
3e41c9d29769 make "metis.ML" building process slightly more robust by eliminating the need for "FILES"; blanchet parents: diff changeset	130
3e41c9d29769 make "metis.ML" building process slightly more robust by eliminating the need for "FILES"; blanchet parents: diff changeset	131	MLTON = mlton
3e41c9d29769 make "metis.ML" building process slightly more robust by eliminating the need for "FILES"; blanchet parents: diff changeset	132
3e41c9d29769 make "metis.ML" building process slightly more robust by eliminating the need for "FILES"; blanchet parents: diff changeset	133	MLTON_OPTS = -runtime 'ram-slop 0.4'
3e41c9d29769 make "metis.ML" building process slightly more robust by eliminating the need for "FILES"; blanchet parents: diff changeset	134
3e41c9d29769 make "metis.ML" building process slightly more robust by eliminating the need for "FILES"; blanchet parents: diff changeset	135	MLTON_SRC = \
3e41c9d29769 make "metis.ML" building process slightly more robust by eliminating the need for "FILES"; blanchet parents: diff changeset	136	src/Portable.sig src/PortableMlton.sml \
3e41c9d29769 make "metis.ML" building process slightly more robust by eliminating the need for "FILES"; blanchet parents: diff changeset	137	$(SRC)
3e41c9d29769 make "metis.ML" building process slightly more robust by eliminating the need for "FILES"; blanchet parents: diff changeset	138
3e41c9d29769 make "metis.ML" building process slightly more robust by eliminating the need for "FILES"; blanchet parents: diff changeset	139	METIS = bin/mlton/metis
3e41c9d29769 make "metis.ML" building process slightly more robust by eliminating the need for "FILES"; blanchet parents: diff changeset	140
43269 3535f16d9714 new Metis version blanchet parents: 42102 diff changeset	141	PROBLEMS2TPTP = bin/mlton/problems2tptp
3535f16d9714 new Metis version blanchet parents: 42102 diff changeset	142
39433 3e41c9d29769 make "metis.ML" building process slightly more robust by eliminating the need for "FILES"; blanchet parents: diff changeset	143	MLTON_TARGETS = \
3e41c9d29769 make "metis.ML" building process slightly more robust by eliminating the need for "FILES"; blanchet parents: diff changeset	144	bin/mlton/selftest \
43269 3535f16d9714 new Metis version blanchet parents: 42102 diff changeset	145	$(METIS) \
3535f16d9714 new Metis version blanchet parents: 42102 diff changeset	146	$(PROBLEMS2TPTP)
39433 3e41c9d29769 make "metis.ML" building process slightly more robust by eliminating the need for "FILES"; blanchet parents: diff changeset	147
3e41c9d29769 make "metis.ML" building process slightly more robust by eliminating the need for "FILES"; blanchet parents: diff changeset	148	bin/mlton/%.sml: $(MLTON_SRC) src/%.sml
3e41c9d29769 make "metis.ML" building process slightly more robust by eliminating the need for "FILES"; blanchet parents: diff changeset	149	@$(MLPP) $(MLPP_OPTS) -c mlton $^ > $@
3e41c9d29769 make "metis.ML" building process slightly more robust by eliminating the need for "FILES"; blanchet parents: diff changeset	150
3e41c9d29769 make "metis.ML" building process slightly more robust by eliminating the need for "FILES"; blanchet parents: diff changeset	151	bin/mlton/%.mlb: bin/mlton/%.sml
3e41c9d29769 make "metis.ML" building process slightly more robust by eliminating the need for "FILES"; blanchet parents: diff changeset	152	echo '$$(SML_LIB)/basis/basis.mlb $$(SML_LIB)/basis/mlton.mlb $(notdir $<)' > $@
3e41c9d29769 make "metis.ML" building process slightly more robust by eliminating the need for "FILES"; blanchet parents: diff changeset	153
3e41c9d29769 make "metis.ML" building process slightly more robust by eliminating the need for "FILES"; blanchet parents: diff changeset	154	bin/mlton/%: bin/mlton/%.mlb
3e41c9d29769 make "metis.ML" building process slightly more robust by eliminating the need for "FILES"; blanchet parents: diff changeset	155	@echo
3e41c9d29769 make "metis.ML" building process slightly more robust by eliminating the need for "FILES"; blanchet parents: diff changeset	156	@echo '***************************'
3e41c9d29769 make "metis.ML" building process slightly more robust by eliminating the need for "FILES"; blanchet parents: diff changeset	157	@echo '* Compile a MLton program *'
3e41c9d29769 make "metis.ML" building process slightly more robust by eliminating the need for "FILES"; blanchet parents: diff changeset	158	@echo '***************************'
3e41c9d29769 make "metis.ML" building process slightly more robust by eliminating the need for "FILES"; blanchet parents: diff changeset	159	@echo
3e41c9d29769 make "metis.ML" building process slightly more robust by eliminating the need for "FILES"; blanchet parents: diff changeset	160	@echo $@
3e41c9d29769 make "metis.ML" building process slightly more robust by eliminating the need for "FILES"; blanchet parents: diff changeset	161	cd bin/mlton ; $(MLTON) $(MLTON_OPTS) $(notdir $<)
3e41c9d29769 make "metis.ML" building process slightly more robust by eliminating the need for "FILES"; blanchet parents: diff changeset	162	@echo
3e41c9d29769 make "metis.ML" building process slightly more robust by eliminating the need for "FILES"; blanchet parents: diff changeset	163
3e41c9d29769 make "metis.ML" building process slightly more robust by eliminating the need for "FILES"; blanchet parents: diff changeset	164	.PHONY: mlton-info
3e41c9d29769 make "metis.ML" building process slightly more robust by eliminating the need for "FILES"; blanchet parents: diff changeset	165	mlton-info:
3e41c9d29769 make "metis.ML" building process slightly more robust by eliminating the need for "FILES"; blanchet parents: diff changeset	166	@echo
3e41c9d29769 make "metis.ML" building process slightly more robust by eliminating the need for "FILES"; blanchet parents: diff changeset	167	@echo '*************************************'
3e41c9d29769 make "metis.ML" building process slightly more robust by eliminating the need for "FILES"; blanchet parents: diff changeset	168	@echo '* Build and test the MLton programs *'
3e41c9d29769 make "metis.ML" building process slightly more robust by eliminating the need for "FILES"; blanchet parents: diff changeset	169	@echo '*************************************'
3e41c9d29769 make "metis.ML" building process slightly more robust by eliminating the need for "FILES"; blanchet parents: diff changeset	170	@echo
3e41c9d29769 make "metis.ML" building process slightly more robust by eliminating the need for "FILES"; blanchet parents: diff changeset	171
3e41c9d29769 make "metis.ML" building process slightly more robust by eliminating the need for "FILES"; blanchet parents: diff changeset	172	.PHONY: mlton
3e41c9d29769 make "metis.ML" building process slightly more robust by eliminating the need for "FILES"; blanchet parents: diff changeset	173	mlton: mlton-info $(MLTON_TARGETS)
3e41c9d29769 make "metis.ML" building process slightly more robust by eliminating the need for "FILES"; blanchet parents: diff changeset	174	$(MAKE) -C test mlton
3e41c9d29769 make "metis.ML" building process slightly more robust by eliminating the need for "FILES"; blanchet parents: diff changeset	175
3e41c9d29769 make "metis.ML" building process slightly more robust by eliminating the need for "FILES"; blanchet parents: diff changeset	176	###############################################################################
3e41c9d29769 make "metis.ML" building process slightly more robust by eliminating the need for "FILES"; blanchet parents: diff changeset	177	# Building using Poly/ML.
3e41c9d29769 make "metis.ML" building process slightly more robust by eliminating the need for "FILES"; blanchet parents: diff changeset	178	###############################################################################
3e41c9d29769 make "metis.ML" building process slightly more robust by eliminating the need for "FILES"; blanchet parents: diff changeset	179
3e41c9d29769 make "metis.ML" building process slightly more robust by eliminating the need for "FILES"; blanchet parents: diff changeset	180	POLYML = poly
3e41c9d29769 make "metis.ML" building process slightly more robust by eliminating the need for "FILES"; blanchet parents: diff changeset	181
3e41c9d29769 make "metis.ML" building process slightly more robust by eliminating the need for "FILES"; blanchet parents: diff changeset	182	POLYML_OPTS =
3e41c9d29769 make "metis.ML" building process slightly more robust by eliminating the need for "FILES"; blanchet parents: diff changeset	183
42102 fcfd07f122d4 new version of Metis 2.3 (29 Dec. 2010) blanchet parents: 39444 diff changeset	184	ifeq ($(shell uname), Darwin)
fcfd07f122d4 new version of Metis 2.3 (29 Dec. 2010) blanchet parents: 39444 diff changeset	185	POLYML_LINK_OPTS = -lpolymain -lpolyml -segprot POLY rwx rwx
fcfd07f122d4 new version of Metis 2.3 (29 Dec. 2010) blanchet parents: 39444 diff changeset	186	else
fcfd07f122d4 new version of Metis 2.3 (29 Dec. 2010) blanchet parents: 39444 diff changeset	187	POLYML_LINK_OPTS = -lpolymain -lpolyml
fcfd07f122d4 new version of Metis 2.3 (29 Dec. 2010) blanchet parents: 39444 diff changeset	188	endif
fcfd07f122d4 new version of Metis 2.3 (29 Dec. 2010) blanchet parents: 39444 diff changeset	189
39433 3e41c9d29769 make "metis.ML" building process slightly more robust by eliminating the need for "FILES"; blanchet parents: diff changeset	190	POLYML_SRC = \
3e41c9d29769 make "metis.ML" building process slightly more robust by eliminating the need for "FILES"; blanchet parents: diff changeset	191	src/Random.sig src/Random.sml \
3e41c9d29769 make "metis.ML" building process slightly more robust by eliminating the need for "FILES"; blanchet parents: diff changeset	192	src/Portable.sig src/PortablePolyml.sml \
3e41c9d29769 make "metis.ML" building process slightly more robust by eliminating the need for "FILES"; blanchet parents: diff changeset	193	$(SRC)
3e41c9d29769 make "metis.ML" building process slightly more robust by eliminating the need for "FILES"; blanchet parents: diff changeset	194
3e41c9d29769 make "metis.ML" building process slightly more robust by eliminating the need for "FILES"; blanchet parents: diff changeset	195	POLYML_TARGETS = \
3e41c9d29769 make "metis.ML" building process slightly more robust by eliminating the need for "FILES"; blanchet parents: diff changeset	196	bin/polyml/selftest \
3e41c9d29769 make "metis.ML" building process slightly more robust by eliminating the need for "FILES"; blanchet parents: diff changeset	197	bin/polyml/problems2tptp \
3e41c9d29769 make "metis.ML" building process slightly more robust by eliminating the need for "FILES"; blanchet parents: diff changeset	198	bin/polyml/metis
3e41c9d29769 make "metis.ML" building process slightly more robust by eliminating the need for "FILES"; blanchet parents: diff changeset	199
3e41c9d29769 make "metis.ML" building process slightly more robust by eliminating the need for "FILES"; blanchet parents: diff changeset	200	bin/polyml/%.sml: src/%.sml $(POLYML_SRC)
3e41c9d29769 make "metis.ML" building process slightly more robust by eliminating the need for "FILES"; blanchet parents: diff changeset	201	@$(MLPP) $(MLPP_OPTS) -c polyml $(POLYML_SRC) > $@
3e41c9d29769 make "metis.ML" building process slightly more robust by eliminating the need for "FILES"; blanchet parents: diff changeset	202	@echo 'fun main () = let' >> $@
3e41c9d29769 make "metis.ML" building process slightly more robust by eliminating the need for "FILES"; blanchet parents: diff changeset	203	@$(MLPP) $(MLPP_OPTS) -c polyml $< >> $@
3e41c9d29769 make "metis.ML" building process slightly more robust by eliminating the need for "FILES"; blanchet parents: diff changeset	204	@echo "in () end; PolyML.export(\"$(basename $(notdir $<))\", main);" >> $@
3e41c9d29769 make "metis.ML" building process slightly more robust by eliminating the need for "FILES"; blanchet parents: diff changeset	205
3e41c9d29769 make "metis.ML" building process slightly more robust by eliminating the need for "FILES"; blanchet parents: diff changeset	206	bin/polyml/%.o: bin/polyml/%.sml
43269 3535f16d9714 new Metis version blanchet parents: 42102 diff changeset	207	cd bin/polyml ; echo "use \"$(notdir $<)\";" \| $(POLYML) $(POLYML_OPTS) > $(basename $(notdir $<)).log
3535f16d9714 new Metis version blanchet parents: 42102 diff changeset	208	@if test $@ -nt $< ; then echo 'compiled $@' ; else cat bin/polyml/$(basename $(notdir $<)).log ; exit 1 ; fi
39433 3e41c9d29769 make "metis.ML" building process slightly more robust by eliminating the need for "FILES"; blanchet parents: diff changeset	209
3e41c9d29769 make "metis.ML" building process slightly more robust by eliminating the need for "FILES"; blanchet parents: diff changeset	210	bin/polyml/%: bin/polyml/%.o
3e41c9d29769 make "metis.ML" building process slightly more robust by eliminating the need for "FILES"; blanchet parents: diff changeset	211	@echo
3e41c9d29769 make "metis.ML" building process slightly more robust by eliminating the need for "FILES"; blanchet parents: diff changeset	212	@echo '*****************************'
3e41c9d29769 make "metis.ML" building process slightly more robust by eliminating the need for "FILES"; blanchet parents: diff changeset	213	@echo '* Compile a Poly/ML program *'
3e41c9d29769 make "metis.ML" building process slightly more robust by eliminating the need for "FILES"; blanchet parents: diff changeset	214	@echo '*****************************'
3e41c9d29769 make "metis.ML" building process slightly more robust by eliminating the need for "FILES"; blanchet parents: diff changeset	215	@echo
3e41c9d29769 make "metis.ML" building process slightly more robust by eliminating the need for "FILES"; blanchet parents: diff changeset	216	@echo $@
42102 fcfd07f122d4 new version of Metis 2.3 (29 Dec. 2010) blanchet parents: 39444 diff changeset	217	cd bin/polyml && $(CC) -o $(notdir $@) $(notdir $<) $(POLYML_LINK_OPTS)
39433 3e41c9d29769 make "metis.ML" building process slightly more robust by eliminating the need for "FILES"; blanchet parents: diff changeset	218	@echo
3e41c9d29769 make "metis.ML" building process slightly more robust by eliminating the need for "FILES"; blanchet parents: diff changeset	219
3e41c9d29769 make "metis.ML" building process slightly more robust by eliminating the need for "FILES"; blanchet parents: diff changeset	220	.PHONY: polyml-info
3e41c9d29769 make "metis.ML" building process slightly more robust by eliminating the need for "FILES"; blanchet parents: diff changeset	221	polyml-info:
3e41c9d29769 make "metis.ML" building process slightly more robust by eliminating the need for "FILES"; blanchet parents: diff changeset	222	@echo
3e41c9d29769 make "metis.ML" building process slightly more robust by eliminating the need for "FILES"; blanchet parents: diff changeset	223	@echo '***************************************'
3e41c9d29769 make "metis.ML" building process slightly more robust by eliminating the need for "FILES"; blanchet parents: diff changeset	224	@echo '* Build and test the Poly/ML programs *'
3e41c9d29769 make "metis.ML" building process slightly more robust by eliminating the need for "FILES"; blanchet parents: diff changeset	225	@echo '***************************************'
3e41c9d29769 make "metis.ML" building process slightly more robust by eliminating the need for "FILES"; blanchet parents: diff changeset	226	@echo
3e41c9d29769 make "metis.ML" building process slightly more robust by eliminating the need for "FILES"; blanchet parents: diff changeset	227
3e41c9d29769 make "metis.ML" building process slightly more robust by eliminating the need for "FILES"; blanchet parents: diff changeset	228	.PHONY: polyml
3e41c9d29769 make "metis.ML" building process slightly more robust by eliminating the need for "FILES"; blanchet parents: diff changeset	229	polyml: polyml-info $(POLYML_TARGETS)
3e41c9d29769 make "metis.ML" building process slightly more robust by eliminating the need for "FILES"; blanchet parents: diff changeset	230	$(MAKE) -C test polyml
3e41c9d29769 make "metis.ML" building process slightly more robust by eliminating the need for "FILES"; blanchet parents: diff changeset	231
3e41c9d29769 make "metis.ML" building process slightly more robust by eliminating the need for "FILES"; blanchet parents: diff changeset	232	###############################################################################
3e41c9d29769 make "metis.ML" building process slightly more robust by eliminating the need for "FILES"; blanchet parents: diff changeset	233	# Development.
3e41c9d29769 make "metis.ML" building process slightly more robust by eliminating the need for "FILES"; blanchet parents: diff changeset	234	##############################################################################
3e41c9d29769 make "metis.ML" building process slightly more robust by eliminating the need for "FILES"; blanchet parents: diff changeset	235
3e41c9d29769 make "metis.ML" building process slightly more robust by eliminating the need for "FILES"; blanchet parents: diff changeset	236	include Makefile.dev
3e41c9d29769 make "metis.ML" building process slightly more robust by eliminating the need for "FILES"; blanchet parents: diff changeset	237
3e41c9d29769 make "metis.ML" building process slightly more robust by eliminating the need for "FILES"; blanchet parents: diff changeset	238	Makefile.dev:
3e41c9d29769 make "metis.ML" building process slightly more robust by eliminating the need for "FILES"; blanchet parents: diff changeset	239	echo > $@

author	wenzelm
	Fri, 11 Jan 2019 22:34:28 +0100
changeset 69634	70f1994988d4
parent 43269	3535f16d9714
child 72004	913162a47d9f
permissions	-rw-r--r--