Coq_makefile : bug when a project file is not in the current directory.

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

5 files changed, 57 insertions, 41 deletions

diff --git a/ide/ideutils.ml b/ide/ideutils.ml
index c6994a8d9..71ff87f00 100644
--- a/ide/ideutils.ml
+++ b/ide/ideutils.ml
@@ -328,7 +328,4 @@ let browse_keyword f text =
   try let u = Lazy.force url_for_keyword text in browse f (doc_url() ^ u)
   with Not_found -> f ("No documentation found for \""^text^"\".\n")
 
-let absolute_filename f =
-  if Filename.is_relative f then
-    Filename.concat (Sys.getcwd ()) f
-  else f
+let absolute_filename f = Minilib.correct_path f (Sys.getcwd ())
diff --git a/ide/minilib.ml b/ide/minilib.ml
index 96d257df6..54be52c19 100644
--- a/ide/minilib.ml
+++ b/ide/minilib.ml
@@ -122,6 +122,8 @@ let canonical_path_name p =
     (* We give up to find a canonical name and just simplify it... *)
     strip_path p
 
+let correct_path f dir = if Filename.is_relative f then Filename.concat dir f else f
+
 (*
   checks if two file names refer to the same (existing) file by
   comparing their device and inode.
diff --git a/ide/minilib.mli b/ide/minilib.mli
index 86f7c8a3f..44e570301 100644
--- a/ide/minilib.mli
+++ b/ide/minilib.mli
@@ -30,8 +30,11 @@ val coqtop_path : string ref
     (avoid exception in win32 without console) *)
 val safe_prerr_endline : string -> unit
 
+val remove_path_dot : string -> string
 val strip_path : string -> string
 val canonical_path_name : string -> string
+(** correct_path f dir = dir/f if f is relative *)
+val correct_path : string -> string -> string
 
 (** checks if two file names refer to the same (existing) file *)
 val same_file : string -> string -> bool
diff --git a/ide/project_file.ml4 b/ide/project_file.ml4
index 9c7a29045..77d002c28 100644
--- a/ide/project_file.ml4
+++ b/ide/project_file.ml4
@@ -38,54 +38,63 @@ let parse f =
     close_in c;
     res
 
-let rec process_cmd_line ((project_file,makefile,install,opt) as opts) l = function
+let rec process_cmd_line orig_dir ((project_file,makefile,install,opt) as opts) l = function
   | [] -> opts,List.rev l
   | ("-h"|"--help") :: _ ->
     raise Parsing_error
   | ("-no-opt"|"-byte") :: r ->
-    process_cmd_line (project_file,makefile,install,false) l r
+    process_cmd_line orig_dir (project_file,makefile,install,false) l r
   | ("-full"|"-opt") :: r ->
-    process_cmd_line (project_file,makefile,install,true) l r
+    process_cmd_line orig_dir (project_file,makefile,install,true) l r
   | "-impredicative-set" :: r ->
     Minilib.safe_prerr_endline "Please now use \"-arg -impredicative-set\" instead of \"-impredicative-set\" alone to be more uniform.";
-    process_cmd_line opts (Arg "-impredicative_set" :: l) r
+    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 (project_file,makefile,false,opt) l r
+    process_cmd_line orig_dir (project_file,makefile,false,opt) l r
   | "-custom" :: com :: dependencies :: file :: r ->
-    process_cmd_line opts (Special (file,dependencies,com) :: l) r
+    process_cmd_line orig_dir opts (Special (file,dependencies,com) :: l) r
   | "-I" :: d :: r ->
-    process_cmd_line opts (Include d :: l) r
+    process_cmd_line orig_dir opts ((Include (Minilib.correct_path d orig_dir)) :: l) r
   | "-R" :: p :: lp :: r ->
-    process_cmd_line opts (RInclude (p,lp) :: l) r
+    process_cmd_line orig_dir opts (RInclude (Minilib.correct_path p orig_dir,lp) :: l) r
   | ("-I"|"-custom") :: _ ->
     raise Parsing_error
   | "-f" :: file :: r ->
+    let file = Minilib.correct_path file orig_dir in
     let () = match project_file with
       | None -> ()
       | Some _ -> Minilib.safe_prerr_endline
 	"Warning: Several features will not work with multiple project files."
-    in process_cmd_line (Some file,makefile,install,opt) l ((parse file)@r)
+    in
+    let (opts',l') = process_cmd_line (Filename.dirname file) (Some file,makefile,install,opt) l (parse file) in
+      process_cmd_line orig_dir opts' l' r
   | ["-f"] ->
     raise Parsing_error
   | "-o" :: file :: r ->
-    let () = match makefile with
-      |None -> ()
-      |Some f ->
-	Minilib.safe_prerr_endline ("Warning: Only one output file in genererated. "^f^" will not.")
-    in process_cmd_line (project_file,Some file,install,opt) l r
+      begin try
+	let _ = String.index file '/' in
+	  raise Parsing_error
+      with Not_found ->
+	let () = match makefile with
+	  |None -> ()
+	  |Some f ->
+	     Minilib.safe_prerr_endline ("Warning: Only one output file in genererated. "^f^" will not.")
+	in process_cmd_line orig_dir (project_file,Some file,install,opt) l r
+      end
   | v :: "=" :: def :: r ->
-    process_cmd_line opts (Def (v,def) :: l) r
+    process_cmd_line orig_dir opts (Def (v,def) :: l) r
   | "-arg" :: a :: r ->
-    process_cmd_line opts (Arg a :: l) r
+    process_cmd_line orig_dir opts (Arg a :: l) r
   | f :: r ->
-    process_cmd_line opts ((
-      if Filename.check_suffix f ".v" then V f
-      else if (Filename.check_suffix f ".ml") then ML f
-      else if (Filename.check_suffix f ".ml4") then ML4 f
-      else if (Filename.check_suffix f ".mli") then MLI f
-      else if (Filename.check_suffix f ".mllib") then MLLIB f
-      else Subdir f) :: l) r
+      let f = Minilib.correct_path f orig_dir in
+	process_cmd_line orig_dir opts ((
+          if Filename.check_suffix f ".v" then V f
+	  else if (Filename.check_suffix f ".ml") then ML f
+	  else if (Filename.check_suffix f ".ml4") then ML4 f
+	  else if (Filename.check_suffix f ".mli") then MLI f
+	  else if (Filename.check_suffix f ".mllib") then MLLIB f
+	  else Subdir f) :: l) r
 
 let rec post_canonize f =
   if Filename.basename f = Filename.current_dir_name
@@ -94,32 +103,36 @@ let rec post_canonize f =
   else f
 
 (* Return: ((v,(mli,ml4,ml,mllib),special,subdir),(i_inc,r_inc),(args,defs)) *)
-let rec split_arguments = function
+let split_arguments =
+  let rec aux = function
   | V n :: r ->
-      let (v,m,o,s),i,d = split_arguments r in ((Minilib.strip_path n::v,m,o,s),i,d)
+	let (v,m,o,s),i,d = aux r in ((Minilib.remove_path_dot n::v,m,o,s),i,d)
   | ML n :: r ->
-      let (v,(mli,ml4,ml,mllib),o,s),i,d = split_arguments r in ((v,(mli,ml4,Minilib.strip_path n::ml,mllib),o,s),i,d)
+      let (v,(mli,ml4,ml,mllib),o,s),i,d = aux r in ((v,(mli,ml4,Minilib.remove_path_dot n::ml,mllib),o,s),i,d)
   | MLI n :: r ->
-      let (v,(mli,ml4,ml,mllib),o,s),i,d = split_arguments r in ((v,(Minilib.strip_path n::mli,ml4,ml,mllib),o,s),i,d)
+      let (v,(mli,ml4,ml,mllib),o,s),i,d = aux r in ((v,(Minilib.remove_path_dot n::mli,ml4,ml,mllib),o,s),i,d)
   | ML4 n :: r ->
-      let (v,(mli,ml4,ml,mllib),o,s),i,d = split_arguments r in ((v,(mli,Minilib.strip_path n::ml4,ml,mllib),o,s),i,d)
+      let (v,(mli,ml4,ml,mllib),o,s),i,d = aux r in ((v,(mli,Minilib.remove_path_dot n::ml4,ml,mllib),o,s),i,d)
   | MLLIB n :: r ->
-      let (v,(mli,ml4,ml,mllib),o,s),i,d = split_arguments r in ((v,(mli,ml4,ml,Minilib.strip_path n::mllib),o,s),i,d)
+      let (v,(mli,ml4,ml,mllib),o,s),i,d = aux r in ((v,(mli,ml4,ml,Minilib.remove_path_dot n::mllib),o,s),i,d)
   | Special (n,dep,c) :: r ->
-      let (v,m,o,s),i,d = split_arguments r in ((v,m,(n,dep,c)::o,s),i,d)
+      let (v,m,o,s),i,d = aux r in ((v,m,(n,dep,c)::o,s),i,d)
   | Subdir n :: r ->
-      let (v,m,o,s),i,d = split_arguments r in ((v,m,o,n::s),i,d)
+      let (v,m,o,s),i,d = aux r in ((v,m,o,n::s),i,d)
   | Include p :: r ->
-      let t,(i,r),d = split_arguments r in (t,((post_canonize p,Minilib.canonical_path_name p)::i,r),d)
+      let t,(i,r),d = aux r in (t,((Minilib.remove_path_dot (post_canonize p),
+				    Minilib.canonical_path_name p)::i,r),d)
   | RInclude (p,l) :: r ->
-      let t,(i,r),d = split_arguments r in (t,(i,(post_canonize p,l,Minilib.canonical_path_name p)::r),d)
+      let t,(i,r),d = aux r in (t,(i,(Minilib.remove_path_dot (post_canonize p),l,
+				      Minilib.canonical_path_name p)::r),d)
   | Def (v,def) :: r ->
-      let t,i,(args,defs) = split_arguments r in (t,i,(args,(v,def)::defs))
+      let t,i,(args,defs) = aux r in (t,i,(args,(v,def)::defs))
   | Arg a :: r ->
-      let t,i,(args,defs) = split_arguments r in (t,i,(a::args,defs))
+      let t,i,(args,defs) = aux r in (t,i,(a::args,defs))
   | [] -> ([],([],[],[],[]),[],[]),([],[]),([],[])
+  in aux
 
-let read_project_file f = split_arguments (snd (process_cmd_line (Some f, None, false, true) [] (parse f)))
+let read_project_file f = split_arguments (snd (process_cmd_line (Filename.dirname f) (Some f, None, false, true) [] (parse f)))
 
 let args_from_project file project_files =
   let contains_file f dir =
diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml
index e26abdb3e..738c1ea2b 100644
--- a/tools/coq_makefile.ml
+++ b/tools/coq_makefile.ml
@@ -70,6 +70,7 @@ coq_makefile [subdirectory] .... [file.v] ... [file.ml[i4]?] ... [file.mllib]
 [-no-install]: build a makefile with no install target
 [-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.
 [-h]: print this usage summary
 [--help]: equivalent to [-h]\n";
   exit 1
@@ -551,7 +552,7 @@ let do_makefile args =
     |[] -> var := false
     |_::_ -> var := true in
   let (project_file,makefile,is_install,opt),l =
-    try Project_file.process_cmd_line (None,None,true,true) [] args
+    try Project_file.process_cmd_line Filename.current_dir_name (None,None,true,true) [] args
     with Project_file.Parsing_error -> usage () in
   let (v_f,(mli_f,ml4_f,ml_f,mllib_f),sps,sds as targets), inc, defs =
     Project_file.split_arguments l in