diff options
| -rw-r--r-- | config/coq_config.mli | 8 | ||||
| -rw-r--r-- | configure.ml | 58 | ||||
| -rw-r--r-- | lib/envars.ml | 8 | ||||
| -rw-r--r-- | tools/coqdoc/cdglobals.ml | 7 |
4 files changed, 53 insertions, 28 deletions
diff --git a/config/coq_config.mli b/config/coq_config.mli index 28a40ca93..2b3bc2c25 100644 --- a/config/coq_config.mli +++ b/config/coq_config.mli @@ -8,11 +8,19 @@ val local : bool (* local use (no installation) *) +(* The fields below are absolute paths *) val coqlib : string (* where the std library is installed *) val configdir : string (* where configuration files are installed *) val datadir : string (* where extra data files are installed *) val docdir : string (* where the doc is installed *) +(* The fields below are paths relative to the installation prefix *) +(* However, if an absolute path, it means discarding the actual prefix *) +val coqlibsuffix : string (* std library relative to installation prefix *) +val configdirsuffix : string (* config files relative to installation prefix *) +val datadirsuffix : string (* data files relative to installation prefix *) +val docdirsuffix : string (* doc directory relative to installation prefix *) + val ocaml : string (* names of ocaml binaries *) val ocamlfind : string val ocamllex : string 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; diff --git a/lib/envars.ml b/lib/envars.ml index b71a3f629..feb5b3497 100644 --- a/lib/envars.ml +++ b/lib/envars.ml @@ -102,13 +102,12 @@ let _ = If the check fails, then [oth ()] is evaluated. Using file system equality seems well enough for this heuristic *) let check_file_else ~dir ~file oth = - let path = if Coq_config.local then coqroot else coqroot / dir in + let path = coqroot / dir in if Sys.file_exists (path / file) then path else oth () let guess_coqlib fail = let prelude = "theories/Init/Prelude.vo" in - let dir = if Coq_config.arch_is_win32 then "lib" else "lib/coq" in - check_file_else ~dir ~file:prelude + check_file_else ~dir:Coq_config.coqlibsuffix ~file:prelude (fun () -> if not Coq_config.local && Sys.file_exists (Coq_config.coqlib / prelude) then Coq_config.coqlib @@ -125,8 +124,7 @@ let set_coqlib ~fail = let coqlib () = !Flags.coqlib let docdir () = - let dir = if Coq_config.arch_is_win32 then "doc" else "share/doc/coq" in - check_file_else ~dir ~file:"html" (fun () -> Coq_config.docdir) + check_file_else ~dir:Coq_config.docdirsuffix ~file:"html" (fun () -> Coq_config.docdir) let coqpath = let coqpath = getenv_else "COQPATH" (fun () -> "") in diff --git a/tools/coqdoc/cdglobals.ml b/tools/coqdoc/cdglobals.ml index 4b5c5d2e5..a1987387f 100644 --- a/tools/coqdoc/cdglobals.ml +++ b/tools/coqdoc/cdglobals.ml @@ -79,12 +79,7 @@ let guess_coqlib () = else 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_is_win32 then ["lib"] - else ["lib/coq"] - in - let coqlib = List.fold_left (/) prefix rpath in + let coqlib = prefix / Coq_config.coqlibsuffix in if Sys.file_exists (coqlib / file) then coqlib else prefix |