Exporting the suffixes needed to build coqlib, docdir, etc.

This allows to centralize in the configuration file the description of
the 3 possible installation layouts (dispatched over directories
shared by multiple application as in unix, self-contained style like
in windows, local non-installation as with option -local).

Also supporting relocalisation when -prefix or -libdir and co is given.

1 files changed, 41 insertions, 17 deletions

diff --git a/configure.ml b/configure.ml
index 1a851ef45..64165fab0 100644
--- a/configure.ml
+++ b/configure.ml
@@ -881,6 +881,9 @@ let install = [
     Relative "latex", Relative "share/texmf/tex/latex/misc", Relative "tools/coqdoc";
  ]
 
+let strip_trailing_slash_if_any p =
+  if p.[String.length p - 1] = '/' then String.sub p 0 (String.length p - 1) else p
+
 let use_suffix prefix = function
   | Relative "" -> prefix
   | Relative suff -> prefix ^ "/" ^ suff
@@ -891,34 +894,48 @@ let relativize = function
   | Relative _ as suffix -> suffix
   | Absolute path -> Relative (String.sub path 1 (String.length path - 1))
 
+let find_suffix prefix path = match prefix with
+  | None -> Absolute path
+  | Some p ->
+     let p = strip_trailing_slash_if_any p in
+     let lpath = String.length path in
+     let lp = String.length p in
+     if lpath > lp && String.sub path 0 lp = p then
+       Relative (String.sub path (lp+1) (lpath - lp - 1))
+     else
+       Absolute path
+
 let do_one_instdir (var,msg,uservalue,selfcontainedlayout,unixlayout,_) =
-  let dir = match !uservalue, !Prefs.prefix with
-    | Some d, _ -> d
-    | _, Some p -> use_suffix p (if arch_is_win32 then selfcontainedlayout else relativize unixlayout)
-    | _ ->
-      let dflt = if unix then use_suffix "/usr/local" unixlayout else use_suffix "C:/coq" selfcontainedlayout in
+  let dir,suffix = match !uservalue, !Prefs.prefix with
+    | Some d, p -> d,find_suffix p d
+    | _, Some p ->
+      let suffix = if arch_is_win32 then selfcontainedlayout else relativize unixlayout in
+      use_suffix p suffix, suffix
+    | _, p ->
+      let suffix = if unix then unixlayout else selfcontainedlayout in
+      let base = if unix then "/usr/local" else "C:/coq" in
+      let dflt = use_suffix base suffix in
       let () = printf "Where should I install %s [%s]? " msg dflt in
       let line = read_line () in
-      if line = "" then dflt else line
-  in (var,msg,dir)
+      if line = "" then (dflt,suffix) else (line,find_suffix p line)
+  in (var,msg,dir,suffix)
 
 let do_one_noinst (var,msg,_,_,_,locallayout) =
-  (var,msg,use_suffix coqtop locallayout)
+  (var,msg,use_suffix coqtop locallayout,locallayout)
 
 let install_dirs =
   let f = if !Prefs.local then do_one_noinst else do_one_instdir in
   List.map f install
 
-let select var = List.find (fun (v,_,_) -> v=var) install_dirs
+let select var = List.find (fun (v,_,_,_) -> v=var) install_dirs
 
-let coqlib = let (_,_,d) = select "COQLIBINSTALL" in d
+let coqlib,coqlibsuffix = let (_,_,d,s) = select "COQLIBINSTALL" in d,s
 
-let docdir = let (_,_,d) = select "DOCDIR" in d
+let docdir,docdirsuffix = let (_,_,d,s) = select "DOCDIR" in d,s
 
-let configdir = let (_,_,d) = select "CONFIGDIR" in d
-
-let datadir = let (_,_,d) = select "DATADIR" in d
+let configdir,configdirsuffix = let (_,_,d,s) = select "CONFIGDIR" in d,s
 
+let datadir,datadirsuffix = let (_,_,d,s) = select "DATADIR" in d,s
 
 (** * OCaml runtime flags *)
 
@@ -984,7 +1001,7 @@ let print_summary () =
   else
     (pr "  Paths for true installation:\n";
      List.iter
-       (fun (_,msg,dir) -> pr "  - %s will be copied in %s\n" msg dir)
+       (fun (_,msg,dir,_) -> pr "  - %s will be copied in %s\n" msg dir)
        install_dirs);
   pr "\n";
   pr "If anything is wrong above, please restart './configure'.\n\n";
@@ -1022,6 +1039,9 @@ let write_configml f =
   let pr_s = pr "let %s = %S\n" in
   let pr_b = pr "let %s = %B\n" in
   let pr_i = pr "let %s = %d\n" in
+  let pr_p s o = pr "let %s = %S\n" s
+    (match o with Relative s -> s | Absolute s -> s)
+  in
   pr "(* DO NOT EDIT THIS FILE: automatically generated by ../configure *)\n";
   pr "(* Exact command that generated this file: *)\n";
   pr "(* %s *)\n\n" (String.concat " " (Array.to_list Sys.argv));
@@ -1031,6 +1051,10 @@ let write_configml f =
   pr_s "configdir" configdir;
   pr_s "datadir" datadir;
   pr_s "docdir" docdir;
+  pr_p "coqlibsuffix" coqlibsuffix;
+  pr_p "configdirsuffix" configdirsuffix;
+  pr_p "datadirsuffix" datadirsuffix;
+  pr_p "docdirsuffix" docdirsuffix;
   pr_s "ocaml" camlexec.top;
   pr_s "ocamlfind" camlexec.find;
   pr_s "ocamllex" camlexec.lex;
@@ -1114,8 +1138,8 @@ let write_makefile f =
   pr "VMBYTEFLAGS=%s\n" (String.concat " " vmbyteflags);
   pr "%s\n\n" !build_loadpath;
   pr "# Paths for true installation\n";
-  List.iter (fun (v,msg,_) -> pr "# %s: path for %s\n" v msg) install_dirs;
-  List.iter (fun (v,_,dir) -> pr "%s=%S\n" v dir) install_dirs;
+  List.iter (fun (v,msg,_,_) -> pr "# %s: path for %s\n" v msg) install_dirs;
+  List.iter (fun (v,_,dir,_) -> pr "%s=%S\n" v dir) install_dirs;
   pr "\n# Coq version\n";
   pr "VERSION=%s\n" coq_version;
   pr "VERSION4MACOS=%s\n\n" coq_macos_version;