configure.ml: our configure script is now written in ML :-)

  configure is now just a minimal wrapper around the new configure.ml.
  This configure.ml is runned with the same ocaml used during
  compilation, and starts with a #load "unix.cma".
  For now, this new configure script is meant to be 99% compatible
  with the old one. Known incompatibilities : the --foo option format
  (with two --) isn't supported anymore, use -foo options instead.
  Let me know if you encounter any other changes.

  Internals:
   - We use our own "run" command (based on Unix.create_process) to avoid
     relying on some specific shell (/bin/sh or cmd.exe).
   - We should have far less issues with filename quoting under windows
     since we almost never rely on (cygwin) shell anymore. This remains
     to be fully tested, though.
   - dev/ocamldebug-coq is slightly different now, to ease its generation

3 files changed, 1149 insertions, 1234 deletions

diff --git a/configure b/configure
index 417934206..09585e59e 100755
--- a/configure
+++ b/configure
@@ -1,1241 +1,37 @@
 #!/bin/sh
 
-##################################
-#
-#  Configuration script for Coq
-#
-##################################
+## This micro-configure shell script is here only to
+## launch the real configuration via ocaml
 
-VERSION=trunk
-VOMAGIC=08511
-STATEMAGIC=58511
-DATE=`LC_ALL=C LANG=C date +"%B %Y"`
+cmd=ocaml
+script=./configure.ml
 
-# Create the bin/ directory if non-existent
-test -d bin || mkdir bin
-
-# a local which command for sh
-which () {
-IFS=":" # set words separator in PATH to be ':' (it allows spaces in dirnames)
-for i in $PATH; do
-  if test -z "$i"; then i=.; fi
-  if [ -f "$i/$1" ] ; then
-        IFS=" "
-        echo "$i/$1"
-        break
-  fi
-done
-}
-
-usage () {
-    printf "Available options for configure are:\n"
-    echo "-help"
-    printf "\tDisplays this help page\n"
-    echo "-prefix <dir>"
-    printf "\tSet installation directory to <dir>\n"
-    echo "-local"
-    printf "\tSet installation directory to the current source tree\n"
-    echo "-coqrunbyteflags <flags>"
-    printf "\tSet link flags for VM-dependent bytecode (coqtop)\n"
-    echo "-coqtoolsbyteflags <flags>"
-    printf "\tSet link flags for VM-independant bytecode (coqdep, coqdoc, ...)\n"
-    echo "-custom"
-    printf "\tGenerate all bytecode executables with -custom (not recommended)\n"
-    echo "-bindir <dir>"
-    echo "-libdir <dir>"
-    echo "-configdir <dir>"
-    echo "-datadir <dir>"
-    echo "-mandir <dir>"
-    echo "-docdir <dir>"
-    printf "\tSpecifies where to install bin/lib/config/data/man/doc files resp.\n"
-    echo "-emacslib <dir>"
-    printf "\tSpecifies where emacs files are to be installed\n"
-    echo "-coqdocdir <dir>"
-    printf "\tSpecifies where Coqdoc style files are to be installed\n"
-    echo "-camldir <dir>"
-    printf "\tSpecifies the path to the OCaml library\n"
-    echo "-lablgtkdir <dir>"
-    printf "\tSpecifies the path to the Lablgtk library\n"
-    echo "-usecamlp5"
-    printf "\tSpecifies to use camlp5 instead of camlp4\n"
-    echo "-usecamlp4"
-    printf "\tSpecifies to use camlp4 instead of camlp5\n"
-    echo "-camlp5dir <dir>"
-    printf "\tSpecifies where to look for the Camlp5 library and tells to use it\n"
-    echo "-arch <arch>"
-    printf "\tSpecifies the architecture\n"
-    echo "-opt"
-    printf "\tSpecifies whether or not to use OCaml *.opt optimized compilers\n"
-    echo "-natdynlink (yes|no)"
-    printf "\tSpecifies whether or not to use dynamic loading of native code\n"
-    echo "-coqide (opt|byte|no)"
-    printf "\tSpecifies whether or not to compile Coqide\n"
-    echo "-nomacintegration"
-    printf "\tSpecifies to not try to build coqide mac integration\n"
-    echo "-browser <command>"
-    printf "\tUse <command> to open URL %%s\n"
-    echo "-nodoc"
-    printf "\tSpecifies to not compile the documentation\n"
-    echo "-with-geoproof (yes|no)"
-    printf "\tSpecifies whether or not to use Geoproof binding\n"
-    echo "-byte-only"
-    printf "\tCompiles only bytecode version of Coq\n"
-    echo "-debug"
-    printf "\tAdd debugging information in the Coq executables\n"
-    echo "-profile"
-    printf "\tAdd profiling information in the Coq executables\n"
-    echo "-annotate"
-    printf "\tCompiles Coq with -dtypes option\n"
-    echo "-typerex"
-    printf "\tCompiles Coq using typerex wrapper\n"
-    echo "-makecmd <command>"
-    printf "\tName of GNU Make command\n"
-    echo "-no-native-compiler"
-    printf "\tDisables compilation to native code for conversion and normalization\n"
-}
-
-
-# Default OCaml binaries
-bytecamlc=ocamlc
-nativecamlc=ocamlopt
-ocamlmklibexec=ocamlmklib
-ocamlexec=ocaml
-ocamldepexec=ocamldep
-ocamldocexec=ocamldoc
-ocamllexexec=ocamllex
-ocamlyaccexec=ocamlyacc
-camlp4oexec=camlp4o
-default_typerex_wrapper="ocp-wrapper -save-types"
-
-
-coq_debug_flag=
-coq_debug_flag_opt=
-coq_profile_flag=
-coq_annotate_flag=
-coq_typerex_wrapper=
-best_compiler=opt
-cflags="-fno-defer-pop -Wall -Wno-unused"
-natdynlink=yes
-
-local=false
-coqrunbyteflags_spec=no
-coqtoolsbyteflags_spec=no
-custom_spec=no
-prefix_spec=no
-bindir_spec=no
-libdir_spec=no
-configdir_spec=no
-datadir_spec=no
-mandir_spec=no
-docdir_spec=no
-emacslib_spec=no
-emacs_spec=no
-camldir_spec=no
-lablgtkdir_spec=no
-coqdocdir_spec=no
-arch_spec=no
-coqide_spec=no
-nomacintegration_spec=no
-browser_spec=no
-wwwcoq_spec=no
-with_geoproof=false
-with_doc=all
-with_doc_spec=no
-force_caml_version=no
-force_caml_version_spec=no
-usecamlp5=yes
-no_native_compiler=false
-
-# Parse command-line arguments
-
-while : ; do
-  case "$1" in
-    "") break;;
-    -help|--help) usage
-                  exit;;
-    -prefix|--prefix) prefix_spec=yes
-                      prefix="$2"
-                      shift;;
-    -local|--local) local=true;;
-    -coqrunbyteflags|--coqrunbyteflags) coqrunbyteflags_spec=yes
-                                        coqrunbyteflags="$2"
-                                        shift;;
-    -coqtoolsbyteflags|--coqtoolsbyteflags) coqtoolsbyteflags_spec=yes
-                                            coqtoolsbyteflags="$2"
-                                            shift;;
-    -custom|--custom) custom_spec=yes;;
-    -bindir|--bindir) bindir_spec=yes
-                      bindir="$2"
-                      shift;;
-    -libdir|--libdir) libdir_spec=yes
-                      libdir="$2"
-                      shift;;
-    -configdir|--configdir) configdir_spec=yes
-                      configdir="$2"
-                      shift;;
-    -datadir|--datadir) datadir_spec=yes
-                      datadir="$2"
-                      shift;;
-    -mandir|--mandir) mandir_spec=yes
-                      mandir="$2"
-                      shift;;
-    -docdir|--docdir) docdir_spec=yes
-                      docdir="$2"
-                      shift;;
-    -emacslib|--emacslib) emacslib_spec=yes
-                          emacslib="$2"
-                          shift;;
-    -emacs |--emacs) emacs_spec=yes
-                     emacs="$2"
-                     printf "Warning: obsolete -emacs option\n"
-                     shift;;
-    -coqdocdir|--coqdocdir) coqdocdir_spec=yes
-                      coqdocdir="$2"
-                      shift;;
-    -camldir|--camldir) camldir_spec=yes
-                        camldir="$2"
-                        shift;;
-    -lablgtkdir|--lablgtkdir) lablgtkdir_spec=yes
-                        lablgtkdir="$2"
-                        shift;;
-    -usecamlp5|--usecamlp5)
-                        usecamlp5=yes;;
-    -usecamlp4|--usecamlp4)
-                        usecamlp5=no;;
-    -camlp5dir|--camlp5dir)
-                        usecamlp5=yes
-                        camlp5dir="$2"
-                        shift;;
-    -arch|--arch) arch_spec=yes
-                  arch=$2
-                  shift;;
-    -opt|--opt) bytecamlc=ocamlc.opt
-                camlp4oexec=camlp4o  # can't add .opt since dyn load'll be required
-                nativecamlc=ocamlopt.opt;;
-    -natdynlink|--natdynlink) case "$2" in
-                          yes) natdynlink=yes;;
-                          *) natdynlink=no
-                        esac
-                        shift;;
-    -coqide|--coqide) coqide_spec=yes
-                      case "$2" in
-                          byte|opt) COQIDE=$2;;
-                          *) COQIDE=no
-                      esac
-                      shift;;
-    -nomacintegration) nomacintegration_spec=yes
-                      shift;;
-    -browser|--browser) browser_spec=yes
-                      BROWSER=$2
-                      shift;;
-    -coqwebsite|--coqwebsite) wwwcoq_spec=yes
-                      WWWCOQ=$2
-                      shift;;
-    -nodoc|--nodoc) with_doc_spec=yes
-                    with_doc=no;;
-    -with-doc|--with-doc) with_doc_spec=yes
-                      case "$2" in
-                          yes|all) with_doc=all;;
-                          *) with_doc=no
-                      esac
-                      shift;;
-    -with-geoproof|--with-geoproof)
-          case "$2" in
-              yes) with_geoproof=true;;
-              no) with_geoproof=false;;
-          esac
-          shift;;
-    -makecmd|--makecmd) makecmd="$2"
-                      shift;;
-    -byte-only|-byteonly|--byteonly|--byte-only) best_compiler=byte;;
-    -debug|--debug) coq_debug_flag=-g;;
-    -profile|--profile) coq_profile_flag=-p;;
-    -annotate|--annotate) coq_annotate_flag=-dtypes;;
-    -typerex|--typerex) coq_typerex_wrapper=$default_typerex_wrapper;;
-    -no-native-compiler|--no-native-compiler) no_native_compiler=true;;
-    -force-caml-version|--force-caml-version|-force-ocaml-version|--force-ocaml-version)
-          force_caml_version_spec=yes
-          force_caml_version=yes;;
-    *) echo "Unknown option \"$1\"." 1>&2; usage; exit 2;;
-  esac
-  shift
-done
-
-if [ $prefix_spec = yes -a $local = true ] ; then
-  echo "Options -prefix and -local are incompatible."
-  echo "Configure script failed!"
-  exit 1
-fi
-
-# compile date
-DATEPGM=`which date`
-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 +"%b %d %Y %H:%M:%S"`;;
-esac
-
-# Architecture
-
-case $arch_spec in
-    no)
-    # 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
-            ARCH=`/bin/uname -s`
-        elif test -x /usr/bin/uname ; then
-            ARCH=`/usr/bin/uname -s`
-        elif test -x /bin/arch ; then
-            ARCH=`/bin/arch`
-        elif test -x /usr/bin/arch ; then
-            ARCH=`/usr/bin/arch`
-        elif test -x /usr/ucb/arch ; then
-            ARCH=`/usr/ucb/arch`
-        else
-            echo "I can not automatically find the name of your architecture."
-            printf "%s"\
-                "Give me a name, please [win32 for Win95, Win98 or WinNT]: "
-            read ARCH
-        fi
-    fi;;
-    yes) ARCH=$arch
-esac
-
-# executable extension
-
-case $ARCH in
-    win32)
-      ARCH_WIN32=true
-      EXE=".exe"
-      DLLEXT=".dll";;
-    *) ARCH_WIN32=false
-       EXE=""
-       DLLEXT=".so"
-esac
-
-# Is the source tree checked out from a recognised
-# version control system ?
-if test -e .svn/entries ; then
-    checkedout=svn
-elif [ -d '{arch}' ]; then
-    checkedout=gnuarch
-elif [ -z "${GIT_DIR}" ] && [ -d .git ] || [ -d "${GIT_DIR}" ]; then
-    checkedout=git
-else
-    checkedout=0
-fi
-
-# make command
-
-MAKE=`which ${makecmd:-make}`  # NB: ${a:-b} is $a, or b when $a is undefined
-if [ "$MAKE" != "" ]; then
-  # Beware of the final \r in Win32
-  MAKEVERSION=`"$MAKE" -v | head -1 | tr -d "\r" | cut -d" " -f3`
-  MAKEVERSIONMAJOR=`echo $MAKEVERSION | cut -d. -f1`
-  MAKEVERSIONMINOR=`echo $MAKEVERSION | cut -d. -f2`
-  if [ "$MAKEVERSIONMAJOR" -gt 3 -o "$MAKEVERSIONMAJOR" -eq 3 -a "$MAKEVERSIONMINOR" -ge 81 ]; then
-      echo "You have GNU Make $MAKEVERSION. Good!"
-  else
-      OK="no"
-      #Extra support for local installation of make 3.81
-      #will be useless when make >= 3.81 will be standard
-      if [ -x ./make ]; then
-          MAKEVERSION=`./make -v | head -1`
-          if [ "$MAKEVERSION" = "GNU Make 3.81" ]; then OK="yes"; fi
-      fi
-      if [ $OK = "no" ]; then
-          echo "GNU Make >= 3.81 is needed."
-          echo "Make 3.81 can be downloaded from ftp://ftp.gnu.org/gnu/make/make-3.81.tar.gz"
-          echo "then locally installed on a Unix-style system by issuing:"
-          echo "  tar xzvf make-3.81.tar.gz"
-          echo "  cd make-3.81"
-          echo "  ./configure"
-          echo "  make"
-          echo "  mv make .."
-          echo "  cd .."
-          echo "Restart then the configure script and later use ./make instead of make."
-          exit 1
-      else
-          echo "You have locally installed GNU Make 3.81. Good!"
-      fi
-  fi
-else
-  echo "Cannot find GNU Make >= 3.81."
-fi
-
-# Browser command
-
-if [ "$browser_spec" = "no" ]; then
-    case $ARCH in
-        win32) BROWSER='start %s' ;;
-        Darwin) BROWSER='open %s' ;;
-        *) BROWSER='firefox -remote "OpenURL(%s,new-tab)" || firefox %s &' ;;
-    esac
-fi
-
-if [ "$wwwcoq_spec" = "no" ]; then
-    WWWCOQ="http://coq.inria.fr/"
-fi
-
-#########################################
-# Objective Caml programs
-
-case $camldir_spec in
-    no) CAMLC=`which $bytecamlc`
-        case "$CAMLC" in
-            "") echo "$bytecamlc is not present in your path!"
-                echo "Give me manually the path to the $bytecamlc executable [/usr/local/bin by default]: "
-                read CAMLC
-
-                case "$CAMLC" in
-                    "") CAMLC=/usr/local/bin/$bytecamlc;;
-                    */ocamlc|*/ocamlc.opt) true;;
-                    */) CAMLC="${CAMLC}"$bytecamlc;;
-                    *) CAMLC="${CAMLC}"/$bytecamlc;;
-                esac
-        esac
-        CAMLBIN=`dirname "$CAMLC"`;;
-    yes) CAMLC=$camldir/$bytecamlc
-
-         CAMLBIN=`dirname "$CAMLC"`
-         bytecamlc="$CAMLC"
-         nativecamlc=$CAMLBIN/$nativecamlc
-         ocamlexec=$CAMLBIN/ocaml
-         ocamldepexec=$CAMLBIN/ocamldep
-         ocamldocexec=$CAMLBIN/ocamldoc
-         ocamllexexec=$CAMLBIN/ocamllex
-         ocamlyaccexec=$CAMLBIN/ocamlyacc
-         ocamlmklibexec=$CAMLBIN/ocamlmklib
-         camlp4oexec=$CAMLBIN/camlp4o
-esac
-
-if test ! -f "$CAMLC" ; then
-    echo "I can not find the executable '$CAMLC'. Have you installed it?"
+if [ ! -f $script ]; then
+    echo "Error: file $script not found in the current directory."
+    echo "Please run the configure script from the root of the coq sources."
     echo "Configuration script failed!"
     exit 1
 fi
 
-# 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" "tools/mingwpath.ml" "$1" ;;
-        *) echo "$1" ;;
-    esac
-}
-
-case $ARCH in
-    win32) CAMLBIN=`mk_win_path "$CAMLBIN"`;;
-esac
-
-# Beware of the final \r in Win32
-CAMLVERSION=`"$CAMLC" -version | tr -d "\r"`
-CAMLLIB=`"$CAMLC" -where | tr -d "\r"`
-
-case $CAMLVERSION in
-    1.*|2.*|3.0*|3.10*|3.11.[01])
-        echo "Your version of Objective-Caml is $CAMLVERSION."
-        if [ "$force_caml_version" = "yes" ]; then
-            echo "*Warning* You are compiling Coq with an outdated version of Objective-Caml."
-        else
-            echo "          You need Objective-Caml 3.11.2 or later."
-            echo "          Configuration script failed!"
-            exit 1
-        fi;;
-    3.11.2|3.12*|4.*)
-        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;;
-esac
-
-CAMLTAG=OCAML`echo $CAMLVERSION | sed -e "s/\([1-9]\)\.\([0-9]*\).*/\1\2/g"`
-
-# For coqmktop & bytecode compiler
-
-if [ "$coq_debug_flag" = "-g" ]; then
-    case $CAMLTAG in
-        OCAML31*|OCAML4*)
-            # Compilation debug flag
-            coq_debug_flag_opt="-g"
-            ;;
-    esac
-fi
-
-# Camlp4 / Camlp5 configuration
-
-# Assume that camlp(4|5) binaries are at the same place as ocaml ones
-# (this should become configurable some day)
-CAMLP4BIN=${CAMLBIN}
-
-case $usecamlp5 in
-  yes)
-    CAMLP4=camlp5
-    CAMLP4MOD=gramlib
-    if [ "$camlp5dir" != "" ]; then
-	if [ -f "$camlp5dir/${CAMLP4MOD}.cma" ]; then
-	    CAMLP4LIB=$camlp5dir
-	    FULLCAMLP4LIB=$camlp5dir
-	else
-	    echo "Cannot find camlp5 libraries in $camlp5dir (camlp5.cma not found)."
-	    echo "Configuration script failed!"
-	    exit 1
-	fi
-    else
-	# Beware of the final \r in Win32
-	camlp5dir="$(camlp5 -where | tr -d '\r')"
-	if [ "$camlp5dir" != "" ]; then
-	    CAMLP4LIB=$camlp5dir
-	    FULLCAMLP4LIB=$camlp5dir
-	elif [ -f "${CAMLLIB}/camlp5/${CAMLP4MOD}.cma" ]; then
-            CAMLP4LIB=+camlp5
-	    FULLCAMLP4LIB=${CAMLLIB}/camlp5
-	elif [ -f "${CAMLLIB}/site-lib/${CAMLP4MOD}.cma" ]; then
-            CAMLP4LIB=+site-lib/camlp5
-	    FULLCAMLP4LIB=${CAMLLIB}/site-lib/camlp5
-	else
-	    echo "No Camlp5 installation found. Looking for Camlp4 instead..."
-	    usecamlp5=no
-	fi
-    fi
-esac
-
-# If we're (still...) going to use Camlp5, let's check its version
-
-case $usecamlp5 in
-  yes)
-    camlp4oexec=`echo "$camlp4oexec" | tr 4 5`
-    case `"$camlp4oexec" -v 2>&1` in
-        *"version 4.0"*|*5.00*)
-            echo "Camlp5 version < 5.01 not supported."
-            echo "Configuration script failed!"
-            exit 1;;
-    esac
-esac
-
-# We might now try to use Camlp4, either by explicit choice or
-# by lack of proper Camlp5 installation
-
-case $usecamlp5 in
-  no)
-    CAMLP4=camlp4
-    CAMLP4MOD=camlp4lib
-    CAMLP4LIB=+camlp4
-    FULLCAMLP4LIB=${CAMLLIB}/camlp4
-
-    if [ ! -f "${FULLCAMLP4LIB}/${CAMLP4MOD}.cma" ]; then
-        echo "No Camlp4 installation found."
-        echo "Configuration script failed!"
-        exit 1
-    fi
-
-    camlp4oexec=${camlp4oexec}rf
-    if [ "`"$camlp4oexec" 2>&1`" != "" ]; then
-        echo "Error: $camlp4oexec not found or not executable."
-        echo "Configuration script failed!"
-        exit 1
-    fi
-esac
-
-# do we have a native compiler: test of ocamlopt and its version
-
-if [ "$best_compiler" = "opt" ] ; then
-  if test -e "$nativecamlc" || test -e "`which $nativecamlc`"; then
-      CAMLOPTVERSION=`"$nativecamlc" -v | sed -n -e 's|.*version* *\(.*\)$|\1|p' `
-      if [ ! -f "${FULLCAMLP4LIB}/${CAMLP4MOD}.cmxa" ]; then
-          best_compiler=byte
-          echo "Cannot find native-code $CAMLP4,"
-          echo "only the bytecode version of Coq will be available."
-      elif [ ! -f "$CAMLLIB"/dynlink.cmxa ]; then
-          best_compiler=byte
-          echo "Cannot find native-code dynlink library,"
-          echo "only the bytecode version of Coq will be available."
-          echo "For building a native-code Coq, you may try to first"
-          echo "compile and install a dummy dynlink.cmxa (see dev/dynlink.ml)"
-          echo "and then run ./configure -natdynlink no"
-      else
-          if [ "$CAMLOPTVERSION" != "$CAMLVERSION" ] ; then
-              echo "Native and bytecode compilers do not have the same version!"
-          fi
-          echo "You have native-code compilation. Good!"
-      fi
-  else
-      best_compiler=byte
-      echo "You have only bytecode compilation."
-  fi
-fi
-
-# Native dynlink
-if [ "$natdynlink" = "yes" -a -f "$CAMLLIB"/dynlink.cmxa ]; then
-    HASNATDYNLINK=true
-else
-    HASNATDYNLINK=false
-fi
-
-case $HASNATDYNLINK,$ARCH,`uname -r`,$CAMLVERSION in
-    true,Darwin,9.*,3.11.*)  # ocaml 3.11.0 dynlink on MacOS 10.5 is buggy
-        NATDYNLINKFLAG=os5fixme;;
-    #Possibly a problem on 10.6.0/10.6.1/10.6.2
-    #May just be a 32 vs 64 problem for all 10.6.*
-    true,Darwin,10.0.*,3.11.*) # Possibly a problem on 10.6.0
-        NATDYNLINKFLAG=os5fixme;;
-    true,Darwin,10.1.*,3.11.*) # Possibly a problem on 10.6.1
-        NATDYNLINKFLAG=os5fixme;;
-    true,Darwin,10.2.*,3.11.*) # Possibly a problem on 10.6.2
-        NATDYNLINKFLAG=os5fixme;;
-    true,Darwin,10.*,3.11.*)
-        if [ `getconf LONG_BIT` = "32" ]; then
-            # Still a problem for x86_32
-            NATDYNLINKFLAG=os5fixme
-        else
-            # Not a problem for x86_64
-            NATDYNLINKFLAG=$HASNATDYNLINK
-        fi;;
-    *)
-        NATDYNLINKFLAG=$HASNATDYNLINK;;
-esac
-
-# OS dependent libraries
-
-OSDEPLIBS="-cclib -lunix"
-case $ARCH in
-  sun4*) OS=`uname -r`
-        case $OS in
-           5*) OS="Sun Solaris $OS"
-               OSDEPLIBS="$OSDEPLIBS -cclib -lnsl -cclib -lsocket";;
-           *) OS="Sun OS $OS"
-        esac;;
-esac
-
-# lablgtk2 and CoqIDE
-
-IDEARCHFLAGS=
-IDEARCHFILE=
-IDEARCHDEF=X11
-
-# -byte-only should imply -coqide byte, unless the user decides otherwise
-
-if [ "$best_compiler" = "byte" -a "$coqide_spec" = "no" ]; then
-    coqide_spec=yes
-    COQIDE=byte
-fi
-
-# Which coqide is asked ? which one is possible ?
-
-if [ "$coqide_spec" = "yes" -a "$COQIDE" = "no" ]; then
-    echo "CoqIde disabled as requested."
-else
-    case $lablgtkdir_spec in
-        no)
-            # Beware of the final \r in Win32
-            lablgtkdirtmp="$(ocamlfind query lablgtk2.sourceview2 2> /dev/null | tr -d '\r')"
-            if [ "$lablgtkdirtmp" != "" ]; then
-                if [ ! -f "$lablgtkdirtmp/gSourceView2.cmi" ]; then
-                    echo "Incomplete Lablgtk2 found by ocamlfind (gSourceView2.cmi not found)."
-                elif [ ! -f "$lablgtkdirtmp/glib.mli" ]; then
-                    echo "Incomplete Lablgtk2 found by ocamlfind (glib.mli not found)."
-                else
-                    lablgtkdirfoundmsg="LabelGtk2 found by ocamlfind"
-                    lablgtkdir=$lablgtkdirtmp
-                    LABLGTKLIB=$lablgtkdir # Pour le message utilisateur
-                fi
-            fi
-            if [ "$lablgtkdir" = "" -a -f "${CAMLLIB}/lablgtk2/gSourceView2.cmi" -a -f "${CAMLLIB}/lablgtk2/glib.mli" ]; then
-                lablgtkdirfoundmsg="LablGtk2 found in ocaml lib directory"
-                lablgtkdir=${CAMLLIB}/lablgtk2
-                LABLGTKLIB=+lablgtk2 # Pour le message utilisateur
-            fi;;
-        yes)
-            if [ ! -d "$lablgtkdir" ]; then
-                echo "$lablgtkdir is not a valid directory."
-                echo "Configuration script failed!"
-                exit 1
-            elif [ ! -f "$lablgtkdir/gSourceView2.cmi" ]; then
-                echo "Incomplete LablGtk2 library (gSourceView2.cmi not found)."
-                echo "Make sure that the GtkSourceView bindings are available."
-                echo "Configuration script failed!"
-                exit 1
-            elif [ ! -f "$lablgtkdir/glib.mli" ]; then
-                echo "Incomplete LablGtk2 library (glib.mli not found)."
-                echo "Configuration script failed!"
-                exit 1
-            else
-                lablgtkdirfoundmsg="LablGtk2 directory found"
-                LABLGTKLIB=$lablgtkdir # Pour le message utilisateur
-            fi;;
-    esac
-    if [ "$lablgtkdir" = "" ]; then
-        echo "LablGtk2 not found: CoqIde will not be available."
-        COQIDE=no
-    elif [ -z "`grep -w convert_with_fallback "$lablgtkdir/glib.mli"`" ]; then
-        echo "$lablgtkdirfoundmsg but too old: CoqIde will not be available."
-        COQIDE=no;
-    elif [ "$coqide_spec" = "yes" -a "$COQIDE" = "byte" ]; then
-        echo "$lablgtkdirfoundmsg, bytecode CoqIde will be used as requested."
-        COQIDE=byte
-    elif [ ! -f "${CAMLLIB}/threads/threads.cmxa" -a -f "${lablgtkdir}/gtkThread.cmx" ]; then
-        echo "$lablgtkdirfoundmsg, not native (or no native threads): bytecode CoqIde will be available."
-        COQIDE=byte
-    else
-        echo "$lablgtkdirfoundmsg, native threads: native CoqIde will be available."
-        COQIDE=opt
-        if [ "$nomacintegration_spec" = "no" ] && lablgtkosxdir=$(ocamlfind query lablgtkosx 2> /dev/null);
-        then
-            IDEARCHFLAGS=lablgtkosx.cmxa
-            IDEARCHDEF=QUARTZ
-        elif [ "$ARCH" = "win32" ];
-        then
-            IDEARCHFLAGS=
-            IDEARCHFILE=ide/ide_win32_stubs.o
-            IDEARCHDEF=WIN32
-        fi
-    fi
-fi
-
-case $COQIDE in
-    byte|opt)
-        LABLGTKINCLUDES="-I $LABLGTKLIB";;
-    no)
-        LABLGTKINCLUDES="";;
-esac
-
-[ x$lablgtkosxdir = x ] || LABLGTKINCLUDES="$LABLGTKINCLUDES -I $lablgtkosxdir"
-
-# strip command
-
-case $ARCH in
-    Darwin) if [ "$HASNATDYNLINK" = "true" ]
-        then
-          STRIPCOMMAND="true"
-        else
-          STRIPCOMMAND="strip"
-        fi;;
-    *)
-    if [ "$coq_profile_flag" = "-p" ] || [ "$coq_debug_flag" = "-g" ]
-    then
-        STRIPCOMMAND="true"
-    else
-        STRIPCOMMAND="strip"
-    fi
-esac
-
-### Test if documentation can be compiled (latex, hevea)
-
-if test "$with_doc" = "all"
-then
-    for cmd in "latex" "hevea" ; do
-        if test ! -x "`which $cmd`"
-        then
-            echo "$cmd was not found; documentation will not be available"
-            with_doc=no
-            break
-        fi
-    done
-fi
-
-###########################################
-# bindir, libdir, mandir, docdir, etc.
-
-COQTOP=$PWD
-
-# OCaml only understand Windows filenames (C:\...)
-case $ARCH in
-    win32) COQTOP=`mk_win_path "$COQTOP"`
-           CAMLBIN=`mk_win_path "$CAMLBIN"`
-           CAMLP4BIN=`mk_win_path "$CAMLP4BIN"`
-esac
-
-# Default installation directories
-
-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";;
-  *)
-         bindir_def=/usr/local/bin
-         libdir_def=/usr/local/lib/coq
-         configdir_def=/etc/xdg/coq
-         datadir_def=/usr/local/share/coq
-         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;;
-esac
-
-askdir () {
-  printf "Where should I install $1 [%s]? " $2
-  read answer
-  if [ "$answer" = "" ]; then answer="$2"; fi
-}
-
-if [ $local = false ]; then
+## Parse the args, only looking for -camldir
+## We avoid using shift to keep "$@" intact
 
-# Installation directories for a non-local build
-
-case $bindir_spec/$prefix_spec in
-    yes/*) BINDIR=$bindir ;;
-    no/yes) BINDIR=$prefix/bin ;;
-    *) askdir "the Coq binaries" $bindir_def
-       BINDIR="$answer";;
-esac
-
-case $libdir_spec/$prefix_spec/$ARCH in
-    yes/*) LIBDIR=$libdir;;
-    no/yes/win32) LIBDIR=$prefix;;
-    no/yes/*) LIBDIR=$prefix/lib/coq ;;
-    *) askdir "the Coq library" $libdir_def
-       LIBDIR="$answer";;
-esac
-libdir_spec=yes
-
-case $configdir_spec/$prefix_spec/$ARCH in
-    yes/*) CONFIGDIR=$configdir;;
-    no/yes/win32) CONFIGDIR=$prefix/config;;
-    no/yes/*) CONFIGDIR=$prefix/etc/xdg/coq;;
-    *) askdir "the Coqide configuration files" $configdir_def
-       CONFIGDIR="$answer";;
-esac
-if [ "$CONFIGDIR" != "$configdir_def" ]; then configdir_spec=yes; fi
-
-case $datadir_spec/$prefix_spec in
-    yes/*) DATADIR=$datadir;;
-    no/yes) DATADIR=$prefix/share/coq;;
-    *) askdir "the Coqide data files" $datadir_def
-        DATADIR="$answer";;
-esac
-if [ "$DATADIR" != "datadir_def" ]; then datadir_spec=yes; fi
-
-case $mandir_spec/$prefix_spec in
-    yes/*) MANDIR=$mandir;;
-    no/yes) MANDIR=$prefix/share/man ;;
-    *) askdir "the Coq man pages" $mandir_def
-       MANDIR="$answer";;
-esac
-
-case $docdir_spec/$prefix_spec in
-    yes/*) DOCDIR=$docdir;;
-    no/yes) DOCDIR=$prefix/share/doc/coq;;
-    *) askdir "the Coq documentation [%s]? " $docdir_def
-       DOCDIR="$answer";;
-esac
-
-case $emacslib_spec/$prefix_spec/$ARCH in
-    yes/*) EMACSLIB=$emacslib;;
-    no/yes/win32) EMACSLIB=$prefix/emacs ;;
-    no/yes/*) EMACSLIB=$prefix/share/emacs/site-lisp ;;
-    *) askdir "the Coq Emacs mode" $emacslib_def
-       EMACSLIB="$answer";;
-esac
-
-case $coqdocdir_spec/$prefix_spec/$ARCH in
-    yes/*) COQDOCDIR=$coqdocdir;;
-    no/yes/win32) COQDOCDIR=$prefix/latex ;;
-    no/yes/*) COQDOCDIR=$prefix/share/emacs/site-lisp ;;
-    *) askdir "Coqdoc TeX/LaTeX files" $coqdocdir_def
-       COQDOCDIR="$answer";;
-esac
-
-else # local build
-    CONFIGDIR=$COQTOP/ide
-    DATADIR=$COQTOP/ide
-    configdir_spec=yes
-    datadir_spec=yes
-fi
-
-# Determine if we enable -custom by default (Windows and MacOS)
-CUSTOM_OS=no
-if [ "$ARCH" = "win32" ] || [ "$ARCH" = "Darwin" ]; then
-    CUSTOM_OS=yes
-fi
-
-BUILDLDPATH="# you might want to set CAML_LD_LIBRARY_PATH by hand!"
-case $coqrunbyteflags_spec/$local/$custom_spec/$CUSTOM_OS in
-    yes/*/*/*) COQRUNBYTEFLAGS="$coqrunbyteflags";;
-    */*/yes/*|*/*/*/yes) COQRUNBYTEFLAGS="-custom";;
-    */true/*/*) COQRUNBYTEFLAGS="-dllib -lcoqrun -dllpath '$COQTOP'/kernel/byterun";;
-    *)
-        COQRUNBYTEFLAGS="-dllib -lcoqrun -dllpath '$LIBDIR'"
-        BUILDLDPATH="export CAML_LD_LIBRARY_PATH='$COQTOP'/kernel/byterun:$CAML_LD_LIBRARY_PATH";;
-esac
-case $coqtoolsbyteflags_spec/$custom_spec/$CUSTOM_OS in
-    yes/*/*) COQTOOLSBYTEFLAGS="$coqtoolsbyteflags";;
-    */yes/*|*/*/yes) COQTOOLSBYTEFLAGS="-custom";;
-    *) COQTOOLSBYTEFLAGS="";;
-esac
-
-
-###########################################
-# Summary of the configuration
-
-echo ""
-echo "  Architecture                      : $ARCH"
-if test ! -z "$OS" ; then
-  echo "  Operating system                  : $OS"
-fi
-echo "  Coq VM bytecode link flags        : $COQRUNBYTEFLAGS"
-echo "  Coq tools bytecode link flags     : $COQTOOLSBYTEFLAGS"
-echo "  OS dependent libraries            : $OSDEPLIBS"
-echo "  Objective-Caml/Camlp4 version     : $CAMLVERSION"
-echo "  Objective-Caml/Camlp4 binaries in : $CAMLBIN"
-echo "  Objective-Caml library in         : $CAMLLIB"
-echo "  Camlp4 library in                 : $CAMLP4LIB"
-if test "$best_compiler" = opt ; then
-echo "  Native dynamic link support       : $HASNATDYNLINK"
-fi
-if test "$COQIDE" != "no"; then
-echo "  Lablgtk2 library in               : $LABLGTKLIB"
-fi
-if test "$IDEARCHDEF" = "QUARTZ"; then
-echo "  Mac OS integration is on"
-fi
-if test "$with_doc" = "all"; then
-echo "  Documentation                     : All"
-else
-echo "  Documentation                     : None"
-fi
-echo "  CoqIde                            : $COQIDE"
-echo "  Web browser                       : $BROWSER"
-echo "  Coq web site                      : $WWWCOQ"
-echo ""
-
-if test "$no_native_compiler" = "true"; then
-echo "  Native compiler for conversion and normalization disabled"
-echo ""
-fi
-
-if test "$local" = "true"; then
-echo "  Local build, no installation..."
-echo ""
-else
-echo "  Paths for true installation:"
-echo "    binaries      will be copied in $BINDIR"
-echo "    library       will be copied in $LIBDIR"
-echo "    config files  will be copied in $CONFIGDIR"
-echo "    data files    will be copied in $DATADIR"
-echo "    man pages     will be copied in $MANDIR"
-echo "    documentation will be copied in $DOCDIR"
-echo "    emacs mode    will be copied in $EMACSLIB"
-echo ""
-fi
-
-##################################################
-# Building the dev/ocamldebug-coq file
-##################################################
-
-OCAMLDEBUGCOQ=dev/ocamldebug-coq
-
-if test "$coq_debug_flag" = "-g" ; then
-  rm -f $OCAMLDEBUGCOQ
-  sed -e "s|COQTOPDIRECTORY|$COQTOP|" \
-      -e "s|CAMLBINDIRECTORY|$CAMLBIN|" \
-      -e "s|CAMLP4LIBDIRECTORY|$FULLCAMLP4LIB|"\
-      $OCAMLDEBUGCOQ.template > $OCAMLDEBUGCOQ
-  chmod a-w,a+x $OCAMLDEBUGCOQ
-fi
-
-##############################################
-# Creation of configuration files
-##############################################
-
-mlconfig_file=config/coq_config.ml
-mymlconfig_file=myocamlbuild_config.ml
-config_file=config/Makefile
-config_template=config/Makefile.template
-
-
-### Warning !!
-### After this line, be careful when using variables,
-### since some of them will be escaped
-
-escape_string () {
-    "$ocamlexec" "tools/escape_string.ml" "$1"
-}
-
-# Escaped version of browser command
-BROWSER=`escape_string "$BROWSER"`
-
-# Under Windows, we now escape the backslashes that will ends in
-# ocaml strings (coq_config.ml) or in Makefile variables.
-
-case $ARCH in
-    win32)
-        BINDIR=`escape_string "$BINDIR"`
-        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 config/coq_config.ml file
-#####################################################
-
-rm -f "$mlconfig_file" "$mymlconfig_file"
-cat << END_OF_COQ_CONFIG > $mlconfig_file
-(* DO NOT EDIT THIS FILE: automatically generated by ../configure *)
-
-let local = $local
-let coqrunbyteflags = "$COQRUNBYTEFLAGS"
-let coqlib = $LIBDIR_OPTION
-let configdir = $CONFIGDIR_OPTION
-let datadir = $DATADIR_OPTION
-let docdir = "$DOCDIR"
-let ocaml = "$ocamlexec"
-let ocamlc = "$bytecamlc"
-let ocamlopt = "$nativecamlc"
-let ocamlmklib = "$ocamlmklibexec"
-let ocamldep = "$ocamldepexec"
-let ocamldoc = "$ocamldocexec"
-let ocamlyacc = "$ocamlyaccexec"
-let ocamllex = "$ocamllexexec"
-let camlbin = "$CAMLBIN"
-let camllib = "$CAMLLIB"
-let camlp4 = "$CAMLP4"
-let camlp4o = "$camlp4oexec"
-let camlp4bin = "$CAMLP4BIN"
-let camlp4lib = "$CAMLP4LIB"
-let camlp4compat = "$CAMLP4COMPAT"
-let coqideincl = "$LABLGTKINCLUDES"
-let cflags = "$cflags"
-let best = "$best_compiler"
-let arch = "$ARCH"
-let arch_is_win32 = $ARCH_WIN32
-let has_coqide = "$COQIDE"
-let gtk_platform = \`$IDEARCHDEF
-let has_natdynlink = $HASNATDYNLINK
-let natdynlinkflag = "$NATDYNLINKFLAG"
-let osdeplibs = "$OSDEPLIBS"
-let version = "$VERSION"
-let caml_version = "$CAMLVERSION"
-let date = "$DATE"
-let compile_date = "$COMPILEDATE"
-let vo_magic_number = $VOMAGIC
-let state_magic_number = $STATEMAGIC
-let exec_extension = "$EXE"
-let with_geoproof = ref $with_geoproof
-let browser = "$BROWSER"
-let wwwcoq = "$WWWCOQ"
-let wwwrefman = wwwcoq ^ "distrib/" ^ version ^ "/refman/"
-let wwwstdlib = wwwcoq ^ "distrib/" ^ version ^ "/stdlib/"
-let localwwwrefman = "file:/" ^ docdir ^ "html/refman"
-let no_native_compiler = $no_native_compiler
-
-
-END_OF_COQ_CONFIG
-
-echo "let plugins_dirs = [" >> "$mlconfig_file"
-find plugins/* \( -name .svn -prune \) -o \( -type d -exec printf "\"%s\";\n" {} \; \) >> "$mlconfig_file"
-echo "]" >> "$mlconfig_file"
-
-chmod a-w "$mlconfig_file"
-ln -sf "$mlconfig_file" "$mymlconfig_file"
-
-###############################################
-# Building the config/Makefile file
-###############################################
-
-rm -f "$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 (gallina.el)
-BINDIR="$BINDIR"
-COQLIBINSTALL="$LIBDIR"
-CONFIGDIR="$CONFIGDIR"
-DATADIR="$DATADIR"
-MANDIR="$MANDIR"
-DOCDIR="$DOCDIR"
-EMACSLIB="$EMACSLIB"
-EMACS=$EMACS
-
-# Path to Coq distribution
-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"
-
-# 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
-
-# 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
+last=
+for i; do
+   case $last in
+       -camldir|--camldir) cmd="$i/ocaml"; break;;
+   esac
+   last=$i
+done
 
-chmod a-w "$config_file"
+## We check that $cmd is ok before the real exec $cmd
 
-##################################################
-# The end
-####################################################
+`$cmd -version > /dev/null 2>&1` && exec $cmd $script "$@"
 
-echo "If anything in the above is wrong, please restart './configure'."
-echo
-echo "*Warning* To compile the system for a new architecture"
-echo "          don't forget to do a 'make clean' before './configure'."
+## If we're still here, something is wrong with $cmd
 
+echo "Error: failed to run $cmd"
+echo "Please use the option -camldir <dir> if 'ocaml' is installed"
+echo "in directory <dir>, or add <dir> to your path."
+echo "Configuration script failed!"
+exit 1
diff --git a/configure.ml b/configure.ml
new file mode 100644
index 000000000..3b5daee3c
--- /dev/null
+++ b/configure.ml
@@ -0,0 +1,1114 @@
+(**********************************)
+
+(**  Configuration script for Coq *)
+
+(**********************************)
+
+(** This file should be run via: ocaml configure.ml <opts>
+    You could also use our wrapper ./configure <opts> *)
+
+#load "unix.cma"
+open Printf
+
+let coq_version = "trunk"
+let vo_magic = 8511
+let state_magic = 58511
+
+let verbose = ref false (* for debugging this script *)
+
+(** * Utility functions *)
+
+let die msg = eprintf "%s\nConfiguration script failed!\n" msg; exit 1
+
+let s2i = int_of_string
+let i2s = string_of_int
+let (/) = Filename.concat
+
+(** Remove the final '\r' that may exists on Win32 *)
+
+let remove_final_cr s =
+  let n = String.length s in
+  if n<>0 && s.[n-1] = '\r' then String.sub s 0 (n-1)
+  else s
+
+let check_exit_code (_,code) = match code with
+  | Unix.WEXITED 0 -> ()
+  | Unix.WEXITED 127 -> failwith "no such command"
+  | Unix.WEXITED n -> failwith ("exit code " ^ i2s n)
+  | Unix.WSIGNALED n -> failwith ("killed by signal " ^ i2s n)
+  | Unix.WSTOPPED n -> failwith ("stopped by signal " ^ i2s n)
+
+(** Below, we'd better read all lines on a channel before closing it,
+    otherwise a SIGPIPE could be encountered by the sub-process *)
+
+let read_first_line_and_close fd =
+  let cin = Unix.in_channel_of_descr fd in
+  let line = try remove_final_cr (input_line cin) with End_of_file -> "" in
+  (try while true do ignore (input_line cin) done with End_of_file -> ());
+  close_in cin;
+  line
+
+(** Run some unix command and read the first line of its output.
+    We avoid Unix.open_process and its non-fully-portable /bin/sh,
+    especially when it comes to quoting the filenames.
+    See open_process_pid in ide/coq.ml for more details.
+    Error messages:
+     - if err=StdErr, any error message goes in the stderr of our script.
+     - if err=StdOut, we merge stderr and stdout (just as 2>&1).
+     - if err=DevNull, we drop the error messages (same as 2>/dev/null). *)
+
+type err = StdErr | StdOut | DevNull
+
+let run ?(fatal=true) ?(err=StdErr) prog args =
+  let argv = Array.of_list (prog::args) in
+  try
+    let out_r,out_w = Unix.pipe () in
+    let nul_r,nul_w = Unix.pipe () in
+    let () = Unix.set_close_on_exec out_r in
+    let () = Unix.set_close_on_exec nul_r in
+    let fd_err = match err with
+      | StdErr -> Unix.stderr
+      | StdOut -> out_w
+      | DevNull -> nul_w
+    in
+    let pid = Unix.create_process prog argv Unix.stdin out_w fd_err in
+    let () = Unix.close out_w in
+    let () = Unix.close nul_w in
+    let line = read_first_line_and_close out_r in
+    let _ = read_first_line_and_close nul_r in
+    let () = check_exit_code (Unix.waitpid [] pid) in
+    line
+  with
+  | _ when not fatal && not !verbose -> ""
+  | e ->
+      let cmd = String.concat " " (prog::args) in
+      let exn = match e with Failure s -> s | _ -> Printexc.to_string e in
+      let msg = sprintf "Error while running '%s' (%s)" cmd exn in
+      if fatal then die msg else (printf "W: %s\n" msg; "")
+
+let tryrun prog args = run ~fatal:false ~err:DevNull prog args
+
+(** Splitting a string at some character *)
+
+let string_split c s =
+  let len = String.length s in
+  let rec split n =
+    try
+      let pos = String.index_from s n c in
+      let dir = String.sub s n (pos-n) in
+      dir :: split (succ pos)
+    with
+      | Not_found -> [String.sub s n (len-n)]
+  in
+  if len = 0 then [] else split 0
+
+(** String prefix test : does [s1] starts with [s2] ? *)
+
+let starts_with s1 s2 =
+  let l1 = String.length s1 and l2 = String.length s2 in
+  l2 <= l1 && s2 = String.sub s1 0 l2
+
+(** Turn a version string such as "4.01.0+rc2" into the list
+    ["4";"01";"1"], stopping at the first non-digit or "." *)
+
+let numeric_prefix_list s =
+  let isnum c = (c = '.' || (c >= '0' && c <= '9')) in
+  let max = String.length s in
+  let i = ref 0 in
+  while !i < max && isnum s.[!i] do incr i done;
+  string_split '.' (String.sub s 0 !i)
+
+(** Combined existence and directory tests *)
+
+let dir_exists f = Sys.file_exists f && Sys.is_directory f
+
+(** Does a file exist and is executable ? *)
+
+let is_executable f =
+  try let () = Unix.access f [Unix.X_OK] in true
+  with Unix.Unix_error _ -> false
+
+(** Equivalent of rm -f *)
+
+let safe_remove f =
+  try Unix.chmod f 0o644; Sys.remove f with _ -> ()
+
+(** The PATH list for searching programs *)
+
+let os_type_win32 = (Sys.os_type = "Win32")
+
+let global_path =
+  try string_split (if os_type_win32 then ';' else ':') (Sys.getenv "PATH")
+  with Not_found -> []
+
+(** A "which" command. May raise [Not_found] *)
+
+let which prog =
+  let rec search = function
+    | [] -> raise Not_found
+    | dir :: path ->
+      let file = if os_type_win32 then dir/prog^".exe" else dir/prog in
+      if is_executable file then file else search path
+  in search global_path
+
+let program_in_path prog =
+  try let _ = which prog in true with Not_found -> false
+
+
+(** * Date *)
+
+(** The short one is displayed when starting coqtop,
+    The long one is used as compile date *)
+
+let months =
+ [| "January";"February";"March";"April";"May";"June";
+    "July";"August";"September";"October";"November";"December" |]
+
+let get_date () =
+  let now = Unix.localtime (Unix.time ()) in
+  let year = 1900+now.Unix.tm_year in
+  let month = months.(now.Unix.tm_mon) in
+  sprintf "%s %d" month year,
+  sprintf "%s %d %d %d:%d:%d" (String.sub month 0 3) now.Unix.tm_mday year
+    now.Unix.tm_hour now.Unix.tm_min now.Unix.tm_sec
+
+let short_date, full_date = get_date ()
+
+
+(** Create the bin/ directory if non-existent *)
+
+let _ = if not (dir_exists "bin") then Unix.mkdir "bin" 0o755
+
+
+(** * Command-line parsing *)
+
+type ide = Opt | Byte | No
+
+let get_bool = function
+  | "true" | "yes" | "y" | "all" -> true
+  | "false" | "no" | "n" -> false
+  | s -> raise (Arg.Bad ("boolean argument expected instead of "^s))
+
+let get_ide = function
+  | "opt" -> Opt
+  | "byte" -> Byte
+  | "no" -> No
+  | s -> raise (Arg.Bad ("(opt|byte|no) argument expected instead of "^s))
+
+let arg_bool r = Arg.String (fun s -> r := get_bool s)
+
+let arg_string_option r = Arg.String (fun s -> r := Some s)
+
+module Prefs = struct
+  let prefix = ref (None : string option)
+  let local = ref false
+  let coqrunbyteflags = ref (None : string option)
+  let coqtoolsbyteflags = ref (None : string option)
+  let custom = ref false
+  let bindir = ref (None : string option)
+  let libdir = ref (None : string option)
+  let configdir = ref (None : string option)
+  let datadir = ref (None : string option)
+  let mandir = ref (None : string option)
+  let docdir = ref (None : string option)
+  let emacslib = ref (None : string option)
+  let coqdocdir = ref (None : string option)
+  let camldir = ref (None : string option)
+  let lablgtkdir = ref (None : string option)
+  let usecamlp5 = ref true
+  let camlp5dir = ref (None : string option)
+  let arch = ref (None : string option)
+  let opt = ref false
+  let natdynlink = ref true
+  let coqide = ref (None : ide option)
+  let macintegration = ref true
+  let browser = ref (None : string option)
+  let withdoc = ref true
+  let geoproof = ref false
+  let byteonly = ref false
+  let debug = ref false
+  let profile = ref false
+  let annotate = ref false
+  let typerex = ref false
+  let makecmd = ref "make"
+  let nativecompiler = ref true
+  let coqwebsite = ref "http://coq.inria.fr/"
+  let force_caml_version = ref false
+end
+
+(* TODO : earlier any option -foo was also available as --foo *)
+
+let args_options = Arg.align [
+  "-prefix", arg_string_option Prefs.prefix,
+    "<dir> Set installation directory to <dir>";
+  "-local", Arg.Set Prefs.local,
+    " Set installation directory to the current source tree";
+  "-coqrunbyteflags", arg_string_option Prefs.coqrunbyteflags,
+    "<flags> Set link flags for VM-dependent bytecode (coqtop)";
+  "-coqtoolsbyteflags", arg_string_option Prefs.coqtoolsbyteflags,
+    "<flags> Set link flags for VM-independant bytecode (coqdep,coqdoc,...)";
+  "-custom", Arg.Set Prefs.custom,
+    " Generate all bytecode executables with -custom (not recommended)";
+  "-bindir", arg_string_option Prefs.bindir,
+    "<dir> Where to install bin files";
+  "-libdir", arg_string_option Prefs.libdir,
+    "<dir> Where to install lib files";
+  "-configdir", arg_string_option Prefs.configdir,
+    "<dir> Where to install config files";
+  "-datadir", arg_string_option Prefs.datadir,
+    "<dir> Where to install data files";
+  "-mandir", arg_string_option Prefs.mandir,
+    "<dir> Where to install man files";
+  "-docdir", arg_string_option Prefs.docdir,
+    "<dir> Where to install doc files";
+  "-emacslib", arg_string_option Prefs.emacslib,
+    "<dir> Where to install emacs files";
+  "-emacs", Arg.String (fun s ->
+      printf "Warning: obsolete -emacs option\n";
+      Prefs.emacslib := Some s),
+    "<dir> (Obsolete) same as -emacslib";
+  "-coqdocdir", arg_string_option Prefs.coqdocdir,
+    "<dir> Where to install Coqdoc style files";
+  "-camldir", arg_string_option Prefs.camldir,
+    "<dir> Specifies the path to the OCaml library";
+  "-lablgtkdir", arg_string_option Prefs.lablgtkdir,
+    "<dir> Specifies the path to the Lablgtk library";
+  "-usecamlp5", Arg.Set Prefs.usecamlp5,
+    " Specifies to use camlp5 instead of camlp4";
+  "-usecamlp4", Arg.Clear Prefs.usecamlp5,
+    " Specifies to use camlp4 instead of camlp5";
+  "-camlp5dir",
+    Arg.String (fun s -> Prefs.usecamlp5:=true; Prefs.camlp5dir:=Some s),
+    "<dir> Specifies where to look for the Camlp5 library and tells to use it";
+  "-arch", arg_string_option Prefs.arch,
+    "<arch> Specifies the architecture";
+  "-opt", Arg.Set Prefs.opt,
+    " Use OCaml *.opt optimized compilers";
+  "-natdynlink", arg_bool Prefs.natdynlink,
+    "(yes|no) Use dynamic loading of native code or not";
+  "-coqide", Arg.String (fun s -> Prefs.coqide := Some (get_ide s)),
+    "(opt|byte|no) Specifies whether or not to compile Coqide";
+  "-nomacintegration", Arg.Clear Prefs.macintegration,
+    " Do not try to build coqide mac integration";
+  "-browser", arg_string_option Prefs.browser,
+    "<command> Use <command> to open URL %s";
+  "-nodoc", Arg.Clear Prefs.withdoc,
+    " Do not compile the documentation";
+  "-with-doc", arg_bool Prefs.withdoc,
+    "(yes|no) Compile the documentation or not";
+  "-with-geoproof", arg_bool Prefs.geoproof,
+    "(yes|no) Use Geoproof binding or not";
+  "-byte-only", Arg.Set Prefs.byteonly,
+    " Compiles only bytecode version of Coq";
+  "-byteonly", Arg.Set Prefs.byteonly,
+    " Compiles only bytecode version of Coq";
+  "-debug", Arg.Set Prefs.debug,
+    " Add debugging information in the Coq executables";
+  "-profile", Arg.Set Prefs.profile,
+    " Add profiling information in the Coq executables";
+  "-annotate", Arg.Set Prefs.annotate,
+    " Compiles Coq with -dtypes option";
+  "-typerex", Arg.Set Prefs.typerex,
+    " Compiles Coq using typerex wrapper";
+  "-makecmd", Arg.Set_string Prefs.makecmd,
+    "<command> Name of GNU Make command";
+  "-no-native-compiler", Arg.Clear Prefs.nativecompiler,
+    " Disables compilation to native code for conversion and normalization";
+  "-coqwebsite", Arg.Set_string Prefs.coqwebsite,
+    " URL of the coq website";
+  "-force-caml-version", arg_bool Prefs.force_caml_version,
+    " Force OCaml version";
+]
+
+let parse_args () =
+  Arg.parse
+    args_options
+    (fun s -> raise (Arg.Bad ("Unknown option: "^s)))
+    "Available options for configure are:";
+  if !Prefs.local && !Prefs.prefix <> None then
+    die "Options -prefix and -local are incompatible."
+
+let _ = parse_args ()
+
+(** Default OCaml binaries *)
+
+type camlexec =
+ { mutable byte : string;
+   mutable opt : string;
+   mutable top : string;
+   mutable mklib : string;
+   mutable dep : string;
+   mutable doc : string;
+   mutable lex : string;
+   mutable yacc : string;
+   mutable p4 : string }
+
+(* TODO: autodetect .opt binaries ? *)
+
+let camlexec =
+  { byte = if !Prefs.opt then "ocamlc.opt" else "ocamlc";
+    opt = if !Prefs.opt then "ocamlopt.opt" else "ocamlopt";
+    top = "ocaml";
+    mklib = "ocamlmklib";
+    dep = "ocamldep";
+    doc = "ocamldoc";
+    lex = "ocamllex";
+    yacc = "ocamlyacc";
+    p4 = "camlp4o" }
+
+let rebase_camlexec dir c =
+  c.byte <- Filename.concat dir c.byte;
+  c.opt <- Filename.concat dir c.opt;
+  c.top <- Filename.concat dir c.top;
+  c.mklib <- Filename.concat dir c.mklib;
+  c.dep <- Filename.concat dir c.dep;
+  c.doc <- Filename.concat dir c.doc;
+  c.lex <- Filename.concat dir c.lex;
+  c.yacc <- Filename.concat dir c.yacc;
+  c.p4 <- Filename.concat dir c.p4
+
+let coq_debug_flag = if !Prefs.debug then "-g" else ""
+let coq_profile_flag = if !Prefs.profile then "-p" else ""
+let coq_annotate_flag = if !Prefs.annotate then "-dtypes" else ""
+let coq_typerex_wrapper =
+  if !Prefs.typerex then "ocb-wrapper -save-types" else ""
+
+let cflags = "-fno-defer-pop -Wall -Wno-unused"
+
+
+(** * Architecture *)
+
+let arch_progs =
+  [("/bin/uname",["-s"]);
+   ("/usr/bin/uname",["-s"]);
+   ("/bin/arch", []);
+   ("/usr/bin/arch", []);
+   ("/usr/ucb/arch", []) ]
+
+let query_arch () =
+  printf "I can not automatically find the name of your architecture.\n";
+  printf "Give me a name, please [win32 for Win95, Win98 or WinNT]: %!";
+  read_line ()
+
+let rec try_archs = function
+  | (prog,args)::rest when is_executable prog ->
+    let arch = tryrun prog args in
+    if arch <> "" then arch else try_archs rest
+  | _ :: rest -> try_archs rest
+  | [] -> query_arch ()
+
+let os_type_cygwin = (Sys.os_type = "Cygwin")
+
+let arch = match !Prefs.arch with
+  | Some a -> a
+  | None ->
+    let arch = tryrun "uname" ["-s"] in
+    if starts_with arch "CYGWIN" then "win32"
+    else if starts_with arch "MINGW32" then "win32"
+    else if arch <> "" then arch
+    else try_archs arch_progs
+
+(** NB: [arch_win32] is broader than [os_type_win32], cf. cygwin *)
+
+let arch_win32 = (arch = "win32")
+
+let exe,dll = if arch_win32 then ".exe",".dll" else "", ".so"
+
+(** * VCS
+
+    Is the source tree checked out from a recognised
+    Version Control System ? *)
+
+let vcs =
+  let git_dir = try Sys.getenv "GIT_DIR" with Not_found -> ".git" in
+  if dir_exists git_dir then "git"
+  else if Sys.file_exists ".svn/entries" then "svn"
+  else if dir_exists "{arch}" then "gnuarch"
+  else "none"
+
+(** * The make command *)
+
+let make =
+  try
+    let version_line = run !Prefs.makecmd ["-v"] in
+    let version = List.nth (string_split ' ' version_line) 2 in
+    match string_split '.' version with
+    | major::minor::_ when (s2i major, s2i minor) >= (3,81) ->
+      printf "You have GNU Make %s. Good!\n" version
+    | _ -> failwith "bad version"
+  with _ -> die "Error: Cannot find GNU Make >= 3.81."
+
+(** * Browser command *)
+
+let browser =
+  match !Prefs.browser with
+  | Some b -> b
+  | None when arch_win32 -> "start %s"
+  | None when arch = "Darwin" -> "open %s"
+  | _ -> "firefox -remote \"OpenURL(%s,new-tab)\" || firefox %s &"
+
+(** * OCaml programs *)
+
+let camlbin, camlc = match !Prefs.camldir with
+  | Some dir ->
+    rebase_camlexec dir camlexec;
+    Filename.dirname camlexec.byte, camlexec.byte
+  | None ->
+    try let camlc = which camlexec.byte in Filename.dirname camlc, camlc
+    with Not_found ->
+      die (sprintf "Error: cannot find '%s' in your path!\n" camlexec.byte ^
+           "Please adjust your path or use the -camldir option of ./configure")
+
+let _ =
+  if not (is_executable camlc) then
+    die ("Error: cannot find the executable '"^camlc^"'.")
+
+let caml_version = run camlc ["-version"]
+let camllib = run camlc ["-where"]
+let camlp4compat = "-loc loc"
+
+(** Caml version as a list of string, e.g. ["4";"00";"1"] *)
+
+let caml_version_list = numeric_prefix_list caml_version
+
+(** Same, with integers in the version list *)
+
+let caml_version_nums =
+  try
+    if List.length caml_version_list < 2 then failwith "bad version";
+    List.map s2i caml_version_list
+  with _ ->
+    die ("I found the OCaml compiler but cannot read its version number!\n" ^
+         "Is it installed properly?")
+
+let check_caml_version () =
+  if caml_version_nums >= [3;11;2] then
+    printf "You have OCaml %s. Good!\n" caml_version
+  else
+    let () = printf "Your version of OCaml is %s.\n" caml_version in
+    if !Prefs.force_caml_version then
+      printf "*Warning* Your version of OCaml is outdated.\n"
+    else
+      die "You need OCaml 3.11.2 or later."
+
+let _ = check_caml_version ()
+
+let coq_debug_flag_opt =
+  if caml_version_nums >= [3;10] then coq_debug_flag else ""
+
+let camltag = match caml_version_list with
+  | x::y::_ -> "OCAML"^x^y
+  | _ -> assert false
+
+
+(** * CamlpX configuration *)
+
+(** We assume that camlp(4|5) binaries are at the same place as ocaml ones
+    (this should become configurable some day). *)
+
+let camlp4bin = camlbin
+
+(* TODO: camlp5dir should rather be the *binary* location, just as camldir *)
+(* TODO: remove the late attempts at finding gramlib.cma *)
+
+exception NoCamlp5
+
+let check_camlp5 testcma = match !Prefs.camlp5dir with
+  | Some dir ->
+    if Sys.file_exists (dir/testcma) then dir
+    else
+      let msg =
+        sprintf "Cannot find camlp5 libraries in '%s' (%s not found)."
+          dir testcma
+      in die msg
+  | None ->
+    let dir = tryrun "camlp5" ["-where"] in
+    if dir <> "" then dir
+    else if Sys.file_exists (camllib/"camlp5"/testcma) then
+      camllib/"camlp5"
+    else if Sys.file_exists (camllib/"site-lib"/"camlp5"/testcma) then
+      camllib/"site-lib"/"camlp5"
+    else
+      let () = printf "No Camlp5 installation found." in
+      let () = printf "Looking for Camlp4 instead...\n" in
+      raise NoCamlp5
+
+let check_camlp5_version () =
+  let s = camlexec.p4 in
+  (* translate 4 into 5 in the binary name *)
+  for i = 0 to String.length s - 1 do
+    if s.[i] = '4' then s.[i] <- '5'
+  done;
+  try
+    let version_line = run ~err:StdOut camlexec.p4 ["-v"] in
+    let version = List.nth (string_split ' ' version_line) 2 in
+    match string_split '.' version with
+    | major::minor::_ when (s2i major, s2i minor) >= (5,1) ->
+      printf "You have Camlp5 %s. Good!\n" version
+    | _ -> failwith "bad version"
+  with _ -> die "Error: unsupported Camlp5 (version < 5.01 or unrecognized).\n"
+
+let config_camlpX () =
+  try
+    if not !Prefs.usecamlp5 then raise NoCamlp5;
+    let lib = "gramlib" in
+    let dir = check_camlp5 (lib^".cma") in
+    let () = check_camlp5_version () in
+    "camlp5", dir, lib
+  with NoCamlp5 ->
+    (* We now try to use Camlp4, either by explicit choice or
+       by lack of proper Camlp5 installation *)
+    let lib = "camlp4lib" in
+    let dir = camllib/"camlp4" in
+    if not (Sys.file_exists (dir/lib^".cma")) then
+      die "No Camlp4 installation found.\n";
+    let () = camlexec.p4 <- camlexec.p4 ^ "rf" in
+    ignore (run camlexec.p4 []);
+    "camlp4", dir, lib
+
+let camlp4, fullcamlp4lib, camlp4mod = config_camlpX ()
+
+let shorten_camllib s =
+  if starts_with s (camllib^"/") then
+    let l = String.length camllib + 1 in
+    "+" ^ String.sub s l (String.length s - l)
+  else s
+
+let camlp4lib = shorten_camllib fullcamlp4lib
+
+
+(** * Native compiler *)
+
+let msg_byteonly () =
+  printf "Only the bytecode version of Coq will be available.\n"
+
+let msg_no_ocamlopt () =
+  printf "Cannot find the OCaml native-code compiler.\n"; msg_byteonly ()
+
+let msg_no_camlp4_cmxa () =
+  printf "Cannot find the native-code library of %s.\n" camlp4; msg_byteonly ()
+
+let msg_no_dynlink_cmxa () =
+  printf "Cannot find native-code dynlink library.\n"; msg_byteonly ();
+  printf "For building a native-code Coq, you may try to first\n";
+  printf "compile and install a dummy dynlink.cmxa (see dev/dynlink.ml)\n";
+  printf "and then run ./configure -natdynlink no\n"
+
+let check_native () =
+  if !Prefs.byteonly then raise Not_found;
+  if not (is_executable camlexec.opt || program_in_path camlexec.opt) then
+    (msg_no_ocamlopt (); raise Not_found);
+  if not (Sys.file_exists (fullcamlp4lib/camlp4mod^".cmxa")) then
+    (msg_no_camlp4_cmxa (); raise Not_found);
+  if not (Sys.file_exists (camllib/"dynlink.cmxa")) then
+    (msg_no_dynlink_cmxa (); raise Not_found);
+  let version = run camlexec.opt ["-version"] in
+  if version <> caml_version then
+    printf
+      "Warning: Native and bytecode compilers do not have the same version!\n";
+  printf "You have native-code compilation. Good!\n"
+
+let best_compiler =
+  try check_native (); "opt" with Not_found -> "byte"
+
+
+(** * Native dynlink *)
+
+let hasnatdynlink = !Prefs.natdynlink && best_compiler = "opt"
+
+(** OCaml 3.11.0 dynlink is buggy on MacOS 10.5, and possibly
+    also on 10.6.(0|1|2) for x86_64 and 10.6.x on x86_32 *)
+
+let needs_MacOS_fix () =
+  match hasnatdynlink, arch, caml_version_nums with
+  | true, "Darwin", 3::11::_ ->
+    (match string_split '.' (run "uname" ["-r"]) with
+    | "9"::_ -> true
+    | "10"::("0"|"1"|"2")::_ -> true
+    | "10"::_ when Sys.word_size = 32 -> true
+    | _ -> false)
+  | _ -> false
+
+let natdynlinkflag =
+  if needs_MacOS_fix () then "os5fixme" else
+    if hasnatdynlink then "true" else "false"
+
+
+(** * OS dependent libraries *)
+
+let osdeplibs = "-cclib -lunix"
+
+let operating_system, osdeplibs =
+  if starts_with arch "sun4" then
+    let os = run "uname" ["-r"] in
+    if starts_with os "5" then
+      "Sun Solaris "^os, osdeplibs^" -cclib -lnsl -cclib -lsocket"
+    else
+      "Sun OS "^os, osdeplibs
+  else
+    (try Sys.getenv "OS" with Not_found -> ""), osdeplibs
+
+
+(** * lablgtk2 and CoqIDE *)
+
+(** Is some location a suitable LablGtk2 installation ? *)
+
+let check_lablgtkdir ?(fatal=false) msg dir =
+  let yell msg = if fatal then die msg else (printf "%s\n" msg; false) in
+  if not (dir_exists dir) then
+    yell (sprintf "No such directory '%s' (%s)." dir msg)
+  else if not (Sys.file_exists (dir/"gSourceView2.cmi")) then
+    yell (sprintf "Incomplete LablGtk2 (%s): no %s/gSourceView2.cmi." msg dir)
+  else if not (Sys.file_exists (dir/"glib.mli")) then
+    yell (sprintf "Incomplete LablGtk2 (%s): no %s/glib.mli." msg dir)
+  else true
+
+(** Detect and/or verify the Lablgtk2 location *)
+
+let get_lablgtkdir () =
+  match !Prefs.lablgtkdir with
+  | Some dir ->
+    let msg = "manually provided" in
+    if check_lablgtkdir ~fatal:true msg dir then dir, msg
+    else "", ""
+  | None ->
+    let msg = "via ocamlfind" in
+    let d1 = tryrun "ocamlfind" ["query";"lablgtk2.sourceview2"] in
+    if d1 <> "" && check_lablgtkdir msg d1 then d1, msg
+    else
+      (* In debian wheezy, ocamlfind knows only of lablgtk2 *)
+      let d2 = tryrun "ocamlfind" ["query";"lablgtk2"] in
+      if d2 <> "" && d2 <> d1 && check_lablgtkdir msg d2 then d2, msg
+      else
+        let msg = "in OCaml library" in
+        let d3 = camllib^"/lablgtk2" in
+        if check_lablgtkdir msg d3 then d3, msg
+        else "", ""
+
+let pr_ide = function No -> "no" | Byte -> "only bytecode" | Opt -> "native"
+
+exception Ide of ide
+
+(** If the user asks an impossible coqide, we abort the configuration *)
+
+let set_ide ide msg = match ide, !Prefs.coqide with
+  | No, Some (Byte|Opt)
+  | Byte, Some Opt -> die (msg^":\n=> cannot build requested CoqIde")
+  | _ ->
+    printf "%s:\n=> %s CoqIde will be built.\n" msg (pr_ide ide);
+    raise (Ide ide)
+
+let lablgtkdir = ref ""
+
+(** Which CoqIde is possible ? Which one is requested ?
+    This function also sets the lablgtkdir reference in case of success. *)
+
+let check_coqide () =
+  if !Prefs.coqide = Some No then set_ide No "CoqIde manually disabled";
+  let dir, via = get_lablgtkdir () in
+  if dir = "" then set_ide No "LablGtk2 not found";
+  let found = sprintf "LablGtk2 found (%s)" via in
+  let test = sprintf "grep -q -w convert_with_fallback %S/glib.mli" dir in
+  if Sys.command test <> 0 then set_ide No (found^" but too old");
+  (* We're now sure to produce at least one kind of coqide *)
+  lablgtkdir := shorten_camllib dir;
+  if !Prefs.coqide = Some Byte then set_ide Byte (found^", bytecode requested");
+  if best_compiler<>"opt" then set_ide Byte (found^", but no native compiler");
+  if not (Sys.file_exists (dir/"gtkThread.cmx")) then
+    set_ide Byte (found^", but no native LablGtk2");
+  if not (Sys.file_exists (camllib/"threads"/"threads.cmxa")) then
+    set_ide Byte (found^", but no native threads");
+  set_ide Opt (found^", with native threads")
+
+let coqide =
+  try check_coqide ()
+  with Ide Opt -> "opt" | Ide Byte -> "byte" | Ide No -> "no"
+
+(** System-specific CoqIde flags *)
+
+let lablgtkincludes = ref ""
+let idearchflags = ref ""
+let idearchfile = ref ""
+let idearchdef = ref "X11"
+
+let coqide_flags () =
+  if !lablgtkdir <> "" then lablgtkincludes := sprintf "-I %S" !lablgtkdir;
+  match coqide, arch with
+    | "opt", "Darwin" when !Prefs.macintegration ->
+      let osxdir = tryrun "ocamlfind" ["query";"lablgtkosx"] in
+      if osxdir <> "" then begin
+        lablgtkincludes := sprintf "%s -I %S" !lablgtkincludes osxdir;
+        idearchflags := "lablgtkosx.cmxa";
+        idearchdef := "QUARTZ"
+      end
+    | "opt", "win32" ->
+      idearchfile := "ide/ide_win32_stubs.o";
+      idearchdef := "WIN32"
+    | _ -> ()
+
+let _ = coqide_flags ()
+
+
+(** * strip command *)
+
+let strip =
+  if arch = "Darwin" then
+    if hasnatdynlink then "true" else "strip"
+  else
+    if !Prefs.profile || !Prefs.debug then "true" else "strip"
+
+
+(** * Documentation : do we have latex, hevea, ... *)
+
+let check_doc () =
+  let err s =
+    printf "%s was not found; documentation will not be available\n" s;
+    raise Not_found
+  in
+  try
+    if not !Prefs.withdoc then raise Not_found;
+    if not (program_in_path "latex") then err "latex";
+    if not (program_in_path "hevea") then err "hevea";
+    true
+  with Not_found -> false
+
+let withdoc = check_doc ()
+
+
+(** * Installation directories : bindir, libdir, mandir, docdir, etc *)
+
+let coqtop = Sys.getcwd ()
+
+let unix = os_type_cygwin || not arch_win32
+
+(** Variable name, description, ref in Prefs, default dir, prefix-relative *)
+
+let install = [
+  "BINDIR", "the Coq binaries", Prefs.bindir,
+    (if unix then "/usr/local/bin" else "C:/coq/bin"),
+    "/bin";
+  "COQLIBINSTALL", "the Coq library", Prefs.libdir,
+    (if unix then "/usr/local/lib/coq" else "C:/coq/lib"),
+    (if arch_win32 then "" else "/lib/coq");
+  "CONFIGDIR", "the Coqide configuration files", Prefs.configdir,
+    (if unix then "/etc/xdg/coq" else "C:/coq/config"),
+    (if arch_win32 then "/config" else "/etc/xdg/coq");
+  "DATADIR", "the Coqide data files", Prefs.datadir,
+    (if unix then "/usr/local/share/coq" else "C:/coq/share"),
+    "/share/coq";
+  "MANDIR", "the Coq man pages", Prefs.mandir,
+    (if unix then "/usr/local/share/man" else "C:/coq/man"),
+    "/share/man";
+  "DOCDIR", "the Coq documentation", Prefs.docdir,
+    (if unix then "/usr/local/share/doc/coq" else "C:/coq/doc"),
+    "/share/doc/coq";
+  "EMACSLIB", "the Coq Emacs mode", Prefs.emacslib,
+    (if unix then "/usr/local/share/emacs/site-lisp" else "C:/coq/emacs"),
+    (if arch_win32 then "/emacs" else "/share/emacs/site-lisp");
+  "COQDOCDIR", "the Coqdoc LaTeX files", Prefs.coqdocdir,
+    (if unix then "/usr/local/share/texmf/tex/latex/misc" else "C:/coq/latex"),
+    (if arch_win32 then "/latex" else "/share/emacs/site-lisp");
+ ]
+
+let do_one_instdir (var,msg,r,dflt,suff) =
+  let dir = match !r, !Prefs.prefix with
+    | Some d, _ -> d
+    | _, Some p -> p^suff
+    | _ ->
+      let () = printf "Where should I install %s [%s]? " msg dflt in
+      let line = read_line () in
+      if line = "" then dflt else line
+  in (var,msg,dir,dir<>dflt)
+
+let do_one_noinst (var,msg,_,_,_) =
+  if var="CONFIGDIR" || var="DATADIR" then (var,msg,coqtop^"/ide",true)
+  else (var,msg,"",false)
+
+let install_dirs =
+  let f = if !Prefs.local then do_one_noinst else do_one_instdir in
+  List.map f install
+
+let select var = List.find (fun (v,_,_,_) -> v=var) install_dirs
+
+let libdir = let (_,_,d,_) = select "COQLIBINSTALL" in d
+
+let docdir = let (_,_,d,_) = select "DOCDIR" in d
+
+let configdir =
+  let (_,_,d,b) = select "CONFIGDIR" in if b then Some d else None
+
+let datadir =
+  let (_,_,d,b) = select "DATADIR" in if b then Some d else None
+
+
+(** * OCaml runtime flags *)
+
+(** Determine if we enable -custom by default (Windows and MacOS) *)
+let custom_os = arch_win32 || arch = "Darwin"
+
+let build_loadpath =
+  ref "# you might want to set CAML_LD_LIBRARY_PATH by hand!"
+
+let config_runtime () =
+  match !Prefs.coqrunbyteflags with
+  | Some flags -> flags
+  | _ when !Prefs.custom || custom_os -> "-custom"
+  | _ when !Prefs.local ->
+    sprintf "-dllib -lcoqrun -dllpath '%s/kernel/byterun'" coqtop
+  | _ ->
+    let ld="CAML_LD_LIBRARY_PATH" in
+    build_loadpath := sprintf "export %s='%s/kernel/byterun':$%s" ld coqtop ld;
+    sprintf "-dllib -lcoqrun -dllpath '%s'" libdir
+
+let coqrunbyteflags = config_runtime ()
+
+let config_tools_runtime () =
+  match !Prefs.coqtoolsbyteflags with
+  | Some flags -> flags
+  | _ when !Prefs.custom || custom_os -> "-custom"
+  | _ -> ""
+
+let coqtoolsbyteflags = config_tools_runtime ()
+
+
+(** * Summary of the configuration *)
+
+let print_summary () =
+  let pr s = printf s in
+  pr "\n";
+  pr "  Architecture                      : %s\n" arch;
+  if operating_system <> "" then
+    pr "  Operating system                  : %s\n" operating_system;
+  pr "  Coq VM bytecode link flags        : %s\n" coqrunbyteflags;
+  pr "  Coq tools bytecode link flags     : %s\n" coqtoolsbyteflags;
+  pr "  OS dependent libraries            : %s\n" osdeplibs;
+  pr "  Objective-Caml/Camlp4 version     : %s\n" caml_version;
+  pr "  Objective-Caml/Camlp4 binaries in : %s\n" camlbin;
+  pr "  Objective-Caml library in         : %s\n" camllib;
+  pr "  Camlp4 library in                 : %s\n" camlp4lib;
+  if best_compiler = "opt" then
+    pr "  Native dynamic link support       : %B\n" hasnatdynlink;
+  if coqide <> "no" then
+    pr "  Lablgtk2 library in               : %s\n" !lablgtkdir;
+  if !idearchdef = "QUARTZ" then
+    pr "  Mac OS integration is on\n";
+  pr "  CoqIde                            : %s\n" coqide;
+  pr "  Documentation                     : %s\n"
+    (if withdoc then "All" else "None");
+  pr "  Web browser                       : %s\n" browser;
+  pr "  Coq web site                      : %s\n\n" !Prefs.coqwebsite;
+  if not !Prefs.nativecompiler then
+    pr "  Native compiler for conversion and normalization disabled\n\n";
+  if !Prefs.local then
+    pr "  Local build, no installation...\n"
+  else
+    (pr "  Paths for true installation:\n";
+     List.iter
+       (fun (_,msg,dir,_) -> pr "  - %s will be copied in %s\n" msg dir)
+       install_dirs);
+  pr "\n";
+  pr "If anything is wrong above, please restart './configure'.\n\n";
+  pr "*Warning* To compile the system for a new architecture\n";
+  pr "          don't forget to do a 'make clean' before './configure'.\n"
+
+let _ = print_summary ()
+
+
+(** * Build the dev/ocamldebug-coq file *)
+
+let write_dbg_wrapper f =
+  safe_remove f;
+  let o = open_out f in
+  let pr s = fprintf o s in
+  pr "#!/bin/sh\n\n";
+  pr "###### ocamldebug-coq : a wrapper around ocamldebug for Coq ######\n\n";
+  pr "# DO NOT EDIT THIS FILE: automatically generated by ../configure #\n\n";
+  pr "export COQTOP=%S\n" coqtop;
+  pr "OCAMLDEBUG=%S\n" (camlbin^"/ocamldebug");
+  pr "CAMLP4LIB=%S\n\n" camlp4lib;
+  pr ". $COQTOP/dev/ocamldebug-coq.run\n";
+  close_out o;
+  Unix.chmod f 0o555
+
+let _ = write_dbg_wrapper "dev/ocamldebug-coq"
+
+
+(** * Build the config/coq_config.ml file (+ link to myocamlbuild_config.ml) *)
+
+let write_configml f =
+  safe_remove f;
+  let o = open_out f in
+  let pr s = fprintf o s in
+  let pr_s = pr "let %s = %S\n" in
+  let pr_b = pr "let %s = %B\n" in
+  let pr_i = pr "let %s = %d\n" in
+  let pr_o s o = pr "let %s = %s\n" s
+    (match o with None -> "None" | Some d -> sprintf "Some %S" d)
+  in
+  pr "(* DO NOT EDIT THIS FILE: automatically generated by ../configure *)\n\n";
+  pr_b "local" !Prefs.local;
+  pr_s "coqrunbyteflags" coqrunbyteflags;
+  pr_o "coqlib" (if !Prefs.local then None else Some libdir);
+  pr_o "configdir" configdir;
+  pr_o "datadir" datadir;
+  pr_s "docdir" docdir;
+  pr_s "ocaml" camlexec.top;
+  pr_s "ocamlc" camlexec.byte;
+  pr_s "ocamlopt" camlexec.opt;
+  pr_s "ocamlmklib" camlexec.mklib;
+  pr_s "ocamldep" camlexec.dep;
+  pr_s "ocamldoc" camlexec.doc;
+  pr_s "ocamlyacc" camlexec.yacc;
+  pr_s "ocamllex" camlexec.lex;
+  pr_s "camlbin" camlbin;
+  pr_s "camllib" camllib;
+  pr_s "camlp4" camlp4;
+  pr_s "camlp4o" camlexec.p4;
+  pr_s "camlp4bin" camlp4bin;
+  pr_s "camlp4lib" camlp4lib;
+  pr_s "camlp4compat" camlp4compat;
+  pr_s "cflags" cflags;
+  pr_s "best" best_compiler;
+  pr_s "osdeplibs" osdeplibs;
+  pr_s "version" coq_version;
+  pr_s "caml_version" caml_version;
+  pr_s "date" short_date;
+  pr_s "compile_date" full_date;
+  pr_s "arch" arch;
+  pr_b "arch_is_win32" arch_win32;
+  pr_s "exec_extension" exe;
+  pr_s "coqideincl" !lablgtkincludes;
+  pr_s "has_coqide" coqide;
+  pr "let gtk_platform = `%s\n" !idearchdef;
+  pr_b "has_natdynlink" hasnatdynlink;
+  pr_s "natdynlinkflag" natdynlinkflag;
+  pr_i "vo_magic_number" vo_magic;
+  pr_i "state_magic_number" state_magic;
+  pr "let with_geoproof = ref %B\n" !Prefs.geoproof;
+  pr_s "browser" browser;
+  pr_s "wwwcoq" !Prefs.coqwebsite;
+  pr_s "wwwrefman" (!Prefs.coqwebsite ^ "distrib/" ^ coq_version ^ "/refman/");
+  pr_s "wwwstdlib" (!Prefs.coqwebsite ^ "distrib/" ^ coq_version ^ "/stdlib/");
+  pr_s "localwwwrefman"  ("file:/" ^ docdir ^ "/html/refman");
+  pr_b "no_native_compiler" (not !Prefs.nativecompiler);
+  pr "\nlet plugins_dirs = [\n";
+  let plugins = Sys.readdir "plugins" in
+  Array.sort compare plugins;
+  Array.iter
+    (fun f ->
+      let f' = "plugins/"^f in
+      if Sys.is_directory f' && f.[0] <> '.' then pr "  %S;\n" f')
+    plugins;
+  pr "]\n";
+  close_out o;
+  Unix.chmod f 0o444
+
+let write_configml_my f f' =
+  write_configml f;
+  if os_type_win32 then
+    write_configml f'
+  else
+    (safe_remove f'; Unix.symlink f f')
+
+let _ = write_configml_my "config/coq_config.ml" "myocamlbuild_config.ml"
+
+
+(** * Build the config/Makefile file *)
+
+let write_makefile f =
+  safe_remove f;
+  let o = open_out f in
+  let pr s = fprintf o s in
+  pr "###### config/Makefile : Configuration file for Coq ##############\n";
+  pr "#                                                                #\n";
+  pr "# This file is generated by the script \"configure\"               #\n";
+  pr "# DO NOT EDIT IT !! DO NOT EDIT IT !! DO NOT EDIT IT !!          #\n";
+  pr "# If something is wrong below, then rerun the script \"configure\" #\n";
+  pr "# with the good options (see the file INSTALL).                  #\n";
+  pr "#                                                                #\n";
+  pr "##################################################################\n\n";
+  pr "#Variable used to detect whether ./configure has run successfully.\n";
+  pr "COQ_CONFIGURED=yes\n\n";
+  pr "# Local use (no installation)\n";
+  pr "LOCAL=%B\n\n" !Prefs.local;
+  pr "# Bytecode link flags for VM (\"-custom\" or \"-dllib -lcoqrun\")\n";
+  pr "COQRUNBYTEFLAGS=%s\n" coqrunbyteflags;
+  pr "COQTOOLSBYTEFLAGS=%s\n" coqtoolsbyteflags;
+  pr "%s\n\n" !build_loadpath;
+  pr "# Paths for true installation\n";
+  List.iter (fun (v,msg,_,_) -> pr "# %s: path for %s\n" v msg) install_dirs;
+  List.iter (fun (v,_,dir,_) -> pr "%s=%S\n" v dir) install_dirs;
+  pr "\n# Coq version\n";
+  pr "VERSION=%s\n\n" coq_version;
+  pr "# Objective-Caml compile command\n";
+  pr "OCAML=%S\n" camlexec.top;
+  pr "OCAMLC=%S\n" camlexec.byte;
+  pr "OCAMLMKLIB=%S\n" camlexec.mklib;
+  pr "OCAMLOPT=%S\n" camlexec.opt;
+  pr "OCAMLDEP=%S\n" camlexec.dep;
+  pr "OCAMLDOC=%S\n" camlexec.doc;
+  pr "OCAMLLEX=%S\n" camlexec.lex;
+  pr "OCAMLYACC=%S\n\n" camlexec.yacc;
+  pr "# The best compiler: native (=opt) or bytecode (=byte)\n";
+  pr "BEST=%s\n\n" best_compiler;
+  pr "# Ocaml version number\n";
+  pr "CAMLVERSION=%s\n\n" camltag;
+  pr "# Ocaml libraries\n";
+  pr "CAMLLIB=%S\n\n" camllib;
+  pr "# Ocaml .h directory\n";
+  pr "CAMLHLIB=%S\n\n" camllib;
+  pr "# Caml link command and Caml make top command\n";
+  pr "CAMLLINK=%S\n" camlexec.byte;
+  pr "CAMLOPTLINK=%S\n\n" camlexec.opt;
+  pr "# Caml flags\n";
+  pr "CAMLFLAGS=-rectypes %s\n" coq_annotate_flag;
+  pr "TYPEREX=%s\n\n" coq_typerex_wrapper;
+  pr "# User compilation flag\n";
+  pr "USERFLAGS=\n\n";
+  pr "# Flags for GCC\n";
+  pr "CFLAGS=%s\n\n" cflags;
+  pr "# Compilation debug flags\n";
+  pr "CAMLDEBUG=%s\n" coq_debug_flag;
+  pr "CAMLDEBUGOPT=%s\n\n" coq_debug_flag_opt;
+  pr "# Compilation profile flag\n";
+  pr "CAMLTIMEPROF=%s\n\n" coq_profile_flag;
+  pr "# Camlp4 : flavor, binaries, libraries ...\n";
+  pr "# NB : avoid using CAMLP4LIB (conflict under Windows)\n";
+  pr "CAMLP4=%s\n" camlp4;
+  pr "CAMLP4O=%S\n" camlexec.p4;
+  pr "CAMLP4COMPAT=%s\n" camlp4compat;
+  pr "MYCAMLP4LIB=%S\n\n" camlp4lib;
+  pr "# Your architecture\n";
+  pr "# Can be obtain by UNIX command arch\n";
+  pr "ARCH=%s\n" arch;
+  pr "HASNATDYNLINK=%s\n\n" natdynlinkflag;
+  pr "# Supplementary libs for some systems, currently:\n";
+  pr "#  . Sun Solaris: -cclib -lunix -cclib -lnsl -cclib -lsocket\n";
+  pr "#  . others     : -cclib -lunix\n";
+  pr "OSDEPLIBS=%s\n\n" osdeplibs;
+  pr "# executable files extension, currently:\n";
+  pr "#  Unix systems:\n";
+  pr "#  Win32 systems : .exe\n";
+  pr "EXE=%s\n" exe;
+  pr "DLLEXT=%s\n\n" dll;
+  pr "# the command MKDIR (try to use mkdirhier if you have problems)\n";
+  pr "MKDIR=mkdir -p\n\n";
+  pr "#the command STRIP\n";
+  pr "# Unix systems and profiling: true\n";
+  pr "# Unix systems and no profiling: strip\n";
+  pr "STRIP=%s\n\n" strip;
+  pr "# LablGTK\n";
+  pr "COQIDEINCLUDES=%s\n\n" !lablgtkincludes;
+  pr "# CoqIde (no/byte/opt)\n";
+  pr "HASCOQIDE=%s\n" coqide;
+  pr "IDEOPTFLAGS=%s\n" !idearchflags;
+  pr "IDEOPTDEPS=%s\n" !idearchfile;
+  pr "IDEOPTINT=%s\n\n" !idearchdef;
+  pr "# Defining REVISION\n";
+  pr "CHECKEDOUT=%s\n\n" vcs;
+  pr "# Option to control compilation and installation of the documentation\n";
+  pr "WITHDOC=%s\n" (if withdoc then "all" else "no");
+  close_out o;
+  Unix.chmod f 0o444
+
+let _ = write_makefile "config/Makefile"
diff --git a/dev/ocamldebug-coq.template b/dev/ocamldebug-coq.run
index ffe4c6b40..aab03f34d 100644
--- a/dev/ocamldebug-coq.template
+++ b/dev/ocamldebug-coq.run
@@ -1,11 +1,16 @@
 #!/bin/sh
 
-# wrap around ocamldebug for Coq
+# Wrapper around ocamldebug for Coq
 
-export COQTOP=COQTOPDIRECTORY
-CAMLBIN=CAMLBINDIRECTORY
-CAMLP4LIB=CAMLP4LIBDIRECTORY
-OCAMLDEBUG=$CAMLBIN/ocamldebug
+# This file is to be launched via the generated script ocamldebug-coq,
+# which will set the env variables $OCAMLDEBUG, $CAMLP4LIB, $COQTOP
+# Anyway, just in case someone tries to use this script directly,
+# here are some reasonable default values
+
+[ -z "$OCAMLDEBUG" ] && OCAMLDEBUG=ocamldebug
+[ -z "$CAMLP4LIB" ] && CAMLP4LIB=+camlp5
+[ -z "$COQTOP" -a -d "$PWD/kernel" ] && COQTOP=$PWD
+[ -z "$COQTOP" -a -d "$PWD/../kernel" ] && COQTOP=`dirname $PWD`
 
 exec $OCAMLDEBUG \
 	-I $CAMLP4LIB \
@@ -26,4 +31,4 @@ exec $OCAMLDEBUG \
         -I $COQTOP/plugins/subtac     -I $COQTOP/plugins/syntax \
         -I $COQTOP/plugins/xml \
         -I $COQTOP/ide \
-	$*
+	"$@"