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

13 files changed, 86 insertions, 58 deletions

diff --git a/config/coq_config.mli b/config/coq_config.mli
index 5e393e320..4ad8dc58f 100644
--- a/config/coq_config.mli
+++ b/config/coq_config.mli
@@ -8,8 +8,7 @@
 
 val local : bool        (* local use (no installation) *)
 
-val coqlib : string     (* where the std library is installed *)
-val coqsrc : string     (* where are the sources *)
+val coqlib : string option (* where the std library is installed *)
 val docdir : string     (* where the doc is installed *)
 
 val ocaml : string      (* names of ocaml binaries *)
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"
diff --git a/ide/coq.ml b/ide/coq.ml
index a5b2d38ab..f635ad407 100644
--- a/ide/coq.ml
+++ b/ide/coq.ml
@@ -16,7 +16,12 @@ let get_version_date () =
     then Coq_config.date
     else "<date not printable>" in
   try
-    let ch = open_in (Coq_config.coqsrc^"/revision") in
+    (* the following makes sense only when running with local layout *)
+    let coqroot = Filename.concat
+      (Filename.dirname Sys.executable_name)
+      Filename.parent_dir_name
+    in
+    let ch = open_in (Filename.concat coqroot "revision") in
     let ver = input_line ch in
     let rev = input_line ch in
     (ver,rev)
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)
diff --git a/lib/envars.mli b/lib/envars.mli
index c8a372906..3f8ac5ecc 100644
--- a/lib/envars.mli
+++ b/lib/envars.mli
@@ -11,7 +11,8 @@
 
 val coqlib : unit -> string
 val docdir : unit -> string
-val coqbin : unit -> string
+val coqbin : string
+val coqroot : string
 (* coqpath is stored in reverse order, since that is the order it
  * gets added to the searc path *)
 val coqpath : unit -> string list
diff --git a/lib/flags.ml b/lib/flags.ml
index 9b19efea7..470cf81f1 100644
--- a/lib/flags.ml
+++ b/lib/flags.ml
@@ -115,9 +115,21 @@ let is_standard_doc_url url =
   url = Coq_config.wwwrefman ||
   url = wwwcompatprefix ^ String.sub Coq_config.wwwrefman n (n'-n)
 
+(* same as in System, but copied here because of dependencies *)
+let canonical_path_name p =
+  let current = Sys.getcwd () in
+  Sys.chdir p;
+  let result = Sys.getcwd () in
+  Sys.chdir current;
+  result
+
 (* Options for changing coqlib *)
 let coqlib_spec = ref false
-let coqlib = ref Coq_config.coqlib
+let coqlib = ref (
+  (* same as Envars.coqroot, but copied here because of dependencies *)
+  Filename.dirname
+    (canonical_path_name (Filename.dirname Sys.executable_name))
+)
 
 (* Options for changing camlbin (used by coqmktop) *)
 let camlbin_spec = ref false
diff --git a/myocamlbuild.ml b/myocamlbuild.ml
index 9f3dca6ac..6ffd3e2a5 100644
--- a/myocamlbuild.ml
+++ b/myocamlbuild.ml
@@ -92,7 +92,6 @@ let flag_dynlink = if hasdynlink then A"-DHasDynlink" else N
 let dep_dynlink = if hasdynlink then N else Sh"-natdynlink no"
 let lablgtkincl = Sh Coq_config.coqideincl
 let local = Coq_config.local
-let coqsrc = Coq_config.coqsrc
 let cflags = S[A"-ccopt";A Coq_config.cflags]
 
 (** Do we want to inspect .ml generated from .ml4 ? *)
@@ -261,10 +260,8 @@ let extra_rules () = begin
        if w32 then cp "config/coq_config.ml" "coq_config.ml" else
        let lines = read_file "config/coq_config.ml" in
        let lines = List.map (fun s -> s^"\n") lines in
-       let srcbuild = Filename.concat coqsrc !_build in
        let line0 = "\n(* Adapted variables for ocamlbuild *)\n" in
-       let line1 = "let coqsrc = \""^srcbuild^"\"\n" in
-       let line2 = "let coqlib = \""^srcbuild^"\"\n" in
+       let line2 = "let coqlib = None\n" in
        (* TODO : line3 isn't completely accurate with respect to ./configure:
 	  the case of -local -coqrunbyteflags foo isn't supported *)
        let line3 =
diff --git a/plugins/xml/xmlcommand.ml b/plugins/xml/xmlcommand.ml
index 78048c8ee..1037bbf08 100644
--- a/plugins/xml/xmlcommand.ml
+++ b/plugins/xml/xmlcommand.ml
@@ -652,7 +652,7 @@ let _ =
        end ;
        Option.iter
 	(fun fn ->
-	  let coqdoc = Filename.concat (Envars.coqbin ()) ("coqdoc" ^ Coq_config.exec_extension) in
+	  let coqdoc = Filename.concat Envars.coqbin ("coqdoc" ^ Coq_config.exec_extension) in
 	  let options = " --html -s --body-only --no-index --latin1 --raw-comments" in
           let command cmd =
            if Sys.command cmd <> 0 then
diff --git a/scripts/coqc.ml b/scripts/coqc.ml
index b1e91cb30..688f7c32a 100644
--- a/scripts/coqc.ml
+++ b/scripts/coqc.ml
@@ -192,7 +192,7 @@ let main () =
     end;
     let coqtopname =
       if !image <> "" then !image
-      else Filename.concat (Envars.coqbin ()) (!binary ^ Coq_config.exec_extension)
+      else Filename.concat Envars.coqbin (!binary ^ Coq_config.exec_extension)
     in
       (*  List.iter (compile coqtopname args) cfiles*)
       Unix.handle_unix_error (compile coqtopname args) cfiles
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") :: [] ->
diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml
index 977b8f4c7..e91cf3353 100644
--- a/toplevel/coqinit.ml
+++ b/toplevel/coqinit.ml
@@ -121,9 +121,8 @@ let init_library_roots () =
 (* Initialises the Ocaml toplevel before launching it, so that it can
    find the "include" file in the *source* directory *)
 let init_ocaml_path () =
-  let coqsrc = Coq_config.coqsrc in
   let add_subdir dl =
-    Mltop.add_ml_dir (List.fold_left (/) coqsrc dl)
+    Mltop.add_ml_dir (List.fold_left (/) Envars.coqroot dl)
   in
     Mltop.add_ml_dir (Envars.coqlib ());
     List.iter add_subdir
diff --git a/toplevel/usage.ml b/toplevel/usage.ml
index 93ef0b201..512632316 100644
--- a/toplevel/usage.ml
+++ b/toplevel/usage.ml
@@ -92,7 +92,6 @@ let print_usage_coqc () =
 let print_config () =
   if Coq_config.local then Printf.printf "LOCAL=1\n" else Printf.printf "LOCAL=0\n";
   Printf.printf "COQLIB=%s/\n" (Envars.coqlib ());
-  (*Printf.printf "COQSRC=%s/\n" Coq_config.coqsrc;*)
   Printf.printf "DOCDIR=%s/\n" (Envars.docdir ());
   Printf.printf "OCAMLDEP=%s\n" Coq_config.ocamldep;
   Printf.printf "OCAMLC=%s\n" Coq_config.ocamlc;