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

7 files changed, 37 insertions, 11 deletions

diff --git a/CHANGES b/CHANGES
index cecbae3d3c..2521e6c750 100644
--- a/CHANGES
+++ b/CHANGES
@@ -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 098b894695..34ba7b0101 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 5af57aefc5..17efcb7b5f 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 0991fb7a12..5cffad06c8 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 3f8ac5ecc2..d2799074eb 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 a683aaae9f..bc840d2d9f 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 e91cf3353d..0c6286d3a2 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 *)