configure: add support of MinGW Win32 environment (fix #2526)

 * Since MinGW/Msys doesn't provide a cygpath utility, we emulate
   it via an ocaml script tools/mingwpath.ml
 * Avoid the crazy sed portions for backslash escaping, instead use
   a more robust ocaml script tools/escape_string.ml based on
   String.escaped
 * No more config/Makefile.template + sed on it, but rather a
   "cat << EOF > ..." as for config/coq_config.ml
 * Normally, support of Cygwin should be preserved, as well as
   mingw32 cross-compilation from linux (cf. myocamlbuild.ml)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15348 85f007b7-540e-0410-9357-904b9bb8a0f7

4 files changed, 253 insertions, 307 deletions

diff --git a/config/Makefile.template b/config/Makefile.template
deleted file mode 100644
index f406ab6fb..000000000
--- a/config/Makefile.template
+++ /dev/null
@@ -1,155 +0,0 @@
-##################################
-#
-#  Configuration file for Coq
-# 
-##################################
-
-#############################################################################
-#
-#  This file is generated by the script "configure"
-#
-#  DO NOT EDIT IT !! DO NOT EDIT IT !! DO NOT EDIT IT !! DO NOT EDIT IT !! 
-#
-#  If something is wrong below, then rerun the script "configure"
-#  with the good options (see the file INSTALL).
-#
-#############################################################################
-
-#Variable used to detect whether ./configure has run successfully.
-COQ_CONFIGURED=yes
-
-# Local use (no installation)
-LOCAL=LOCALINSTALLATION
-
-# Bytecode link flags for VM ("-custom" or "-dllib -lcoqrun")
-COQRUNBYTEFLAGS=XCOQRUNBYTEFLAGS
-COQTOOLSBYTEFLAGS=XCOQTOOLSBYTEFLAGS
-BUILDLDPATH=
-
-# Paths for true installation
-# BINDIR=path where coqtop, coqc, coqmktop, coq-tex, coqdep, gallina and
-#        do_Makefile will reside
-# LIBDIR=path where the Coq library will reside
-# MANDIR=path where to install manual pages
-# EMACSDIR=path where to put Coq's Emacs mode (coq.el)
-BINDIR="BINDIRDIRECTORY"
-COQLIBINSTALL="COQLIBDIRECTORY"
-CONFIGDIR="CONFIGDIRDIRECTORY"
-DATADIR="DATADIRDIRECTORY"
-MANDIR="MANDIRDIRECTORY"
-DOCDIR="DOCDIRDIRECTORY"
-EMACSLIB="EMACSLIBDIRECTORY"
-EMACS=EMACSCOMMAND
-
-# Path to Coq distribution
-COQSRC=COQSRCDIRECTORY
-VERSION=COQVERSION
-
-# Directory containing Camlp4 binaries. Can be empty if camlp4 is in the PATH
-CAMLP4BIN="CAMLP4BINDIRECTORY"
-
-# Ocaml version number
-CAMLVERSION=CAMLTAG
-
-# Ocaml libraries
-CAMLLIB="CAMLLIBDIRECTORY"
-
-# Ocaml .h directory
-CAMLHLIB="CAMLLIBDIRECTORY"
-
-# Camlp4 library directory (avoid CAMLP4LIB used on Windows)
-CAMLP4=CAMLP4VARIANT
-CAMLP4O=CAMLP4TOOL
-CAMLP4COMPAT=CAMLP4COMPATFLAGS
-MYCAMLP4LIB="CAMLP4LIBDIRECTORY"
-
-# LablGTK
-COQIDEINCLUDES=LABLGTKINCLUDES
-
-# Objective-Caml compile command 
-OCAML="OCAMLEXEC"
-OCAMLC="BYTECAMLC"
-OCAMLMKLIB="OCAMLMKLIBEXEC"
-OCAMLOPT="NATIVECAMLC"
-OCAMLDEP="OCAMLDEPEXEC"
-OCAMLDOC="OCAMLDOCEXEC"
-OCAMLLEX="OCAMLLEXEXEC"
-OCAMLYACC="OCAMLYACCEXEC"
-
-# Caml link command and Caml make top command
-CAMLLINK="BYTECAMLC"
-CAMLOPTLINK="NATIVECAMLC"
-CAMLMKTOP="CAMLMKTOPEXEC"
-
-# Caml flags
-CAMLFLAGS=-rectypes CAMLANNOTATEFLAG
-TYPEREX=TYPEREXCMD
-
-# Compilation debug flags
-CAMLDEBUG=COQDEBUGFLAG
-CAMLDEBUGOPT=COQDEBUGFLAGOPT
-
-# User compilation flag
-USERFLAGS=
-
-# Flags for GCC
-CFLAGS=CCOMPILEFLAGS
-
-# Compilation profile flag
-CAMLTIMEPROF=COQPROFILEFLAG
-
-# The best compiler: native (=opt) or bytecode (=byte) if no native compiler
-BEST=BESTCOMPILER
-
-# Your architecture
-# Can be obtain by UNIX command arch
-ARCH=ARCHITECTURE
-HASNATDYNLINK=HASNATIVEDYNLINK
-
-# Your C compiler and co
-CC="CCEXEC"
-AR="AREXEC"
-RANLIB="RANLIBEXEC"
-
-# Supplementary libs for some systems, currently:
-#  . Sun Solaris: -cclib -lunix -cclib -lnsl -cclib -lsocket
-#  . others     : -cclib -lunix
-#  . windows	: -cclib -lunix
-
-OSDEPLIBS=OSDEPENDENTLIBS
-
-# executable files extension, currently:
-#  Unix systems:
-#  Win32 systems : .exe
-EXE=EXECUTEEXTENSION
-DLLEXT=DLLEXTENSION
-
-# the command MKDIR (try to replace it with mkdirhier if you have problems)
-MKDIR=mkdir -p
-
-# where to put the coqdoc.sty style file
-COQDOCDIR="COQDOCDIRECTORY"
-
-# command to update TeX' kpathsea database
-#MKTEXLSR=MKTEXLSRCOMMAND
-
-#the command STRIP 
-# Unix systems and profiling: true
-# Unix systems and no profiling: strip
-# Win32 systems: true (actually strip is bogus)
-STRIP=STRIPCOMMAND
-
-# CoqIde (no/byte/opt)
-HASCOQIDE=COQIDEOPT
-IDEOPTFLAGS=IDEARCHFLAGS
-IDEOPTDEPS=IDEARCHFILE
-IDEOPTINT=IDEARCHDEF
-
-# Defining REVISION
-CHECKEDOUT=CHECKEDOUTSOURCETREE
-
-# Option to control compilation and installation of the documentation
-WITHDOC=WITHDOCOPT
-
-# make or sed are bogus and believe lines not terminating by a return
-# are inexistent
diff --git a/configure b/configure
index ed9a99e8f..9a1970fb9 100755
--- a/configure
+++ b/configure
@@ -297,17 +297,19 @@ case $DATEPGM in
     "") echo "I can't find the program \"date\" in your path."
         echo "Please give me the current date"
 	read COMPILEDATE;;
-    *)  COMPILEDATE=`LC_ALL=C LANG=C date +"%h %d %Y %H:%M:%S"`;;
+    *)  COMPILEDATE=`LC_ALL=C LANG=C date +"%b %d %Y %H:%M:%S"`;;
 esac
 
 # Architecture
 
 case $arch_spec in
     no) 
-    # First we test if we are running a Cygwin system
+    # First we test if we are running a Cygwin or Mingw/Msys system
     if [ `uname -s | cut -c -6` = "CYGWIN" ] ; then
 	ARCH="win32"
 	CYGWIN=yes
+    elif [ `uname -s | cut -c -7` = "MINGW32" ]; then
+	ARCH="win32"
     else
 	# If not, we determine the architecture
 	if test -x /bin/uname ; then
@@ -442,9 +444,19 @@ if test ! -f "$CAMLC" ; then
     exit 1
 fi
 
-# Under Windows, OCaml only understands Windows filenames (C:\...)
+# Under Windows, we need to convert from cygwin/mingw paths (/c/Program Files/Ocaml)
+# to more windows-looking paths (c:/Program Files/Ocaml). Note that / are kept
+
+mk_win_path () {
+    case $ARCH,$CYGWIN in
+	win32,yes) cygpath -m "$1" ;;
+	win32*) "$ocamlexec" "$COQSRC/tools/mingwpath.ml" "$1" ;;
+	*) echo "$1" ;;
+    esac
+}
+
 case $ARCH in
-    win32) CAMLBIN=`cygpath -m ${CAMLBIN}`;;
+    win32) CAMLBIN=`mk_win_path "$CAMLBIN"`;;
 esac
 
 CAMLVERSION=`"$bytecamlc" -version`
@@ -490,7 +502,7 @@ if [ "$coq_debug_flag" = "-g" ]; then
 fi
 
 # Native dynlink
-if [ "$natdynlink" = "yes" -a -f `"$CAMLC" -where`/dynlink.cmxa ]; then
+if [ "$natdynlink" = "yes" -a -f "$CAMLLIB"/dynlink.cmxa ]; then
     HASNATDYNLINK=true
 else
     HASNATDYNLINK=false
@@ -600,18 +612,17 @@ fi
 
 # OS dependent libraries
 
-case $ARCH in
+OSDEPLIBS="-cclib -lunix"
+case $ARCH,$CYGWIN in
   sun4*) OS=`uname -r`
 	case $OS in
 	   5*) OS="Sun Solaris $OS"
-	       OSDEPLIBS="-cclib -lunix -cclib -lnsl -cclib -lsocket";;
+	       OSDEPLIBS="$OSDEPLIBS -cclib -lnsl -cclib -lsocket";;
 	   *) OS="Sun OS $OS"
-	      OSDEPLIBS="-cclib -lunix"
         esac;;
-  win32) OS="Win32" 
-	 OSDEPLIBS="-cclib -lunix"
+  win32,yes) OS="Win32 (Cygwin)"
 	 cflags="-mno-cygwin $cflags";;
-  *) OSDEPLIBS="-cclib -lunix"
+  win32,*) OS="Win32 (MinGW)";;
 esac
 
 # lablgtk2 and CoqIDE
@@ -691,9 +702,6 @@ esac
 # strip command
 
 case $ARCH in
-    win32)
-	# true -> strip : it exists under cygwin !
-	STRIPCOMMAND="strip";; 
     Darwin) if [ "$HASNATDYNLINK" = "true" ]
 	then
 	  STRIPCOMMAND="true"
@@ -709,13 +717,6 @@ case $ARCH in
     fi
 esac
 
-# mktexlsr
-#MKTEXLSR=`which mktexlsr`
-#case $MKTEXLSR in
-#    "") MKTEXLSR=true;;
-#esac
-
-# "
 ### Test if documentation can be compiled (latex, hevea)
 
 if test "$with_doc" = "all" 
@@ -739,20 +740,20 @@ esac
 
 # OCaml only understand Windows filenames (C:\...)
 case $ARCH in
-    win32) COQTOP=`cygpath -m ${COQTOP}`
+    win32) COQTOP=`mk_win_path "$COQTOP"`
 esac
 
 case $ARCH$CYGWIN in
   win32)
-	 W32PREF='C:\\coq\\'
-	 bindir_def=${W32PREF}bin
-	 libdir_def=${W32PREF}lib
-	 configdir_def=${W32PREF}config
-	 datadir_def=${W32PREF}share
-	 mandir_def=${W32PREF}man
-	 docdir_def=${W32PREF}doc
-	 emacslib_def=${W32PREF}emacs
-         coqdocdir_def=${W32PREF}latex;;
+	 W32PREF='C:\coq\'
+	 bindir_def="${W32PREF}bin"
+	 libdir_def="${W32PREF}lib"
+	 configdir_def="${W32PREF}config"
+	 datadir_def="${W32PREF}share"
+	 mandir_def="${W32PREF}man"
+	 docdir_def="${W32PREF}doc"
+	 emacslib_def="${W32PREF}emacs"
+	 coqdocdir_def="${W32PREF}latex";;
   *)
 	 bindir_def=/usr/local/bin
 	 libdir_def=/usr/local/lib/coq
@@ -761,7 +762,7 @@ case $ARCH$CYGWIN in
 	 mandir_def=/usr/local/share/man
 	 docdir_def=/usr/local/share/doc/coq
 	 emacslib_def=/usr/local/share/emacs/site-lisp
-         coqdocdir_def=/usr/local/share/texmf/tex/latex/misc;;
+	 coqdocdir_def=/usr/local/share/texmf/tex/latex/misc;;
 esac
 
 emacs_def=emacs
@@ -770,7 +771,7 @@ case $bindir_spec/$prefix_spec/$local in
     yes/*/*) BINDIR=$bindir ;;
     */yes/*) BINDIR=$prefix/bin ;;
     */*/true) BINDIR=$COQTOP/bin ;;
-    *) printf "Where should I install the Coq binaries [$bindir_def]? "
+    *)  printf "Where should I install the Coq binaries [%s]? " "$bindir_def"
         read BINDIR
 	case $BINDIR in
 	    "") BINDIR=$bindir_def;;
@@ -787,7 +788,7 @@ case $libdir_spec/$prefix_spec/$local in
           *)  LIBDIR=$prefix/lib/coq ;;
         esac ;;
     */*/true) LIBDIR=$COQTOP ;;
-    *)  printf "Where should I install the Coq library [$libdir_def]? "
+    *)  printf "Where should I install the Coq library [%s]? " "$libdir_def"
         read LIBDIR
         libdir_spec=yes
 	case $LIBDIR in
@@ -796,11 +797,6 @@ case $libdir_spec/$prefix_spec/$local in
 	esac;;
 esac
 
-case $libdir_spec in
-    yes) LIBDIR_OPTION="Some \"$LIBDIR\"";;
-    *) LIBDIR_OPTION="None";;
-esac
-
 case $configdir_spec/$prefix_spec/$local in
     yes/*/*) CONFIGDIR=$configdir;;
     */yes/*) configdir_spec=yes
@@ -810,7 +806,7 @@ case $configdir_spec/$prefix_spec/$local in
 	esac;;
     */*/true) CONFIGDIR=$COQTOP/ide
     configdir_spec=yes;;
-    *)  printf "Where should I install the Coqide configuration files [$configdir_def]? "
+    *)  printf "Where should I install the Coqide configuration files [%s]? " "$configdir_def"
         read CONFIGDIR
 	case $CONFIGDIR in
 	    "") CONFIGDIR=$configdir_def;;
@@ -818,17 +814,12 @@ case $configdir_spec/$prefix_spec/$local in
 	esac;;
 esac
 
-case $configdir_spec in
-    yes) CONFIGDIR_OPTION="Some \"$CONFIGDIR\"";;
-    *) CONFIGDIR_OPTION="None";;
-esac
-
 case $datadir_spec/$prefix_spec/$local in
     yes/*/*) DATADIR=$datadir;;
     */yes/*) DATADIR=$prefix/share/coq;;
     */*/true) DATADIR=$COQTOP/ide
         datadir_spec=yes;;
-    *)  printf "Where should I install the Coqide data files [$datadir_def]? "
+    *)  printf "Where should I install the Coqide data files [%s]? " "$datadir_def"
         read DATADIR
 	case $DATADIR in
 	    "") DATADIR=$datadir_def;;
@@ -836,17 +827,11 @@ case $datadir_spec/$prefix_spec/$local in
 	esac;;
 esac
 
-case $datadir_spec in
-    yes) DATADIR_OPTION="Some \"$DATADIR\"";;
-    *) DATADIR_OPTION="None";;
-esac
-
-
 case $mandir_spec/$prefix_spec/$local in
     yes/*/*) MANDIR=$mandir;;
     */yes/*) MANDIR=$prefix/share/man ;;
     */*/true) MANDIR=$COQTOP/man ;;
-    *)  printf "Where should I install the Coq man pages [$mandir_def]? "
+    *)  printf "Where should I install the Coq man pages [%s]? "  "$mandir_def"
         read MANDIR
 	case $MANDIR in
 	    "") MANDIR=$mandir_def;;
@@ -858,7 +843,7 @@ case $docdir_spec/$prefix_spec/$local in
     yes/*/*) DOCDIR=$docdir;;
     */yes/*) DOCDIR=$prefix/share/doc/coq;;
     */*/true) DOCDIR=$COQTOP/doc;;
-    *)  printf "Where should I install the Coq documentation [$docdir_def]? "
+    *)  printf "Where should I install the Coq documentation [%s]? " "$docdir_def"
         read DOCDIR
 	case $DOCDIR in
 	    "") DOCDIR=$docdir_def;;
@@ -874,7 +859,7 @@ case $emacslib_spec/$prefix_spec/$local in
           *)  EMACSLIB=$prefix/share/emacs/site-lisp ;;
         esac ;;
     */*/true) EMACSLIB=$COQTOP/tools/emacs ;;
-    *) printf "Where should I install the Coq Emacs mode [$emacslib_def]? "
+    *)  printf "Where should I install the Coq Emacs mode [%s]? " "$emacslib_def"
         read EMACSLIB
 	case $EMACSLIB in
 	    "") EMACSLIB=$emacslib_def;;
@@ -890,7 +875,7 @@ case $coqdocdir_spec/$prefix_spec/$local in
           *)  COQDOCDIR=$prefix/share/emacs/site-lisp ;;
         esac ;;
     */*/true) COQDOCDIR=$COQTOP/tools/coqdoc ;;
-    *) printf "Where should I install Coqdoc TeX/LaTeX files [$coqdocdir_def]? "
+    *)  printf "Where should I install Coqdoc TeX/LaTeX files [%s]? " "$coqdocdir_def"
         read COQDOCDIR
 	case $COQDOCDIR in
 	    "") COQDOCDIR=$coqdocdir_def;;
@@ -920,14 +905,14 @@ case $coqtoolsbyteflags_spec/$custom_spec/$CUSTOM_OS in
 esac
 
 # case $emacs_spec in
-#     no) printf "Which Emacs command should I use to compile coq.el [$emacs_def]? "
+#     no) printf "Which Emacs command should I use to compile coq.el [%s]? " "$emacs_def"
 #         read EMACS
 	
 # 	case $EMACS in
-# 	    "") EMACS=$emacs_def;;
+# 	    "") EMACS="$emacs_def";;
 # 	    *) true;;
 # 	esac;;
-#     yes) EMACS=$emacs;;
+#     yes) EMACS="$emacs";;
 # esac
 
 
@@ -1007,51 +992,65 @@ config_template="$COQSRC/config/Makefile.template"
 ### After this line, be careful when using variables,
 ### since some of them (e.g. $COQSRC) will be escaped
 
-
-# An escaped version of a variable
-escape_var () {
-"$ocamlexec" 2>&1 1>/dev/null <<EOF
-  prerr_endline(String.escaped(Sys.getenv"$VAR"));;
-EOF
+escape_string () {
+    "$ocamlexec" "$COQSRC/tools/escape_string.ml" "$1"
 }
 
 # Escaped version of browser command
-export BROWSER
-BROWSER=`VAR=BROWSER escape_var`
+BROWSER=`escape_string "$BROWSER"`
+
+# Under Windows, we now escape the backslashes that will ends in
+# ocaml strings (coq_config.ml) or in Makefile variables.
 
-# damned backslashes under M$Windows
 case $ARCH in
     win32)
-	COQTOP=`echo $COQTOP |sed -e 's|\\\|\\\\\\\|g'`
-	BINDIR=`echo $BINDIR |sed -e 's|\\\|\\\\\\\|g'`
-	COQSRC=`cygpath -m $COQSRC |sed -e 's|\\\|\\\\\\\|g'`
-	LIBDIR=`echo $LIBDIR |sed -e 's|\\\|\\\\\\\|g'`
-	CONFIGDIR=`echo $CONFIGDIR |sed -e 's|\\\|\\\\\\\|g'`
-	DATADIR=`echo $DATADIR |sed -e 's|\\\|\\\\\\\|g'`
-	CAMLBIN=`echo $CAMLBIN |sed -e 's|\\\|\\\\\\\|g'`
-	CAMLLIB=`echo $CAMLLIB |sed -e 's|\\\|\\\\\\\|g'`
-	MANDIR=`echo $MANDIR |sed -e 's|\\\|\\\\\\\|g'`
-	DOCDIR=`echo $DOCDIR |sed -e 's|\\\|\\\\\\\|g'`
-	EMACSLIB=`echo $EMACSLIB |sed -e 's|\\\|\\\\\\\|g'`
-	COQDOCDIR=`echo $COQDOCDIR |sed -e 's|\\\|\\\\\\\|g'`
-	CAMLP4BIN=`echo $CAMLP4BIN |sed -e 's|\\\|\\\\\\\|g'`
-	CAMLP4LIB=`echo $CAMLP4LIB |sed -e 's|\\\|\\\\\\\|g'`
-	LABLGTKINCLUDES=`echo $LABLGTKINCLUDES |sed -e 's|\\\|\\\\\\\|g'`
-	COQRUNBYTEFLAGS=`echo $COQRUNBYTEFLAGS |sed -e 's|\\\|\\\\\\\|g'`
-	COQTOOLSBYTEFLAGS=`echo $COQTOOLSBYTEFLAGS |sed -e 's|\\\|\\\\\\\|g'`
-	BUILDLDPATH=`echo $BUILDLDPATH |sed -e 's|\\\|\\\\\\\|g'`
-	ocamlexec=`echo $ocamlexec |sed -e 's|\\\|\\\\\\\|g'`
-	bytecamlc=`echo $bytecamlc |sed -e 's|\\\|\\\\\\\|g'`
-	nativecamlc=`echo $nativecamlc |sed -e 's|\\\|\\\\\\\|g'`
-	ocamlmklibexec=`echo $ocamlmklibexec |sed -e 's|\\\|\\\\\\\|g'`
-	ocamldepexec=`echo $ocamldepexec |sed -e 's|\\\|\\\\\\\|g'`
-	ocamldocexec=`echo $ocamldocexec |sed -e 's|\\\|\\\\\\\|g'`
-	ocamllexexec=`echo $ocamllexexec |sed -e 's|\\\|\\\\\\\|g'`
-	ocamlyaccexec=`echo $ocamlyaccexec |sed -e 's|\\\|\\\\\\\|g'`
-	camlp4oexec=`echo $camlp4oexec |sed -e 's|\\\|\\\\\\\|g'`
+	COQSRC=`mk_win_path "$COQSRC"`
+
+	COQTOP=`escape_string "$COQTOP"`
+	BINDIR=`escape_string "$BINDIR"`
+	COQSRC=`escape_string "$COQSRC"`
+	LIBDIR=`escape_string "$LIBDIR"`
+	CONFIGDIR=`escape_string "$CONFIGDIR"`
+	DATADIR=`escape_string "$DATADIR"`
+	CAMLBIN=`escape_string "$CAMLBIN"`
+	CAMLLIB=`escape_string "$CAMLLIB"`
+	MANDIR=`escape_string "$MANDIR"`
+	DOCDIR=`escape_string "$DOCDIR"`
+	EMACSLIB=`escape_string "$EMACSLIB"`
+	COQDOCDIR=`escape_string "$COQDOCDIR"`
+	CAMLP4BIN=`escape_string "$CAMLP4BIN"`
+	CAMLP4LIB=`escape_string "$CAMLP4LIB"`
+	LABLGTKINCLUDES=`escape_string "$LABLGTKINCLUDES"`
+	COQRUNBYTEFLAGS=`escape_string "$COQRUNBYTEFLAGS"`
+	COQTOOLSBYTEFLAGS=`escape_string "$COQTOOLSBYTEFLAGS"`
+	BUILDLDPATH=`escape_string "$BUILDLDPATH"`
+	ocamlexec=`escape_string "$ocamlexec"`
+	bytecamlc=`escape_string "$bytecamlc"`
+	nativecamlc=`escape_string "$nativecamlc"`
+	ocamlmklibexec=`escape_string "$ocamlmklibexec"`
+	ocamldepexec=`escape_string "$ocamldepexec"`
+	ocamldocexec=`escape_string "$ocamldocexec"`
+	ocamllexexec=`escape_string "$ocamllexexec"`
+	ocamlyaccexec=`escape_string "$ocamlyaccexec"`
+	camlp4oexec=`escape_string "$camlp4oexec"`
     ;;
 esac
 
+case $libdir_spec in
+    yes) LIBDIR_OPTION="Some \"$LIBDIR\"";;
+    *) LIBDIR_OPTION="None";;
+esac
+
+case $configdir_spec in
+    yes) CONFIGDIR_OPTION="Some \"$CONFIGDIR\"";;
+    *) CONFIGDIR_OPTION="None";;
+esac
+
+case $datadir_spec in
+    yes) DATADIR_OPTION="Some \"$DATADIR\"";;
+    *) DATADIR_OPTION="None";;
+esac
+
 #####################################################
 # Building the $COQTOP/config/coq_config.ml file
 #####################################################
@@ -1131,63 +1130,149 @@ ln -sf "$mlconfig_file" "$mymlconfig_file"
 
 rm -f "$config_file"
 
-sed -e "s|LOCALINSTALLATION|$local|" \
-    -e "s|XCOQRUNBYTEFLAGS|$COQRUNBYTEFLAGS|" \
-    -e "s|XCOQTOOLSBYTEFLAGS|$COQTOOLSBYTEFLAGS|" \
-    -e "s|COQSRCDIRECTORY|$COQSRC|" \
-    -e "s|COQVERSION|$VERSION|" \
-    -e "s|BINDIRDIRECTORY|$BINDIR|" \
-    -e "s|COQLIBDIRECTORY|$LIBDIR|" \
-    -e "s|CONFIGDIRDIRECTORY|$CONFIGDIR|" \
-    -e "s|DATADIRDIRECTORY|$DATADIR|" \
-    -e "s|BUILDLDPATH=|$BUILDLDPATH|" \
-    -e "s|MANDIRDIRECTORY|$MANDIR|" \
-    -e "s|DOCDIRDIRECTORY|$DOCDIR|" \
-    -e "s|EMACSLIBDIRECTORY|$EMACSLIB|" \
-    -e "s|EMACSCOMMAND|$EMACS|" \
-    -e "s|COQDOCDIRECTORY|$COQDOCDIR|" \
-    -e "s|MKTEXLSRCOMMAND|$MKTEXLSR|" \
-    -e "s|ARCHITECTURE|$ARCH|" \
-    -e "s|OSDEPENDENTLIBS|$OSDEPLIBS|" \
-    -e "s|OSDEPENDENTP4OPTFLAGS|$OSDEPP4OPTFLAGS|" \
-    -e "s|CAMLLIBDIRECTORY|$CAMLLIB|" \
-    -e "s|CAMLTAG|$CAMLTAG|" \
-    -e "s|CAMLP4VARIANT|$CAMLP4|" \
-    -e "s|CAMLP4BINDIRECTORY|$CAMLP4BIN|" \
-    -e "s|CAMLP4LIBDIRECTORY|$CAMLP4LIB|" \
-    -e "s|CAMLP4TOOL|$camlp4oexec|" \
-    -e "s|CAMLP4COMPATFLAGS|$CAMLP4COMPAT|" \
-    -e "s|LABLGTKINCLUDES|$LABLGTKINCLUDES|" \
-    -e "s|COQDEBUGFLAGOPT|$coq_debug_flag_opt|" \
-    -e "s|COQDEBUGFLAG|$coq_debug_flag|" \
-    -e "s|COQPROFILEFLAG|$coq_profile_flag|" \
-    -e "s|CAMLANNOTATEFLAG|$coq_annotate_flag|" \
-    -e "s|TYPEREXCMD|$coq_typerex_wrapper|" \
-    -e "s|CCOMPILEFLAGS|$cflags|" \
-    -e "s|BESTCOMPILER|$best_compiler|" \
-    -e "s|DLLEXTENSION|$DLLEXT|" \
-    -e "s|EXECUTEEXTENSION|$EXE|" \
-    -e "s|BYTECAMLC|$bytecamlc|" \
-    -e "s|OCAMLMKLIBEXEC|$ocamlmklibexec|" \
-    -e "s|NATIVECAMLC|$nativecamlc|" \
-    -e "s|OCAMLEXEC|$ocamlexec|" \
-    -e "s|OCAMLDEPEXEC|$ocamldepexec|" \
-    -e "s|OCAMLDOCEXEC|$ocamldocexec|" \
-    -e "s|OCAMLLEXEXEC|$ocamllexexec|" \
-    -e "s|OCAMLYACCEXEC|$ocamlyaccexec|" \
-    -e "s|CAMLMKTOPEXEC|$ocamlmktopexec|" \
-    -e "s|CCEXEC|$gcc_exec|" \
-    -e "s|AREXEC|$ar_exec|" \
-    -e "s|RANLIBEXEC|$ranlib_exec|" \
-    -e "s|STRIPCOMMAND|$STRIPCOMMAND|" \
-    -e "s|COQIDEOPT|$COQIDE|" \
-    -e "s|IDEARCHFLAGS|$IDEARCHFLAGS|" \
-    -e "s|IDEARCHFILE|$IDEARCHFILE|" \
-    -e "s|IDEARCHDEF|$IDEARCHDEF|" \
-    -e "s|CHECKEDOUTSOURCETREE|$checkedout|" \
-    -e "s|WITHDOCOPT|$with_doc|" \
-    -e "s|HASNATIVEDYNLINK|$NATDYNLINKFLAG|" \
-      "$config_template" > "$config_file"
+cat << END_OF_MAKEFILE > $config_file
+###### config/Makefile : Configuration file for Coq ##############
+#                                                                #
+# This file is generated by the script "configure"               #
+# DO NOT EDIT IT !! DO NOT EDIT IT !! DO NOT EDIT IT !!          #
+# If something is wrong below, then rerun the script "configure" #
+# with the good options (see the file INSTALL).                  #
+#                                                                #
+##################################################################
+
+#Variable used to detect whether ./configure has run successfully.
+COQ_CONFIGURED=yes
+
+# Local use (no installation)
+LOCAL=$local
+
+# Bytecode link flags for VM ("-custom" or "-dllib -lcoqrun")
+COQRUNBYTEFLAGS=$COQRUNBYTEFLAGS
+COQTOOLSBYTEFLAGS=$COQTOOLSBYTEFLAGS
+$BUILDLDPATH
+
+# Paths for true installation
+# BINDIR=path where coqtop, coqc, coqmktop, coq-tex, coqdep, gallina and
+#        do_Makefile will reside
+# LIBDIR=path where the Coq library will reside
+# MANDIR=path where to install manual pages
+# EMACSDIR=path where to put Coq's Emacs mode (coq.el)
+BINDIR="$BINDIR"
+COQLIBINSTALL="$LIBDIR"
+CONFIGDIR="$CONFIGDIR"
+DATADIR="$DATADIR"
+MANDIR="$MANDIR"
+DOCDIR="$DOCDIR"
+EMACSLIB="$EMACSLIB"
+EMACS=$EMACS
+
+# Path to Coq distribution
+COQSRC="$COQSRC"
+VERSION=$VERSION
+
+# Ocaml version number
+CAMLVERSION=$CAMLTAG
+
+# Ocaml libraries
+CAMLLIB="$CAMLLIB"
+
+# Ocaml .h directory
+CAMLHLIB="$CAMLLIB"
+
+# Camlp4 : flavor, binaries, libraries ...
+# NB : CAMLP4BIN can be empty if camlp4 is in the PATH
+# NB : avoid using CAMLP4LIB (conflict under Windows)
+CAMLP4BIN="$CAMLP4BIN"
+CAMLP4=$CAMLP4
+CAMLP4O=$camlp4oexec
+CAMLP4COMPAT=$CAMLP4COMPAT
+MYCAMLP4LIB="$CAMLP4LIB"
+
+# LablGTK
+COQIDEINCLUDES=$LABLGTKINCLUDES
+
+# Objective-Caml compile command
+OCAML="$ocamlexec"
+OCAMLC="$bytecamlc"
+OCAMLMKLIB="$ocamlmklibexec"
+OCAMLOPT="$nativecamlc"
+OCAMLDEP="$ocamldepexec"
+OCAMLDOC="$ocamldocexec"
+OCAMLLEX="$ocamllexexec"
+OCAMLYACC="$ocamlyaccexec"
+
+# Caml link command and Caml make top command
+CAMLLINK="$bytecamlc"
+CAMLOPTLINK="$nativecamlc"
+CAMLMKTOP="$ocamlmktopexec"
+
+# Caml flags
+CAMLFLAGS=-rectypes $coq_annotate_flag
+TYPEREX=$coq_typerex_wrapper
+
+# Compilation debug flags
+CAMLDEBUG=$coq_debug_flag
+CAMLDEBUGOPT=$coq_debug_flag_opt
+
+# User compilation flag
+USERFLAGS=
+
+# Flags for GCC
+CFLAGS=$cflags
+
+# Compilation profile flag
+CAMLTIMEPROF=$coq_profile_flag
+
+# The best compiler: native (=opt) or bytecode (=byte) if no native compiler
+BEST=$best_compiler
+
+# Your architecture
+# Can be obtain by UNIX command arch
+ARCH=$ARCH
+HASNATDYNLINK=$NATDYNLINKFLAG
+
+# Your C compiler and co
+CC="$gcc_exec"
+AR="$ar_exec"
+RANLIB="$ranlib_exec"
+
+# Supplementary libs for some systems, currently:
+#  . Sun Solaris: -cclib -lunix -cclib -lnsl -cclib -lsocket
+#  . others     : -cclib -lunix
+OSDEPLIBS=$OSDEPLIBS
+
+# executable files extension, currently:
+#  Unix systems:
+#  Win32 systems : .exe
+EXE=$EXE
+DLLEXT=$DLLEXT
+
+# the command MKDIR (try to replace it with mkdirhier if you have problems)
+MKDIR=mkdir -p
+
+# where to put the coqdoc.sty style file
+COQDOCDIR="$COQDOCDIR"
+
+#the command STRIP
+# Unix systems and profiling: true
+# Unix systems and no profiling: strip
+STRIP=$STRIPCOMMAND
+
+# CoqIde (no/byte/opt)
+HASCOQIDE=$COQIDE
+IDEOPTFLAGS=$IDEARCHFLAGS
+IDEOPTDEPS=$IDEARCHFILE
+IDEOPTINT=$IDEARCHDEF
+
+# Defining REVISION
+CHECKEDOUT=$checkedout
+
+# Option to control compilation and installation of the documentation
+WITHDOC=$with_doc
+
+# make or sed are bogus and believe lines not terminating by a return
+# are inexistent
+END_OF_MAKEFILE
 
 chmod a-w "$config_file"
 
diff --git a/tools/escape_string.ml b/tools/escape_string.ml
new file mode 100644
index 000000000..50e8faada
--- /dev/null
+++ b/tools/escape_string.ml
@@ -0,0 +1 @@
+print_string (String.escaped Sys.argv.(1))
diff --git a/tools/mingwpath.ml b/tools/mingwpath.ml
new file mode 100644
index 000000000..f01b62cce
--- /dev/null
+++ b/tools/mingwpath.ml
@@ -0,0 +1,15 @@
+(** Mingwpath *)
+
+(** Converts mingw-encoded filenames such as:
+
+      /c/Program Files/Ocaml/bin
+
+    to a more windows-friendly form (but still with / instead of \) :
+
+      c:/Program Files/Ocaml/bin
+
+    This nice hack was suggested by Benjamin Monate (cf bug #2526)
+    to mimic the cygwin-specific tool cygpath
+*)
+
+print_string Sys.argv.(1)