Add -coqtoolsbyteflags and -custom to ./configure...

...and use -custom by default on Windows and MacOS (backport r11895)

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

5 files changed, 47 insertions, 17 deletions

diff --git a/CHANGES b/CHANGES
index 1ccda6344..d1a8e41bd 100644
--- a/CHANGES
+++ b/CHANGES
@@ -491,9 +491,10 @@ Miscellaneous
   "Test Printing Let for ref" and "Test Printing If for ref".
 - An overhauled build system (new Makefiles); see dev/doc/build-system.txt.
 - Add -browser option to configure script.
-- Build a shared library for the C part of Coq, and use it by default.
-  Bytecode executables are now pure. The behaviour is configurable with
-  the -coqrunbyteflags configure option.
+- Build a shared library for the C part of Coq, and use it by default on
+  non-(Windows or MacOS) systems. Bytecode executables are now pure. The
+  behaviour is configurable with -coqrunbyteflags, -coqtoolsbyteflags and
+  -custom configure options.
 - Complexity tests can be skipped by setting the environment variable
   COQTEST_SKIPCOMPLEXITY.
 
diff --git a/INSTALL b/INSTALL
index b9b7a6194..00feb1681 100644
--- a/INSTALL
+++ b/INSTALL
@@ -344,6 +344,6 @@ DYNAMICALLY LOADED LIBRARIES FOR BYTECODE EXECUTABLES.
        where <path> is the directory where the dllcoqrun.so is installed;
      - (not recommended) compile bytecode executables with a custom OCaml
        runtime by using:
-         ./configure -coqrunbyteflags -custom ...
+         ./configure -custom ...
        be aware that stripping executables generated this way, or performing
        other executable-specific operations, will make them useless.
diff --git a/Makefile.build b/Makefile.build
index a7442c457..c95c053df 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -200,7 +200,7 @@ $(CHICKENOPT): checker/check.cmxa checker/main.ml
 
 $(CHICKENBYTE): checker/check.cma checker/main.ml
 	$(SHOW)'OCAMLC -o $@'
-	$(HIDE)$(OCAMLC) $(CHKBYTEFLAGS) -o $@ str.cma unix.cma gramlib.cma $^
+	$(HIDE)$(OCAMLC) $(CHKBYTEFLAGS) $(COQTOOLSBYTEFLAGS) -o $@ str.cma unix.cma gramlib.cma $^
 
 $(CHICKEN): $(ORDER_ONLY_SEP) $(BESTCHICKEN)
 	cd bin && ln -sf coqchk.$(BEST)$(EXE) coqchk$(EXE)
@@ -593,27 +593,27 @@ tools:: $(TOOLS) $(DEBUGPRINTERS)
 
 $(COQDEP): $(COQDEPCMO)
 	$(SHOW)'OCAMLC -o $@'
-	$(HIDE)$(OCAMLC) $(BYTEFLAGS) -o $@ str.cma unix.cma gramlib.cma $^ $(OSDEPLIBS)
+	$(HIDE)$(OCAMLC) $(BYTEFLAGS) $(COQTOOLSBYTEFLAGS) -o $@ str.cma unix.cma gramlib.cma $^ $(OSDEPLIBS)
 
 $(GALLINA): $(GALLINACMO)
 	$(SHOW)'OCAMLC -o $@'
-	$(HIDE)$(OCAMLC) $(BYTEFLAGS) -o $@ $^
+	$(HIDE)$(OCAMLC) $(BYTEFLAGS) $(COQTOOLSBYTEFLAGS) -o $@ $^
 
 $(COQMAKEFILE): config/coq_config.cmo tools/coq_makefile.cmo
 	$(SHOW)'OCAMLC -o $@'
-	$(HIDE)$(OCAMLC) $(BYTEFLAGS) -o $@ str.cma $^
+	$(HIDE)$(OCAMLC) $(BYTEFLAGS) $(COQTOOLSBYTEFLAGS) -o $@ str.cma $^
 
 $(COQTEX): tools/coq-tex.cmo
 	$(SHOW)'OCAMLC -o $@'
-	$(HIDE)$(OCAMLC) $(BYTEFLAGS) -o $@ str.cma $^
+	$(HIDE)$(OCAMLC) $(BYTEFLAGS) $(COQTOOLSBYTEFLAGS) -o $@ str.cma $^
 
 $(COQWC): tools/coqwc.cmo
 	$(SHOW)'OCAMLC -o $@'
-	$(HIDE)$(OCAMLC) $(BYTEFLAGS) -o $@ $^
+	$(HIDE)$(OCAMLC) $(BYTEFLAGS) $(COQTOOLSBYTEFLAGS) -o $@ $^
 
 $(COQDOC): $(COQDOCCMO)
 	$(SHOW)'OCAMLC -o $@'
-	$(HIDE)$(OCAMLC) $(BYTEFLAGS) -o $@ str.cma unix.cma $^
+	$(HIDE)$(OCAMLC) $(BYTEFLAGS) $(COQTOOLSBYTEFLAGS) -o $@ str.cma unix.cma $^
 
 ###########################################################################
 # Installation
diff --git a/config/Makefile.template b/config/Makefile.template
index 35e2a2d7d..6f9fac3c1 100644
--- a/config/Makefile.template
+++ b/config/Makefile.template
@@ -23,6 +23,7 @@ LOCAL=LOCALINSTALLATION
 
 # Bytecode link flags for VM ("-custom" or "-dllib -lcoqrun")
 COQRUNBYTEFLAGS=XCOQRUNBYTEFLAGS
+COQTOOLSBYTEFLAGS=XCOQTOOLSBYTEFLAGS
 BUILDLDPATH=
 
 # Paths for true installation
diff --git a/configure b/configure
index ec6eab64b..037e9f73b 100755
--- a/configure
+++ b/configure
@@ -36,7 +36,11 @@ usage () {
     echo "-local"
     printf "\tSet installation directory to the current source tree\n"
     echo "-coqrunbyteflags"
-    printf "\tSet link flags for VM-dependent bytecode\n"
+    printf "\tSet link flags for VM-dependent bytecode (coqtop)\n"
+    echo "-coqtoolsbyteflags"
+    printf "\tSet link flags for VM-independant bytecode (coqdep, coqdoc, ...)\n"
+    echo "-custom"
+    printf "\tGenerate all bytecode executables with -custom (not recommended)\n"
     echo "-src"
     printf "\tSpecifies the source directory\n"
     echo "-bindir"
@@ -114,6 +118,8 @@ ranlib_exec=ranlib
 
 local=false
 coqrunbyteflags_spec=no
+coqtoolsbyteflags_spec=no
+custom_spec=no
 src_spec=no
 prefix_spec=no
 bindir_spec=no
@@ -150,6 +156,11 @@ while : ; do
     -coqrunbyteflags|--coqrunbyteflags) coqrunbyteflags_spec=yes
                                         coqrunbyteflags="$2"
                                         shift;;
+    -coqtoolsbyteflags|--coqtoolsbyteflags) coqtoolsbyteflags_spec=yes
+                                            coqtoolsbyteflags="$2"
+                                            shift;;
+    -custom|--custom) custom_spec=yes
+                      shift;;
     -src|--src) src_spec=yes
                 COQSRC="$2"
 	        shift;;
@@ -780,12 +791,25 @@ case $coqdocdir_spec/$prefix_spec/$local in
 	esac;;
 esac
 
+# Determine if we enable -custom by default (Windows and MacOS)
+CUSTOM_OS=no
+if [ "$ARCH" = "win32" ] || [ "`uname -s`" = "Darwin" ]; then
+    CUSTOM_OS=yes
+fi
+
 BUILDLDPATH="# you might want to set CAML_LD_LIBRARY_PATH by hand!"
-case $coqrunbyteflags_spec/$local in
-    yes/*) COQRUNBYTEFLAGS="$coqrunbyteflags";;
-    */true) COQRUNBYTEFLAGS="-dllib -lcoqrun -dllpath $COQTOP/kernel/byterun";;
-    *) COQRUNBYTEFLAGS="-dllib -lcoqrun -dllpath $LIBDIR"
-       BUILDLDPATH="export CAML_LD_LIBRARY_PATH=$COQTOP/kernel/byterun";;
+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";;
+esac
+case $coqtoolsbyteflags_spec/$custom_spec/$CUSTOM_OS in
+    yes/*/*) COQTOOLSBYTEFLAGS="$coqtoolsbyteflags";;
+    */yes/*|*/*/yes) COQTOOLSBYTEFLAGS="-custom";;
+    *) COQTOOLSBYTEFLAGS="";;
 esac
 
 # case $emacs_spec in
@@ -809,6 +833,7 @@ 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"
@@ -877,6 +902,7 @@ case $ARCH in
 	ESCCAMLP4LIB=`echo $CAMLP4LIB |sed -e 's|\\\|\\\\\\\|g'`
 	ESCLABLGTKINCLUDES=`echo $LABLGTKINCLUDES |sed -e 's|\\\|\\\\\\\|g'`
 	ESCCOQRUNBYTEFLAGS=`echo $COQRUNBYTEFLAGS |sed -e 's|\\\|\\\\\\\|g'`
+	ESCCOQTOOLSBYTEFLAGS=`echo $COQTOOLSBYTEFLAGS |sed -e 's|\\\|\\\\\\\|g'`
 	ESCBUILDLDPATH=`echo $BUILDLDPATH |sed -e 's|\\\|\\\\\\\|g'`
 ;;
     *)
@@ -895,6 +921,7 @@ case $ARCH in
    	ESCCAMLP4LIB="$CAMLP4LIB"
 	ESCLABLGTKINCLUDES="$LABLGTKINCLUDES"
 	ESCCOQRUNBYTEFLAGS="$COQRUNBYTEFLAGS"
+	ESCCOQTOOLSBYTEFLAGS="$COQTOOLSBYTEFLAGS"
 	ESCBUILDLDPATH="$BUILDLDPATH"
 	;;
 esac
@@ -954,6 +981,7 @@ rm -f "$COQSRC/config/Makefile"
 
 sed -e "s|LOCALINSTALLATION|$local|" \
     -e "s|XCOQRUNBYTEFLAGS|$ESCCOQRUNBYTEFLAGS|" \
+    -e "s|XCOQTOOLSBYTEFLAGS|$ESCCOQTOOLSBYTEFLAGS|" \
     -e "s|COQSRCDIRECTORY|$COQSRC|" \
     -e "s|COQVERSION|$VERSION|" \
     -e "s|BINDIRDIRECTORY|$ESCBINDIR|" \