X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2FMakefile;h=fcf51b5d05f46ffc252d9b8eaad6a8c3ddb8d6b1;hb=50a9ed8c6207145fccf59e6a5dbbff935cd2c6d7;hp=46ad75c29d602211385858475d789c5101f1e62d;hpb=bc76b4d2f3c380894259b45fad52cf85ae6cee18;p=helm.git diff --git a/helm/software/matita/Makefile b/helm/software/matita/Makefile index 46ad75c29..fcf51b5d0 100644 --- a/helm/software/matita/Makefile +++ b/helm/software/matita/Makefile @@ -5,18 +5,27 @@ include ../Makefile.defs NULL = H=@ -OCAML_FLAGS = -pp $(CAMLP4O) +ifeq ($(ANNOT),true) + ANNOTOPTION = -dtypes +else + ANNOTOPTION = +endif + +OCAML_FLAGS = -pp $(CAMLP5O) -rectypes $(ANNOTOPTION) +OCAMLDEP_FLAGS = -pp $(CAMLP5O) PKGS = -package "$(MATITA_REQUIRES)" CPKGS = -package "$(MATITA_CREQUIRES)" OCAML_THREADS_FLAGS = -thread OCAML_DEBUG_FLAGS = -g +#OCAML_PROF=p -p a +#OCAMLOPT_DEBUG_FLAGS = -p 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) +OCAMLC = $(OCAMLFIND) ocamlc$(OCAML_PROF) $(OCAMLC_FLAGS) $(OCAML_DEBUG_FLAGS) +OCAMLOPT = $(OCAMLFIND) opt $(OCAMLC_FLAGS) $(OCAMLOPT_DEBUG_FLAGS) +OCAMLDEP = $(OCAMLFIND) ocamldep $(OCAMLDEP_FLAGS) INSTALL_PROGRAMS= matita matitac -INSTALL_PROGRAMS_LINKS_MATITA= cicbrowser -INSTALL_PROGRAMS_LINKS_MATITAC= matitadep matitamake matitaclean matitaprover +INSTALL_PROGRAMS_LINKS_MATITA= +INSTALL_PROGRAMS_LINKS_MATITAC= matitadep matitaclean matitawiki MATITA_FLAGS = -noprofile NODB=false @@ -24,74 +33,63 @@ ifeq ($(NODB),true) MATITA_FLAGS += -nodb endif -# objects for matita (GTK GUI) -CMOS = \ - buildTimeConf.cmo \ - lablGraphviz.cmo \ - matitaTypes.cmo \ - matitaMisc.cmo \ - matitamakeLib.cmo \ - matitaInit.cmo \ - matitaExcPp.cmo \ - matitaEngine.cmo \ - matitacLib.cmo \ - applyTransformation.cmo \ - matitaGtkMisc.cmo \ - matitaScript.cmo \ - matitaGeneratedGui.cmo \ - matitaMathView.cmo \ - matitaGui.cmo \ +MLI = \ + lablGraphviz.mli \ + matitaTypes.mli \ + matitaMisc.mli \ + applyTransformation.mli \ + matitaEngine.mli \ + matitaExcPp.mli \ + matitacLib.mli \ + matitaInit.mli \ + matitaGtkMisc.mli \ + matitaAutoGui.mli \ + virtuals.mli \ + matitaScript.mli \ + predefined_virtuals.mli \ + matitaMathView.mli \ + matitaGui.mli \ $(NULL) -# objects for matitac (batch compiler) -CCMOS = \ - buildTimeConf.cmo \ - matitaTypes.cmo \ - matitaMisc.cmo \ - matitamakeLib.cmo \ - matitaInit.cmo \ - matitaExcPp.cmo \ - matitaEngine.cmo \ - matitacLib.cmo \ - matitaprover.cmo \ +CMLI = \ + matitaTypes.mli \ + matitaMisc.mli \ + applyTransformation.mli \ + matitaEngine.mli \ + matitaExcPp.mli \ + matitacLib.mli \ + matitaInit.mli \ + matitaWiki.mli \ $(NULL) -MAINCMOS = \ - matitadep.cmo \ - matitaclean.cmo \ - matitamake.cmo \ - gragrep.cmo \ +MAINCMLI = \ + matitadep.mli \ + matitaclean.mli \ $(NULL) +# objects for matita (GTK GUI) +ML = buildTimeConf.ml matitaGeneratedGui.ml $(MLI:%.mli=%.ml) +# objects for matitac (batch compiler) +CML = buildTimeConf.ml $(CMLI:%.mli=%.ml) +MAINCML = $(MAINCMLI:%.mli=%.ml) + PROGRAMS_BYTE = \ - matita matitac cicbrowser matitadep matitaclean matitamake matitaprover -PROGRAMS = $(PROGRAMS_BYTE) matitatop + matita matitac matitadep matitaclean \ + matitawiki +PROGRAMS = $(PROGRAMS_BYTE) PROGRAMS_OPT = $(patsubst %,%.opt,$(PROGRAMS_BYTE)) -NOINST_PROGRAMS = dump_moo gragrep +NOINST_PROGRAMS = dump_moo NOINST_PROGRAMS_OPT = $(patsubst %,%.opt,$(EXTRA_PROGRAMS)) .PHONY: all all: $(PROGRAMS) $(NOINST_PROGRAMS) -# all: matita.conf.xml $(PROGRAMS) coq.moo - -# matita.conf.xml: matita.conf.xml.sample -# $(H)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 - -# coq.moo: library/legacy/coq.ma matitac -# ./matitac $(MATITA_FLAGS) $< -# coq.moo.opt: library/legacy/coq.ma matitac.opt -# ./matitac.opt $(MATITA_FLAGS) $< +CMOS = $(ML:%.ml=%.cmo) +CCMOS = $(CML:%.ml=%.cmo) +MAINCMOS = $(MAINCML:%.ml=%.cmo) CMXS = $(patsubst %.cmo,%.cmx,$(CMOS)) CCMXS = $(patsubst %.cmo,%.cmx,$(CCMOS)) MAINCMXS = $(patsubst %.cmo,%.cmx,$(MAINCMOS)) +$(CMOS) : $(LIB_DEPS) +$(CMXOS): $(LIBX_DEPS) + 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)) @@ -115,6 +113,12 @@ links: $(H)ln -sf matita.opt matita $(H)ln -sf matitac.opt matitac +linkonly: + $(H)echo " OCAMLC matita.ml" + $(H)$(OCAMLC) $(PKGS) -linkpkg -o matita $(CMOS) $(OCAML_DEBUG_FLAGS) matita.ml + $(H)echo " OCAMLC matitac.ml" + $(H)$(OCAMLC) $(CPKGS) -linkpkg -o matitac $(CCMOS) $(MAINCMOS) $(OCAML_DEBUG_FLAGS) matitac.ml +.PHONY: linkonly matita: matita.ml $(LIB_DEPS) $(CMOS) $(H)echo " OCAMLC $<" $(H)$(OCAMLC) $(PKGS) -linkpkg -o $@ $(CMOS) matita.ml @@ -136,52 +140,42 @@ matitac.opt: matitac.ml $(CLIBX_DEPS) $(CCMXS) $(MAINCMXS) $(H)echo " OCAMLOPT $<" $(H)$(OCAMLOPT) $(CPKGS) -linkpkg -o $@ $(CCMXS) $(MAINCMXS) matitac.ml -matitatop: matitatop.ml $(CLIB_DEPS) $(CCMOS) +rottener: rottener.ml $(CLIB_DEPS) $(CCMOS) $(MAINCMOS) $(H)echo " OCAMLC $<" - $(H)$(OCAMLC) $(CPKGS) -linkpkg -o $@ toplevellib.cma $(CCMOS) $< - -matitaprover: matitac - $(H)test -f $@ || ln -s $< $@ -matitaprover.opt: matitac.opt - $(H)test -f $@ || ln -s $< $@ + $(H)$(OCAMLC) $(CPKGS) -package lablgtk2 -linkpkg -o $@ $(CCMOS) $(MAINCMOS) rottener.ml +rottener.opt: rottener.ml $(CLIBX_DEPS) $(CCMXS) $(MAINCMXS) + $(H)echo " OCAMLOPT $<" + $(H)$(OCAMLOPT) $(CPKGS) -package lablgtk2 -linkpkg -o $@ $(CCMXS) $(MAINCMXS) rottener.ml +clean-rottened: + find . -type f -name "*.ma.*.rottened" -exec rm {} \; matitadep: matitac $(H)test -f $@ || ln -s $< $@ matitadep.opt: matitac.opt $(H)test -f $@ || ln -s $< $@ -matitaclean: matitac +matitawiki: matitac $(H)test -f $@ || ln -s $< $@ -matitaclean.opt: matitac.opt +matitawiki.opt: matitac.opt $(H)test -f $@ || ln -s $< $@ -matitamake: matitac - $(H)test -f $@ || ln -s $< $@ -matitamake.opt: matitac.opt - $(H)test -f $@ || ln -s $< $@ - -gragrep: matitac - $(H)test -f $@ || ln -s $< $@ -gragrep.opt: matitac.opt - $(H)test -f $@ || ln -s $< $@ - -cicbrowser: matita +matitaclean: matitac $(H)test -f $@ || ln -s $< $@ -cicbrowser.opt: matita.opt +matitaclean.opt: matitac.opt $(H)test -f $@ || ln -s $< $@ -matitaGeneratedGui.ml matitaGeneratedGui.mli: matita.glade +matitaGeneratedGui.ml: matita.glade $(H)$(LABLGLADECC) -embed $< > matitaGeneratedGui.ml - $(H)rm -f matitaGeneratedGui.mli - $(H)#$(OCAMLC) $(PKGS) -i matitaGeneratedGui.ml > matitaGeneratedGui.mli .PHONY: clean clean: $(H)rm -rf *.cma *.cmo *.cmi *.cmx *.cmxa *.a *.o \ $(PROGRAMS) $(PROGRAMS_OPT) \ + rottener rottener.opt \ $(NOINST_PROGRAMS) $(NOINST_PROGRAMS_OPT) \ $(PROGRAMS_STATIC) \ $(PROGRAMS_UPX) \ + *.stamp \ $(NULL) .PHONY: distclean @@ -193,18 +187,30 @@ distclean: clean $(H)rm -f matita.conf.xml.sample $(H)rm -rf .matita -TEST_DIRS = \ - library \ - tests \ - contribs/LAMBDA-TYPES \ - contribs/PREDICATIVE-TOPOLOGY \ +TEST_DIRS = \ + legacy \ + library \ + contribs/character \ + tests \ + contribs/dama/dama \ + contribs/assembly \ + contribs/CoRN \ + contribs/RELATIONAL \ + contribs/LOGIC \ + contribs/limits \ + $(NULL) + +# library_auto +TEST_DIRS_OPT = \ + $(TEST_DIRS) \ +# contribs/LAMBDA-TYPES \ $(NULL) .PHONY: tests tests.opt cleantests cleantests.opt tests: $(foreach d,$(TEST_DIRS),$(d)-test) -tests.opt: $(foreach d,$(TEST_DIRS),$(d)-test-opt) +tests.opt: $(foreach d,$(TEST_DIRS_OPT),$(d)-test-opt) cleantests: $(foreach d,$(TEST_DIRS),$(d)-cleantests) -cleantests.opt: $(foreach d,$(TEST_DIRS),$(d)-cleantests-opt) +cleantests.opt: $(foreach d,$(TEST_DIRS_OPT),$(d)-cleantests-opt) %-test: matitac matitadep matitaclean -cd $* && make -k clean all @@ -219,22 +225,25 @@ cleantests.opt: $(foreach d,$(TEST_DIRS),$(d)-cleantests-opt) ifeq ($(DISTRIBUTED),yes) -dist_library: dist_library@standard-library -dist_library@%: - $(H)echo "MATITAMAKE init $*" - $(H)(cd $(DESTDIR) && ./matitamake init $* $(DESTDIR)/ma/$*) - $(H)echo "MATITAMAKE publish $*" - $(H)(cd $(DESTDIR) && ./matitamake publish $*) - $(H)echo "MATITAMAKE destroy $*" - $(H)(cd $(DESTDIR) && ./matitamake destroy $*) + +dist_library: install_preliminaries + $(H)echo "depend" + $(H)cd $(WHERE)/ma/standard-library;(HOME=$(WHERE) USER=builder MATITA_RT_BASE_DIR=$(WHERE) MATITA_FLAGS='$(MATITA_CFLAGS)' $(WHERE)/matitadep) + $(H)echo "publish" + $(H)cd $(WHERE)/ma/standard-library;(HOME=$(WHERE) USER=builder MATITA_RT_BASE_DIR=$(WHERE) MATITA_FLAGS='$(MATITA_CFLAGS)' $(WHERE)/matitac -system -noinnertypes) + $(H)echo "destroy" + $(H)cd $(WHERE)/ma/standard-library;(HOME=$(WHERE) USER=builder MATITA_RT_BASE_DIR=$(WHERE) MATITA_FLAGS='$(MATITA_CFLAGS)' $(WHERE)/matitaclean) +# sqlite3 only + $(H)cp $(WHERE)/.matita/matita.db $(WHERE)/metadata.db || true +#$(H)rm -rf $(WHERE)/.matita/ touch $@ endif -dist_pre: matitaGeneratedGui.ml matitaGeneratedGui.mli +dist_pre: matitaGeneratedGui.ml $(MAKE) -C dist/ dist_pre -DESTDIR = $(RT_BASE_DIR) +WHERE = $(DESTDIR)/$(RT_BASE_DIR) INSTALL_STUFF = \ icons/ \ help/ \ @@ -245,7 +254,6 @@ INSTALL_STUFF = \ matita.conf.xml \ closed.xml \ gtkmathview.matita.conf.xml \ - template_makefile.in \ AUTHORS \ LICENSE \ $(NULL) @@ -256,30 +264,33 @@ else INSTALL_STUFF_BIN = $(INSTALL_PROGRAMS) endif -install: install_preliminaries dist_library install_conclusion +install-arch: install_preliminaries +install-indep: + +install_preliminaries : install_preliminaries.stamp -install_preliminaries: - install -d $(DESTDIR)/ma/ - cp -a $(INSTALL_STUFF) $(DESTDIR) +install_preliminaries.stamp: + $(H)install -d $(WHERE)/ma/ + $(H)cp -a $(INSTALL_STUFF) $(WHERE) ifeq ($(HAVE_OCAMLOPT),yes) - install -s $(INSTALL_STUFF_BIN) $(DESTDIR) - for p in $(INSTALL_PROGRAMS); do ln -fs $$p.opt $(DESTDIR)/$$p; done + $(H)install -s $(INSTALL_STUFF_BIN) $(WHERE) + $(H)for p in $(INSTALL_PROGRAMS); do ln -fs $$p.opt $(WHERE)/$$p; done else - install $(INSTALL_STUFF_BIN) $(DESTDIR) + $(H)install $(INSTALL_STUFF_BIN) $(WHERE) endif - for p in $(INSTALL_PROGRAMS_LINKS_MATITAC); do \ - ln -fs matitac $(DESTDIR)/$$p;\ + $(H)for p in $(INSTALL_PROGRAMS_LINKS_MATITAC); do \ + ln -fs matitac $(WHERE)/$$p;\ done - for p in $(INSTALL_PROGRAMS_LINKS_MATITA); do \ - ln -fs matita $(DESTDIR)/$$p;\ + $(H)for p in $(INSTALL_PROGRAMS_LINKS_MATITA); do \ + ln -fs matita $(WHERE)/$$p;\ done - cp -a library/ $(DESTDIR)/ma/standard-library - cp -a contribs/ $(DESTDIR)/ma/ + $(H)cp -a library/ $(WHERE)/ma/standard-library + $(H)cp -a nlibrary/ $(WHERE)/ma/new-standard-library -install_conclusion: + $(H)touch install_preliminaries.stamp uninstall: - rm -rf $(DESTDIR) + $(H)rm -rf $(WHERE) STATIC_LINK = dist/static_link/static_link # for matita @@ -298,6 +309,14 @@ STATIC_CLIBS = \ gdome \ mysqlclient \ $(NULL) +STATIC_CLIBS_PROVER = \ + $(STATIC_CLIBS) \ + z \ + pcre \ + expat \ + xml2 \ + glib-2.0 \ + $(NULL) STATIC_EXTRA_CLIBS = PROGRAMS_STATIC = $(patsubst %,%.static,$(PROGRAMS_OPT)) PROGRAMS_UPX = $(patsubst %,%.upx,$(PROGRAMS_STATIC)) @@ -331,15 +350,9 @@ matitac.opt.static: $(STATIC_LINK) $(CLIBX_DEPS) $(CCMXS) $(MAINCMXS) matitac.ml strip $@ matitadep.opt.static: matitac.opt.static $(H)test -f $@ || ln -s $< $@ -matitaprover.opt.static: matitac.opt.static - $(H)test -f $@ || ln -s $< $@ matitaclean.opt.static: matitac.opt.static $(H)test -f $@ || ln -s $< $@ -matitamake.opt.static: matitac.opt.static - $(H)test -f $@ || ln -s $< $@ -cicbrowser.opt.static: matita.opt.static - $(H)test -f $@ || ln -s $< $@ -cicbrowser.opt.static.upx: matita.opt.static.upx +matitawiki.opt.static: matitac.opt.static $(H)test -f $@ || ln -s $< $@ %.upx: % @@ -349,26 +362,55 @@ cicbrowser.opt.static.upx: matita.opt.static.upx # }}} End of distribution stuff +# {{{ Deps and automatic rules tags: TAGS .PHONY: TAGS TAGS: $(H)cd ..; otags -vi -r components/ matita/ -#.depend: matitaGeneratedGui.ml matitaGeneratedGui.mli *.ml *.mli - .PHONY: depend - -depend: + +depend: $(H)echo " OCAMLDEP" $(H)$(OCAMLDEP) *.ml *.mli > .depend -depend.opt: +depend.opt: $(H)echo " OCAMLDEP -native" - $(H)$(OCAMLDEP) -native *.ml *.mli > .depend + $(H)$(OCAMLDEP) -native *.ml *.mli > .depend.opt + +# this should be sligtly better, since should work with 'make all opt' +MAKECMDGOALS_DELIM=$(addprefix _x_,$(addsuffix _x_,$(MAKECMDGOALS))) +ifneq (,$(findstring _x_all_x_,$(MAKECMDGOALS_DELIM))) + # if we 'make all opt' the deps for 'all' should be fine also for opt + # if we 'make opt all' it should not work... + INCLUDE_MANDATORY=yes + TO_INCLUDE+=.depend + TO_DEPEND_ON=$(LIB_DEPS) +else ifneq (,$(findstring _x_opt_x_,$(MAKECMDGOALS_DELIM))) + INCLUDE_MANDATORY=yes + TO_INCLUDE+=.depend.opt + TO_DEPEND_ON=$(LIBX_DEPS) +else ifneq (,$(findstring _x_world_x_,$(MAKECMDGOALS_DELIM))) + ifeq ($(HAVE_OCAMLOPT),yes) + INCLUDE_MANDATORY=yes + TO_INCLUDE+=.depend.opt + TO_DEPEND_ON=$(LIBX_DEPS) + else + INCLUDE_MANDATORY=yes + TO_INCLUDE+=.depend + TO_DEPEND_ON=$(LIB_DEPS) + endif +else + TO_INCLUDE+=.depend + INCLUDE_MANDATORY=no + TO_DEPEND_ON=$(LIB_DEPS) +endif + +$(MLI:%.mli=%.cmi) $(ML:%.ml=%.cmo) $(ML:%.ml=%.cmx): $(TO_DEPEND_ON) -ifneq ($(MAKECMDGOALS), depend) - ifneq ($(MAKECMDGOALS), depend.opt) - include .depend - endif +ifeq (no,$(INCLUDE_MANDATORY)) + -include $(TO_INCLUDE) +else + include $(TO_INCLUDE) endif %.cmi: %.mli @@ -384,17 +426,11 @@ endif $(H)echo " OCAMLC -dtypes $<" $(H)$(OCAMLC) -dtypes $(PKGS) -c $< -$(CMOS): $(LIB_DEPS) -$(CMOS:%.cmo=%.cmx): $(LIBX_DEPS) +deps.ps: deps.dot + dot -Tps -o $@ $< +deps.dot: .depend + ./dep2dot.rb < $< | tred > $@ -ifeq ($(MAKECMDGOALS),all) - $(CMOS:%.cmo=%.cmi): $(LIB_DEPS) -endif -ifeq ($(MAKECMDGOALS),) - $(CMOS:%.cmo=%.cmi): $(LIB_DEPS) -endif -ifeq ($(MAKECMDGOALS),opt) - $(CMOS:%.cmo=%.cmi): $(LIBX_DEPS) -endif +# }}} End of deps and automatic rules # vim: set foldmethod=marker: