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