Teach coq_makefile how to install into XDG_DATA_HOME.

From Tom Prince.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14693 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 21 insertions, 10 deletions

diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml
index 6d1e8277b4..f529665902 100644
--- a/tools/coq_makefile.ml
+++ b/tools/coq_makefile.ml
@@ -68,7 +68,9 @@ coq_makefile [subdirectory] .... [file.v] ... [file.ml[i4]?] ... [file.mllib]
 [-byte]: compile with byte-code version of coq
 [-opt]: compile with native-code version of coq
 [-arg opt]: send option \"opt\" to coqc
-[-no-install]: build a makefile with no install target
+[-install opt]: where opt is \"user\" to install into user directory,
+  \"none\" to build a makefile with no install target or
+  \"global\" to install in $COQLIB directory (default behavior)
 [-f file]: take the contents of file as arguments
 [-o file]: output should go in file file
 	Output file outside the current directory is forbidden.
@@ -322,7 +324,7 @@ in
     if !some_mlpackfile then mlpack_rules ();
     if !some_vfile then v_rules ()
 
-let variables opt (args,defs) =
+let variables is_install opt (args,defs) =
   let var_aux (v,def) = print v; print "="; print def; print "\n" in
     section "Variables definitions.";
     List.iter var_aux defs;
@@ -356,10 +358,19 @@ let variables opt (args,defs) =
     print "CAMLP4OPTIONS?=\n";
     print "PP?=-pp \"$(CAMLP4BIN)$(CAMLP4)o -I $(CAMLLIB) -I . $(COQSRCLIBS) $(CAMLP4EXTEND) $(GRAMMARS) $(CAMLP4OPTIONS) -impl\"\n";
     print "\n";
-    section "Install Paths";
-    print "COQLIBINSTALL=${COQLIB}/user-contrib\n";
-    print "COQDOCINSTALL=${DOCDIR}/user-contrib\n";
-    print "\n"
+    match is_install with
+      | Project_file.NoInstall -> ()
+      | Project_file.TraditionalInstall ->
+          section "Install Paths";
+          print "COQLIBINSTALL=${COQLIB}/user-contrib\n";
+          print "COQDOCINSTALL=${DOCDIR}/user-contrib\n";
+          print "\n"
+      | Project_file.UserInstall ->
+          section "Install Paths";
+          print "XDG_DATA_HOME?=$(HOME)/.local/share\n";
+          print "COQLIBINSTALL=$(XDG_DATA_HOME)/coq\n";
+          print "COQDOCINSTALL=$(XDG_DATA_HOME)/doc/coq\n";
+          print "\n"
 
 let parameters () =
   print "NOARG: all\n\n# \n";
@@ -616,7 +627,7 @@ let do_makefile args =
     |[] -> var := false
     |_::_ -> var := true in
   let (project_file,makefile,is_install,opt),l =
-    try Project_file.process_cmd_line Filename.current_dir_name (None,None,true,true) [] args
+    try Project_file.process_cmd_line Filename.current_dir_name (None,None,Project_file.TraditionalInstall,true) [] args
     with Project_file.Parsing_error -> usage () in
   let (v_f,(mli_f,ml4_f,ml_f,mllib_f,mlpack_f),sps,sds as targets), inc, defs =
     Project_file.split_arguments l in
@@ -640,7 +651,7 @@ let do_makefile args =
     List.iter check_dep (Str.split (Str.regexp "[ \t]+") dependencies)) sps;
 
   let inc = ensure_root_dir targets inc in
-  if is_install then warn_install_at_root_directory targets inc;
+  if is_install <> Project_file.NoInstall then warn_install_at_root_directory targets inc;
   check_overlapping_include inc;
   banner ();
   header_includes ();
@@ -648,11 +659,11 @@ let do_makefile args =
   command_line args;
   parameters ();
   include_dirs inc;
-  variables opt defs;
+  variables is_install opt defs;
   all_target targets inc;
   implicit ();
   standard opt;
-  if is_install then install targets inc;
+  if is_install <> Project_file.NoInstall then install targets inc;
   clean sds sps;
   make_makefile sds;
   warning ();