From 9043add656177eeac1491a73d2f3ab92bec0013c Mon Sep 17 00:00:00 2001 From: Benjamin Barenblat Date: Sat, 29 Dec 2018 14:31:27 -0500 Subject: Imported Upstream version 8.8.2 --- lib/envars.ml | 114 +++++++++++++++++++++++++++++++--------------------------- 1 file changed, 61 insertions(+), 53 deletions(-) (limited to 'lib/envars.ml') diff --git a/lib/envars.ml b/lib/envars.ml index 89ce5283..be82bfe9 100644 --- a/lib/envars.ml +++ b/lib/envars.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* [] | Some x -> [x] - let home ~warn = getenv_else "HOME" (fun () -> try (Sys.getenv "HOMEDRIVE")^(Sys.getenv "HOMEPATH") with Not_found -> @@ -81,9 +81,6 @@ let expand_path_macros ~warn s = (** {2 Coq paths} *) -let relative_base = - Filename.dirname (Filename.dirname Sys.executable_name) - let coqbin = CUnix.canonical_path_name (Filename.dirname Sys.executable_name) @@ -98,25 +95,26 @@ let _ = if Coq_config.arch_is_win32 then Unix.putenv "PATH" (coqbin ^ ";" ^ getenv_else "PATH" (fun () -> "")) +(** Add a local installation suffix (unless the suffix is itself + absolute in which case the prefix does not matter) *) +let use_suffix prefix suffix = + if String.length suffix > 0 && suffix.[0] = '/' then suffix else prefix / suffix + (** [check_file_else ~dir ~file oth] checks if [file] exists in - the installation directory [dir] given relatively to [coqroot]. - If this Coq is only locally built, then [file] must be in [coqroot]. + the installation directory [dir] given relatively to [coqroot], + which maybe has been relocated. 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 = use_suffix 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 () -> - let coqlib = match Coq_config.coqlib with - | Some coqlib -> coqlib - | None -> coqroot - in - if Sys.file_exists (coqlib / prelude) then coqlib + if not Coq_config.local && Sys.file_exists (Coq_config.coqlib / prelude) + then Coq_config.coqlib else fail "cannot guess a path for Coq libraries; please use -coqlib option") @@ -130,8 +128,19 @@ 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) + (* This assumes implicitly that the suffix is non-trivial *) + let path = use_suffix coqroot Coq_config.docdirsuffix in + if Sys.file_exists path then path else Coq_config.docdir + +let datadir () = + (* This assumes implicitly that the suffix is non-trivial *) + let path = use_suffix coqroot Coq_config.datadirsuffix in + if Sys.file_exists path then path else Coq_config.datadir + +let configdir () = + (* This assumes implicitly that the suffix is non-trivial *) + let path = use_suffix coqroot Coq_config.configdirsuffix in + if Sys.file_exists path then path else Coq_config.configdir let coqpath = let coqpath = getenv_else "COQPATH" (fun () -> "") in @@ -146,31 +155,23 @@ let coqpath = let exe s = s ^ Coq_config.exec_extension -let guess_ocamlfind () = which (user_path ()) (exe "ocamlfind") - -let ocamlfind () = - if !Flags.ocamlfind_spec then !Flags.ocamlfind else - if !Flags.boot then Coq_config.ocamlfind else - try guess_ocamlfind () / "ocamlfind" with Not_found -> Coq_config.ocamlfind - -(** {2 Camlp4 paths} *) +let ocamlfind () = Coq_config.ocamlfind -let guess_camlp4bin () = which (user_path ()) (exe Coq_config.camlp4) +(** {2 Camlp5 paths} *) -let camlp4bin () = - if !Flags.camlp4bin_spec then !Flags.camlp4bin else - if !Flags.boot then Coq_config.camlp4bin else - try guess_camlp4bin () - with Not_found -> - Coq_config.camlp4bin +let guess_camlp5bin () = which (user_path ()) (exe "camlp5") -let camlp4 () = camlp4bin () / exe Coq_config.camlp4 +let camlp5bin () = + if !Flags.boot then Coq_config.camlp5bin else + try guess_camlp5bin () + with Not_found -> + Coq_config.camlp5bin -let camlp4lib () = +let camlp5lib () = if !Flags.boot then - Coq_config.camlp4lib + Coq_config.camlp5lib else - let ex, res = CUnix.run_command (ocamlfind () ^ " query " ^ Coq_config.camlp4) in + let ex, res = CUnix.run_command (ocamlfind () ^ " query camlp5") in match ex with | Unix.WEXITED 0 -> String.strip res | _ -> "/dev/null" @@ -190,20 +191,27 @@ let xdg_data_dirs warn = try List.map coqify (path_to_list (Sys.getenv "XDG_DATA_DIRS")) with - | Not_found when String.equal Sys.os_type "Win32" -> [relative_base / "share"] - | Not_found -> ["/usr/local/share/coq";"/usr/share/coq"] + | Not_found -> [datadir ()] in - xdg_data_home warn :: sys_dirs @ opt2list Coq_config.datadir - -let xdg_config_dirs warn = - let sys_dirs = - try - List.map coqify (path_to_list (Sys.getenv "XDG_CONFIG_DIRS")) - with - | Not_found when String.equal Sys.os_type "Win32" -> [relative_base / "config"] - | Not_found -> ["/etc/xdg/coq"] - in - xdg_config_home warn :: sys_dirs @ opt2list Coq_config.configdir + xdg_data_home warn :: sys_dirs let xdg_dirs ~warn = List.filter Sys.file_exists (xdg_data_dirs warn) + +(* Print the configuration information *) + +let print_config ?(prefix_var_name="") f coq_src_subdirs = + let open Printf in + fprintf f "%sLOCAL=%s\n" prefix_var_name (if Coq_config.local then "1" else "0"); + fprintf f "%sCOQLIB=%s/\n" prefix_var_name (coqlib ()); + fprintf f "%sDOCDIR=%s/\n" prefix_var_name (docdir ()); + fprintf f "%sOCAMLFIND=%s\n" prefix_var_name (ocamlfind ()); + fprintf f "%sCAMLP5O=%s\n" prefix_var_name Coq_config.camlp5o; + fprintf f "%sCAMLP5BIN=%s/\n" prefix_var_name (camlp5bin ()); + fprintf f "%sCAMLP5LIB=%s\n" prefix_var_name (camlp5lib ()); + fprintf f "%sCAMLP5OPTIONS=%s\n" prefix_var_name Coq_config.camlp5compat; + fprintf f "%sCAMLFLAGS=%s\n" prefix_var_name Coq_config.caml_flags; + fprintf f "%sHASNATDYNLINK=%s\n" prefix_var_name + (if Coq_config.has_natdynlink then "true" else "false"); + fprintf f "%sCOQ_SRC_SUBDIRS=%s\n" prefix_var_name (String.concat " " coq_src_subdirs) + -- cgit v1.2.3