]> matita.cs.unibo.it Git - helm.git/commitdiff
removed the need of REQUIRES in libraries Makefile, they are now queried from the...
authorStefano Zacchiroli <zack@upsilon.cc>
Thu, 24 Nov 2005 08:39:51 +0000 (08:39 +0000)
committerStefano Zacchiroli <zack@upsilon.cc>
Thu, 24 Nov 2005 08:39:51 +0000 (08:39 +0000)
28 files changed:
helm/ocaml/METAS/meta.helm-cic_disambiguation.src
helm/ocaml/METAS/meta.helm-extlib.src
helm/ocaml/METAS/meta.helm-paramodulation.src
helm/ocaml/Makefile.common.in
helm/ocaml/cic/Makefile
helm/ocaml/cic_disambiguation/Makefile
helm/ocaml/cic_notation/Makefile
helm/ocaml/cic_omdoc/Makefile
helm/ocaml/cic_proof_checking/Makefile
helm/ocaml/cic_transformations/Makefile
helm/ocaml/cic_unification/Makefile
helm/ocaml/extlib/Makefile
helm/ocaml/getter/Makefile
helm/ocaml/hbugs/Makefile
helm/ocaml/hmysql/Makefile
helm/ocaml/logger/Makefile
helm/ocaml/mathql/Makefile
helm/ocaml/mathql_generator/Makefile
helm/ocaml/mathql_interpreter/Makefile
helm/ocaml/metadata/Makefile
helm/ocaml/paramodulation/Makefile
helm/ocaml/registry/Makefile
helm/ocaml/tactics/Makefile
helm/ocaml/thread/Makefile
helm/ocaml/urimanager/Makefile
helm/ocaml/utf8_macros/Makefile
helm/ocaml/xml/Makefile
helm/ocaml/xmldiff/Makefile

index d4c29fd7851aaed166e122f540dfe6a223706510..80d468c4a117f3a270cb3acef107413cae1df1f4 100644 (file)
@@ -1,4 +1,4 @@
-requires="helm-tactics helm-cic_transformations"
+requires="helm-tactics helm-cic_notation"
 version="0.0.1"
 archive(byte)="cic_disambiguation.cma"
 archive(native)="cic_disambiguation.cmxa"
index 0bc6287deb3f4568d76277d3ba0d5d0cfedc286f..bfee89e3dbcf1d4ff23ef7436f86b9ffd28256ea 100644 (file)
@@ -1,4 +1,4 @@
-requires="unix"
+requires="unix camlp4.gramlib"
 version="0.0.1"
 archive(byte)="extlib.cma"
 archive(native)="extlib.cmxa"
index 57dedd068b8365859a8840a05124eebebb20b177..6fe6c989833c34e9014eb429eaa71845988db51b 100644 (file)
@@ -1,4 +1,4 @@
-requires="helm-registry helm-cic_transformations helm-tactics helm-cic_disambiguation mysql"
+requires="helm-registry helm-tactics helm-cic_disambiguation mysql"
 version="0.0.1"
 archive(byte)="paramodulation.cma"
 archive(native)="paramodulation.cmxa"
index 501a411dae2d96e30fb21ebd78c0fad67b70f763..af5ecab861fabb342cbdb6704871c0a76c7a1bf1 100644 (file)
@@ -1,6 +1,5 @@
 # This Makefile must be included by another one defining:
 #  $PACKAGE
-#  $REQUIRES
 #  $PREDICATES
 #  $INTERFACE_FILES
 #  $IMPLEMENTATION_FILES
@@ -18,6 +17,7 @@ OCAMLOPTIONS = -package "$(REQUIRES)" -predicates "$(PREDICATES)" -thread
 OCAMLDEBUGOPTIONS = -g
 OCAMLARCHIVEOPTIONS =
 OCAMLFIND = OCAMLPATH=$(OCAMLPATH):$$OCAMLPATH @OCAMLFIND@
+REQUIRES := $(shell $(OCAMLFIND) -query -format '%(requires)' helm-$(PACKAGE))
 OCAMLC = $(OCAMLFIND) ocamlc $(OCAMLDEBUGOPTIONS) $(OCAMLOPTIONS) $(PREPROCOPTIONS)
 OCAMLOPT = $(OCAMLFIND) opt $(OCAMLOPTIONS) $(PREPROCOPTIONS)
 OCAMLDEP = $(OCAMLFIND) ocamldep -package "camlp4,$(REQUIRES)" $(SYNTAXOPTIONS)
index d73177b456faead9a7412e05b75b414bcf91f54e..a8f06e93847fffe518539b8f7dbef6f097cb9f38 100644 (file)
@@ -1,5 +1,4 @@
 PACKAGE = cic
-REQUIRES = helm-urimanager helm-xml expat
 PREDICATES =
 
 INTERFACE_FILES = \
index 1c80b4e0af8a9113d22340a400cfc7de6831a335..a94d8cebc40b838beeeb560e0d9a60c267521b5e 100644 (file)
@@ -1,9 +1,5 @@
 
 PACKAGE = cic_disambiguation
-REQUIRES = \
-       helm-tactics helm-logger helm-cic_unification helm-cic_notation \
-       helm-utf8_macros \
-       ulex
 NOTATIONS = number
 INTERFACE_FILES =              \
        disambiguateTypes.mli   \
index cfd1ad505d61ec46a0d4bca013ad52b0c4e06056..21c9a4e8c60d734e41bef88cfa18bcab3ea86aa3 100644 (file)
@@ -1,13 +1,6 @@
 
 PACKAGE = cic_notation
 NULL =
-REQUIRES = \
-       helm-cic                \
-       helm-utf8_macros        \
-       camlp4.gramlib          \
-       helm-cic_proof_checking \
-       ulex                    \
-       $(NULL)
 INTERFACE_FILES = \
        renderingAttrs.mli      \
        cicNotationUtil.mli     \
index 80d1d351a0536cc106ce99a3b139c9fe5867a55e..f4c3b5b6ffce0ff2e12f3e1f537daf804e15f986 100644 (file)
@@ -1,5 +1,4 @@
 PACKAGE = cic_omdoc
-REQUIRES = helm-cic_proof_checking
 PREDICATES =
 
 INTERFACE_FILES =              \
index 352a53016d6b5b2aa28a407a1a2a755c086b47ab..b5d1baa1a6ca23316a381d97d0ac26def8e6e96e 100644 (file)
@@ -1,6 +1,5 @@
 
 PACKAGE = cic_proof_checking
-REQUIRES = helm-cic helm-logger helm-getter helm-xml
 PREDICATES =
 
 REDUCTION_IMPLEMENTATION = cicReductionMachine.ml
index 4a8977aa76254bbf99b43505e026b68af3803de1..c5b5eaf09d9a741bea767ff7f8e75f054dd4f74c 100644 (file)
@@ -1,13 +1,4 @@
 PACKAGE = cic_transformations
-REQUIRES =                     \
-       gdome2                  \
-       helm-xml                \
-       helm-cic_proof_checking \
-       helm-cic_omdoc          \
-       helm-registry           \
-       helm-utf8_macros        \
-       helm-cic_notation       \
-       $(NULL)
 PREDICATES =
 
 # modules which have both a .ml and a .mli
index 7f1c8f3514b9737c49a6c484713aeda5d7ee9a51..caad677674d5534d017768f28cd2c84812b6260d 100644 (file)
@@ -1,5 +1,4 @@
 PACKAGE = cic_unification
-REQUIRES = helm-cic_proof_checking
 PREDICATES =
 
 INTERFACE_FILES = \
index c8df533ed43eaa80f4b9648e68ab206959042446..76370ee7307ef7abfb4cee96f04c4ed9ded9b6b6 100644 (file)
@@ -1,5 +1,4 @@
 PACKAGE = extlib
-REQUIRES = unix camlp4.gramlib
 PREDICATES =
 
 INTERFACE_FILES = \
index c6450d17814c145ffb20997bcaae2a59e64d668b..9ebca237ab9fad7823d9dfa63d40f34c449768ae 100644 (file)
@@ -1,10 +1,6 @@
 
 PACKAGE = getter
 
-REQUIRES = \
-       http unix pcre zip \
-       helm-xml helm-logger helm-urimanager helm-registry
-
 INTERFACE_FILES =              \
        http_getter_wget.mli    \
        http_getter_logger.mli  \
index 542bd2e3ab044d827f45f9c5032604dbaca80ab0..c38ac3e92de5a0fdf5d028bcda02466e7e8203e3 100644 (file)
@@ -12,9 +12,6 @@
 #      client        -> builds hbugs client
 
 PACKAGE = hbugs
-REQUIRES =     \
-       pcre lablgtk2.glade     \
-       helm-thread helm-xml helm-pxp helm-tactics helm-registry
 
 IMPLEMENTATION_FILES =                         \
        hbugs_misc.ml                   \
index f8ae017441e1aaf4ce0ff7f77753d72ae00d9f88..2ae1d4e59b619e524126a84c851c16dfb6a65650 100644 (file)
@@ -1,5 +1,4 @@
 PACKAGE = hmysql
-REQUIRES = mysql helm-registry helm-extlib 
 PREDICATES =
 
 INTERFACE_FILES = \
index 95b8c5510f4643562b1db9b3582e7b90b102956b..dab9f5cb30b77c00c788f3de87cbb3e0bf409c1e 100644 (file)
@@ -1,6 +1,5 @@
 
 PACKAGE = logger
-REQUIRES =
 INTERFACE_FILES = \
        helmLogger.mli
 IMPLEMENTATION_FILES = \
index 203d043713521140a51825b023947157d49b9ec2..17cafb431be4da2eb6959dc1ae86f338c5943519 100644 (file)
@@ -1,5 +1,5 @@
 PACKAGE = mathql
-REQUIRES = helm-cic
+
 PREDICATES =
 
 INTERFACE_FILES =
index a72f17ab26df09d19ee0df578b127a937321827f..cf8e820d99d5d3ee10c9987e49a831f62060c329 100644 (file)
@@ -1,7 +1,5 @@
 PACKAGE = mathql_generator
 
-REQUIRES = helm-cic helm-cic_proof_checking helm-mathql
-
 PREDICATES =
 
 INTERFACE_FILES = mQGUtil.mli mQueryGenerator.mli \
index e47b37a53cc6b249f60fc1f1004c20926ef0f26d..bdd7381359d12b4d9c88a7843a78721aea1b60db 100644 (file)
@@ -1,6 +1,4 @@
 PACKAGE = mathql_interpreter
-REQUIRES = helm-urimanager helm-mathql mysql postgres helm-registry
-#natile-galax 
 
 PREDICATES =
 
index c876b48100ad7035929fa18c225df08ba194951e..29ca2d3bce9862f90f841ea1c04387fb7fdb9cb6 100644 (file)
@@ -1,5 +1,4 @@
 PACKAGE = metadata
-REQUIRES = mysql helm-cic_proof_checking helm-hmysql
 PREDICATES =
 
 INTERFACE_FILES = \
index 7a3dbf626cfd1ba945f8add6e28c1428998653da..b65317cc2c540ed22021701a72632cc74b2d7c3a 100644 (file)
@@ -1,12 +1,5 @@
 PACKAGE = paramodulation
 
-REQUIRES = \
-       helm-registry \
-       helm-cic_transformations \
-       helm-tactics \
-       helm-cic_disambiguation \
-       mysql
-
 INTERFACE_FILES = \
        utils.mli \
        inference.mli 
@@ -18,13 +11,8 @@ IMPLEMENTATION_FILES = $(INTERFACE_FILES:%.mli=%.ml) \
        indexing.ml \
        saturation.ml 
 
-#       saturate_main.ml
-#      test_indexing.ml 
-
-
 include ../Makefile.common
 
-
 paramodulation.cmo: $(IMPLEMENTATION_FILES:%.ml=%.cmo)
        $(OCAMLC) -pack -o $@ $(IMPLEMENTATION_FILES:%.ml=%.cmo)
 
index e92099f6e23019724eb3da8c0183d69089c27d1f..4d3e0a52c0dca2fd70cea00613258a4a320b39a9 100644 (file)
@@ -1,6 +1,5 @@
 
 PACKAGE = registry
-REQUIRES = str netstring unix helm-xml
 INTERFACE_FILES = helm_registry.mli
 IMPLEMENTATION_FILES = helm_registry.ml
 
index 7f48873a02992a36a2ec3b55e80d8c7f8a3394cd..88372bf04419462c270fccd342a90bb10aa54f75 100644 (file)
@@ -1,10 +1,4 @@
 PACKAGE = tactics
-REQUIRES = \
-       pcre \
-       helm-cic_proof_checking \
-       helm-cic_unification \
-       mysql \
-       helm-metadata
 
 INTERFACE_FILES = \
        proofEngineTypes.mli \
index e39e5993c7c729ee24b5f21ea78406fa58458096..24a96b6e988de3c516e141b85b89d68ff4fbe3e7 100644 (file)
@@ -1,6 +1,5 @@
 
 PACKAGE = thread
-REQUIRES = threads
 INTERFACE_FILES = threadSafe.mli extThread.mli
 IMPLEMENTATION_FILES = $(INTERFACE_FILES:%.mli=%.ml)
 
index 8d5691aaf6f34b3ffb3ba188d550bf0d75fb2393..afd7d4442543c5374a6bb5b7dbf39a890d75ce0c 100644 (file)
@@ -1,5 +1,4 @@
 PACKAGE = urimanager
-REQUIRES = str
 PREDICATES =
 
 INTERFACE_FILES = uriManager.mli
index 31a1939ce436eecaf8faede3917e7fd121bd24ca..190f6cf6d815d4493a688e1d29963483368ad472 100644 (file)
@@ -1,5 +1,4 @@
 PACKAGE = utf8_macros
-REQUIRES = 
 PREDICATES =
 MAKE_TABLE_PACKAGES = helm-xml
 
index fabd2dfcecc0aa5799035d6b354221a0ea8295c6..6ca7bd944067dac40e1b342b84d41e81b8c5ccb7 100644 (file)
@@ -1,5 +1,4 @@
 PACKAGE = xml
-REQUIRES = zip expat helm-extlib
 PREDICATES =
 
 INTERFACE_FILES =      \
index 20a49c09701a2fac99504ccccb36e812b6b89ded..62492069ed009eefdd5633f3aeead4ee719745d1 100644 (file)
@@ -1,5 +1,4 @@
 PACKAGE = xmldiff
-REQUIRES = gdome2
 PREDICATES =
 
 INTERFACE_FILES = xmlDiff.mli