X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2FMakefile;h=fcf51b5d05f46ffc252d9b8eaad6a8c3ddb8d6b1;hb=b367de0252e88d6b0476648d5ceac7e4aeffca27;hp=6bdba1baff31adaccce39610dac044f0d3499c32;hpb=54ddd51bfebe9afc46db2eaa1a20ae971a467fd7;p=helm.git

diff --git a/helm/software/matita/Makefile b/helm/software/matita/Makefile
index 6bdba1baf..fcf51b5d0 100644
--- a/helm/software/matita/Makefile
+++ b/helm/software/matita/Makefile
@@ -5,7 +5,13 @@ include ../Makefile.defs
 NULL =
 H=@
 
-OCAML_FLAGS = -pp $(CAMLP5O) -rectypes
+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)"
@@ -31,9 +37,9 @@ MLI = \
 	lablGraphviz.mli	\
 	matitaTypes.mli		\
 	matitaMisc.mli		\
+	applyTransformation.mli	\
 	matitaEngine.mli	\
 	matitaExcPp.mli 	\
-	applyTransformation.mli	\
 	matitacLib.mli		\
 	matitaInit.mli		\
 	matitaGtkMisc.mli	\
@@ -47,9 +53,9 @@ MLI = \
 CMLI =				\
 	matitaTypes.mli		\
 	matitaMisc.mli		\
+	applyTransformation.mli	\
 	matitaEngine.mli	\
 	matitaExcPp.mli 	\
-	applyTransformation.mli	\
 	matitacLib.mli		\
 	matitaInit.mli		\
 	matitaWiki.mli		\
@@ -63,7 +69,7 @@ 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 matitadep matitaclean \
 	matitawiki
@@ -181,23 +187,23 @@ distclean: clean
 	$(H)rm -f matita.conf.xml.sample
 	$(H)rm -rf .matita
 
-TEST_DIRS = 				\
-	legacy                          \
-	library 			\
-	contribs/character              \
-	tests 			        \
-	contribs/dama/dama		\
-	contribs/assembly		\
-	contribs/CoRN	 	        \
-	contribs/RELATIONAL	 	\
-	contribs/LOGIC	       	        \
-	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 	\
+TEST_DIRS_OPT = 		\
+	$(TEST_DIRS)            \
+#	contribs/LAMBDA-TYPES 	\
 	$(NULL)
 
 .PHONY: tests tests.opt cleantests cleantests.opt
@@ -227,9 +233,9 @@ dist_library: install_preliminaries
 	$(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
+# sqlite3 only
 	$(H)cp $(WHERE)/.matita/matita.db  $(WHERE)/metadata.db || true
-	#$(H)rm -rf $(WHERE)/.matita/
+#$(H)rm -rf $(WHERE)/.matita/
 	touch $@
 
 endif
@@ -259,7 +265,7 @@ INSTALL_STUFF_BIN = $(INSTALL_PROGRAMS)
 endif
 
 install-arch: install_preliminaries 
-install-indep: dist_library 
+install-indep: 
 
 install_preliminaries : install_preliminaries.stamp
 
@@ -279,6 +285,7 @@ endif
 		ln -fs matita $(WHERE)/$$p;\
 	done
 	$(H)cp -a library/ $(WHERE)/ma/standard-library
+	$(H)cp -a nlibrary/ $(WHERE)/ma/new-standard-library
 
 	$(H)touch install_preliminaries.stamp
 
@@ -362,7 +369,7 @@ TAGS:
 	$(H)cd ..; otags -vi -r components/ matita/
 
 .PHONY: depend
-	
+
 depend: 
 	$(H)echo "  OCAMLDEP"
 	$(H)$(OCAMLDEP) *.ml *.mli > .depend