summaryrefslogtreecommitdiff
path: root/lib/envars.ml
diff options
context:
space:
mode:
Diffstat (limited to 'lib/envars.ml')
-rw-r--r--lib/envars.ml114
1 files changed, 61 insertions, 53 deletions
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 *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
+(* * The Coq Proof Assistant / The Coq Development Team *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* <O___,, * (see CREDITS file for the list of authors) *)
(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
open Util
@@ -23,8 +25,6 @@ let ( / ) a b =
let coqify d = d / "coq"
-let opt2list = function None -> [] | 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)
+
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-07 07:40:45 +0000