BIN_DIR = /usr/local/bin
-REQUIRES = helm-cic_proof_checking
+REQUIRES = helm-cic_proof_checking http
PREDICATES =
OCAMLOPTIONS = -package "$(REQUIRES)" -predicates "$(PREDICATES)"
-OCAMLC = ocamlfind ocamlc $(OCAMLOPTIONS)
+OCAMLC = ocamlfind ocamlc $(OCAMLOPTIONS) -g
OCAMLOPT = ocamlfind ocamlopt $(OCAMLOPTIONS)
OCAMLDEP = ocamldep
-all: proofChecker
-opt: proofChecker.opt
+LIBRARIES = $(shell ocamlfind query -recursive -predicates "byte $(PREDICATES)" -format "%d/%a" $(REQUIRES))
+LIBRARIES_OPT = $(shell ocamlfind query -recursive -predicates "native $(PREDICATES)" -format "%d/%a" $(REQUIRES))
+
+all: $(PROOFCHECKEROBJS) proofChecker
+opt: $(PROOFCHECKEROBJS:.cmo=.cmx) proofChecker.opt
DEPOBJS = proofChecker.ml
depend:
$(OCAMLDEP) $(DEPOBJS) > .depend
-proofChecker: $(PROOFCHECKEROBJS)
+proofChecker: $(PROOFCHECKEROBJS) $(LIBRARIES)
$(OCAMLC) -linkpkg -o proofChecker $(PROOFCHECKEROBJS)
-proofChecker.opt: $(PROOFCHECKEROBJS:.cmo=.cmx)
+proofChecker.opt: $(PROOFCHECKEROBJS:.cmo=.cmx) $(LIBRARIES_OPT)
$(OCAMLOPT) -linkpkg -o proofChecker.opt $(PROOFCHECKEROBJS:.cmo=.cmx)
.SUFFIXES: .ml .mli .cmo .cmi .cmx
-.ml.cmo:
+.ml.cmo: $(LIBRARIES)
$(OCAMLC) -c $<
-.mli.cmi:
+.mli.cmi: $(LIBRARIES)
$(OCAMLC) -c $<
-.ml.cmx:
+.ml.cmx: $(LIBRARIES_OPT)
$(OCAMLOPT) -c $<
clean: