diff options
author | pboutill <pboutill@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-11-20 20:02:54 +0000 |
---|---|---|
committer | pboutill <pboutill@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-11-20 20:02:54 +0000 |
commit | 1c535a5a1e6f4dcc35bd67a99a7236c6e7a222ab (patch) | |
tree | 7803c5a9ed6bb9327d24ac0920e4f3e96b111a04 | |
parent | 665652844458aa9826e425864781860504bf1836 (diff) |
Add support for XDG_DATA_HOME and XDG_DATA_DIRS.
From Tom Prince
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14692 85f007b7-540e-0410-9357-904b9bb8a0f7
-rw-r--r-- | CHANGES | 4 | ||||
-rw-r--r-- | checker/checker.ml | 5 | ||||
-rw-r--r-- | doc/refman/RefMan-com.tex | 5 | ||||
-rw-r--r-- | lib/envars.ml | 22 | ||||
-rw-r--r-- | lib/envars.mli | 3 | ||||
-rw-r--r-- | tools/coqdep.ml | 4 | ||||
-rw-r--r-- | toplevel/coqinit.ml | 5 |
7 files changed, 37 insertions, 11 deletions
@@ -199,8 +199,8 @@ CoqIDE Tools -- Coq now searches directories specified in COQPATH and user-contribs before - the standard library. +- Coq now searches directories specified in COQPATH, $XDG_DATA_HOME/coq, + $XDG_DATA_DIRS/coq, and user-contribs before the standard library. - coq_makefile major cleanup. * mli taken into account, ml not preproccessed anymore, ml4 work * mlihtml generates doc of mli, install-doc install the html doc in DOCDIR diff --git a/checker/checker.ml b/checker/checker.ml index 098b89469..34ba7b010 100644 --- a/checker/checker.ml +++ b/checker/checker.ml @@ -102,7 +102,8 @@ let set_rec_include d p = let init_load_path () = let coqlib = Envars.coqlib () in let user_contrib = coqlib/"user-contrib" in - let coqpath = Envars.coqpath () in + let xdg_dirs = Envars.xdg_dirs in + let coqpath = Envars.coqpath in let plugins = coqlib/"plugins" in (* NOTE: These directories are searched from last to first *) (* first standard library *) @@ -112,6 +113,8 @@ let init_load_path () = (* then user-contrib *) if Sys.file_exists user_contrib then add_rec_path ~unix_path:user_contrib ~coq_root:Check.default_root_prefix; + (* then directories in XDG_DATA_DIRS and XDG_DATA_HOME *) + List.iter (fun s -> add_rec_path ~unix_path:s ~coq_root:Check.default_root_prefix) xdg_dirs; (* then directories in COQPATH *) List.iter (fun s -> add_rec_path ~unix_path:s ~coq_root:Check.default_root_prefix) coqpath; (* then current directory *) diff --git a/doc/refman/RefMan-com.tex b/doc/refman/RefMan-com.tex index 5af57aefc..17efcb7b5 100644 --- a/doc/refman/RefMan-com.tex +++ b/doc/refman/RefMan-com.tex @@ -82,6 +82,11 @@ only for developers that are writing their own tactics and are using (defined at installation time). So these variables are useful only if you move the \Coq\ binaries and library after installation. +Coq will also honor \verb:$XDG_DATA_HOME: and \verb:$XDG_DATA_DIRS: (see +\{http://standards.freedesktop.org/basedir-spec/basedir-spec-latest.html}). +Coq adds \verb:${XDG_DATA_HOME}/coq: and \verb:${XDG_DATA_DIRS}/coq: to its +search path. + \section[Options]{Options\index{Options of the command line} \label{vmoption} \label{coqoptions}} diff --git a/lib/envars.ml b/lib/envars.ml index 0991fb7a1..5cffad06c 100644 --- a/lib/envars.ml +++ b/lib/envars.ml @@ -51,11 +51,26 @@ let path_to_list p = let sep = if Sys.os_type = "Win32" then ';' else ':' in Util.split_string_at sep p -let coqpath () = +let xdg_data_home = + Filename.concat + (System.getenv_else "XDG_DATA_HOME" (Filename.concat System.home ".local/share")) + "coq" + +let xdg_data_dirs = + try + List.map (fun dir -> Filename.concat dir "coq") (path_to_list (Sys.getenv "XDG_DATA_DIRS")) + with Not_found -> [ "/usr/local/share/coq"; "/usr/share/coq" ] + +let xdg_dirs = + let dirs = xdg_data_home :: xdg_data_dirs + in + List.rev (List.filter Sys.file_exists dirs) + +let coqpath = try let path = Sys.getenv "COQPATH" in - List.rev (path_to_list path) - with _ -> [] + List.rev (List.filter Sys.file_exists (path_to_list path)) + with Not_found -> [] let rec which l f = match l with @@ -89,7 +104,6 @@ let camllib () = let _,res = System.run_command (fun x -> x) (fun _ -> ()) com in Util.strip res -(* TODO : essayer aussi camlbin *) let camlp4bin () = if !Flags.camlp4bin_spec then !Flags.camlp4bin else if !Flags.boot then Coq_config.camlp4bin else diff --git a/lib/envars.mli b/lib/envars.mli index 3f8ac5ecc..d2799074e 100644 --- a/lib/envars.mli +++ b/lib/envars.mli @@ -15,7 +15,8 @@ val coqbin : string val coqroot : string (* coqpath is stored in reverse order, since that is the order it * gets added to the searc path *) -val coqpath : unit -> string list +val xdg_dirs : string list +val coqpath : string list val camlbin : unit -> string val camlp4bin : unit -> string diff --git a/tools/coqdep.ml b/tools/coqdep.ml index a683aaae9..bc840d2d9 100644 --- a/tools/coqdep.ml +++ b/tools/coqdep.ml @@ -200,8 +200,8 @@ let coqdep () = add_rec_dir add_coqlib_known (coqlib//"plugins") ["Coq"]; let user = coqlib//"user-contrib" in if Sys.file_exists user then add_rec_dir add_coqlib_known user []; - let coqpath = Envars.coqpath () in - List.iter (fun s -> add_rec_dir add_coqlib_known s []) coqpath; + List.iter (fun s -> add_rec_dir add_coqlib_known s []) Envars.xdg_dirs; + List.iter (fun s -> add_rec_dir add_coqlib_known s []) Envars.coqpath; end; List.iter (fun (f,d) -> add_mli_known f d) !mliAccu; List.iter (fun (f,d) -> add_mllib_known f d) !mllibAccu; diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml index e91cf3353..0c6286d3a 100644 --- a/toplevel/coqinit.ml +++ b/toplevel/coqinit.ml @@ -91,7 +91,8 @@ let theories_dirs_map = [ let init_load_path () = let coqlib = Envars.coqlib () in let user_contrib = coqlib/"user-contrib" in - let coqpath = Envars.coqpath () in + let xdg_dirs = Envars.xdg_dirs in + let coqpath = Envars.coqpath in let dirs = ["states";"plugins"] in (* NOTE: These directories are searched from last to first *) (* first, developer specific directory to open *) @@ -105,6 +106,8 @@ let init_load_path () = (* then user-contrib *) if Sys.file_exists user_contrib then Mltop.add_rec_path ~unix_path:user_contrib ~coq_root:Nameops.default_root_prefix; + (* then directories in XDG_DATA_DIRS and XDG_DATA_HOME *) + List.iter (fun s -> Mltop.add_rec_path ~unix_path:s ~coq_root:Nameops.default_root_prefix) xdg_dirs; (* then directories in COQPATH *) List.iter (fun s -> Mltop.add_rec_path ~unix_path:s ~coq_root:Nameops.default_root_prefix) coqpath; (* then current directory *) |