Added an option --enable-annot to the configure to compile with -dtypes

diff --git a/helm/software/Makefile.defs.in b/helm/software/Makefile.defs.in
index faa0c41f448abde5786d9262b5e5d5a46133220d..d7a7620d5949bcfd9eb6cac398a823ad8843ec79 100644 (file)
--- a/helm/software/Makefile.defs.in
+++ b/helm/software/Makefile.defs.in
@@ -7,6 +7,7 @@ CAMLP5O = @CAMLP5O@
 LABLGLADECC = @LABLGLADECC@
 HAVE_OCAMLOPT = @HAVE_OCAMLOPT@
 DISTRIBUTED = @DISTRIBUTED@
+ANNOT = @ANNOT@
 
 MATITA_REQUIRES = @FINDLIB_REQUIRES@
 MATITA_CREQUIRES = @FINDLIB_CREQUIRES@

diff --git a/helm/software/components/Makefile.common b/helm/software/components/Makefile.common
index 5090dcc78309151231efaa2eee9f923fec0c2c3e..7a4727c769b0b1f4ae0dc0ebdd53e21f06a25030 100644 (file)
--- a/helm/software/components/Makefile.common
+++ b/helm/software/components/Makefile.common
@@ -11,10 +11,16 @@ H=@
 
 # $OCAMLFIND must be set to a meaningful vaule, including OCAMLPATH=
 
+ifeq ($(ANNOT),true)
+  ANNOTOPTION = -dtypes
+else
+  ANNOTOPTION =
+endif
+
 PREPROCOPTIONS = -pp camlp5o
 SYNTAXOPTIONS = -syntax camlp5o
 PREREQ =
-OCAMLOPTIONS = -package "$(REQUIRES)" -predicates "$(PREDICATES)" -thread -rectypes
+OCAMLOPTIONS = -package "$(REQUIRES)" -predicates "$(PREDICATES)" -thread -rectypes $(ANNOTOPTION)
 OCAMLDEBUGOPTIONS = -g
 #OCAML_PROF=p -p a
 OCAMLARCHIVEOPTIONS =

diff --git a/helm/software/configure.ac b/helm/software/configure.ac
index 9fbae9851e0cca3e659781e5f9d3bee9b95505c8..8b3437393c000113a3e46c017895f9f3d4a7026e 100644 (file)
--- a/helm/software/configure.ac
+++ b/helm/software/configure.ac
@@ -147,6 +147,25 @@ else
 fi
 AC_MSG_RESULT($MSG)
 
+AC_MSG_CHECKING(--enable-annot argument)
+AC_ARG_ENABLE(annot,
+  [  --enable-annot      Turn on -dtypes compilation option],
+  [GIVEN="yes";
+   case "${enableval}" in
+   yes) ANNOT=true;;
+   no)  ANNOT=false;;
+   *) AC_MSG_ERROR(bad value ${enableval} for --enable-annot) ;;
+  esac],
+  [GIVEN="no"; ANNOT="false"])
+MSG=$GIVEN
+if test "$ANNOT" = "true"; then
+  MSG="$MSG, type annotation enabled."
+else
+  MSG="$MSG, type annotation disabled."
+fi
+AC_MSG_RESULT($MSG)
+
+
 AC_MSG_CHECKING(--with-runtime-dir argument)
 AC_ARG_WITH(runtime-dir,
   [  --with-runtime-dir      Runtime directory (current working directory if not given)],
@@ -176,6 +195,7 @@ AC_MSG_RESULT($MSG)
 AC_SUBST(CAMLP5O)
 AC_SUBST(DBHOST)
 AC_SUBST(DEBUG)
+AC_SUBST(ANNOT)
 AC_SUBST(DISTRIBUTED)
 AC_SUBST(FINDLIB_CREQUIRES)
 AC_SUBST(FINDLIB_REQUIRES)

diff --git a/helm/software/matita/Makefile b/helm/software/matita/Makefile
index 8502bc7b80d2023073db29b44d3ecc4a31097845..e822326d489c2fc4002dc8a7f52bb60f67b6bf24 100644 (file)
--- 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)"
@@ -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
@@ -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
@@ -362,7 +368,7 @@ TAGS:
        $(H)cd ..; otags -vi -r components/ matita/
 
 .PHONY: depend
-       
+
 depend: 
        $(H)echo "  OCAMLDEP"
        $(H)$(OCAMLDEP) *.ml *.mli > .depend