X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2FMakefile;h=ad5a18892524466da938e2e6f8e9d0714adb3ee1;hb=f2e7cb9757a151382ed3a70d1a610e8f729a6597;hp=27febffb70b43d580f955618dd5a3b60f12fecf6;hpb=3160525c13f570858fe43319bb75239f46831f0a;p=helm.git

diff --git a/matita/Makefile b/matita/Makefile
index 27febffb7..ad5a18892 100644
--- a/matita/Makefile
+++ b/matita/Makefile
@@ -5,18 +5,21 @@ include ../Makefile.defs
 NULL =
 H=@
 
-OCAML_FLAGS = -pp $(CAMLP4O)
+OCAML_FLAGS = -pp $(CAMLP5O) -rectypes
+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
+INSTALL_PROGRAMS_LINKS_MATITAC= matitadep matitamake matitaclean matitaprover matitawiki
 
 MATITA_FLAGS = -noprofile
 NODB=false
@@ -24,42 +27,50 @@ ifeq ($(NODB),true)
 	MATITA_FLAGS += -nodb
 endif
 
-# objects for matita (GTK GUI)
-CMOS =				\
-	buildTimeConf.cmo	\
-	matitaTypes.cmo		\
-	matitaMisc.cmo		\
-	matitamakeLib.cmo	\
-	matitaInit.cmo		\
-	matitaExcPp.cmo 	\
-	matitaEngine.cmo	\
-	matitacLib.cmo		\
-	matitaScript.cmo	\
-	matitaGeneratedGui.cmo	\
-	matitaGtkMisc.cmo	\
-	applyTransformation.cmo	\
-	matitaMathView.cmo 	\
-	matitaGui.cmo		\
+MLI = \
+	lablGraphviz.mli	\
+	matitaTypes.mli		\
+	matitaMisc.mli		\
+	matitamakeLib.mli	\
+	matitaExcPp.mli 	\
+	matitaInit.mli		\
+	matitaEngine.mli	\
+	applyTransformation.mli	\
+	matitaAutoGui.mli	\
+	matitacLib.mli		\
+	matitaprover.mli        \
+	matitaGtkMisc.mli	\
+	matitaScript.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		\
+CMLI =				\
+	matitaTypes.mli		\
+	matitaMisc.mli		\
+	matitamakeLib.mli	\
+	matitaExcPp.mli 	\
+	matitaInit.mli		\
+	matitaEngine.mli	\
+	applyTransformation.mli	\
+	matitacLib.mli		\
+	matitaWiki.mli		\
+	matitaprover.mli        \
 	$(NULL)
-MAINCMOS =			\
-	matitadep.cmo		\
-	matitaclean.cmo		\
-	matitamake.cmo		\
-	gragrep.cmo 		\
+MAINCMLI =			\
+	matitadep.mli		\
+	matitaclean.mli		\
+	matitamake.mli		\
+	gragrep.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
+	matita matitac cicbrowser matitadep matitaclean \
+	matitamake matitaprover matitawiki
 PROGRAMS = $(PROGRAMS_BYTE) matitatop
 PROGRAMS_OPT = $(patsubst %,%.opt,$(PROGRAMS_BYTE))
 NOINST_PROGRAMS = dump_moo gragrep
@@ -67,29 +78,16 @@ 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))
@@ -110,7 +108,15 @@ links:
 			$(INSTALL_PROGRAMS_LINKS_MATITA); do\
 		ln -sf $$X.opt $$X;\
 	done
-
+	$(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) matita.ml
+	$(H)echo "  OCAMLC matitac.ml"
+	$(H)$(OCAMLC) $(CPKGS) -linkpkg -o matitac $(CCMOS) $(MAINCMOS) matitac.ml
+.PHONY: linkonly
 matita: matita.ml $(LIB_DEPS) $(CMOS)
 	$(H)echo "  OCAMLC $<"
 	$(H)$(OCAMLC) $(PKGS) -linkpkg -o $@ $(CMOS) matita.ml
@@ -136,11 +142,21 @@ matitatop: matitatop.ml $(CLIB_DEPS) $(CCMOS)
 	$(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 $< $@
+
 matitadep: matitac
 	$(H)test -f $@ || ln -s $< $@
 matitadep.opt: matitac.opt
 	$(H)test -f $@ || ln -s $< $@
 
+matitawiki: matitac
+	$(H)test -f $@ || ln -s $< $@
+matitawiki.opt: matitac.opt
+	$(H)test -f $@ || ln -s $< $@
+
 matitaclean: matitac
 	$(H)test -f $@ || ln -s $< $@
 matitaclean.opt: matitac.opt
@@ -161,10 +177,8 @@ cicbrowser: matita
 cicbrowser.opt: matita.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:
@@ -173,6 +187,7 @@ clean:
 		$(NOINST_PROGRAMS) $(NOINST_PROGRAMS_OPT) \
 		$(PROGRAMS_STATIC) \
 		$(PROGRAMS_UPX) \
+		*.stamp \
 		$(NULL)
 
 .PHONY: distclean
@@ -185,17 +200,27 @@ distclean: clean
 	$(H)rm -rf .matita
 
 TEST_DIRS = 				\
+	legacy                          \
 	library 			\
 	tests 				\
+	dama				\
+	contribs/CoRN	 	        \
+	contribs/RELATIONAL	 	\
+	contribs/LOGIC	       	 	\
 	contribs/LAMBDA-TYPES 		\
 	contribs/PREDICATIVE-TOPOLOGY 	\
 	$(NULL)
 
+#	library_auto 			
+TEST_DIRS_OPT = 			\
+	$(TEST_DIRS)        \
+	$(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
@@ -210,19 +235,26 @@ cleantests.opt: $(foreach d,$(TEST_DIRS),$(d)-cleantests-opt)
 
 ifeq ($(DISTRIBUTED),yes)
 
-dist_library: dist_library@standard-library
-dist_library@%:
+
+dist_library: install_preliminaries dist_library@standard-library
+dist_library@%: 
 	$(H)echo "MATITAMAKE init $*"
-	$(H)(cd $(DESTDIR) && ./matitamake init $* $(DESTDIR)/ma/$*)
+	$(H)(HOME=$(WHERE) USER=builder MATITA_RT_BASE_DIR=$(WHERE) MATITA_FLAGS='$(MATITA_CFLAGS)' $(WHERE)/matitamake init $* $(WHERE)/ma/$*)
 	$(H)echo "MATITAMAKE publish $*"
-	$(H)(cd $(DESTDIR) && ./matitamake publish $*)
+	$(H)(HOME=$(WHERE) USER=builder MATITA_RT_BASE_DIR=$(WHERE) MATITA_FLAGS='$(MATITA_CFLAGS)' $(WHERE)/matitamake publish $*)
 	$(H)echo "MATITAMAKE destroy $*"
-	$(H)(cd $(DESTDIR) && ./matitamake destroy $*)
+	$(H)(HOME=$(WHERE) USER=builder MATITA_RT_BASE_DIR=$(WHERE) MATITA_FLAGS='$(MATITA_CFLAGS)' $(WHERE)/matitamake destroy $*)
+	# sqlite3 only
+	$(H)cp $(WHERE)/.matita/matita.db  $(WHERE)/metadata.db || true
+	#$(H)rm -rf $(WHERE)/.matita/
 	touch $@
 
 endif
 
-DESTDIR = $(RT_BASE_DIR)
+dist_pre: matitaGeneratedGui.ml
+	$(MAKE) -C dist/ dist_pre
+
+WHERE = $(DESTDIR)/$(RT_BASE_DIR)
 INSTALL_STUFF = 			\
 	icons/ 				\
 	help/ 				\
@@ -244,30 +276,32 @@ else
 INSTALL_STUFF_BIN = $(INSTALL_PROGRAMS)
 endif
 
-install: install_preliminaries dist_library install_conclusion
+install-arch: install_preliminaries 
+install-indep: dist_library 
+
+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/
-
-install_conclusion:
+	$(H)cp -a library/ $(WHERE)/ma/standard-library
+	#$(H)cp -a contribs/ $(WHERE)/ma/
+	$(H)touch install_preliminaries.stamp
 
 uninstall:
-	rm -rf $(DESTDIR)
+	$(H)rm -rf $(WHERE)
 
 STATIC_LINK = dist/static_link/static_link
 # for matita
@@ -286,6 +320,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))
@@ -317,10 +359,17 @@ matitac.opt.static: $(STATIC_LINK) $(CLIBX_DEPS) $(CCMXS) $(MAINCMXS) matitac.ml
 		$(OCAMLOPT) $(CPKGS) -linkpkg -o $@ $(CCMXS) $(MAINCMXS) matitac.ml \
 		$(STATIC_EXTRA_CLIBS)
 	strip $@
+matitaprover.opt.static: $(STATIC_LINK) $(CLIBX_DEPS) $(CCMXS) $(MAINCMXS) matitac.ml
+	$(STATIC_LINK) $(STATIC_CLIBS_PROVER) -- \
+		$(OCAMLOPT) $(CPKGS) -linkpkg -o $@ $(CCMXS) $(MAINCMXS) matitac.ml \
+		$(STATIC_EXTRA_CLIBS);
+	strip $@
 matitadep.opt.static: matitac.opt.static
 	$(H)test -f $@ || ln -s $< $@
 matitaclean.opt.static: matitac.opt.static
 	$(H)test -f $@ || ln -s $< $@
+matitawiki.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
@@ -335,26 +384,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
@@ -370,17 +448,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: