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

2 files changed, 35 insertions, 31 deletions

diff --git a/tools/coqdoc/cdglobals.ml b/tools/coqdoc/cdglobals.ml
index a412e6865..6b8a3f5e7 100644
--- a/tools/coqdoc/cdglobals.ml
+++ b/tools/coqdoc/cdglobals.ml
@@ -49,21 +49,40 @@ type glob_source_t =
 
 let glob_source = ref DotGlob
 
+(*s Manipulations of paths and path aliases *)
+
+let normalize_path p =
+  (* We use the Unix subsystem to normalize a physical path (relative
+     or absolute) and get rid of symbolic links, relative links (like
+     ./ or ../ in the middle of the path; it's tricky but it
+     works... *)
+  (* Rq: Sys.getcwd () returns paths without '/' at the end *)
+  let orig = Sys.getcwd () in
+  Sys.chdir p;
+  let res = Sys.getcwd () in
+  Sys.chdir orig;
+  res
+
+let normalize_filename f =
+  let basename = Filename.basename f in
+  let dirname = Filename.dirname f in
+  normalize_path dirname, basename
+
 (** A weaker analog of the function in Envars *)
 
 let guess_coqlib () =
   let file = "states/initial.coq" in
-  if Sys.file_exists (Filename.concat Coq_config.coqlib file)
-  then Coq_config.coqlib
-  else
-    let coqbin = Filename.dirname Sys.executable_name in
-    let prefix = Filename.dirname coqbin in
-    let rpath = if Coq_config.local then [] else
-	(if Coq_config.arch = "win32" then ["lib"] else ["lib";"coq"]) in
-    let coqlib = List.fold_left Filename.concat prefix rpath in
-    if Sys.file_exists (Filename.concat coqlib file) then coqlib
-    else
-      Coq_config.coqlib
+  match Coq_config.coqlib with
+    | Some coqlib when Sys.file_exists (Filename.concat coqlib file) ->
+      coqlib
+    | Some _ | None ->
+      let coqbin = normalize_path (Filename.dirname Sys.executable_name) in
+      let prefix = Filename.dirname coqbin in
+      let rpath = if Coq_config.local then [] else
+	  (if Coq_config.arch = "win32" then ["lib"] else ["lib";"coq"]) in
+      let coqlib = List.fold_left Filename.concat prefix rpath in
+      if Sys.file_exists (Filename.concat coqlib file) then coqlib
+      else prefix
 
 let header_trailer = ref true
 let header_file = ref ""
diff --git a/tools/coqdoc/main.ml b/tools/coqdoc/main.ml
index 98204a856..7dc2c3bf2 100644
--- a/tools/coqdoc/main.ml
+++ b/tools/coqdoc/main.ml
@@ -106,25 +106,6 @@ let check_if_file_exists f =
   end
 
 
-(*s Manipulations of paths and path aliases *)
-
-let normalize_path p =
-  (* We use the Unix subsystem to normalize a physical path (relative
-     or absolute) and get rid of symbolic links, relative links (like
-     ./ or ../ in the middle of the path; it's tricky but it
-     works... *)
-  (* Rq: Sys.getcwd () returns paths without '/' at the end *)
-  let orig = Sys.getcwd () in
-  Sys.chdir p;
-  let res = Sys.getcwd () in
-  Sys.chdir orig;
-  res
-
-let normalize_filename f =
-  let basename = Filename.basename f in
-  let dirname = Filename.dirname f in
-  normalize_path dirname, basename
-
 (* [paths] maps a physical path to a name *)
 let paths = ref []
 
@@ -354,7 +335,11 @@ let parse () =
     | ("--coqlib" | "-coqlib") :: [] ->
 	usage ()
     | ("--boot" | "-boot") :: rem ->
-	Cdglobals.coqlib_path := Coq_config.coqsrc; parse_rec rem
+	Cdglobals.coqlib_path := normalize_path (
+          Filename.concat
+            (Filename.dirname Sys.executable_name)
+            Filename.parent_dir_name
+        ); parse_rec rem
     | ("--coqlib_path" | "-coqlib_path") :: d :: rem ->
 	Cdglobals.coqlib_path := d; parse_rec rem
     | ("--coqlib_path" | "-coqlib_path") :: [] ->