From: Matthias Puech <puech@cs.mcgill.ca>
Date: Thu, 30 Apr 2009 13:28:13 +0000 (+0000)
Subject: Added an option --enable-annot to the configure to compile with -dtypes
X-Git-Tag: make_still_working~4027
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=66ed4f33ff67b9fe0c28ce4a37eee4834e78e115;p=helm.git

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 faa0c41f4..d7a7620d5 100644
--- 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 5090dcc78..7a4727c76 100644
--- 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 9fbae9851..8b3437393 100644
--- 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 8502bc7b8..e822326d4 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)"
@@ -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