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

2 files changed, 40 insertions, 14 deletions

diff --git a/ide/project_file.ml4 b/ide/project_file.ml4
index 1aad25d511..806e40d767 100644
--- a/ide/project_file.ml4
+++ b/ide/project_file.ml4
@@ -12,6 +12,10 @@ type target =
   | Include of string
   | RInclude of string * string (* -R physicalpath logicalpath *)
 
+type install =
+  | NoInstall
+  | TraditionalInstall
+  | UserInstall
 
 exception Parsing_error
 let rec parse_string = parser
@@ -51,8 +55,19 @@ let rec process_cmd_line orig_dir ((project_file,makefile,install,opt) as opts)
     Minilib.safe_prerr_endline "Please now use \"-arg -impredicative-set\" instead of \"-impredicative-set\" alone to be more uniform.";
     process_cmd_line orig_dir opts (Arg "-impredicative_set" :: l) r
   | "-no-install" :: r ->
-    if not install then Minilib.safe_prerr_endline "Warning: -no-install sets more than once.";
-    process_cmd_line orig_dir (project_file,makefile,false,opt) l r
+    Minilib.safe_prerr_endline "Option -no-install is deprecated. Use \"-install none\" instead";
+    process_cmd_line orig_dir (project_file,makefile,NoInstall,opt) l r
+  | "-install" :: d :: r ->
+    if install <> TraditionalInstall then Minilib.safe_prerr_endline "Warning: -install sets more than once.";
+    let install =
+      match d with
+	| "user" -> UserInstall
+	| "none" -> NoInstall
+	| "global" -> TraditionalInstall
+	| _ -> Minilib.safe_prerr_endline (String.concat "" ["Warning: invalid option '"; d; "' passed to -install."]);
+          install
+    in
+    process_cmd_line orig_dir (project_file,makefile,install,opt) l r
   | "-custom" :: com :: dependencies :: file :: r ->
     process_cmd_line orig_dir opts (Special (file,dependencies,com) :: l) r
   | "-I" :: d :: r ->
@@ -80,7 +95,7 @@ let rec process_cmd_line orig_dir ((project_file,makefile,install,opt) as opts)
 	let () = match makefile with
 	  |None -> ()
 	  |Some f ->
-	     Minilib.safe_prerr_endline ("Warning: Only one output file in genererated. "^f^" will not.")
+	     Minilib.safe_prerr_endline ("Warning: Only one output file is genererated. "^f^" will not be.")
 	in process_cmd_line orig_dir (project_file,Some file,install,opt) l r
       end
   | v :: "=" :: def :: r ->
@@ -143,7 +158,7 @@ let split_arguments =
 
 let read_project_file f =
   split_arguments
-    (snd (process_cmd_line (Filename.dirname f) (Some f, None, false, true) [] (parse f)))
+    (snd (process_cmd_line (Filename.dirname f) (Some f, None, NoInstall, true) [] (parse f)))
 
 let args_from_project file project_files default_name =
   let is_f = Minilib.same_file file in
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 ();