CoqProject_file: API and code cleanup (tuples -> records)

4 files changed, 260 insertions, 245 deletions

diff --git a/ide/coqide.ml b/ide/coqide.ml
index e47db8d19..ec3ea69bb 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -46,7 +46,7 @@ open Session
 
 (** The arguments that will be passed to coqtop. No quoting here, since
     no /bin/sh when using create_process instead of open_process. *)
-let custom_project_files = ref []
+let custom_project_file = ref None
 let sup_args = ref []
 
 let logfile = ref None
@@ -81,17 +81,27 @@ let pr_exit_status = function
   | Unix.WEXITED 0 -> " succeeded"
   | _ -> " failed"
 
-let make_coqtop_args = function
-  |None -> "", !sup_args
-  |Some the_file ->
-    let get_args f = CoqProject_file.args_from_project f
-      !custom_project_files project_file_name#get
-    in
-    match read_project#get with
-      |Ignore_args -> "", !sup_args
-      |Append_args ->
-         let fname, args = get_args the_file in fname, args @ !sup_args
-      |Subst_args -> get_args the_file
+let make_coqtop_args fname =
+  let open CoqProject_file in
+  let base_args = match read_project#get with
+    | Ignore_args -> !sup_args
+    | Append_args -> !sup_args
+    | Subst_args -> [] in
+  if read_project#get = Ignore_args then "", base_args
+  else
+    match !custom_project_file, fname with
+    | Some (d,proj), _ -> d, coqtop_args_from_project proj @ base_args
+    | None, None -> "", base_args
+    | None, Some the_file ->
+       match
+         CoqProject_file.find_project_file
+           ~from:(Filename.dirname the_file)
+           ~projfile_name:project_file_name#get
+       with
+       | None -> "", base_args
+       | Some proj -> 
+           proj, coqtop_args_from_project (read_project_file proj) @ base_args
+;;
 
 (** Setting drag & drop on widgets *)
 
@@ -1345,9 +1355,11 @@ let read_coqide_args argv =
       if coqtop = None then filter_coqtop (Some prog) project_files out args
       else (output_string stderr "Error: multiple -coqtop options"; exit 1)
     |"-f" :: file :: args ->
+      if project_files <> None then
+        (output_string stderr "Error: multiple -f options"; exit 1);
       let d = CUnix.canonical_path_name (Filename.dirname file) in
       let p = CoqProject_file.read_project_file file in
-      filter_coqtop coqtop ((d,p) :: project_files) out args
+      filter_coqtop coqtop (Some (d,p)) out args
     |"-f" :: [] ->
       output_string stderr "Error: missing project file name"; exit 1
     |"-coqtop" :: [] ->
@@ -1364,11 +1376,11 @@ let read_coqide_args argv =
       (* argument added by MacOS during .app launch *)
       filter_coqtop coqtop project_files out args
     |arg::args -> filter_coqtop coqtop project_files (arg::out) args
-    |[] -> (coqtop,List.rev project_files,List.rev out)
+    |[] -> (coqtop,project_files,List.rev out)
   in
-  let coqtop,project_files,argv = filter_coqtop None [] [] argv in
+  let coqtop,project_files,argv = filter_coqtop None None [] argv in
   Ideutils.custom_coqtop := coqtop;
-  custom_project_files := project_files;
+  custom_project_file := project_files;
   argv
 
 
diff --git a/lib/coqProject_file.ml4 b/lib/coqProject_file.ml4
index d32273bc2..9327f173e 100644
--- a/lib/coqProject_file.ml4
+++ b/lib/coqProject_file.ml4
@@ -6,29 +6,77 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-type target =
-  | ML of string (* ML file : foo.ml -> (ML "foo.ml") *)
-  | MLI of string (* MLI file : foo.mli -> (MLI "foo.mli") *)
-  | ML4 of string (* ML4 file : foo.ml4 -> (ML4 "foo.ml4") *)
-  | MLLIB of string (* MLLIB file : foo.mllib -> (MLLIB "foo.mllib") *)
-  | MLPACK of string (* MLLIB file : foo.mlpack -> (MLLIB "foo.mlpack") *)
-  | V of string  (* V file : foo.v -> (V "foo") *)
-  | Arg of string
-  | Special of string * string * bool * string
-    (* file, dependencies, is_phony, command *)
-  | Subdir of string
-  | Def of string * string (* X=foo -> Def ("X","foo") *)
-  | MLInclude of string (* -I physicalpath *)
-  | Include of string * string (* -Q physicalpath logicalpath *)
-  | RInclude of string * string (* -R physicalpath logicalpath *)
-
-type install =
+type project = {
+  project_file  : string option;
+  makefile : string option;
+  install_kind  : install option;
+  use_ocamlopt : bool;
+
+  v_files : string list;
+  mli_files : string list;
+  ml4_files : string list;
+  ml_files : string list;
+  mllib_files : string list;
+  mlpack_files : string list;
+
+  extra_targets : extra_target list;
+  subdirs : string list;
+  ml_includes : path list;
+  r_includes  : (path * logic_path) list;
+  q_includes  : (path * logic_path) list;
+  extra_args : string list;
+  defs : (string * string) list;
+}
+and extra_target = {
+  target : string;
+  dependencies : string;
+  phony : bool;
+  command : string;
+}
+and logic_path = string
+and path = { path : string; canonical_path : string }
+and install =
   | NoInstall
   | TraditionalInstall
   | UserInstall
-  | UnspecInstall
 
-exception Parsing_error
+(* TODO generate with PPX *)
+let mk_project project_file makefile install_kind use_ocamlopt = {
+  project_file;
+  makefile;
+  install_kind;
+  use_ocamlopt;
+
+  v_files = [];
+  mli_files = [];
+  ml4_files = [];
+  ml_files = [];
+  mllib_files = [];
+  mlpack_files = [];
+  extra_targets = [];
+  subdirs = [];
+  ml_includes = [];
+  r_includes = [];
+  q_includes = [];
+  extra_args = [];
+  defs = [];
+}
+
+(********************* utils ********************************************)
+
+let rec post_canonize f =
+  if Filename.basename f = Filename.current_dir_name
+  then let dir = Filename.dirname f in
+    if dir = Filename.current_dir_name then f else post_canonize dir
+  else f
+
+(* Avoid Sys.is_directory raise an exception (if the file does not exists) *)
+let is_directory f = Sys.file_exists f && Sys.is_directory f
+
+(********************* parser *******************************************)
+
+exception Parsing_error of string
+
 let rec parse_string = parser
   | [< '' ' | '\n' | '\t' >] -> ""
   | [< 'c; s >] -> (String.make 1 c)^(parse_string s)
@@ -36,7 +84,7 @@ let rec parse_string = parser
 and parse_string2 = parser
   | [< ''"' >] -> ""
   | [< 'c; s >] -> (String.make 1 c)^(parse_string2 s)
-  | [< >] -> raise Parsing_error
+  | [< >] -> raise (Parsing_error "unterminated string")
 and parse_skip_comment = parser
   | [< ''\n'; s >] -> s
   | [< 'c; s >] -> parse_skip_comment s
@@ -48,165 +96,117 @@ and parse_args = parser
   | [< 'c; str = parse_string; s >] -> ((String.make 1 c) ^ str) :: (parse_args s)
   | [< >] -> []
 
-
 let parse f =
   let c = open_in f in
   let res = parse_args (Stream.of_channel c) in
-    close_in c;
-    res
-
-let rec process_cmd_line orig_dir ((project_file,makefile,install,opt) as opts) l = function
-  | [] -> opts, l
-  | ("-h"|"--help") :: _ ->
-    raise Parsing_error
-  | ("-no-opt"|"-byte") :: r ->
-    process_cmd_line orig_dir (project_file,makefile,install,false) l r
-  | ("-full"|"-opt") :: r ->
-    process_cmd_line orig_dir (project_file,makefile,install,true) l r
-  | "-impredicative-set" :: r ->
-    Feedback.msg_warning (Pp.str "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 ->
-    Feedback.msg_warning (Pp.(++) (Pp.str "Option -no-install is deprecated.") (Pp.(++) (Pp.spc ()) (Pp.str "Use \"-install none\" instead")));
-    process_cmd_line orig_dir (project_file,makefile,NoInstall,opt) l r
+  close_in c;
+  res
+;;
+
+let process_cmd_line orig_dir proj args =
+  let error s = Feedback.msg_error (Pp.str (s^".")); exit 1 in
+  let mk_path d =
+    let p = CUnix.correct_path d orig_dir in
+    { path = CUnix.remove_path_dot (post_canonize p);
+      canonical_path = CUnix.canonical_path_name p } in
+  let rec aux proj = function
+  | [] -> proj
+  | "-impredicative-set" :: _ ->
+    error "Use \"-arg -impredicative-set\" instead of \"-impredicative-set\""
+  | "-no-install" :: _ ->
+    error "Use \"-install none\" instead of \"-no-install\""
+  | "-custom" :: _ ->
+    error "Use \"-extra[-phony] target deps command\" instead of \"-custom command deps target\""
+  
+  | ("-no-opt"|"-byte") :: r -> aux { proj with use_ocamlopt =  false } r
+  | ("-full"|"-opt") :: r -> aux { proj with use_ocamlopt =  true } r
   | "-install" :: d :: r ->
-    if install <> UnspecInstall then Feedback.msg_warning (Pp.str "-install sets more than once.");
-    let install =
-      match d with
-	| "user" -> UserInstall
-	| "none" -> NoInstall
-	| "global" -> TraditionalInstall
-	| _ -> Feedback.msg_warning (Pp.(++) (Pp.str "invalid option '") (Pp.(++) (Pp.str d) (Pp.str "' passed to -install.")));
-          install
-    in
-    process_cmd_line orig_dir (project_file,makefile,install,opt) l r
-  | "-custom" :: com :: dependencies :: file :: r ->
-    Feedback.msg_warning (Pp.app
-    (Pp.str "Please now use \"-extra[-phony] result deps command\" instead of \"-custom command deps result\".")
-    (Pp.pr_arg Pp.str "It follows makefile target declaration order and has a clearer semantic.")
-    );
-    process_cmd_line orig_dir opts (Special (file,dependencies,false,com) :: l) r
-  | "-extra" :: file :: dependencies :: com :: r ->
-    process_cmd_line orig_dir opts (Special (file,dependencies,false,com) :: l) r
-  | "-extra-phony" :: target :: dependencies :: com :: r ->
-    process_cmd_line orig_dir opts (Special (target,dependencies,true,com) :: l) r
+    if proj.install_kind <> None then
+      Feedback.msg_warning (Pp.str "-install set more than once.");
+    let install = match d with
+      | "user" -> UserInstall
+      | "none" -> NoInstall
+      | "global" -> TraditionalInstall
+      | _ -> error ("invalid option \""^d^"\" passed to -install") in
+    aux { proj with install_kind = Some install } r
+  | "-extra" :: target :: dependencies :: command :: r ->
+    let tgt = { target; dependencies; phony = false; command } in
+    aux { proj with extra_targets = proj.extra_targets @ [tgt] } r
+  | "-extra-phony" :: target :: dependencies :: command :: r ->
+    let tgt = { target; dependencies; phony = true; command } in
+    aux { proj with extra_targets = proj.extra_targets @ [tgt] } r
+
   | "-Q" :: d :: lp :: r ->
-    process_cmd_line orig_dir opts ((Include (CUnix.correct_path d orig_dir, lp)) :: l) r
+    aux { proj with q_includes = proj.q_includes @ [mk_path d,lp] } r
   | "-I" :: d :: r ->
-    process_cmd_line orig_dir opts ((MLInclude (CUnix.correct_path d orig_dir)) :: l) r
-  | "-R" :: p :: lp :: r ->
-    process_cmd_line orig_dir opts (RInclude (CUnix.correct_path p orig_dir,lp) :: l) r
-  | ("-Q"|"-R"|"-I"|"-custom"|"-extra"|"-extra-phony") :: _ ->
-    raise Parsing_error
+    aux { proj with ml_includes = proj.ml_includes @ [mk_path d] } r
+  | "-R" :: d :: lp :: r ->
+    aux { proj with r_includes = proj.r_includes @ [mk_path d,lp] } r
+
   | "-f" :: file :: r ->
     let file = CUnix.remove_path_dot (CUnix.correct_path file orig_dir) in
-    let () = match project_file with
+    let () = match proj.project_file with
       | None -> ()
       | Some _ -> Feedback.msg_warning (Pp.str
-	"Several features will not work with multiple project files.")
+	"Multiple project files are deprecated.")
     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
+    let proj = aux { proj with project_file = Some file } (parse file) in
+    aux proj r
+
   | "-o" :: file :: r ->
-      begin try
-	let _ = String.index file '/' in
-	  raise Parsing_error
-      with Not_found ->
-	let () = match makefile with
-	  |None -> ()
-	  |Some f ->
-	     Feedback.msg_warning (Pp.(++) (Pp.str "Only one output file is genererated. ") (Pp.(++) (Pp.str f) (Pp.str " will not be.")))
-	in process_cmd_line orig_dir (project_file,Some file,install,opt) l r
-      end
+    if String.contains file '/' then
+      error "Output file must be in the current directory";
+    if proj.makefile <> None then
+      error "Option -o given more than once";
+    aux { proj with makefile = Some file } r  
   | v :: "=" :: def :: r ->
-    process_cmd_line orig_dir opts (Def (v,def) :: l) r
+    aux { proj with defs = proj.defs @ [v,def] } r
   | "-arg" :: a :: r ->
-    process_cmd_line orig_dir opts (Arg a :: l) r
+    aux { proj with extra_args = proj.extra_args @ [a] } r
   | f :: r ->
       let f = CUnix.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 if (Filename.check_suffix f ".mlpack") then MLPACK f
-	  else Subdir f) :: l) r
-
-let process_cmd_line orig_dir opts l args =
-  let (opts, l) = process_cmd_line orig_dir opts l args in
-  opts, List.rev l
+      let proj =
+        if is_directory f then { proj with subdirs = proj.subdirs @ [f] }
+        else match CUnix.get_extension f with
+        | ".v" -> { proj with v_files = proj.v_files @ [f] }
+        | ".ml" -> { proj with ml_files = proj.ml_files @ [f] }
+        | ".ml4" -> { proj with ml4_files = proj.ml4_files @ [f] }
+        | ".mli" -> { proj with mli_files = proj.mli_files @ [f] }
+        | ".mllib" -> { proj with mllib_files = proj.mllib_files @ [f] }
+        | ".mlpack" -> { proj with mlpack_files = proj.mlpack_files @ [f] }
+        | _ -> raise (Parsing_error ("Unknown option "^f)) in
+      aux proj r
+ in
+   aux proj args
 
-let rec post_canonize f =
-  if Filename.basename f = Filename.current_dir_name
-  then let dir = Filename.dirname f in
-    if dir = Filename.current_dir_name then f else post_canonize dir
-  else f
+ (******************************* API ************************************)
 
-(* Return: ((v,(mli,ml4,ml,mllib,mlpack),special,subdir),(ml_inc,q_inc,r_inc),(args,defs)) *)
-let split_arguments args =
-  List.fold_right
-    (fun a ((v,(mli,ml4,ml,mllib,mlpack as m),o,s as t),
-            (ml_inc,q_inc,r_inc as i),(args,defs as d)) ->
-     match a with
-     | V n ->
-        ((CUnix.remove_path_dot n::v,m,o,s),i,d)
-     | ML n ->
-        ((v,(mli,ml4,CUnix.remove_path_dot n::ml,mllib,mlpack),o,s),i,d)
-     | MLI n ->
-        ((v,(CUnix.remove_path_dot n::mli,ml4,ml,mllib,mlpack),o,s),i,d)
-     | ML4 n ->
-        ((v,(mli,CUnix.remove_path_dot n::ml4,ml,mllib,mlpack),o,s),i,d)
-     | MLLIB n ->
-        ((v,(mli,ml4,ml,CUnix.remove_path_dot n::mllib,mlpack),o,s),i,d)
-     | MLPACK n ->
-        ((v,(mli,ml4,ml,mllib,CUnix.remove_path_dot n::mlpack),o,s),i,d)
-     | Special (n,dep,is_phony,c) ->
-        ((v,m,(n,dep,is_phony,c)::o,s),i,d)
-     | Subdir n ->
-        ((v,m,o,n::s),i,d)
-     | MLInclude p ->
-        let ml_new = (CUnix.remove_path_dot (post_canonize p),
-                      CUnix.canonical_path_name p) in
-        (t,(ml_new::ml_inc,q_inc,r_inc),d)
-     | Include (p,l) ->
-        let q_new = (CUnix.remove_path_dot (post_canonize p),l,
-		     CUnix.canonical_path_name p) in
-        (t,(ml_inc,q_new::q_inc,r_inc),d)
-     | RInclude (p,l) ->
-        let r_new = (CUnix.remove_path_dot (post_canonize p),l,
-		     CUnix.canonical_path_name p) in
-        (t,(ml_inc,q_inc,r_new::r_inc),d)
-     | Def (v,def) ->
-        (t,i,(args,(v,def)::defs))
-     | Arg a ->
-        (t,i,(a::args,defs)))
-    args (([],([],[],[],[],[]),[],[]),([],[],[]),([],[]))
+let cmdline_args_to_project ~curdir args =
+  process_cmd_line curdir (mk_project None None None true) args
 
 let read_project_file f =
-  split_arguments
-    (snd (process_cmd_line (Filename.dirname f) (Some f, None, NoInstall, true) [] (parse f)))
-
-let args_from_project file project_files default_name =
-  let build_cmd_line ml_inc i_inc r_inc args =
-    List.fold_right (fun (_,i) o -> "-I" :: i :: o) ml_inc
-      (List.fold_right (fun (_,l,i) o -> "-Q" :: i :: l :: o) i_inc
-        (List.fold_right (fun (_,l,p) o -> "-R" :: p :: l :: o) r_inc
-	  (List.fold_right (fun a o -> parse_args (Stream.of_string a) @ o) args [])))
-  in try
-      let (fname,(_,(ml_inc,i_inc,r_inc),(args,_))) = List.hd project_files in
-	fname, build_cmd_line ml_inc i_inc r_inc args
-    with Failure _ ->
-      let rec find_project_file dir = try
-	let fname = Filename.concat dir default_name in
-	let ((v_files,_,_,_),(ml_inc,i_inc,r_inc),(args,_)) =
-          read_project_file fname in
-	fname, build_cmd_line ml_inc i_inc r_inc args
-      with Sys_error s ->
-	let newdir = Filename.dirname dir in
-	  if dir = newdir then "",[] else find_project_file newdir
-      in find_project_file (Filename.dirname file)
+  process_cmd_line (Filename.dirname f)
+    (mk_project (Some f) None (Some NoInstall) true) (parse f)
+
+let rec find_project_file ~from ~projfile_name =
+  let fname = Filename.concat from projfile_name in
+  if Sys.file_exists fname then Some fname
+  else
+    let newdir = Filename.dirname from in
+    if newdir = "" || newdir = "/" then None
+    else find_project_file ~from:newdir ~projfile_name
+;;
+
+let coqtop_args_from_project
+  { ml_includes; r_includes; q_includes; extra_args }
+=
+  let map = List.map in
+  let args =
+    map (fun { canonical_path = i } -> ["-I"; i]) ml_includes @
+    map (fun ({ canonical_path = i }, l) -> ["-Q"; i; l]) q_includes @
+    map (fun ({ canonical_path = p }, l) -> ["-R"; p; l]) r_includes @
+    [extra_args] in
+  List.flatten args
+;;
 
 (* vim:set ft=ocaml: *)
diff --git a/lib/coqProject_file.mli b/lib/coqProject_file.mli
index 36513dbde..2bcf658fc 100644
--- a/lib/coqProject_file.mli
+++ b/lib/coqProject_file.mli
@@ -6,63 +6,44 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-type target =
-  | ML of string (* ML file : foo.ml -> (ML "foo.ml") *)
-  | MLI of string (* MLI file : foo.mli -> (MLI "foo.mli") *)
-  | ML4 of string (* ML4 file : foo.ml4 -> (ML4 "foo.ml4") *)
-  | MLLIB of string (* MLLIB file : foo.mllib -> (MLLIB "foo.mllib") *)
-  | MLPACK of string (* MLLIB file : foo.mlpack -> (MLLIB "foo.mlpack") *)
-  | V of string  (* V file : foo.v -> (V "foo") *)
-  | Arg of string
-  | Special of string * string * bool * string
-    (* file, dependencies, is_phony, command *)
-  | Subdir of string
-  | Def of string * string (* X=foo -> Def ("X","foo") *)
-  | MLInclude of string (* -I physicalpath *)
-  | Include of string * string (* -Q physicalpath logicalpath *)
-  | RInclude of string * string (* -R physicalpath logicalpath *)
-
-type install =
+exception Parsing_error of string
+
+type project = {
+  project_file  : string option;
+  makefile : string option;
+  install_kind  : install option;
+  use_ocamlopt : bool;
+
+  v_files : string list;
+  mli_files : string list;
+  ml4_files : string list;
+  ml_files : string list;
+  mllib_files : string list;
+  mlpack_files : string list;
+
+  extra_targets : extra_target list;
+  subdirs : string list;
+  ml_includes : path list;
+  r_includes  : (path * logic_path) list;
+  q_includes  : (path * logic_path) list;
+  extra_args : string list;
+  defs : (string * string) list;
+}
+and extra_target = {
+  target : string;
+  dependencies : string;
+  phony : bool;
+  command : string;
+}
+and logic_path = string
+and path = { path : string; canonical_path : string }
+and install =
   | NoInstall
   | TraditionalInstall
   | UserInstall
-  | UnspecInstall
-
-exception Parsing_error
-
-val args_from_project : 
-           string ->
-           (string *
-            ('a *
-             (('b * string) list * ('c * string * string) list *
-              ('d * string * string) list) *
-             (string list * 'e)))
-           list -> string -> string * string list
-
-val read_project_file :
-           string ->
-           (string list *
-            (string list * string list * string list * string list *
-             string list) *
-            (string * string * bool * string) list * string list) *
-           ((string * string) list * (string * string * string) list *
-            (string * string * string) list) *
-           (string list * (string * string) list)
-
-val process_cmd_line :
-           string ->
-           string option * string option * install * bool ->
-           target list ->
-           string list ->
-           (string option * string option * install * bool) * target list
 
-val split_arguments :
-           target list ->
-           (string list *
-            (string list * string list * string list * string list *
-             string list) *
-            (string * string * bool * string) list * string list) *
-           ((string * string) list * (string * string * string) list *
-            (string * string * string) list) *
-           (string list * (string * string) list)
+val cmdline_args_to_project : curdir:string -> string list -> project
+val read_project_file : string -> project
+val coqtop_args_from_project : project -> string list
+val find_project_file : from:string -> projfile_name:string -> string option
 
diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml
index d72916232..0b2c40170 100644
--- a/tools/coq_makefile.ml
+++ b/tools/coq_makefile.ml
@@ -282,7 +282,7 @@ let where_put_doc = function
 	"$(INSTALLDEFAULTROOT)"
 
 let install (vfiles,(mlis,ml4s,mls,mllibs,mlpacks),_,sds) inc = function
-  |CoqProject_file.NoInstall -> ()
+  |Some CoqProject_file.NoInstall -> ()
   |is_install ->
     let not_empty = function |[] -> false |_::_ -> true in
     let cmos = List.rev_append mlpacks (List.rev_append mls ml4s) in
@@ -295,7 +295,7 @@ let install (vfiles,(mlis,ml4s,mls,mllibs,mlpacks),_,sds) inc = function
        ("CMOFILES",cmos);("CMIFILES",cmis);("CMAFILES",mllibs)]
       inc in
     let doc_dir = where_put_doc inc in
-    if is_install = CoqProject_file.UnspecInstall then begin
+    if is_install = None then begin
 	print "userinstall:\n\t+$(MAKE) USERINSTALL=true install\n\n"
     end;
     if not_empty cmxss then begin
@@ -533,8 +533,8 @@ let variables is_install opt (args,defs) =
 \n  $(CAMLP4EXTEND) $(GRAMMARS) $(CAMLP4OPTIONS) -impl'\n\n";
     end;
     match is_install with
-      | CoqProject_file.NoInstall -> ()
-      | CoqProject_file.UnspecInstall ->
+      | Some CoqProject_file.NoInstall -> ()
+      | None ->
         section "Install Paths.";
 	print "ifdef USERINSTALL\n";
         print "XDG_DATA_HOME?=\"$(HOME)/.local/share\"\n";
@@ -545,13 +545,13 @@ let variables is_install opt (args,defs) =
         print "COQDOCINSTALL=\"${DOCDIR}user-contrib\"\n";
         print "COQTOPINSTALL=\"${COQLIB}toploop\"\n";
 	print "endif\n\n"
-      | CoqProject_file.TraditionalInstall ->
+      | Some CoqProject_file.TraditionalInstall ->
           section "Install Paths.";
           print "COQLIBINSTALL=\"${COQLIB}user-contrib\"\n";
           print "COQDOCINSTALL=\"${DOCDIR}user-contrib\"\n";
           print "COQTOPINSTALL=\"${COQLIB}toploop\"\n";
           print "\n"
-      | CoqProject_file.UserInstall ->
+      | Some CoqProject_file.UserInstall ->
           section "Install Paths.";
           print "XDG_DATA_HOME?=\"$(HOME)/.local/share\"\n";
           print "COQLIBINSTALL=$(XDG_DATA_HOME)/coq\n";
@@ -890,16 +890,38 @@ let merlin targets (ml_inc,_,_) =
   print "\n"
 
 let do_makefile args =
+  let open CoqProject_file in
   let has_file var = function
     |[] -> var := false
     |_::_ -> var := true in
-  let (project_file,makefile,is_install,opt),l =
-    try
-      CoqProject_file.process_cmd_line Filename.current_dir_name
-       (None,None,CoqProject_file.UnspecInstall,true) [] args
-    with CoqProject_file.Parsing_error -> usage () in
-  let (v_f,(mli_f,ml4_f,ml_f,mllib_f,mlpack_f),sps,sds as targets), inc, defs =
-    CoqProject_file.split_arguments l in
+  let { 
+    project_file = project_file;
+    makefile;
+    install_kind = is_install;
+    use_ocamlopt = opt;
+    v_files = v_f;
+    mli_files = mli_f;
+    ml4_files = ml4_f;
+    ml_files = ml_f;
+    mllib_files = mllib_f;
+    mlpack_files = mlpack_f;
+    extra_targets;
+    subdirs = sds;
+    ml_includes;
+    r_includes;
+    q_includes;
+    extra_args;
+    defs;
+  } =
+    try cmdline_args_to_project Filename.current_dir_name args
+    with Parsing_error s -> prerr_endline s; usage () in
+  let sps = List.map (fun { target = fn; dependencies = d; phony = p; command = c } -> fn, d, p, c) extra_targets in
+  let targets = (v_f,(mli_f,ml4_f,ml_f,mllib_f,mlpack_f),sps,sds) in
+  let inc =
+    List.map (fun ({ path = p; canonical_path = c }) -> p,c) ml_includes,
+    List.map (fun ({ path = p; canonical_path = c },l) -> p,l,c) q_includes,
+    List.map (fun ({ path = p; canonical_path = c },l) -> p,l,c) r_includes in
+  let defs = extra_args, defs in
 
   let () = match project_file with |None -> () |Some f -> make_name := f in
   let () = match makefile with
@@ -920,7 +942,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 <> CoqProject_file.NoInstall then begin
+  if is_install <> (Some CoqProject_file.NoInstall) then begin
     warn_install_at_root_directory targets inc;
   end;
   check_overlapping_include inc;