From 7be6aeb94aa8da17732511a4844bd108976f947f Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Thu, 2 Feb 2006 14:02:18 +0000 Subject: [PATCH] no more multiple configure/Makefile, just one for both ocaml/ and matita/ --- helm/Makefile | 2 +- helm/Makefile.defs.in | 7 + helm/configure.ac | 75 +++++++--- helm/matita/{Makefile.in => Makefile} | 121 +++++----------- helm/matita/configure.ac | 134 ------------------ helm/ocaml/{Makefile.in => Makefile} | 26 +--- .../{Makefile.common.in => Makefile.common} | 16 +-- helm/ocaml/Makefile.defs.in | 1 - helm/ocaml/acic_content/Makefile | 1 + helm/ocaml/cic/Makefile | 1 + helm/ocaml/cic_acic/Makefile | 1 + helm/ocaml/cic_disambiguation/Makefile | 2 + helm/ocaml/cic_proof_checking/Makefile | 1 + .../cic_proof_checking/utilities/Makefile | 6 +- helm/ocaml/cic_unification/Makefile | 1 + helm/ocaml/configure.ac | 55 ------- helm/ocaml/content_pres/Makefile | 1 + helm/ocaml/extlib/Makefile | 1 + helm/ocaml/getter/Makefile | 1 + helm/ocaml/grafite/Makefile | 1 + helm/ocaml/grafite_engine/Makefile | 1 + helm/ocaml/grafite_parser/Makefile | 1 + helm/ocaml/hbugs/Makefile | 1 + helm/ocaml/hgdome/Makefile | 1 + helm/ocaml/hmysql/Makefile | 1 + helm/ocaml/lexicon/Makefile | 1 + helm/ocaml/library/Makefile | 1 + helm/ocaml/logger/Makefile | 1 + helm/ocaml/metadata/Makefile | 1 + helm/ocaml/metadata/extractor/Makefile | 2 +- helm/ocaml/metadata/table_creator/Makefile | 2 +- helm/ocaml/registry/Makefile | 1 + helm/ocaml/tactics/Makefile | 1 + helm/ocaml/tactics/paramodulation/Makefile | 1 + helm/ocaml/thread/Makefile | 1 + helm/ocaml/urimanager/Makefile | 1 + helm/ocaml/utf8_macros/Makefile | 1 + helm/ocaml/whelp/Makefile | 1 + helm/ocaml/xml/Makefile | 1 + helm/ocaml/xmldiff/Makefile | 1 + 40 files changed, 150 insertions(+), 326 deletions(-) create mode 100644 helm/Makefile.defs.in rename helm/matita/{Makefile.in => Makefile} (63%) delete mode 100644 helm/matita/configure.ac rename helm/ocaml/{Makefile.in => Makefile} (78%) rename helm/ocaml/{Makefile.common.in => Makefile.common} (91%) delete mode 100644 helm/ocaml/Makefile.defs.in delete mode 100644 helm/ocaml/configure.ac diff --git a/helm/Makefile b/helm/Makefile index 2eb93cd41..62b41c430 100644 --- a/helm/Makefile +++ b/helm/Makefile @@ -1,6 +1,6 @@ BASENAME = matita -VERSION = 0.1.0 +VERSION = @MATITA_VERSION@ NULL = DISTDIR = $(BASENAME)-$(VERSION) diff --git a/helm/Makefile.defs.in b/helm/Makefile.defs.in new file mode 100644 index 000000000..28adb2a19 --- /dev/null +++ b/helm/Makefile.defs.in @@ -0,0 +1,7 @@ +OCAMLFIND = OCAMLPATH=@OCAMLPATH@ @OCAMLFIND@ +CAMLP4O = @CAMLP4O@ +LABLGLADECC = @LABLGLADECC@ +HAVE_OCAMLOPT = @HAVE_OCAMLOPT@ + +MATITA_REQUIRES = @FINDLIB_REQUIRES@ +MATITA_CREQUIRES = @FINDLIB_CREQUIRES@ diff --git a/helm/configure.ac b/helm/configure.ac index c07a962ae..176763719 100644 --- a/helm/configure.ac +++ b/helm/configure.ac @@ -1,9 +1,9 @@ -AC_INIT(matitaTypes.ml) +AC_INIT(matita/matitaTypes.ml) # Distribution settings (i.e. settings to be manipulated before a release) DEBUG_DEFAULT="true" -RT_BASE_DIR_DEFAULT="`pwd`" -MATITA_VERSION="0.0.1" +RT_BASE_DIR_DEFAULT="`pwd`/matita" +MATITA_VERSION="0.1.0" # End of distribution settings AC_CHECK_PROG(HAVE_OCAMLC, ocamlc, yes, no) @@ -32,6 +32,53 @@ if test $HAVE_CAMLP4O = "yes"; then else AC_MSG_ERROR(could not find camlp4o) fi + +# look for METAS dir + +OCAMLPATH="" +LIBSPATH="" +if test -d libs ; then + OCAMLPATH=`pwd`/libs/METAS + LIBSPATH=`pwd`/libs +fi +if test -d ocaml ; then + OCAMLPATH=`pwd`/ocaml/METAS + LIBSPATH=`pwd`/ocaml +fi +if test -z $OCAMLPATH; then + AC_MSG_ERROR(could not find METAS directory) +fi + +# creating META.* + +echo -n "creating METAs ... " +for f in $OCAMLPATH/meta.*.src; do + basename=`basename $f` + metaname=`echo $basename | sed 's/meta\.\(.*\)\.src/\1/'` + dirname=`echo $metaname | sed 's/^helm-//'` + metafile="$OCAMLPATH/META.$metaname" + cp $f $metafile + echo "directory=\"$LIBSPATH/$dirname\"" >> $metafile +done +echo "done" + +# (libs) findlib requisites + +FINDLIB_LIBSREQUIRES="\ +expat \ +gdome2 \ +http \ +lablgtk2 \ +lablgtkmathview \ +lablgtksourceview \ +mysql \ +netstring \ +ulex \ +zip \ +" + +# (Matita) findlib requisites + FINDLIB_COMREQUIRES="\ helm-cic_disambiguation \ helm-grafite \ @@ -40,12 +87,6 @@ helm-grafite_parser \ helm-hgdome \ helm-tactics \ " -FINDLIB_CLEANREQUIRES="$FINDLIB_COMREQUIRES" -FINDLIB_DEPREQUIRES="$FINDLIB_COMREQUIRES" -FINDLIB_MAKEREQUIRES=" \ -helm-registry \ -helm-extlib \ -" FINDLIB_CREQUIRES=" \ $FINDLIB_COMREQUIRES \ " @@ -56,10 +97,10 @@ lablgtkmathview \ lablgtksourceview \ helm-xmldiff \ " -for r in $FINDLIB_REQUIRES +for r in $FINDLIB_LIBSREQUIRES $FINDLIB_REQUIRES do AC_MSG_CHECKING(for $r ocaml library) - if OCAMLPATH=../ocaml/METAS $OCAMLFIND query $r &> /dev/null; then + if OCAMLPATH=$OCAMLPATH $OCAMLFIND query $r &> /dev/null; then AC_MSG_RESULT(yes) else AC_MSG_ERROR(could not find $r ocaml library) @@ -117,18 +158,16 @@ AC_SUBST(DEBUG) AC_SUBST(TRANSFORMER_MODULE) AC_SUBST(FINDLIB_REQUIRES) AC_SUBST(FINDLIB_CREQUIRES) -AC_SUBST(FINDLIB_DEPREQUIRES) -AC_SUBST(FINDLIB_CLEANREQUIRES) -AC_SUBST(FINDLIB_MAKEREQUIRES) AC_SUBST(HAVE_OCAMLOPT) AC_SUBST(LABLGLADECC) AC_SUBST(OCAMLFIND) +AC_SUBST(OCAMLPATH) AC_SUBST(RT_BASE_DIR) AC_SUBST(MATITA_VERSION) AC_OUTPUT([ - matita.conf.xml.sample - buildTimeConf.ml - Makefile - gtkmathview.matita.conf.xml + matita/matita.conf.xml.sample + matita/buildTimeConf.ml + matita/gtkmathview.matita.conf.xml + Makefile.defs ]) diff --git a/helm/matita/Makefile.in b/helm/matita/Makefile similarity index 63% rename from helm/matita/Makefile.in rename to helm/matita/Makefile index af543d640..3f65ab538 100644 --- a/helm/matita/Makefile.in +++ b/helm/matita/Makefile @@ -1,25 +1,13 @@ export SHELL=/bin/bash -NULL = +include ../Makefile.defs -MAKEFLAGS+=--no-print-directory -OCAMLPATH = ../ocaml/METAS/ -OCAMLFIND = OCAMLPATH=$(OCAMLPATH):$$OCAMLPATH @OCAMLFIND@ -CAMLP4O = @CAMLP4O@ -LABLGLADECC = @LABLGLADECC@ -REQUIRES = @FINDLIB_REQUIRES@ -CREQUIRES = @FINDLIB_CREQUIRES@ -DEPREQUIRES = @FINDLIB_DEPREQUIRES@ -CLEANREQUIRES = @FINDLIB_CLEANREQUIRES@ -MAKEREQUIRES = @FINDLIB_MAKEREQUIRES@ -HAVE_OCAMLOPT = @HAVE_OCAMLOPT@ +NULL = +H=@ OCAML_FLAGS = -pp $(CAMLP4O) -PKGS = -package "$(REQUIRES)" -CPKGS = -package "$(CREQUIRES)" -DEPPKGS = -package "$(DEPREQUIRES)" -CLEANPKGS = -package "$(CLEANREQUIRES)" -MAKEPKGS = -package "$(MAKEREQUIRES)" +PKGS = -package "$(MATITA_REQUIRES)" +CPKGS = -package "$(MATITA_CREQUIRES)" OCAML_THREADS_FLAGS = -thread OCAML_DEBUG_FLAGS = -g OCAMLC_FLAGS = $(OCAML_FLAGS) $(OCAML_THREADS_FLAGS) @@ -66,12 +54,6 @@ MAINCMOS = \ matitaclean.cmo \ matitamake.cmo \ $(NULL) -DEPCMOS = $(CCMOS) -CLEANCMOS = $(CCMOS) -MAKECMOS = \ - buildTimeConf.cmo \ - matitamakeLib.cmo \ - $(NULL) PROGRAMS_BYTE = matita matitac cicbrowser matitadep matitaclean matitamake dump_moo PROGRAMS = $(PROGRAMS_BYTE) matitatop PROGRAMS_OPT = $(patsubst %,%.opt,$(PROGRAMS_BYTE)) @@ -109,19 +91,10 @@ ifeq ($(HAVE_OCAMLOPT),yes) CMXS = $(patsubst %.cmo,%.cmx,$(CMOS)) CCMXS = $(patsubst %.cmo,%.cmx,$(CCMOS)) MAINCMXS = $(patsubst %.cmo,%.cmx,$(MAINCMOS)) -DEPCMXS = $(patsubst %.cmo,%.cmx,$(DEPCMOS)) -CLEANCMXS = $(patsubst %.cmo,%.cmx,$(CLEANCMOS)) -MAKECMXS = $(patsubst %.cmo,%.cmx,$(MAKECMOS)) -LIB_DEPS := $(shell $(OCAMLFIND) query -recursive -predicates "byte" -format "%d/%a" $(REQUIRES)) -LIBX_DEPS := $(shell $(OCAMLFIND) query -recursive -predicates "native" -format "%d/%a" $(REQUIRES)) -CLIB_DEPS := $(shell $(OCAMLFIND) query -recursive -predicates "byte" -format "%d/%a" $(CREQUIRES)) -CLIBX_DEPS := $(shell $(OCAMLFIND) query -recursive -predicates "native" -format "%d/%a" $(CREQUIRES)) -DEPLIB_DEPS := $(shell $(OCAMLFIND) query -recursive -predicates "byte" -format "%d/%a" $(DEPREQUIRES)) -DEPLIBX_DEPS := $(shell $(OCAMLFIND) query -recursive -predicates "native" -format "%d/%a" $(DEPREQUIRES)) -CLEANLIB_DEPS := $(shell $(OCAMLFIND) query -recursive -predicates "byte" -format "%d/%a" $(CLEANREQUIRES)) -CLEANLIBX_DEPS := $(shell $(OCAMLFIND) query -recursive -predicates "native" -format "%d/%a" $(CLEANREQUIRES)) -MAKELIB_DEPS := $(shell $(OCAMLFIND) query -recursive -predicates "byte" -format "%d/%a" $(MAKEREQUIRES)) -MAKELIBX_DEPS := $(shell $(OCAMLFIND) query -recursive -predicates "native" -format "%d/%a" $(MAKEREQUIRES)) +LIB_DEPS := $(shell $(OCAMLFIND) query -recursive -predicates "byte" -format "%d/%a" $(MATITA_REQUIRES)) +LIBX_DEPS := $(shell $(OCAMLFIND) query -recursive -predicates "native" -format "%d/%a" $(MATITA_REQUIRES)) +CLIB_DEPS := $(shell $(OCAMLFIND) query -recursive -predicates "byte" -format "%d/%a" $(MATITA_CREQUIRES)) +CLIBX_DEPS := $(shell $(OCAMLFIND) query -recursive -predicates "native" -format "%d/%a" $(MATITA_CREQUIRES)) .PHONY: opt opt: $(PROGRAMS_OPT) coq.moo.opt .PHONY: upx @@ -134,46 +107,41 @@ opt: endif -matita: $(LIB_DEPS) $(CMOS) matita.ml - $(OCAMLC) $(PKGS) -linkpkg -o $@ $(CMOS) matita.ml -matita.opt: $(LIBX_DEPS) $(CMXS) matita.ml - $(OCAMLOPT) $(PKGS) -linkpkg -o $@ $(CMXS) matita.ml - -dump_moo: buildTimeConf.cmo dump_moo.ml - $(OCAMLC) $(PKGS) -linkpkg -o $@ $^ -dump_moo.opt: buildTimeConf.cmx dump_moo.ml - $(OCAMLOPT) $(PKGS) -linkpkg -o $@ $^ - -matitac: $(CLIB_DEPS) $(CCMOS) $(MAINCMOS) matitac.ml - $(OCAMLC) $(CPKGS) -linkpkg -o $@ $(CCMOS) $(MAINCMOS) matitac.ml -matitac.opt: $(CLIBX_DEPS) $(CCMXS) $(MAINCMXS) matitac.ml - $(OCAMLOPT) $(CPKGS) -linkpkg -o $@ $(CCMXS) $(MAINCMXS) matitac.ml +matita: matita.ml $(LIB_DEPS) $(CMOS) + @echo "OCAMLC $<" + $(H)$(OCAMLC) $(PKGS) -linkpkg -o $@ $(CMOS) matita.ml +matita.opt: matita.ml $(LIBX_DEPS) $(CMXS) + @echo "OCAMLOPT $<" + $(H)$(OCAMLOPT) $(PKGS) -linkpkg -o $@ $(CMXS) matita.ml + +dump_moo: dump_moo.ml buildTimeConf.cmo + @echo "OCAMLC $<" + $(H)$(OCAMLC) $(PKGS) -linkpkg -o $@ buildTimeConf.cmo $< +dump_moo.opt: dump_moo.ml buildTimeConf.cmx + @echo "OCAMLOPT $<" + $(H)$(OCAMLOPT) $(PKGS) -linkpkg -o $@ buildTimeConf.cmx $< + +matitac: matitac.ml $(CLIB_DEPS) $(CCMOS) $(MAINCMOS) + @echo "OCAMLC $<" + $(H)$(OCAMLC) $(CPKGS) -linkpkg -o $@ $(CCMOS) $(MAINCMOS) matitac.ml +matitac.opt: matitac.ml $(CLIBX_DEPS) $(CCMXS) $(MAINCMXS) + @echo "OCAMLOPT $<" + $(H)$(OCAMLOPT) $(CPKGS) -linkpkg -o $@ $(CCMXS) $(MAINCMXS) matitac.ml matitatop: matitatop.ml $(CLIB_DEPS) $(CCMOS) - $(OCAMLC) $(CPKGS) -linkpkg -o $@ toplevellib.cma $(CCMOS) $< + @echo "OCAMLC $<" + $(H)$(OCAMLC) $(CPKGS) -linkpkg -o $@ toplevellib.cma $(CCMOS) $< -# matitadep: matitadep.ml $(DEPLIB_DEPS) $(DEPCMOS) -# $(OCAMLC) $(DEPPKGS) -linkpkg -o $@ $(DEPCMOS) $< -# matitadep.opt: matitadep.ml $(DEPLIB_DEPS) $(DEPCMXS) -# $(OCAMLOPT) $(DEPPKGS) -linkpkg -o $@ $(DEPCMXS) $< matitadep: matitac @test -f $@ || ln -s $< $@ matitadep.opt: matitac.opt @test -f $@ || ln -s $< $@ -# matitaclean: matitaclean.ml $(CLEANLIB_DEPS) $(CLEANCMOS) -# $(OCAMLC) $(CLEANPKGS) -linkpkg -o $@ $(CLEANCMOS) $< -# matitaclean.opt: matitaclean.ml $(CLEANLIB_DEPS) $(CLEANCMXS) -# $(OCAMLOPT) $(CLEANPKGS) -linkpkg -o $@ $(CLEANCMXS) $< matitaclean: matitac @test -f $@ || ln -s $< $@ matitaclean.opt: matitac.opt @test -f $@ || ln -s $< $@ -# matitamake: matitamake.ml $(MAKECMOS) -# $(OCAMLC) $(MAKEPKGS) -linkpkg -o $@ $(MAKECMOS) $< -# matitamake.opt: matitamake.ml $(MAKECMXS) -# $(OCAMLOPT) $(MAKEPKGS) -linkpkg -o $@ $(MAKECMXS) $< matitamake: matitac @test -f $@ || ln -s $< $@ matitamake.opt: matitac.opt @@ -270,25 +238,10 @@ matitac.opt.static: $(STATIC_LINK) $(CLIBX_DEPS) $(CCMXS) $(MAINCMXS) matitac.ml $(OCAMLOPT) $(CPKGS) -linkpkg -o $@ $(CCMXS) $(MAINCMXS) matitac.ml \ $(STATIC_EXTRA_CLIBS) strip $@ -# matitadep.opt.static: $(STATIC_LINK) matitadep.ml $(DEPLIB_DEPS) $(DEPCMXS) -# $(STATIC_LINK) $(STATIC_CLIBS) -- \ -# $(OCAMLOPT) $(DEPPKGS) -linkpkg -o $@ $(DEPCMXS) $< \ -# $(STATIC_EXTRA_CLIBS) -# strip $@ matitadep.opt.static: matitac.opt.static @test -f $@ || ln -s $< $@ -# matitaclean.opt.static: $(STATIC_LINK) matitaclean.ml $(CLEANLIB_DEPS) $(CLEANCMXS) -# $(STATIC_LINK) $(STATIC_CLIBS) -- \ -# $(OCAMLOPT) $(CLEANPKGS) -linkpkg -o $@ $(CLEANCMXS) $< \ -# $(STATIC_EXTRA_CLIBS) -# strip $@ matitaclean.opt.static: matitac.opt.static @test -f $@ || ln -s $< $@ -# matitamake.opt.static: $(STATIC_LINK) matitamake.ml $(MAKECMXS) -# $(STATIC_LINK) $(STATIC_CLIBS) -- \ -# $(OCAMLOPT) $(PKGS) -linkpkg -o $@ $(MAKECMXS) $< \ -# $(STATIC_EXTRA_CLIBS) -# strip $@ matitamake.opt.static: matitac.opt.static @test -f $@ || ln -s $< $@ cicbrowser.opt.static: matita.opt.static @@ -326,13 +279,17 @@ depend: include .depend %.cmi: %.mli - $(OCAMLC) $(PKGS) -c $< + @echo "OCAMLC $<" + $(H)$(OCAMLC) $(PKGS) -c $< %.cmo %.cmi: %.ml - $(OCAMLC) $(PKGS) -c $< + @echo "OCAMLC $<" + $(H)$(OCAMLC) $(PKGS) -c $< %.cmx: %.ml - $(OCAMLOPT) $(PKGS) -c $< + @echo "OCAMLOPT $<" + $(H)$(OCAMLOPT) $(PKGS) -c $< %.annot: %.ml - $(OCAMLC) -dtypes $(PKGS) -c $< + @echo "OCAMLC -dtypes $<" + $(H)$(OCAMLC) -dtypes $(PKGS) -c $< $(CMOS): $(LIB_DEPS) $(CMOS:%.cmo=%.cmx): $(LIBX_DEPS) diff --git a/helm/matita/configure.ac b/helm/matita/configure.ac deleted file mode 100644 index c07a962ae..000000000 --- a/helm/matita/configure.ac +++ /dev/null @@ -1,134 +0,0 @@ -AC_INIT(matitaTypes.ml) - -# Distribution settings (i.e. settings to be manipulated before a release) -DEBUG_DEFAULT="true" -RT_BASE_DIR_DEFAULT="`pwd`" -MATITA_VERSION="0.0.1" -# End of distribution settings - -AC_CHECK_PROG(HAVE_OCAMLC, ocamlc, yes, no) -if test $HAVE_OCAMLC = "no"; then - AC_MSG_ERROR(could not find ocamlc) -fi -AC_CHECK_PROG(HAVE_OCAMLOPT, ocamlopt, yes, no) -if test $HAVE_OCAMLOPT = "no"; then - AC_MSG_WARN(could not find ocamlopt: native code compilation disabled) -fi -AC_CHECK_PROG(HAVE_OCAMLFIND, ocamlfind, yes, no) -if test $HAVE_OCAMLFIND = "yes"; then - OCAMLFIND="ocamlfind" -else - AC_MSG_ERROR(could not find ocamlfind) -fi -AC_CHECK_PROG(HAVE_LABLGLADECC, lablgladecc2, yes, no) -if test $HAVE_LABLGLADECC = "yes"; then - LABLGLADECC="lablgladecc2" -else - AC_MSG_ERROR(could not find lablgladecc2) -fi -AC_CHECK_PROG(HAVE_CAMLP4O, camlp4o, yes, no) -if test $HAVE_CAMLP4O = "yes"; then - CAMLP4O="camlp4o" -else - AC_MSG_ERROR(could not find camlp4o) -fi -FINDLIB_COMREQUIRES="\ -helm-cic_disambiguation \ -helm-grafite \ -helm-grafite_engine \ -helm-grafite_parser \ -helm-hgdome \ -helm-tactics \ -" -FINDLIB_CLEANREQUIRES="$FINDLIB_COMREQUIRES" -FINDLIB_DEPREQUIRES="$FINDLIB_COMREQUIRES" -FINDLIB_MAKEREQUIRES=" \ -helm-registry \ -helm-extlib \ -" -FINDLIB_CREQUIRES=" \ -$FINDLIB_COMREQUIRES \ -" -FINDLIB_REQUIRES="\ -$FINDLIB_CREQUIRES \ -lablgtk2.glade \ -lablgtkmathview \ -lablgtksourceview \ -helm-xmldiff \ -" -for r in $FINDLIB_REQUIRES -do - AC_MSG_CHECKING(for $r ocaml library) - if OCAMLPATH=../ocaml/METAS $OCAMLFIND query $r &> /dev/null; then - AC_MSG_RESULT(yes) - else - AC_MSG_ERROR(could not find $r ocaml library) - fi -done - -OCAMLFIND_COMMANDS="" -# AC_CHECK_PROG(HAVE_OCAMLC_OPT, ocamlc.opt, yes, no) -# if test $HAVE_OCAMLC_OPT = "yes"; then -# if test "$OCAMLFIND_COMMANDS" = ""; then -# OCAMLFIND_COMMANDS="ocamlc=ocamlc.opt" -# else -# OCAMLFIND_COMMANDS="$OCAMLFIND_COMMANDS ocamlc=ocamlc.opt" -# fi -# fi -# AC_CHECK_PROG(HAVE_OCAMLOPT_OPT, ocamlopt.opt, yes, no) -# if test $HAVE_OCAMLOPT_OPT = "yes"; then -# if test "$OCAMLFIND_COMMANDS" = ""; then -# OCAMLFIND_COMMANDS="ocamlopt=ocamlopt.opt" -# else -# OCAMLFIND_COMMANDS="$OCAMLFIND_COMMANDS ocamlopt=ocamlopt.opt" -# fi -# fi -if test "$OCAMLFIND_COMMANDS" != ""; then - OCAMLFIND="OCAMLFIND_COMMANDS='$OCAMLFIND_COMMANDS' $OCAMLFIND" -fi - -AC_MSG_CHECKING(--enable-debug argument) -AC_ARG_ENABLE(debug, - [ --enable-debug Turn on debugging], - [GIVEN="yes"; - case "${enableval}" in - yes) DEBUG=true ;; - no) DEBUG=false ;; - *) AC_MSG_ERROR(bad value ${enableval} for --enable-debug) ;; - esac], - [GIVEN="no"; DEBUG="$DEBUG_DEFAULT"]) -MSG=$GIVEN -if test "$DEBUG" = "true"; then - MSG="$MSG, debugging enabled." -else - MSG="$MSG, debugging disabled." -fi -AC_MSG_RESULT($MSG) - -AC_MSG_CHECKING(--with-runtime-dir argument) -AC_ARG_WITH(runtime-dir, - [ --with-runtime-dir Runtime directory (current working directory if not given)], - [ RT_BASE_DIR="${withval}" ], - [ RT_BASE_DIR="$RT_BASE_DIR_DEFAULT" ]) -AC_MSG_RESULT($RT_BASE_DIR) - -AC_SUBST(CAMLP4O) -AC_SUBST(DEBUG) -AC_SUBST(TRANSFORMER_MODULE) -AC_SUBST(FINDLIB_REQUIRES) -AC_SUBST(FINDLIB_CREQUIRES) -AC_SUBST(FINDLIB_DEPREQUIRES) -AC_SUBST(FINDLIB_CLEANREQUIRES) -AC_SUBST(FINDLIB_MAKEREQUIRES) -AC_SUBST(HAVE_OCAMLOPT) -AC_SUBST(LABLGLADECC) -AC_SUBST(OCAMLFIND) -AC_SUBST(RT_BASE_DIR) -AC_SUBST(MATITA_VERSION) - -AC_OUTPUT([ - matita.conf.xml.sample - buildTimeConf.ml - Makefile - gtkmathview.matita.conf.xml -]) diff --git a/helm/ocaml/Makefile.in b/helm/ocaml/Makefile similarity index 78% rename from helm/ocaml/Makefile.in rename to helm/ocaml/Makefile index 7ab72ed24..0d1867293 100644 --- a/helm/ocaml/Makefile.in +++ b/helm/ocaml/Makefile @@ -1,6 +1,8 @@ export SHELL=/bin/bash +include ../Makefile.defs + # Warning: the modules must be in compilation order NULL = MODULES = \ @@ -33,16 +35,11 @@ MODULES = \ tactics/paramodulation \ $(NULL) -OCAMLFIND_DEST_DIR = @OCAMLFIND_DEST_DIR@ -OCAMLPATH = @OCAMLFIND_META_DIR@ -OCAMLFIND = OCAMLPATH=$(OCAMLPATH):$$OCAMLPATH @OCAMLFIND@ - METAS = $(filter-out %/paramodulation,$(MODULES:%=METAS/META.helm-%)) all: metas $(MODULES:%=%.all) opt: metas $(MODULES:%=%.opt) world: all opt -metas: $(METAS) depend: $(MODULES:%=%.depend) install: $(MODULES:%=%.install) uninstall: $(MODULES:%=%.uninstall) @@ -62,33 +59,24 @@ EXTRA_DIST_CLEAN = \ .clustersdep.dot \ $(NULL) -clean_metas: - rm -f $(METAS) distclean: clean clean_metas + rm -f $(METAS) rm -f configure config.log config.cache config.status rm -f Makefile Makefile.common $(EXTRA_DIST_CLEAN) .PHONY: all opt world metas depend install uninstall clean clean_metas distclean %.all: - @OCAMLPATH=$(OCAMLPATH):$$OCAMLPATH $(MAKE) -C $* all + $(MAKE) -C $* all %.opt: - @OCAMLPATH=$(OCAMLPATH):$$OCAMLPATH $(MAKE) -C $* opt + $(MAKE) -C $* opt %.clean: - @OCAMLPATH=$(OCAMLPATH):$$OCAMLPATH $(MAKE) -C $* clean + $(MAKE) -C $* clean %.depend: - @OCAMLPATH=$(OCAMLPATH):$$OCAMLPATH $(MAKE) -C $* depend + $(MAKE) -C $* depend %.stats: @$(MAKE) -C $* .stats -$(MODULES:%=%.install): - cd $(@:%.install=%) && make install - export TARGET=$(OCAMLFIND_META_DIR)/$(@:%.install=META.helm-%) ; \ - cp METAS/$(@:%.install=meta.helm-%.src) $$TARGET && \ - echo "directory=\"$(OCAMLFIND_DEST_DIR)/$(@:%.install=%)\"" >> $$TARGET -$(MODULES:%=%.uninstall): - cd $(@:%.uninstall=%) && make uninstall - rm -f $(OCAMLFIND_META_DIR)/$(@:%.uninstall=META.helm-%) METAS/META.helm-%: METAS/meta.helm-%.src cp $< $@ && echo "directory=\"$(shell pwd)/$*\"" >> $@ diff --git a/helm/ocaml/Makefile.common.in b/helm/ocaml/Makefile.common similarity index 91% rename from helm/ocaml/Makefile.common.in rename to helm/ocaml/Makefile.common index 800bcf7c7..1a8b029f9 100644 --- a/helm/ocaml/Makefile.common.in +++ b/helm/ocaml/Makefile.common @@ -9,8 +9,7 @@ H=@ # $EXTRA_OBJECTS_TO_CLEAN # and put in a directory where there is a .depend file. -OCAMLFIND_DEST_DIR = @OCAMLFIND_DEST_DIR@ -OCAMLPATH = @OCAMLFIND_META_DIR@ +# $OCAMLFIND must be set to a meaningful vaule, including OCAMLPATH= PREPROCOPTIONS = -pp camlp4o SYNTAXOPTIONS = -syntax camlp4o @@ -18,7 +17,6 @@ PREREQ = 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) @@ -31,7 +29,7 @@ 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 = \ +LIBRARIES_DEPS := \ $(foreach X,$(filter-out /usr/lib/ocaml%,$(LIBRARIES)),\ $(wildcard \ $(shell dirname $(X))/*.mli \ @@ -95,23 +93,17 @@ $(PACKAGE).ps: .dep.dot %.ml: %.mll $(OCAMLLEX) $< +ifneq ($(MAKECMDGOALS), clean) $(IMPLEMENTATION_FILES:%.ml=%.cmo): $(LIBRARIES) $(IMPLEMENTATION_FILES:%.ml=%.cmi): $(LIBRARIES_DEPS) $(IMPLEMENTATION_FILES:%.ml=%.cmx): $(LIBRARIES_OPT) +endif clean: rm -f *.cm[ioax] *.cmxa *.o *.a *.annot $(EXTRA_OBJECTS_TO_CLEAN) if [ -f test ]; then rm -f test; else true; fi if [ -f test.opt ]; then rm -f test.opt; else true; fi -install: - mkdir $(OCAMLFIND_DEST_DIR)/$(PACKAGE) - cp $(OBJECTS_TO_INSTALL) $(OCAMLFIND_DEST_DIR)/$(PACKAGE) - -uninstall: - cd $(OCAMLFIND_DEST_DIR)/$(PACKAGE) && rm -f $(OBJECTS_TO_INSTALL) - rmdir $(OCAMLFIND_DEST_DIR)/$(PACKAGE) - backup: cd ..; tar cvzf $(PACKAGE)_$(shell date +%s).tar.gz $(PACKAGE) diff --git a/helm/ocaml/Makefile.defs.in b/helm/ocaml/Makefile.defs.in deleted file mode 100644 index a3681d0c5..000000000 --- a/helm/ocaml/Makefile.defs.in +++ /dev/null @@ -1 +0,0 @@ -OCAMLFIND = OCAMLPATH=@OCAMLPATH@ @OCAMLFIND@ diff --git a/helm/ocaml/acic_content/Makefile b/helm/ocaml/acic_content/Makefile index cc4da3781..862a9eefb 100644 --- a/helm/ocaml/acic_content/Makefile +++ b/helm/ocaml/acic_content/Makefile @@ -16,4 +16,5 @@ IMPLEMENTATION_FILES = \ cicNotationPt.ml \ $(INTERFACE_FILES:%.mli=%.ml) +include ../../Makefile.defs include ../Makefile.common diff --git a/helm/ocaml/cic/Makefile b/helm/ocaml/cic/Makefile index 4e36af019..f3d9df425 100644 --- a/helm/ocaml/cic/Makefile +++ b/helm/ocaml/cic/Makefile @@ -16,4 +16,5 @@ IMPLEMENTATION_FILES = \ EXTRA_OBJECTS_TO_INSTALL = cic.ml cic.cmi EXTRA_OBJECTS_TO_CLEAN = +include ../../Makefile.defs include ../Makefile.common diff --git a/helm/ocaml/cic_acic/Makefile b/helm/ocaml/cic_acic/Makefile index a7f1e19cf..2669afb11 100644 --- a/helm/ocaml/cic_acic/Makefile +++ b/helm/ocaml/cic_acic/Makefile @@ -9,4 +9,5 @@ INTERFACE_FILES = \ $(NULL) IMPLEMENTATION_FILES = $(INTERFACE_FILES:%.mli=%.ml) +include ../../Makefile.defs include ../Makefile.common diff --git a/helm/ocaml/cic_disambiguation/Makefile b/helm/ocaml/cic_disambiguation/Makefile index 9c231dd87..cd03e8281 100644 --- a/helm/ocaml/cic_disambiguation/Makefile +++ b/helm/ocaml/cic_disambiguation/Makefile @@ -15,7 +15,9 @@ clean: distclean: rm -f macro_table.dump +include ../../Makefile.defs include ../Makefile.common + OCAMLARCHIVEOPTIONS += -linkall disambiguateTypes.cmi: disambiguateTypes.mli diff --git a/helm/ocaml/cic_proof_checking/Makefile b/helm/ocaml/cic_proof_checking/Makefile index bb9647926..8e2f99a15 100644 --- a/helm/ocaml/cic_proof_checking/Makefile +++ b/helm/ocaml/cic_proof_checking/Makefile @@ -23,6 +23,7 @@ EXTRA_OBJECTS_TO_INSTALL = \ cicMiniReduction.cmo cicMiniReduction.cmx cicMiniReduction.o EXTRA_OBJECTS_TO_CLEAN = +include ../../Makefile.defs include ../Makefile.common cicReduction.cmo: OCAMLOPTIONS+=-rectypes diff --git a/helm/ocaml/cic_proof_checking/utilities/Makefile b/helm/ocaml/cic_proof_checking/utilities/Makefile index 174546634..383391d70 100644 --- a/helm/ocaml/cic_proof_checking/utilities/Makefile +++ b/helm/ocaml/cic_proof_checking/utilities/Makefile @@ -2,8 +2,8 @@ UTILITIES = create_environment parse_library list_uris UTILITIES_OPT = $(patsubst %,%.opt,$(UTILITIES)) LINKOPTS = -linkpkg -thread LIBS = helm-cic_proof_checking -OCAMLC = ocamlfind ocamlc $(LINKOPTS) -package $(LIBS) -OCAMLOPT = ocamlfind opt $(LINKOPTS) -package $(LIBS) +OCAMLC = $(OCAMLFIND) ocamlc $(LINKOPTS) -package $(LIBS) +OCAMLOPT = $(OCAMLFIND) opt $(LINKOPTS) -package $(LIBS) all: $(UTILITIES) @echo -n opt: $(UTILITIES_OPT) @@ -17,3 +17,5 @@ opt: $(UTILITIES_OPT) clean: rm -f $(UTILITIES) $(UTILITIES_OPT) *.cm[iox] *.o +include ../../../Makefile.defs + diff --git a/helm/ocaml/cic_unification/Makefile b/helm/ocaml/cic_unification/Makefile index 3db00fe5c..62be3a61c 100644 --- a/helm/ocaml/cic_unification/Makefile +++ b/helm/ocaml/cic_unification/Makefile @@ -9,4 +9,5 @@ INTERFACE_FILES = \ IMPLEMENTATION_FILES = $(INTERFACE_FILES:%.mli=%.ml) EXTRA_OBJECTS_TO_INSTALL = +include ../../Makefile.defs include ../Makefile.common diff --git a/helm/ocaml/configure.ac b/helm/ocaml/configure.ac deleted file mode 100644 index ec6498a7b..000000000 --- a/helm/ocaml/configure.ac +++ /dev/null @@ -1,55 +0,0 @@ -AC_INIT(Makefile.in) - -AC_CHECK_PROG(HAVE_OCAMLC, ocamlc, yes, no) -if test $HAVE_OCAMLC = "no"; then - AC_MSG_ERROR(could not find ocamlc in PATH, please make sure ocaml is installed) -fi - -AC_CHECK_PROG(HAVE_OCAMLFIND, ocamlfind, yes, no) -if test $HAVE_OCAMLFIND = "no"; then - AC_MSG_ERROR(could not find ocamlfind in PATH, please make sure findlib is installed) -else - OCAMLFIND=ocamlfind -fi - -OCAMLFIND_COMMANDS="" -AC_CHECK_PROG(HAVE_OCAMLC_OPT, ocamlc.opt, yes, no) -if test $HAVE_OCAMLC_OPT = "yes"; then - if test "$OCAMLFIND_COMMANDS" = ""; then - OCAMLFIND_COMMANDS="ocamlc=ocamlc.opt" - else - OCAMLFIND_COMMANDS="$OCAMLFIND_COMMANDS ocamlc=ocamlc.opt" - fi -fi -AC_CHECK_PROG(HAVE_OCAMLOPT_OPT, ocamlopt.opt, yes, no) -if test $HAVE_OCAMLOPT_OPT = "yes"; then - if test "$OCAMLFIND_COMMANDS" = ""; then - OCAMLFIND_COMMANDS="ocamlopt=ocamlopt.opt" - else - OCAMLFIND_COMMANDS="$OCAMLFIND_COMMANDS ocamlopt=ocamlopt.opt" - fi -fi -AC_CHECK_PROG(HAVE_OCAMLDEP_OPT, ocamldep.opt, yes, no) -if test $HAVE_OCAMLDEP_OPT = "yes"; then - if test "$OCAMLFIND_COMMANDS" = ""; then - OCAMLFIND_COMMANDS="ocamldep=ocamldep.opt" - else - OCAMLFIND_COMMANDS="$OCAMLFIND_COMMANDS ocamldep=ocamldep.opt" - fi -fi -if test "$OCAMLFIND_COMMANDS" != ""; then - OCAMLFIND="OCAMLFIND_COMMANDS='$OCAMLFIND_COMMANDS' $OCAMLFIND" -fi - -AC_MSG_CHECKING("where to install the META files") -OCAMLFIND_META_DIR=`pwd`/METAS -AC_MSG_RESULT($OCAMLFIND_META_DIR) - -AC_SUBST(OCAMLFIND) -AC_SUBST(OCAMLFIND_META_DIR) - -AC_OUTPUT([ - Makefile - Makefile.common -]) - diff --git a/helm/ocaml/content_pres/Makefile b/helm/ocaml/content_pres/Makefile index 459b793f0..0cd8b4226 100644 --- a/helm/ocaml/content_pres/Makefile +++ b/helm/ocaml/content_pres/Makefile @@ -40,6 +40,7 @@ cicNotationParser.cmx: OCAMLOPT = $(OCAMLOPT_P4) cicNotationLexer.ml.annot: OCAMLC = $(OCAMLC_P4) cicNotationParser.ml.annot: OCAMLC = $(OCAMLC_P4) +include ../../Makefile.defs include ../Makefile.common # cross compatibility among ocaml 3.09 and ocaml 3.08, to be removed as diff --git a/helm/ocaml/extlib/Makefile b/helm/ocaml/extlib/Makefile index c67778af4..d2e5cddf6 100644 --- a/helm/ocaml/extlib/Makefile +++ b/helm/ocaml/extlib/Makefile @@ -13,4 +13,5 @@ IMPLEMENTATION_FILES = \ EXTRA_OBJECTS_TO_INSTALL = EXTRA_OBJECTS_TO_CLEAN = +include ../../Makefile.defs include ../Makefile.common diff --git a/helm/ocaml/getter/Makefile b/helm/ocaml/getter/Makefile index 9ebca237a..0f2132eec 100644 --- a/helm/ocaml/getter/Makefile +++ b/helm/ocaml/getter/Makefile @@ -16,5 +16,6 @@ IMPLEMENTATION_FILES = \ http_getter_types.ml \ $(INTERFACE_FILES:%.mli=%.ml) +include ../../Makefile.defs include ../Makefile.common diff --git a/helm/ocaml/grafite/Makefile b/helm/ocaml/grafite/Makefile index 182cd4561..6eb3e7a78 100644 --- a/helm/ocaml/grafite/Makefile +++ b/helm/ocaml/grafite/Makefile @@ -10,4 +10,5 @@ IMPLEMENTATION_FILES = \ $(INTERFACE_FILES:%.mli=%.ml) +include ../../Makefile.defs include ../Makefile.common diff --git a/helm/ocaml/grafite_engine/Makefile b/helm/ocaml/grafite_engine/Makefile index e72acd29c..d810e1be2 100644 --- a/helm/ocaml/grafite_engine/Makefile +++ b/helm/ocaml/grafite_engine/Makefile @@ -9,4 +9,5 @@ INTERFACE_FILES = \ $(NULL) IMPLEMENTATION_FILES = $(INTERFACE_FILES:%.mli=%.ml) +include ../../Makefile.defs include ../Makefile.common diff --git a/helm/ocaml/grafite_parser/Makefile b/helm/ocaml/grafite_parser/Makefile index 25896da87..8482825a6 100644 --- a/helm/ocaml/grafite_parser/Makefile +++ b/helm/ocaml/grafite_parser/Makefile @@ -42,4 +42,5 @@ test_dep: test_dep.ml $(PACKAGE).cma @echo " OCAMLC $<" @$(OCAMLC) $(LOCAL_LINKOPTS) -o $@ $< +include ../../Makefile.defs include ../Makefile.common diff --git a/helm/ocaml/hbugs/Makefile b/helm/ocaml/hbugs/Makefile index c38ac3e92..4170d8081 100644 --- a/helm/ocaml/hbugs/Makefile +++ b/helm/ocaml/hbugs/Makefile @@ -24,6 +24,7 @@ INTERFACE_FILES = \ hbugs_types.mli \ $(patsubst %.ml, %.mli, $(IMPLEMENTATION_FILES)) +include ../../Makefile.defs include ../Makefile.common include .tutors.ml include .generated_tutors.ml diff --git a/helm/ocaml/hgdome/Makefile b/helm/ocaml/hgdome/Makefile index a7bb4dbb6..9630da26a 100644 --- a/helm/ocaml/hgdome/Makefile +++ b/helm/ocaml/hgdome/Makefile @@ -8,4 +8,5 @@ INTERFACE_FILES = \ IMPLEMENTATION_FILES = $(INTERFACE_FILES:%.mli=%.ml) +include ../../Makefile.defs include ../Makefile.common diff --git a/helm/ocaml/hmysql/Makefile b/helm/ocaml/hmysql/Makefile index 2ae1d4e59..8a83eb23e 100644 --- a/helm/ocaml/hmysql/Makefile +++ b/helm/ocaml/hmysql/Makefile @@ -8,4 +8,5 @@ IMPLEMENTATION_FILES = \ EXTRA_OBJECTS_TO_INSTALL = EXTRA_OBJECTS_TO_CLEAN = +include ../../Makefile.defs include ../Makefile.common diff --git a/helm/ocaml/lexicon/Makefile b/helm/ocaml/lexicon/Makefile index 0e9c09526..b8582baca 100644 --- a/helm/ocaml/lexicon/Makefile +++ b/helm/ocaml/lexicon/Makefile @@ -14,4 +14,5 @@ IMPLEMENTATION_FILES = \ $(INTERFACE_FILES:%.mli=%.ml) +include ../../Makefile.defs include ../Makefile.common diff --git a/helm/ocaml/library/Makefile b/helm/ocaml/library/Makefile index 74a61aed5..4f0ca3eb8 100644 --- a/helm/ocaml/library/Makefile +++ b/helm/ocaml/library/Makefile @@ -16,4 +16,5 @@ INTERFACE_FILES = \ IMPLEMENTATION_FILES = \ $(INTERFACE_FILES:%.mli=%.ml) +include ../../Makefile.defs include ../Makefile.common diff --git a/helm/ocaml/logger/Makefile b/helm/ocaml/logger/Makefile index dab9f5cb3..39d690084 100644 --- a/helm/ocaml/logger/Makefile +++ b/helm/ocaml/logger/Makefile @@ -5,5 +5,6 @@ INTERFACE_FILES = \ IMPLEMENTATION_FILES = \ $(INTERFACE_FILES:%.mli=%.ml) +include ../../Makefile.defs include ../Makefile.common diff --git a/helm/ocaml/metadata/Makefile b/helm/ocaml/metadata/Makefile index 0a2496451..d02d021a5 100644 --- a/helm/ocaml/metadata/Makefile +++ b/helm/ocaml/metadata/Makefile @@ -12,6 +12,7 @@ IMPLEMENTATION_FILES = $(INTERFACE_FILES:%.mli=%.ml) EXTRA_OBJECTS_TO_INSTALL = EXTRA_OBJECTS_TO_CLEAN = +include ../../Makefile.defs include ../Makefile.common all: all_table_creator all_extractor diff --git a/helm/ocaml/metadata/extractor/Makefile b/helm/ocaml/metadata/extractor/Makefile index 7c2aec0e5..579a5655f 100644 --- a/helm/ocaml/metadata/extractor/Makefile +++ b/helm/ocaml/metadata/extractor/Makefile @@ -1,4 +1,3 @@ -OCAMLFIND=ocamlfind all: extractor extractor_manager @echo -n @@ -34,3 +33,4 @@ export: extractor.opt extractor_manager.opt ./extractor_manager.opt 1>export.out 2>export.err include .depend +include ../../../Makefile.defs diff --git a/helm/ocaml/metadata/table_creator/Makefile b/helm/ocaml/metadata/table_creator/Makefile index 06335681c..c54e52d4a 100644 --- a/helm/ocaml/metadata/table_creator/Makefile +++ b/helm/ocaml/metadata/table_creator/Makefile @@ -1,5 +1,4 @@ REQUIRES = mysql helm-metadata -OCAMLFIND = ocamlfind INTERFACE_FILES = IMPLEMENTATION_FILES = $(INTERFACE_FILES:%.mli=%.ml) @@ -33,3 +32,4 @@ clean: rm -f table_creator table_creator.opt table_destructor table_destructor.opt include .depend +include ../../../Makefile.defs diff --git a/helm/ocaml/registry/Makefile b/helm/ocaml/registry/Makefile index 4d3e0a52c..bb9715ab4 100644 --- a/helm/ocaml/registry/Makefile +++ b/helm/ocaml/registry/Makefile @@ -3,5 +3,6 @@ PACKAGE = registry INTERFACE_FILES = helm_registry.mli IMPLEMENTATION_FILES = helm_registry.ml +include ../../Makefile.defs include ../Makefile.common diff --git a/helm/ocaml/tactics/Makefile b/helm/ocaml/tactics/Makefile index db8cc9231..c7bf44694 100644 --- a/helm/ocaml/tactics/Makefile +++ b/helm/ocaml/tactics/Makefile @@ -28,6 +28,7 @@ tactics.mli: tactics.ml *Tactics.mli *Tactic.mli fourierR.mli ring.mli paramodul STATS_EXCLUDE = tactics.mli +include ../../Makefile.defs include ../Makefile.common OCAMLOPTIONS+= -I paramodulation diff --git a/helm/ocaml/tactics/paramodulation/Makefile b/helm/ocaml/tactics/paramodulation/Makefile index ba8bd40aa..f1b613400 100644 --- a/helm/ocaml/tactics/paramodulation/Makefile +++ b/helm/ocaml/tactics/paramodulation/Makefile @@ -2,6 +2,7 @@ PACKAGE = dummy LOCALLINKOPTS = -package helm-cic_disambiguation,helm-content_pres,helm-grafite,helm-grafite_parser,helm-tactics +include ../../../Makefile.defs include ../../Makefile.common all $(PACKAGE).cma :saturate diff --git a/helm/ocaml/thread/Makefile b/helm/ocaml/thread/Makefile index db722abaa..46f009e07 100644 --- a/helm/ocaml/thread/Makefile +++ b/helm/ocaml/thread/Makefile @@ -6,6 +6,7 @@ IMPLEMENTATION_FILES = $(INTERFACE_FILES:%.mli=%.ml) all: thread_fake.cma opt: thread_fake.cmxa +include ../../Makefile.defs include ../Makefile.common fake/threadSafe.cmi: fake/threadSafe.mli diff --git a/helm/ocaml/urimanager/Makefile b/helm/ocaml/urimanager/Makefile index afd7d4442..592c0854e 100644 --- a/helm/ocaml/urimanager/Makefile +++ b/helm/ocaml/urimanager/Makefile @@ -6,4 +6,5 @@ IMPLEMENTATION_FILES = $(INTERFACE_FILES:%.mli=%.ml) EXTRA_OBJECTS_TO_INSTALL = EXTRA_OBJECTS_TO_CLEAN = +include ../../Makefile.defs include ../Makefile.common diff --git a/helm/ocaml/utf8_macros/Makefile b/helm/ocaml/utf8_macros/Makefile index 952b9f597..2b737627f 100644 --- a/helm/ocaml/utf8_macros/Makefile +++ b/helm/ocaml/utf8_macros/Makefile @@ -38,5 +38,6 @@ extra_clean: STATS_EXCLUDE = utf8MacroTable.ml +include ../../Makefile.defs include ../Makefile.common diff --git a/helm/ocaml/whelp/Makefile b/helm/ocaml/whelp/Makefile index f43c77fa9..6d8d3958f 100644 --- a/helm/ocaml/whelp/Makefile +++ b/helm/ocaml/whelp/Makefile @@ -7,4 +7,5 @@ INTERFACE_FILES = \ IMPLEMENTATION_FILES = $(INTERFACE_FILES:%.mli=%.ml) +include ../../Makefile.defs include ../Makefile.common diff --git a/helm/ocaml/xml/Makefile b/helm/ocaml/xml/Makefile index 6ca7bd944..7948435aa 100644 --- a/helm/ocaml/xml/Makefile +++ b/helm/ocaml/xml/Makefile @@ -8,4 +8,5 @@ IMPLEMENTATION_FILES = $(INTERFACE_FILES:%.mli=%.ml) EXTRA_OBJECTS_TO_INSTALL = EXTRA_OBJECTS_TO_CLEAN = +include ../../Makefile.defs include ../Makefile.common diff --git a/helm/ocaml/xmldiff/Makefile b/helm/ocaml/xmldiff/Makefile index 62492069e..afffaeefb 100644 --- a/helm/ocaml/xmldiff/Makefile +++ b/helm/ocaml/xmldiff/Makefile @@ -6,4 +6,5 @@ IMPLEMENTATION_FILES = $(INTERFACE_FILES:%.mli=%.ml) EXTRA_OBJECTS_TO_INSTALL = EXTRA_OBJECTS_TO_CLEAN = +include ../../Makefile.defs include ../Makefile.common -- 2.39.2