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, 17 insertions, 11 deletions

diff --git a/lib/envars.ml b/lib/envars.ml
index 4f33ccb7f..0991fb7a1 100644
--- a/lib/envars.ml
+++ b/lib/envars.ml
@@ -9,34 +9,40 @@
 (* This file gathers environment variables needed by Coq to run (such
    as coqlib) *)
 
-let coqbin () =
-  if !Flags.boot || Coq_config.local
-  then Filename.concat Coq_config.coqsrc "bin"
-  else System.canonical_path_name (Filename.dirname Sys.executable_name)
+let coqbin =
+  System.canonical_path_name (Filename.dirname Sys.executable_name)
+
+(* The following only makes sense when executables are running from
+   source tree (e.g. during build or in local mode). *)
+let coqroot = Filename.dirname coqbin
 
 (* On win32, we add coqbin to the PATH at launch-time (this used to be
    done in a .bat script). *)
 
 let _ =
   if Coq_config.arch = "win32" then
-    Unix.putenv "PATH" (coqbin() ^ ";" ^ System.getenv_else "PATH" "")
+    Unix.putenv "PATH" (coqbin ^ ";" ^ System.getenv_else "PATH" "")
 
 let reldir instdir testfile oth =
-  let prefix = Filename.dirname (coqbin ()) in
   let rpath = if Coq_config.local then [] else instdir in
-  let out = List.fold_left Filename.concat prefix rpath in
+  let out = List.fold_left Filename.concat coqroot rpath in
   if Sys.file_exists (Filename.concat out testfile) then out else oth ()
 
 let guess_coqlib () =
   let file = "states/initial.coq" in
     reldir (if Coq_config.arch = "win32" then ["lib"] else ["lib";"coq"]) file
-      (fun () -> if Sys.file_exists (Filename.concat Coq_config.coqlib file)
-                 then Coq_config.coqlib
-                 else Util.error "cannot guess a path for Coq libraries; please use -coqlib option")
+      (fun () ->
+        let coqlib = match Coq_config.coqlib with
+          | Some coqlib -> coqlib
+          | None -> coqroot
+        in
+        if Sys.file_exists (Filename.concat coqlib file)
+        then coqlib
+        else Util.error "cannot guess a path for Coq libraries; please use -coqlib option")
 
 let coqlib () =
   if !Flags.coqlib_spec then !Flags.coqlib else
-    (if !Flags.boot then Coq_config.coqsrc else guess_coqlib ())
+    (if !Flags.boot then coqroot else guess_coqlib ())
 
 let docdir () =
   reldir (if Coq_config.arch = "win32" then ["doc"] else ["share";"doc";"coq"]) "html" (fun () -> Coq_config.docdir)