|
1 ############################################################################### |
|
2 # METIS MAKEFILE |
|
3 # Copyright (c) 2001 Joe Hurd, distributed under the GNU GPL version 2 |
|
4 ############################################################################### |
|
5 |
|
6 .SUFFIXES: |
|
7 |
|
8 ############################################################################### |
|
9 # The default action. |
|
10 ############################################################################### |
|
11 |
|
12 .PHONY: default |
|
13 default: mosml |
|
14 |
|
15 ############################################################################### |
|
16 # Cleaning temporary files. |
|
17 ############################################################################### |
|
18 |
|
19 TEMP = \ |
|
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/*.o |
|
26 |
|
27 .PHONY: clean |
|
28 clean: |
|
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 |
|
42 test: |
|
43 $(MAKE) -C test |
|
44 |
|
45 ############################################################################### |
|
46 # Source files. |
|
47 ############################################################################### |
|
48 |
|
49 SRC = \ |
|
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 |
|
89 EXTRA_SRC = \ |
|
90 src/problems.sml |
|
91 |
|
92 ############################################################################### |
|
93 # The ML preprocessor. |
|
94 ############################################################################### |
|
95 |
|
96 MLPP = scripts/mlpp |
|
97 |
|
98 MLPP_OPTS = |
|
99 |
|
100 ############################################################################### |
|
101 # Building using Moscow ML. |
|
102 ############################################################################### |
|
103 |
|
104 MOSMLC = mosmlc -toplevel -q |
|
105 |
|
106 MOSML_SRC = \ |
|
107 src/Portable.sig src/PortableMosml.sml \ |
|
108 $(SRC) |
|
109 |
|
110 MOSML_TARGETS = \ |
|
111 bin/mosml/problems2tptp \ |
|
112 bin/mosml/metis |
|
113 |
|
114 include bin/mosml/Makefile.src |
|
115 |
|
116 .PHONY: mosml-info |
|
117 mosml-info: |
|
118 @echo |
|
119 @echo '*****************************************' |
|
120 @echo '* Build and test the Moscow ML programs *' |
|
121 @echo '*****************************************' |
|
122 @echo |
|
123 |
|
124 .PHONY: mosml |
|
125 mosml: mosml-info $(MOSML_OBJ) $(MOSML_TARGETS) test |
|
126 |
|
127 ############################################################################### |
|
128 # Building using MLton. |
|
129 ############################################################################### |
|
130 |
|
131 MLTON = mlton |
|
132 |
|
133 MLTON_OPTS = -runtime 'ram-slop 0.4' |
|
134 |
|
135 MLTON_SRC = \ |
|
136 src/Portable.sig src/PortableMlton.sml \ |
|
137 $(SRC) |
|
138 |
|
139 METIS = bin/mlton/metis |
|
140 |
|
141 MLTON_TARGETS = \ |
|
142 bin/mlton/selftest \ |
|
143 bin/mlton/problems2tptp \ |
|
144 $(METIS) |
|
145 |
|
146 bin/mlton/%.sml: $(MLTON_SRC) src/%.sml |
|
147 @$(MLPP) $(MLPP_OPTS) -c mlton $^ > $@ |
|
148 |
|
149 bin/mlton/%.mlb: bin/mlton/%.sml |
|
150 echo '$$(SML_LIB)/basis/basis.mlb $$(SML_LIB)/basis/mlton.mlb $(notdir $<)' > $@ |
|
151 |
|
152 bin/mlton/%: bin/mlton/%.mlb |
|
153 @echo |
|
154 @echo '***************************' |
|
155 @echo '* Compile a MLton program *' |
|
156 @echo '***************************' |
|
157 @echo |
|
158 @echo $@ |
|
159 cd bin/mlton ; $(MLTON) $(MLTON_OPTS) $(notdir $<) |
|
160 @echo |
|
161 |
|
162 .PHONY: mlton-info |
|
163 mlton-info: |
|
164 @echo |
|
165 @echo '*************************************' |
|
166 @echo '* Build and test the MLton programs *' |
|
167 @echo '*************************************' |
|
168 @echo |
|
169 |
|
170 .PHONY: mlton |
|
171 mlton: mlton-info $(MLTON_TARGETS) |
|
172 $(MAKE) -C test mlton |
|
173 |
|
174 ############################################################################### |
|
175 # Building using Poly/ML. |
|
176 ############################################################################### |
|
177 |
|
178 POLYML = poly |
|
179 |
|
180 POLYML_OPTS = |
|
181 |
|
182 POLYML_SRC = \ |
|
183 src/Random.sig src/Random.sml \ |
|
184 src/Portable.sig src/PortablePolyml.sml \ |
|
185 $(SRC) |
|
186 |
|
187 POLYML_TARGETS = \ |
|
188 bin/polyml/selftest \ |
|
189 bin/polyml/problems2tptp \ |
|
190 bin/polyml/metis |
|
191 |
|
192 bin/polyml/%.sml: src/%.sml $(POLYML_SRC) |
|
193 @$(MLPP) $(MLPP_OPTS) -c polyml $(POLYML_SRC) > $@ |
|
194 @echo 'fun main () = let' >> $@ |
|
195 @$(MLPP) $(MLPP_OPTS) -c polyml $< >> $@ |
|
196 @echo "in () end; PolyML.export(\"$(basename $(notdir $<))\", main);" >> $@ |
|
197 |
|
198 bin/polyml/%.o: bin/polyml/%.sml |
|
199 cd bin/polyml ; echo "use \"$(notdir $<)\";" | $(POLYML) $(POLYML_OPTS) |
|
200 |
|
201 bin/polyml/%: bin/polyml/%.o |
|
202 @echo |
|
203 @echo '*****************************' |
|
204 @echo '* Compile a Poly/ML program *' |
|
205 @echo '*****************************' |
|
206 @echo |
|
207 @echo $@ |
|
208 cd bin/polyml && $(CC) -o $(notdir $@) $(notdir $<) -lpolymain -lpolyml |
|
209 @echo |
|
210 |
|
211 .PHONY: polyml-info |
|
212 polyml-info: |
|
213 @echo |
|
214 @echo '***************************************' |
|
215 @echo '* Build and test the Poly/ML programs *' |
|
216 @echo '***************************************' |
|
217 @echo |
|
218 |
|
219 .PHONY: polyml |
|
220 polyml: polyml-info $(POLYML_TARGETS) |
|
221 $(MAKE) -C test polyml |
|
222 |
|
223 ############################################################################### |
|
224 # Development. |
|
225 ############################################################################## |
|
226 |
|
227 include Makefile.dev |
|
228 |
|
229 Makefile.dev: |
|
230 echo > $@ |