]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/matita/Makefile
improved check in delift for flexible lc entries.
[helm.git] / helm / software / matita / Makefile
index b593d505d47195c90f712a38445a6d7ab7247c7b..d8d81bf3713159caa7007221f6cd0922f7a13d9f 100644 (file)
@@ -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)"
@@ -36,9 +42,11 @@ MLI = \
        applyTransformation.mli \
        matitacLib.mli          \
        matitaInit.mli          \
-       matitaAutoGui.mli       \
        matitaGtkMisc.mli       \
+       matitaAutoGui.mli       \
+       virtuals.mli            \
        matitaScript.mli        \
+       predefined_virtuals.mli \
        matitaMathView.mli      \
        matitaGui.mli           \
        $(NULL)
@@ -61,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
@@ -179,21 +187,23 @@ distclean: clean
        $(H)rm -f matita.conf.xml.sample
        $(H)rm -rf .matita
 
-TEST_DIRS =                            \
-       legacy                          \
-       library                         \
-       tests                           \
-       dama                            \
-       contribs/CoRN                   \
-       contribs/RELATIONAL             \
-       contribs/LOGIC                  \
-       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)        \
+TEST_DIRS_OPT =                \
+       $(TEST_DIRS)            \
+       contribs/LAMBDA-TYPES   \
        $(NULL)
 
 .PHONY: tests tests.opt cleantests cleantests.opt
@@ -216,17 +226,16 @@ cleantests.opt: $(foreach d,$(TEST_DIRS_OPT),$(d)-cleantests-opt)
 ifeq ($(DISTRIBUTED),yes)
 
 
-dist_library: install_preliminaries dist_library@library
-dist_library@%: 
-       $(H)echo "depend $*"
-       $(H)cd $*;(HOME=$(WHERE) USER=builder MATITA_RT_BASE_DIR=$(WHERE) MATITA_FLAGS='$(MATITA_CFLAGS)' $(WHERE)/matitadep)
-       $(H)echo "publish $*"
-       $(H)cd $*;(HOME=$(WHERE) USER=builder MATITA_RT_BASE_DIR=$(WHERE) MATITA_FLAGS='$(MATITA_CFLAGS)' $(WHERE)/matitac -system -noinnertypes)
-       $(H)echo "destroy $*"
-       $(H)cd $*;(HOME=$(WHERE) USER=builder MATITA_RT_BASE_DIR=$(WHERE) MATITA_FLAGS='$(MATITA_CFLAGS)' $(WHERE)/matitaclean)
-       # sqlite3 only
+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/
+#$(H)rm -rf $(WHERE)/.matita/
        touch $@
 
 endif
@@ -359,7 +368,7 @@ TAGS:
        $(H)cd ..; otags -vi -r components/ matita/
 
 .PHONY: depend
-       
+
 depend: 
        $(H)echo "  OCAMLDEP"
        $(H)$(OCAMLDEP) *.ml *.mli > .depend