In Coq_config: get rid of coqsrc and make coqlib optional

I assume that once Coq is installed in non-local mode and run from its
installed path, sources are no longer available. The coqsrc variable
doesn't make any sense, then, and its intended value can always be
inferred from Sys.executable_name. Moving it to Envars.coqroot.

Make coqlib optional. Currently, it is set to None only in -local mode
or with ocamlbuild. When set to None, -local layout is assumed
(binaries in ./bin, library in .). The behaviour should not be changed
when an explicit coqlib has been given to ./configure.

This commit should make it possible to run a Coq compiled with -local
from anywhere (no hard-coded absolute path embedded in the
executables, intermediary step to bug #2565). It WILL BREAK settings
re-using source trees after installation in non-local mode (are there
actual use cases for that?).

Hard-coded absolute paths still remain:
 - in the build system, so the need to re-run ./configure after moving
   the source tree is still expected for now;
 - in coqrunbyteflags, I think we are limited by ocaml itself;
 - docdir.
All absolute paths should be removed, ultimately.

As a side-effect, simplify computing of Envars.coqbin. I don't see any
good reason to keep it as a function.

Disclaimers:
 - initialization of Sys.executable_name is not consistent across all
   architectures; relying so much on it might trigger bugs. I'm pretty
   sure something will explode if one adds arbitrary symlinks on top of
   that;
 - ocamlbuild stuff not tested.

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

1 files changed, 8 insertions, 2 deletions

diff --git a/configure b/configure
index 0a7619740..f771c5e30 100755
--- a/configure
+++ b/configure
@@ -757,6 +757,7 @@ esac
 case $libdir_spec/$prefix_spec/$local in
     yes/*/*) LIBDIR=$libdir;;
     */yes/*)
+        libdir_spec=yes
         case $ARCH in
           win32) LIBDIR=$prefix ;;
           *)  LIBDIR=$prefix/lib/coq ;;
@@ -764,12 +765,18 @@ case $libdir_spec/$prefix_spec/$local in
     */*/true) LIBDIR=$COQTOP ;;
     *)  printf "Where should I install the Coq library [$libdir_def]? "
         read LIBDIR
+        libdir_spec=yes
 	case $LIBDIR in
 	    "") LIBDIR=$libdir_def;;
 	    *) true;;
 	esac;;
 esac
 
+case $libdir_spec in
+    yes) LIBDIR_OPTION="Some \"$LIBDIR\"";;
+    *) LIBDIR_OPTION="None";;
+esac
+
 case $mandir_spec/$prefix_spec/$local in
     yes/*/*) MANDIR=$mandir;;
     */yes/*) MANDIR=$prefix/man ;;
@@ -1001,8 +1008,7 @@ cat << END_OF_COQ_CONFIG > $mlconfig_file
 
 let local = $local
 let coqrunbyteflags = "$COQRUNBYTEFLAGS"
-let coqlib = "$LIBDIR"
-let coqsrc = "$COQSRC"
+let coqlib = $LIBDIR_OPTION
 let docdir = "$DOCDIR"
 let ocaml = "$ocamlexec"
 let ocamlc = "$bytecamlc"