aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
-rw-r--r--Makefile10
-rw-r--r--config/Makefile.template1
-rwxr-xr-xconfigure28
3 files changed, 26 insertions, 13 deletions
diff --git a/Makefile b/Makefile
index aa9aac648..9daaeea4a 100644
--- a/Makefile
+++ b/Makefile
@@ -77,8 +77,8 @@ LOCALINCLUDES=-I config -I tools -I tools/coqdoc \
MLINCLUDES=$(LOCALINCLUDES) -I $(MYCAMLP4LIB)
-BYTEFLAGS=$(MLINCLUDES) $(CAMLDEBUG)
-OPTFLAGS=$(MLINCLUDES) $(CAMLTIMEPROF) -noassert
+BYTEFLAGS=$(MLINCLUDES) $(CAMLDEBUG) -w y
+OPTFLAGS=$(MLINCLUDES) $(CAMLTIMEPROF) -w y -noassert
OCAMLDEP=ocamldep
DEPFLAGS=$(LOCALINCLUDES)
@@ -1485,7 +1485,7 @@ ML4FILES +=parsing/g_basevernac.ml4 parsing/g_minicoq.ml4 \
parsing/q_coqast.cmo: parsing/q_coqast.ml4
$(SHOW)'OCAMLC4 $<'
- $(HIDE)$(OCAMLC) $(BYTEFLAGS) -pp "$(CAMLP4O) $(CAMLP4EXTENDFLAGS) pa_ifdef.cmo -impl" -c -impl $<
+ $(HIDE)$(OCAMLC) $(BYTEFLAGS) -pp "$(CAMLP4O) $(CAMLP4EXTENDFLAGS) pa_ifdef.cmo $(CAMLP4COMPAT) -impl" -c -impl $<
# toplevel/mltop.ml4 (ifdef Byte)
@@ -1611,11 +1611,11 @@ parsing/lexer.cmo: parsing/lexer.ml4
.ml4.cmx:
$(SHOW)'OCAMLOPT4 $<'
- $(HIDE)$(OCAMLOPT) $(OPTFLAGS) -pp "$(CAMLP4O) $(CAMLP4EXTENDFLAGS) `$(CAMLP4DEPS) $<` -impl" -c -impl $<
+ $(HIDE)$(OCAMLOPT) $(OPTFLAGS) -pp "$(CAMLP4O) $(CAMLP4EXTENDFLAGS) `$(CAMLP4DEPS) $<` $(CAMLP4COMPAT) -impl" -c -impl $<
.ml4.cmo:
$(SHOW)'OCAMLC4 $<'
- $(HIDE)$(OCAMLC) $(BYTEFLAGS) -pp "$(CAMLP4O) $(CAMLP4EXTENDFLAGS) `$(CAMLP4DEPS) $<` -impl" -c -impl $<
+ $(HIDE)$(OCAMLC) $(BYTEFLAGS) -pp "$(CAMLP4O) $(CAMLP4EXTENDFLAGS) `$(CAMLP4DEPS) $<` $(CAMLP4COMPAT) -impl" -c -impl $<
#.v.vo:
# $(BOOTCOQTOP) -compile $*
diff --git a/config/Makefile.template b/config/Makefile.template
index f05caeff9..9432a8843 100644
--- a/config/Makefile.template
+++ b/config/Makefile.template
@@ -45,6 +45,7 @@ CAMLHLIB=CAMLLIBDIRECTORY/caml
# Camlp4 library directory (avoid CAMLP4LIB used on Windows)
CAMLP4O=CAMLP4TOOL
+CAMLP4COMPAT=CAMLP4COMPATFLAGS
MYCAMLP4LIB=CAMLP4LIBDIRECTORY
# Objective-Caml compile command
diff --git a/configure b/configure
index 856b62d28..f0d134ece 100755
--- a/configure
+++ b/configure
@@ -293,16 +293,25 @@ CAMLBIN=`dirname "$CAMLC"`
CAMLVERSION=`"$CAMLC" -v | sed -n -e 's|.*version* *\(.*\)$|\1|p' `
case $CAMLVERSION in
- 1.*|2.*|3.00|3.01|3.02|3.03|3.03alpha|3.04|3.05beta|3.05)
+ 1.*|2.*|3.00|3.01|3.02|3.03|3.03alpha|3.04|3.05beta|3.05|3.08.0)
echo "Your version of Objective-Caml is $CAMLVERSION."
- echo "You need Objective-Caml 3.06 or later !"
+ if [ "$CAMLVERSION" = "3.08.0" ] ; then
+ echo "You need Objective-Caml 3.06 or later (to the exception of 3.08.0)!"
+ else
+ echo "You need Objective-Caml 3.06 or later!";
+ fi
+ echo "Configuration script failed!"
+ exit 1;;
+ 3.06|3.07*|3.08*)
+ echo "You have Objective-Caml $CAMLVERSION. Good!";;
+ ?*)
+ CAMLP4COMPAT="-loc loc"
+ echo "You have Objective-Caml $CAMLVERSION. Good!";;
+ *)
+ echo "I found the Objective-Caml compiler but cannot find its version number!"
+ echo "Is it installed properly ?"
echo "Configuration script failed!"
exit 1;;
- ?*) echo "You have Objective-Caml $CAMLVERSION. Good!";;
- *) echo "I found the Objective-Caml compiler but cannot find its version number!"
- echo "Is it installed properly ?"
- echo "Configuration script failed!"
- exit 1;;
esac
CAMLTAG=OCAML`echo $CAMLVERSION | sed -e "s/\([1-9]\)\.\([0-9]*\).*/\1\2/g"`
@@ -501,6 +510,7 @@ sed -e "s|LOCALINSTALLATION|$local|" \
-e "s|CAMLP4BINDIRECTORY|$CAMLP4BIN|" \
-e "s|CAMLP4LIBDIRECTORY|$CAMLP4LIB|" \
-e "s|CAMLP4TOOL|$camlp4o|" \
+ -e "s|CAMLP4COMPATFLAGS|$CAMLP4COMPAT|" \
-e "s|COQDEBUGFLAG|$coq_debug_flag|" \
-e "s|COQPROFILEFLAG|$coq_profile_flag|" \
-e "s|BESTCOMPILER|$best_compiler|" \
@@ -536,7 +546,9 @@ if test "$coq_debug_flag" = "-g" ; then
fi
# Compatibility with previous name
-ln -s `basename $OCAMLDEBUGCOQ` $COQTOP/dev/ocamldebug-v7
+if [ ! -f $COQTOP/dev/ocamldebug-v7 ] ; then
+ ln -s `basename $OCAMLDEBUGCOQ` $COQTOP/dev/ocamldebug-v7
+fi
echo "If anything in the above is wrong, please restart './configure'"
echo