From 25020ba614315ce143f657511696fb7bf5135b00 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Thu, 10 Nov 2016 19:29:29 +0100 Subject: Dead code (xdg_config_dirs). --- lib/envars.ml | 10 ---------- lib/envars.mli | 1 - 2 files changed, 11 deletions(-) (limited to 'lib') diff --git a/lib/envars.ml b/lib/envars.ml index 79516bb1bf..0974368f62 100644 --- a/lib/envars.ml +++ b/lib/envars.ml @@ -191,16 +191,6 @@ let xdg_data_dirs warn = 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 - let xdg_dirs ~warn = List.filter Sys.file_exists (xdg_data_dirs warn) diff --git a/lib/envars.mli b/lib/envars.mli index b164e789d2..c33a08c405 100644 --- a/lib/envars.mli +++ b/lib/envars.mli @@ -66,7 +66,6 @@ val camlp4 : unit -> string *) val xdg_config_home : (string -> unit) -> string val xdg_data_home : (string -> unit) -> string -val xdg_config_dirs : (string -> unit) -> string list val xdg_data_dirs : (string -> unit) -> string list val xdg_dirs : warn : (string -> unit) -> string list -- cgit v1.2.3 From 417ac448411ce924444915da8e7e6fb81a12bc57 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Fri, 11 Nov 2016 11:11:20 +0100 Subject: Configuration: always giving a value to configdir and datadir. They were not used for looking for coqide files in the situation when the effective installation path happens to be exactly the installation path proposed by default, while relevant files were however (possibly) installed in these directories. --- lib/envars.ml | 4 +--- 1 file changed, 1 insertion(+), 3 deletions(-) (limited to 'lib') diff --git a/lib/envars.ml b/lib/envars.ml index 0974368f62..989a18db99 100644 --- a/lib/envars.ml +++ b/lib/envars.ml @@ -23,8 +23,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 -> @@ -189,7 +187,7 @@ let xdg_data_dirs warn = | Not_found when String.equal Sys.os_type "Win32" -> [relative_base / "share"] | Not_found -> ["/usr/local/share/coq";"/usr/share/coq"] in - xdg_data_home warn :: sys_dirs @ opt2list Coq_config.datadir + xdg_data_home warn :: sys_dirs @ [Coq_config.datadir] let xdg_dirs ~warn = List.filter Sys.file_exists (xdg_data_dirs warn) -- cgit v1.2.3 From d53ba17d1761261593c598b6a88cfd6ce0eb3514 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sat, 12 Nov 2016 03:08:56 +0100 Subject: Using Coq_config.local rather than None to tell that Coq_config.coqlib is local. This goes towards an approach where a local layout can be seen as an installed layout. --- lib/envars.ml | 7 ++----- 1 file changed, 2 insertions(+), 5 deletions(-) (limited to 'lib') diff --git a/lib/envars.ml b/lib/envars.ml index 989a18db99..b71a3f6297 100644 --- a/lib/envars.ml +++ b/lib/envars.ml @@ -110,11 +110,8 @@ let guess_coqlib fail = let dir = if Coq_config.arch_is_win32 then "lib" else "lib/coq" in check_file_else ~dir ~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") -- cgit v1.2.3 From 58935ddbaf6f0e2470716d30f70ea18a9f8151c4 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sat, 12 Nov 2016 03:08:34 +0100 Subject: 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. --- lib/envars.ml | 8 +++----- 1 file changed, 3 insertions(+), 5 deletions(-) (limited to 'lib') diff --git a/lib/envars.ml b/lib/envars.ml index b71a3f6297..feb5b34972 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 -- cgit v1.2.3 From 66b98ecd41bac232bbee19a9b3484feefd71df3c Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sat, 12 Nov 2016 03:47:08 +0100 Subject: Generalizing to docdir and datadir the test for a relocated installation. Also standardizing the choice of the default datadir (I don't see why we should add by default both /usr/local/share/coq and /usr/share/coq when we know that the installation is in only one of them). Open question: test for possible relocation of the installed coq should be done on raw dirname of the executable or on the standardization of this name wrt symbolic links? --- lib/envars.ml | 28 ++++++++++++++++++---------- 1 file changed, 18 insertions(+), 10 deletions(-) (limited to 'lib') diff --git a/lib/envars.ml b/lib/envars.ml index feb5b34972..78f14273db 100644 --- a/lib/envars.ml +++ b/lib/envars.ml @@ -79,9 +79,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) @@ -96,13 +93,18 @@ 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 = coqroot / dir in + let path = use_suffix coqroot dir in if Sys.file_exists (path / file) then path else oth () let guess_coqlib fail = @@ -124,7 +126,14 @@ let set_coqlib ~fail = let coqlib () = !Flags.coqlib let docdir () = - check_file_else ~dir:Coq_config.docdirsuffix ~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 coqpath = let coqpath = getenv_else "COQPATH" (fun () -> "") in @@ -179,10 +188,9 @@ 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 @ [Coq_config.datadir] + xdg_data_home warn :: sys_dirs let xdg_dirs ~warn = List.filter Sys.file_exists (xdg_data_dirs warn) -- cgit v1.2.3 From 5c875b6ab907cb48b0d06aba48d4c733cfd2ff06 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sat, 12 Nov 2016 04:01:29 +0100 Subject: Relying on computation done in Envars to discover the installation directories. This allows to share the test for possible relocalisation done in envars.ml. --- lib/envars.ml | 5 +++++ lib/envars.mli | 12 +++++++++--- 2 files changed, 14 insertions(+), 3 deletions(-) (limited to 'lib') diff --git a/lib/envars.ml b/lib/envars.ml index 78f14273db..bc8012297f 100644 --- a/lib/envars.ml +++ b/lib/envars.ml @@ -135,6 +135,11 @@ let datadir () = 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 let make_search_path path = diff --git a/lib/envars.mli b/lib/envars.mli index c33a08c405..c8bbf17d96 100644 --- a/lib/envars.mli +++ b/lib/envars.mli @@ -27,12 +27,18 @@ val home : warn:(string -> unit) -> string (** [coqlib] is the path to the Coq library. *) val coqlib : unit -> string +(** [docdir] is the path to the installed documentation. *) +val docdir : unit -> string + +(** [datadir] is the path to the installed data directory. *) +val datadir : unit -> string + +(** [configdir] is the path to the installed config directory. *) +val configdir : unit -> string + (** [set_coqlib] must be runned once before any access to [coqlib] *) val set_coqlib : fail:(string -> string) -> unit -(** [docdir] is the path to the Coq documentation. *) -val docdir : unit -> string - (** [coqbin] is the name of the current executable. *) val coqbin : string -- cgit v1.2.3