X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FMakefile.in;h=127f8a407638086f975ada39664ed1da040f4253;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=428492209c6f4baacd421db3541c560eec715636;hpb=9d8e81db720417f58591ea42f72c6750b886a83d;p=helm.git diff --git a/helm/matita/Makefile.in b/helm/matita/Makefile.in index 428492209..127f8a407 100644 --- a/helm/matita/Makefile.in +++ b/helm/matita/Makefile.in @@ -1,59 +1,149 @@ +export SHELL=/bin/bash +NULL = + +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@ OCAML_FLAGS = -pp $(CAMLP4O) PKGS = -package "$(REQUIRES)" CPKGS = -package "$(CREQUIRES)" +DEPPKGS = -package "$(DEPREQUIRES)" +CLEANPKGS = -package "$(CLEANREQUIRES)" +MAKEPKGS = -package "$(MAKEREQUIRES)" OCAML_THREADS_FLAGS = -thread OCAML_DEBUG_FLAGS = -g OCAMLC_FLAGS = $(OCAML_FLAGS) $(OCAML_THREADS_FLAGS) OCAMLC = $(OCAMLFIND) ocamlc $(OCAMLC_FLAGS) $(OCAML_DEBUG_FLAGS) OCAMLOPT = $(OCAMLFIND) opt $(OCAMLC_FLAGS) OCAMLDEP = $(OCAMLFIND) ocamldep $(OCAML_FLAGS) + +MATITA_FLAGS = -noprofile +NODB=false +ifeq ($(NODB),true) + MATITA_FLAGS += -nodb +endif + # objects for matita (GTK GUI) CMOS = \ buildTimeConf.cmo \ matitaLog.cmo \ matitaTypes.cmo \ + matitaMoo.cmo \ matitaMisc.cmo \ matitaDb.cmo \ + matitamakeLib.cmo \ + matitaInit.cmo \ matitaSync.cmo \ matitaDisambiguator.cmo \ + matitaExcPp.cmo \ + matitacleanLib.cmo \ matitaEngine.cmo \ + matitacLib.cmo \ matitaScript.cmo \ matitaGeneratedGui.cmo \ matitaGtkMisc.cmo \ + matitaMathView.cmo \ matitaGui.cmo \ - matitaMathView.cmo + $(NULL) # objects for matitac (batch compiler) CCMOS = \ buildTimeConf.cmo \ matitaLog.cmo \ matitaTypes.cmo \ + matitaMoo.cmo \ matitaMisc.cmo \ matitaDb.cmo \ + matitamakeLib.cmo \ + matitaInit.cmo \ matitaSync.cmo \ matitaDisambiguator.cmo \ - matitaEngine.cmo + matitaExcPp.cmo \ + matitacleanLib.cmo \ + matitaEngine.cmo \ + matitacLib.cmo \ + $(NULL) +MAINCMOS = \ + matitadep.cmo \ + matitaclean.cmo \ + matitamake.cmo \ + $(NULL) +DEPCMOS = $(CCMOS) +CLEANCMOS = $(CCMOS) +MAKECMOS = \ + buildTimeConf.cmo \ + matitaLog.cmo \ + matitamakeLib.cmo \ + $(NULL) +PROGRAMS_BYTE = matita matitac cicbrowser matitadep matitaclean matitamake dump_moo +PROGRAMS = $(PROGRAMS_BYTE) matitatop +PROGRAMS_OPT = $(patsubst %,%.opt,$(PROGRAMS_BYTE)) + +.PHONY: all +all: matita.conf.xml $(PROGRAMS) coq.moo +matita.conf.xml: matita.conf.xml.sample + @if diff matita.conf.xml.sample matita.conf.xml 1>/dev/null 2>/dev/null; then\ + touch matita.conf.xml;\ + else\ + echo;\ + echo "matita.conf.xml.sample is newer than matita.conf.xml";\ + echo;\ + echo "PLEASE update your configuration file!";\ + echo "(copying matita.conf.xml.sample should work)";\ + echo;\ + false;\ + fi -all: matita matitac cicbrowser +matita.conf.xml.sample: matita.conf.xml.sample.in + autoconf + ./configure + @echo + @echo "WARNING: The configuration sample file has changed!" + @echo + +coq.moo: coq.ma matitac + ./matitac $(MATITA_FLAGS) coq.ma +coq.moo.opt: coq.ma matitac.opt + ./matitac.opt $(MATITA_FLAGS) coq.ma 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)) -opt: matita.opt matitac.opt cicbrowser.opt +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)) +.PHONY: opt +opt: $(PROGRAMS_OPT) coq.moo.opt +.PHONY: upx +upx: $(PROGRAMS_UPX) coq.moo.opt + else + opt: @echo "Native code compilation is disabled" + endif matita: $(LIB_DEPS) $(CMOS) matita.ml @@ -61,11 +151,46 @@ matita: $(LIB_DEPS) $(CMOS) matita.ml matita.opt: $(LIBX_DEPS) $(CMXS) matita.ml $(OCAMLOPT) $(PKGS) -linkpkg -o $@ $(CMXS) matita.ml -matitac: $(LIB_DEPS) $(CCMOS) matitac.ml - $(OCAMLC) $(CPKGS) -linkpkg -o $@ $(CCMOS) matitac.ml -matitac.opt: $(LIBX_DEPS) $(CCMXS) matitac.ml - $(OCAMLOPT) $(CPKGS) -linkpkg -o $@ $(CCMXS) matitac.ml +dump_moo: buildTimeConf.cmo matitaLog.cmo matitaMoo.cmo dump_moo.ml + $(OCAMLC) $(PKGS) -linkpkg -o $@ $^ +dump_moo.opt: buildTimeConf.cmx matitaLog.cmx matitaMoo.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 + +matitatop: matitatop.ml $(CLIB_DEPS) $(CCMOS) + $(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 + @test -f $@ || ln -s $< $@ + cicbrowser: matita @test -f $@ || ln -s $< $@ cicbrowser.opt: matita.opt @@ -75,30 +200,132 @@ matitaGeneratedGui.ml matitaGeneratedGui.mli: matita.glade $(LABLGLADECC) -embed $< > matitaGeneratedGui.ml $(OCAMLC) $(PKGS) -i matitaGeneratedGui.ml > matitaGeneratedGui.mli -%.cmi: %.mli - $(OCAMLC) $(PKGS) -c $< -%.cmo %.cmi: %.ml - $(OCAMLC) $(PKGS) -c $< -%.cmx: %.ml - $(OCAMLOPT) $(PKGS) -c $< -%.annot: %.ml - $(OCAMLC) -dtypes $(PKGS) -c $< - +.PHONY: clean clean: - rm -rf *.cma *.cmo *.cmi *.cmx *.cmxa *.a *.o \ - matita matita.opt matitac matitac.opt \ - cicbrowser cicbrowser.opt + rm -rf *.cma *.cmo *.cmi *.cmx *.cmxa *.a *.o \ + $(PROGRAMS) \ + $(PROGRAMS_OPT) \ + $(PROGRAMS_STATIC) \ + $(PROGRAMS_UPX) \ + $(NULL) + +tests: matitac matitadep matitaclean + @-(cd library && make -k clean all) + @-(cd tests && make -k clean all) + @-(cd tests/bad_tests && make -k clean all) + @-(cd contribs/LAMBDA-TYPES && make -k clean all) + @-(cd contribs/PREDICATIVE-TOPOLOGY && make -k clean all) +tests.opt: matitac.opt matitadep.opt matitaclean.opt + @-(cd library && make -k clean.opt opt) + @-(cd tests && make -k clean.opt opt) + @-(cd tests/bad_tests && make -k clean.opt opt) + @-(cd contribs/LAMBDA-TYPES && make -k clean.opt opt) + @-(cd contribs/PREDICATIVE-TOPOLOGY && make -k clean.opt opt) +cleantests: matitaclean + @(cd library && make clean) + @(cd tests && make clean) + @(cd tests/bad_tests && make clean) + @(cd contribs/LAMBDA-TYPES && make clean) + @(cd contribs/PREDICATIVE-TOPOLOGY && make clean) +cleantests.opt: matitaclean.opt + @(cd library && make clean.opt) + @(cd tests && make clean.opt) + @(cd tests/bad_tests && make clean) + @(cd contribs/LAMBDA-TYPES && make clean.opt) + @(cd contribs/PREDICATIVE-TOPOLOGY && make clean.opt) +.PHONY: tests tests.opt cleantests cleantests.opt + +# {{{ Distribution stuff + +STATIC_LINK = dist/static_link/static_link +# for matita +STATIC_LIBS = \ + t1 t1x \ + gtkmathview_gmetadom mathview mathview_backend_gtk mathview_frontend_gmetadom \ + gtksourceview-1.0 \ + gdome gmetadom_gdome_cpp_smart \ + stdc++ \ + mysqlclient \ + expat \ + $(NULL) +STATIC_EXTRA_LIBS = -cclib -lt1x -cclib -lstdc++ +# for matitac & co +STATIC_CLIBS = \ + gdome \ + mysqlclient \ + $(NULL) +STATIC_EXTRA_CLIBS = +PROGRAMS_STATIC = $(patsubst %,%.static,$(PROGRAMS_OPT)) +PROGRAMS_UPX = $(patsubst %,%.upx,$(PROGRAMS_STATIC)) + +ifeq ($(HAVE_OCAMLOPT),yes) +static: $(STATIC_LINK) $(PROGRAMS_STATIC) coq.moo.opt +else +upx: + @echo "Native code compilation is disabled" +static: + @echo "Native code compilation is disabled" +endif + +$(STATIC_LINK): + $(MAKE) -C dist/ $(STATIC_LINK) + +matita.opt.static: $(STATIC_LINK) $(LIBX_DEPS) $(CMXS) matita.ml + $(STATIC_LINK) $(STATIC_LIBS) -- \ + $(OCAMLOPT) $(PKGS) -linkpkg -o $@ $(CMXS) matita.ml \ + $(STATIC_EXTRA_LIBS) + strip $@ +dump_moo.opt.static: $(STATIC_LINK) buildTimeConf.cmx matitaLog.cmx matitaMoo.cmx dump_moo.ml + $(STATIC_LINK) $(STATIC_CLIBS) -- \ + $(OCAMLOPT) $(PKGS) -linkpkg -o $@ $^ \ + $(STATIC_EXTRA_CLIBS) + strip $@ +matitac.opt.static: $(STATIC_LINK) $(CLIBX_DEPS) $(CCMXS) $(MAINCMXS) matitac.ml + $(STATIC_LINK) $(STATIC_CLIBS) -- \ + $(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 + @test -f $@ || ln -s $< $@ +cicbrowser.opt.static.upx: matita.opt.static.upx + @test -f $@ || ln -s $< $@ + +.PHONY: distclean distclean: clean + $(MAKE) -C dist/ clean rm -f matitaGeneratedGui.ml matitaGeneratedGui.mli rm -f config.log config.status Makefile buildTimeConf.ml rm -f matita.glade.bak matita.gladep.bak rm -rf autom4te.cache/ + rm -f configure matita.conf.xml.sample -tests: matita - @scripts/do_tests.sh ./matitac /dev/null tests/*.ma -tests.opt: matitac.opt - @scripts/do_tests.sh ./matitac.opt /dev/null tests/*.ma -.PHONY: tests tests.opt +%.upx: % + cp $< $@ + strip $@ + upx $@ + +# }}} End of distribution stuff tags: TAGS .PHONY: TAGS @@ -106,12 +333,21 @@ TAGS: cd ..; otags -vi -r ocaml/ matita/ #.depend: matitaGeneratedGui.ml matitaGeneratedGui.mli *.ml *.mli + +.PHONY: depend depend: $(OCAMLDEP) *.ml *.mli > .depend include .depend -.PHONY: all opt clean distclean depend +%.cmi: %.mli + $(OCAMLC) $(PKGS) -c $< +%.cmo %.cmi: %.ml + $(OCAMLC) $(PKGS) -c $< +%.cmx: %.ml + $(OCAMLOPT) $(PKGS) -c $< +%.annot: %.ml + $(OCAMLC) -dtypes $(PKGS) -c $< $(CMOS): $(LIB_DEPS) $(CMOS:%.cmo=%.cmx): $(LIBX_DEPS) @@ -125,3 +361,5 @@ endif ifeq ($(MAKECMDGOALS),opt) $(CMOS:%.cmo=%.cmi): $(LIBX_DEPS) endif + +# vim: set foldmethod=marker: