###############################################################################
# METIS MAKEFILE
# Copyright (c) 2001 Joe Hurd, distributed under the BSD License
###############################################################################
.SUFFIXES:
###############################################################################
# The default action.
###############################################################################
.PHONY: default
default: mosml
###############################################################################
# Cleaning temporary files.
###############################################################################
TEMP = \
$(MOSML_TARGETS) \
bin/mosml/*.sml bin/mosml/*.ui bin/mosml/*.uo bin/mosml/a.out \
$(MLTON_TARGETS) \
bin/mlton/*.sml bin/mlton/*.mlb \
$(POLYML_TARGETS) \
bin/polyml/*.sml bin/polyml/*.log bin/polyml/*.o
.PHONY: clean
clean:
@echo
@echo '********************'
@echo '* Clean everything *'
@echo '********************'
@echo
rm -f $(TEMP)
$(MAKE) -C test $@
###############################################################################
# Testing.
###############################################################################
.PHONY: test
test:
$(MAKE) -C test
###############################################################################
# Source files.
###############################################################################
SRC = \
src/Useful.sig src/Useful.sml \
src/Lazy.sig src/Lazy.sml \
src/Ordered.sig src/Ordered.sml \
src/Map.sig src/Map.sml \
src/KeyMap.sig src/KeyMap.sml \
src/Set.sig src/Set.sml \
src/ElementSet.sig src/ElementSet.sml \
src/Sharing.sig src/Sharing.sml \
src/Stream.sig src/Stream.sml \
src/Heap.sig src/Heap.sml \
src/Print.sig src/Print.sml \
src/Parse.sig src/Parse.sml \
src/Name.sig src/Name.sml \
src/NameArity.sig src/NameArity.sml \
src/Term.sig src/Term.sml \
src/Subst.sig src/Subst.sml \
src/Atom.sig src/Atom.sml \
src/Formula.sig src/Formula.sml \
src/Literal.sig src/Literal.sml \
src/Thm.sig src/Thm.sml \
src/Proof.sig src/Proof.sml \
src/Rule.sig src/Rule.sml \
src/Normalize.sig src/Normalize.sml \
src/Model.sig src/Model.sml \
src/Problem.sig src/Problem.sml \
src/TermNet.sig src/TermNet.sml \
src/AtomNet.sig src/AtomNet.sml \
src/LiteralNet.sig src/LiteralNet.sml \
src/Subsume.sig src/Subsume.sml \
src/KnuthBendixOrder.sig src/KnuthBendixOrder.sml \
src/Rewrite.sig src/Rewrite.sml \
src/Units.sig src/Units.sml \
src/Clause.sig src/Clause.sml \
src/Active.sig src/Active.sml \
src/Waiting.sig src/Waiting.sml \
src/Resolution.sig src/Resolution.sml \
src/Tptp.sig src/Tptp.sml \
src/Options.sig src/Options.sml
EXTRA_SRC = \
src/problems.sml
###############################################################################
# The ML preprocessor.
###############################################################################
MLPP = scripts/mlpp
MLPP_OPTS =
###############################################################################
# Building using Moscow ML.
###############################################################################
MOSMLC = mosmlc -toplevel -q
MOSML_SRC = \
src/Portable.sig src/PortableMosml.sml \
$(SRC)
MOSML_TARGETS = \
bin/mosml/problems2tptp \
bin/mosml/metis
include bin/mosml/Makefile.src
.PHONY: mosml-info
mosml-info:
@echo
@echo '*****************************************'
@echo '* Build and test the Moscow ML programs *'
@echo '*****************************************'
@echo
.PHONY: mosml
mosml: mosml-info $(MOSML_OBJ) $(MOSML_TARGETS) test
###############################################################################
# Building using MLton.
###############################################################################
MLTON = mlton
MLTON_OPTS = -runtime 'ram-slop 0.4'
MLTON_SRC = \
src/Portable.sig src/PortableMlton.sml \
$(SRC)
METIS = bin/mlton/metis
PROBLEMS2TPTP = bin/mlton/problems2tptp
MLTON_TARGETS = \
bin/mlton/selftest \
$(METIS) \
$(PROBLEMS2TPTP)
bin/mlton/%.sml: $(MLTON_SRC) src/%.sml
@$(MLPP) $(MLPP_OPTS) -c mlton $^ > $@
bin/mlton/%.mlb: bin/mlton/%.sml
echo '$$(SML_LIB)/basis/basis.mlb $$(SML_LIB)/basis/mlton.mlb $(notdir $<)' > $@
bin/mlton/%: bin/mlton/%.mlb
@echo
@echo '***************************'
@echo '* Compile a MLton program *'
@echo '***************************'
@echo
@echo $@
cd bin/mlton ; $(MLTON) $(MLTON_OPTS) $(notdir $<)
@echo
.PHONY: mlton-info
mlton-info:
@echo
@echo '*************************************'
@echo '* Build and test the MLton programs *'
@echo '*************************************'
@echo
.PHONY: mlton
mlton: mlton-info $(MLTON_TARGETS)
$(MAKE) -C test mlton
###############################################################################
# Building using Poly/ML.
###############################################################################
POLYML = poly
POLYML_OPTS =
ifeq ($(shell uname), Darwin)
POLYML_LINK_OPTS = -lpolymain -lpolyml -segprot POLY rwx rwx
else
POLYML_LINK_OPTS = -lpolymain -lpolyml
endif
POLYML_SRC = \
src/Random.sig src/Random.sml \
src/Portable.sig src/PortablePolyml.sml \
$(SRC)
POLYML_TARGETS = \
bin/polyml/selftest \
bin/polyml/problems2tptp \
bin/polyml/metis
bin/polyml/%.sml: src/%.sml $(POLYML_SRC)
@$(MLPP) $(MLPP_OPTS) -c polyml $(POLYML_SRC) > $@
@echo 'fun main () = let' >> $@
@$(MLPP) $(MLPP_OPTS) -c polyml $< >> $@
@echo "in () end; PolyML.export(\"$(basename $(notdir $<))\", main);" >> $@
bin/polyml/%.o: bin/polyml/%.sml
cd bin/polyml ; echo "use \"$(notdir $<)\";" | $(POLYML) $(POLYML_OPTS) > $(basename $(notdir $<)).log
@if test $@ -nt $< ; then echo 'compiled $@' ; else cat bin/polyml/$(basename $(notdir $<)).log ; exit 1 ; fi
bin/polyml/%: bin/polyml/%.o
@echo
@echo '*****************************'
@echo '* Compile a Poly/ML program *'
@echo '*****************************'
@echo
@echo $@
cd bin/polyml && $(CC) -o $(notdir $@) $(notdir $<) $(POLYML_LINK_OPTS)
@echo
.PHONY: polyml-info
polyml-info:
@echo
@echo '***************************************'
@echo '* Build and test the Poly/ML programs *'
@echo '***************************************'
@echo
.PHONY: polyml
polyml: polyml-info $(POLYML_TARGETS)
$(MAKE) -C test polyml
###############################################################################
# Development.
##############################################################################
include Makefile.dev
Makefile.dev:
echo > $@