-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"
-requires="unix"
+requires="unix camlp4.gramlib"
version="0.0.1"
archive(byte)="extlib.cma"
archive(native)="extlib.cmxa"
-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"
# This Makefile must be included by another one defining:
# $PACKAGE
-# $REQUIRES
# $PREDICATES
# $INTERFACE_FILES
# $IMPLEMENTATION_FILES
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)
PACKAGE = cic
-REQUIRES = helm-urimanager helm-xml expat
PREDICATES =
INTERFACE_FILES = \
PACKAGE = cic_disambiguation
-REQUIRES = \
- helm-tactics helm-logger helm-cic_unification helm-cic_notation \
- helm-utf8_macros \
- ulex
NOTATIONS = number
INTERFACE_FILES = \
disambiguateTypes.mli \
PACKAGE = cic_notation
NULL =
-REQUIRES = \
- helm-cic \
- helm-utf8_macros \
- camlp4.gramlib \
- helm-cic_proof_checking \
- ulex \
- $(NULL)
INTERFACE_FILES = \
renderingAttrs.mli \
cicNotationUtil.mli \
PACKAGE = cic_omdoc
-REQUIRES = helm-cic_proof_checking
PREDICATES =
INTERFACE_FILES = \
PACKAGE = cic_proof_checking
-REQUIRES = helm-cic helm-logger helm-getter helm-xml
PREDICATES =
REDUCTION_IMPLEMENTATION = cicReductionMachine.ml
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
PACKAGE = cic_unification
-REQUIRES = helm-cic_proof_checking
PREDICATES =
INTERFACE_FILES = \
PACKAGE = extlib
-REQUIRES = unix camlp4.gramlib
PREDICATES =
INTERFACE_FILES = \
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 \
# 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 \
PACKAGE = hmysql
-REQUIRES = mysql helm-registry helm-extlib
PREDICATES =
INTERFACE_FILES = \
PACKAGE = logger
-REQUIRES =
INTERFACE_FILES = \
helmLogger.mli
IMPLEMENTATION_FILES = \
PACKAGE = mathql
-REQUIRES = helm-cic
+
PREDICATES =
INTERFACE_FILES =
PACKAGE = mathql_generator
-REQUIRES = helm-cic helm-cic_proof_checking helm-mathql
-
PREDICATES =
INTERFACE_FILES = mQGUtil.mli mQueryGenerator.mli \
PACKAGE = mathql_interpreter
-REQUIRES = helm-urimanager helm-mathql mysql postgres helm-registry
-#natile-galax
PREDICATES =
PACKAGE = metadata
-REQUIRES = mysql helm-cic_proof_checking helm-hmysql
PREDICATES =
INTERFACE_FILES = \
PACKAGE = paramodulation
-REQUIRES = \
- helm-registry \
- helm-cic_transformations \
- helm-tactics \
- helm-cic_disambiguation \
- mysql
-
INTERFACE_FILES = \
utils.mli \
inference.mli
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)
PACKAGE = registry
-REQUIRES = str netstring unix helm-xml
INTERFACE_FILES = helm_registry.mli
IMPLEMENTATION_FILES = helm_registry.ml
PACKAGE = tactics
-REQUIRES = \
- pcre \
- helm-cic_proof_checking \
- helm-cic_unification \
- mysql \
- helm-metadata
INTERFACE_FILES = \
proofEngineTypes.mli \
PACKAGE = thread
-REQUIRES = threads
INTERFACE_FILES = threadSafe.mli extThread.mli
IMPLEMENTATION_FILES = $(INTERFACE_FILES:%.mli=%.ml)
PACKAGE = urimanager
-REQUIRES = str
PREDICATES =
INTERFACE_FILES = uriManager.mli
PACKAGE = utf8_macros
-REQUIRES =
PREDICATES =
MAKE_TABLE_PACKAGES = helm-xml
PACKAGE = xml
-REQUIRES = zip expat helm-extlib
PREDICATES =
INTERFACE_FILES = \
PACKAGE = xmldiff
-REQUIRES = gdome2
PREDICATES =
INTERFACE_FILES = xmlDiff.mli