]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/Makefile.common.in
Added a new section on automation
[helm.git] / helm / ocaml / Makefile.common.in
index 9dff7894208c365a65473fd681eab2bbebf6cd3c..2dc345235a59af72613cfc7935b3e1b4cb1c0d7e 100644 (file)
@@ -1,3 +1,5 @@
+H=@
+
 # This Makefile must be included by another one defining:
 #  $PACKAGE
 #  $PREDICATES
@@ -29,6 +31,13 @@ OCAMLOPT_P4 = $(OCAMLFIND) opt $(OCAMLOPTIONS) $(SYNTAXOPTIONS)
 
 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))
+LIBRARIES_DEPS = \
+       $(foreach X,$(filter-out /usr/lib/ocaml%,$(LIBRARIES)),\
+               $(wildcard \
+                       $(shell dirname $(X))/*.mli \
+                       $(shell dirname $(X))/*.ml \
+                       $(shell dirname $(X))/paramodulation/*.ml \
+                       $(shell dirname $(X))/paramodultation/*.mli))
 
 
 ARCHIVE = $(PACKAGE).cma
@@ -39,18 +48,22 @@ OBJECTS_TO_INSTALL = $(ARCHIVE) $(ARCHIVE_OPT) $(ARCHIVE_OPT:%.cmxa=%.a) \
 DEPEND_FILES = $(INTERFACE_FILES) $(IMPLEMENTATION_FILES)
 
 $(ARCHIVE): $(IMPLEMENTATION_FILES:%.ml=%.cmo) $(LIBRARIES)
-       if [ $(PACKAGE) != dummy ]; then \
+       $(H)if [ $(PACKAGE) != dummy ]; then \
+       echo "  OCAMLC -a $@";\
        $(OCAMLC) $(OCAMLARCHIVEOPTIONS) -a -o $@ \
                $(IMPLEMENTATION_FILES:%.ml=%.cmo); fi
 
 $(ARCHIVE_OPT): $(IMPLEMENTATION_FILES:%.ml=%.cmx) $(LIBRARIES_OPT)
-       if [ $(PACKAGE) != dummy ]; then \
+       $(H)if [ $(PACKAGE) != dummy ]; then \
+       echo "  OCAMLOPT -a $@";\
        $(OCAMLOPT) $(OCAMLARCHIVEOPTIONS) -a -o $@ \
                $(IMPLEMENTATION_FILES:%.ml=%.cmx); fi
 
 prereq: $(PREREQ)
 all: prereq $(IMPLEMENTATION_FILES:%.ml=%.cmo) $(ARCHIVE)
+       @echo -n 
 opt: prereq $(IMPLEMENTATION_FILES:%.ml=%.cmx) $(ARCHIVE_OPT)
+       @echo -n 
 world: all opt
 test: test.ml $(ARCHIVE)
        $(OCAMLC) $(ARCHIVE) -linkpkg -o $@ $<
@@ -67,11 +80,14 @@ $(PACKAGE).ps: .dep.dot
        ocamldot < .depend > $@
 
 %.cmi: %.mli
-       $(OCAMLC) -c $<
+       @echo "  OCAMLC $<"
+       $(H)$(OCAMLC) -c $<
 %.cmo %.cmi: %.ml
-       $(OCAMLC) -c $<
+       @echo "  OCAMLC $<"
+       $(H)$(OCAMLC) -c $<
 %.cmx: %.ml
-       $(OCAMLOPT) -c $<
+       @echo "  OCAMLOPT $<"
+       $(H)$(OCAMLOPT) -c $<
 %.annot: %.ml
        $(OCAMLC) -dtypes $(PKGS) -c $<
 %.ml %.mli: %.mly
@@ -80,6 +96,7 @@ $(PACKAGE).ps: .dep.dot
        $(OCAMLLEX) $<
 
 $(IMPLEMENTATION_FILES:%.ml=%.cmo): $(LIBRARIES)
+$(IMPLEMENTATION_FILES:%.ml=%.cmi): $(LIBRARIES_DEPS)
 $(IMPLEMENTATION_FILES:%.ml=%.cmx): $(LIBRARIES_OPT)
 
 clean:
@@ -120,17 +137,5 @@ ifneq ($(MAKECMDGOALS), depend)
    include .depend   
 endif
 
-ifeq ($(MAKECMDGOALS), all)
-   $(IMPLEMENTATION_FILES:%.ml=%.cmi): $(LIBRARIES)
-endif
-
-ifeq ($(MAKECMDGOALS), opt)
-   $(IMPLEMENTATION_FILES:%.ml=%.cmi): $(LIBRARIES_OPT)
-endif
-
-ifeq ($(MAKECMDGOALS),)
-   $(IMPLEMENTATION_FILES:%.ml=%.cmi): $(LIBRARIES)
-endif
-
 NULL =