Add source (project file / command line) to project fields.

4 files changed, 102 insertions, 82 deletions

diff --git a/lib/coqProject_file.ml4 b/lib/coqProject_file.ml4
index f1ec4b455..238e26c42 100644
--- a/lib/coqProject_file.ml4
+++ b/lib/coqProject_file.ml4
@@ -6,29 +6,32 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+type arg_source = CmdLine | ProjectFile
+
+type 'a sourced = { thing : 'a; source : arg_source }
+
 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;
-
-  ml_includes : path list;
-  r_includes  : (path * logic_path) list;
-  q_includes  : (path * logic_path) list;
-  extra_args : string list;
-  defs : (string * string) list;
-  
-  extra_targets : extra_target list;
-  subdirs : string list;
-
-  cmdline_vfiles : string list;
+  v_files : string sourced list;
+  mli_files : string sourced list;
+  ml4_files : string sourced list;
+  ml_files : string sourced list;
+  mllib_files : string sourced list;
+  mlpack_files : string sourced list;
+
+  ml_includes : path sourced list;
+  r_includes  : (path * logic_path) sourced list;
+  q_includes  : (path * logic_path) sourced list;
+  extra_args : string sourced list;
+  defs : (string * string) sourced list;
+
+  (* deprecated in favor of a Makefile.local using :: rules *)
+  extra_targets : extra_target sourced list;
+  subdirs : string sourced list;
 }
 and extra_target = {
   target : string;
@@ -63,7 +66,6 @@ let mk_project project_file makefile install_kind use_ocamlopt = {
   q_includes = [];
   extra_args = [];
   defs = [];
-  cmdline_vfiles = [];
 }
 
 (********************* utils ********************************************)
@@ -115,6 +117,7 @@ let exists_dir dir =
 
 let process_cmd_line orig_dir proj args =
   let parsing_project_file = ref (proj.project_file <> None) in
+  let sourced x = { thing = x; source = if !parsing_project_file then ProjectFile else CmdLine } in
   let orig_dir = (* avoids turning foo.v in ./foo.v *)
     if orig_dir = "." then "" else orig_dir in
   let error s = Format.eprintf "@[%a]@@\n%!" Pp.pp_with Pp.(str (s^".")); exit 1 in
@@ -144,17 +147,17 @@ let process_cmd_line orig_dir proj args =
     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
+    aux { proj with extra_targets = proj.extra_targets @ [sourced 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
+    aux { proj with extra_targets = proj.extra_targets @ [sourced tgt] } r
 
   | "-Q" :: d :: lp :: r ->
-    aux { proj with q_includes = proj.q_includes @ [mk_path d,lp] } r
+    aux { proj with q_includes = proj.q_includes @ [sourced (mk_path d,lp)] } r
   | "-I" :: d :: r ->
-    aux { proj with ml_includes = proj.ml_includes @ [mk_path d] } r
+    aux { proj with ml_includes = proj.ml_includes @ [sourced (mk_path d)] } r
   | "-R" :: d :: lp :: r ->
-    aux { proj with r_includes = proj.r_includes @ [mk_path d,lp] } r
+    aux { proj with r_includes = proj.r_includes @ [sourced (mk_path d,lp)] } r
 
   | "-f" :: file :: r ->
     if !parsing_project_file then
@@ -179,26 +182,21 @@ let process_cmd_line orig_dir proj args =
       error "Option -o given more than once";
     aux { proj with makefile = Some file } r  
   | v :: "=" :: def :: r ->
-    aux { proj with defs = proj.defs @ [v,def] } r
+    aux { proj with defs = proj.defs @ [sourced (v,def)] } r
   | "-arg" :: a :: r ->
-    aux { proj with extra_args = proj.extra_args @ [a] } r
+    aux { proj with extra_args = proj.extra_args @ [sourced a] } r
   | f :: r ->
       let f = CUnix.correct_path f orig_dir in
       let proj =
-        if exists_dir f then { proj with subdirs = proj.subdirs @ [f] }
+        if exists_dir f then { proj with subdirs = proj.subdirs @ [sourced f] }
         else match CUnix.get_extension f with
           | ".v" ->
-            let { cmdline_vfiles } = proj in
-            let cmdline_vfiles = if !parsing_project_file
-              then cmdline_vfiles
-              else cmdline_vfiles @ [f]
-            in
-            { proj with v_files = proj.v_files @ [f]; cmdline_vfiles }
-        | ".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] }
+            { proj with v_files = proj.v_files @ [sourced f] }
+        | ".ml" -> { proj with ml_files = proj.ml_files @ [sourced f] }
+        | ".ml4" -> { proj with ml4_files = proj.ml4_files @ [sourced f] }
+        | ".mli" -> { proj with mli_files = proj.mli_files @ [sourced f] }
+        | ".mllib" -> { proj with mllib_files = proj.mllib_files @ [sourced f] }
+        | ".mlpack" -> { proj with mlpack_files = proj.mlpack_files @ [sourced f] }
         | _ -> raise (Parsing_error ("Unknown option "^f)) in
       aux proj r
  in
@@ -222,16 +220,26 @@ let rec find_project_file ~from ~projfile_name =
     else find_project_file ~from:newdir ~projfile_name
 ;;
 
+let map_sourced_list f l = List.map (fun x -> f x.thing) l
+;;
+
 let coqtop_args_from_project
   { ml_includes; r_includes; q_includes; extra_args }
 =
-  let map = List.map in
+  let map = map_sourced_list  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
+    [map (fun x -> x) extra_args] in
   List.flatten args
 ;;
 
+let filter_cmdline l = CList.map_filter
+    (function {thing; source=CmdLine} -> Some thing | {source=ProjectFile} -> None)
+    l
+;;
+
+let forget_source {thing} = thing
+
 (* vim:set ft=ocaml: *)
diff --git a/lib/coqProject_file.mli b/lib/coqProject_file.mli
index 8702da1f4..68bc5dfe4 100644
--- a/lib/coqProject_file.mli
+++ b/lib/coqProject_file.mli
@@ -8,30 +8,32 @@
 
 exception Parsing_error of string
 
+type arg_source = CmdLine | ProjectFile
+
+type 'a sourced = { thing : 'a; source : arg_source }
+
 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;
+  v_files : string sourced list;
+  mli_files : string sourced list;
+  ml4_files : string sourced list;
+  ml_files : string sourced list;
+  mllib_files : string sourced list;
+  mlpack_files : string sourced 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;
+  ml_includes : path sourced list;
+  r_includes  : (path * logic_path) sourced list;
+  q_includes  : (path * logic_path) sourced list;
+  extra_args : string sourced list;
+  defs : (string * string) sourced list;
 
   (* deprecated in favor of a Makefile.local using :: rules *)
-  extra_targets : extra_target list;
-  subdirs : string list;
-
-  cmdline_vfiles : string list; (** The subset of [v_files] not from the [project_file].*)
+  extra_targets : extra_target sourced list;
+  subdirs : string sourced list;
 }
 and extra_target = {
   target : string;
@@ -51,3 +53,8 @@ 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
 
+val map_sourced_list : ('a -> 'b) -> 'a sourced list -> 'b list
+
+val filter_cmdline : 'a sourced list -> 'a list
+
+val forget_source : 'a sourced -> 'a
diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml
index d495cde2f..ae29c95f4 100644
--- a/tools/coq_makefile.ml
+++ b/tools/coq_makefile.ml
@@ -11,6 +11,8 @@
 open CoqProject_file
 open Printf
 
+let (>) f g = fun x -> g (f x)
+
 let output_channel = ref stdout
 let makefile_name = ref "Makefile"
 let make_name = ref ""
@@ -173,21 +175,22 @@ let generate_conf_extra_target oc sps =
   in
     if sps <> [] then
       section oc "Extra targets. (-extra and -extra-phony, DEPRECATED)";
-    List.iter pr_path sps
+    List.iter (forget_source > pr_path) sps
 
 let generate_conf_subdirs oc sds =
   if sds <> [] then section oc "Subdirectories. (DEPRECATED)";
-  List.iter (fprintf oc ".PHONY:%s\n") sds;
-  List.iter (fprintf oc "post-all::\n\tcd \"%s\" && $(MAKE) all\n") sds;
-  List.iter (fprintf oc "clean::\n\tcd \"%s\" && $(MAKE) clean\n") sds;
-  List.iter (fprintf oc "archclean::\n\tcd \"%s\" && $(MAKE) archclean\n") sds;
-  List.iter (fprintf oc "install-extra::\n\tcd \"%s\" && $(MAKE) install\n") sds
+  let iter f = List.iter (forget_source > f) in
+  iter (fprintf oc ".PHONY:%s\n") sds;
+  iter (fprintf oc "post-all::\n\tcd \"%s\" && $(MAKE) all\n") sds;
+  iter (fprintf oc "clean::\n\tcd \"%s\" && $(MAKE) clean\n") sds;
+  iter (fprintf oc "archclean::\n\tcd \"%s\" && $(MAKE) archclean\n") sds;
+  iter (fprintf oc "install-extra::\n\tcd \"%s\" && $(MAKE) install\n") sds
    
 
 let generate_conf_includes oc { ml_includes; r_includes; q_includes } =
   section oc "Path directives (-I, -R, -Q).";
   let module S = String in
-  let open List in
+  let map = map_sourced_list in
   let dash1 opt v = sprintf "-%s %s" opt (quote v) in
   let dash2 opt v1 v2 = sprintf "-%s %s %s" opt (quote v1) (quote v2) in
   fprintf oc "COQMF_OCAMLLIBS = %s\n"
@@ -217,10 +220,10 @@ let generate_conf_coq_config oc args =
 ;;
 
 let generate_conf_files oc
-  { v_files; mli_files; ml4_files; ml_files; mllib_files; mlpack_files; cmdline_vfiles }
+  { v_files; mli_files; ml4_files; ml_files; mllib_files; mlpack_files; }
 =
   let module S = String in
-  let open List in
+  let map = map_sourced_list in
   section oc "Project files.";
   fprintf oc "COQMF_VFILES = %s\n"      (S.concat " " (map quote v_files));
   fprintf oc "COQMF_MLIFILES = %s\n"    (S.concat " " (map quote mli_files));
@@ -228,7 +231,8 @@ let generate_conf_files oc
   fprintf oc "COQMF_ML4FILES = %s\n"    (S.concat " " (map quote ml4_files));
   fprintf oc "COQMF_MLPACKFILES = %s\n" (S.concat " " (map quote mlpack_files));
   fprintf oc "COQMF_MLLIBFILES = %s\n"  (S.concat " " (map quote mllib_files));
-  fprintf oc "COQMF_CMDLINE_VFILES = %s\n" (S.concat " " (map quote cmdline_vfiles));
+  let cmdline_vfiles = filter_cmdline v_files in
+  fprintf oc "COQMF_CMDLINE_VFILES = %s\n" (S.concat " " (List.map quote cmdline_vfiles));
 ;;
 
 let rec all_start_with prefix = function
@@ -245,12 +249,12 @@ let rec logic_gcd acc = function
       else acc
 
 let generate_conf_doc oc { defs; q_includes; r_includes } =
-  let includes = List.map snd (q_includes @ r_includes) in
+  let includes = List.map (forget_source > snd) (q_includes @ r_includes) in
   let logpaths = List.map (CString.split '.') includes in
   let gcd = logic_gcd [] logpaths in
   let root =
     if gcd = [] then
-      if not (List.mem_assoc "INSTALLDEFAULTROOT" defs) then begin
+      if not (List.exists (fun x -> fst x.thing = "INSTALLDEFAULTROOT") defs) then begin
          let destination = "orphan_" ^ (String.concat "_" includes) in
          eprintf "Warning: no common logical root\n";
          eprintf "Warning: in such case INSTALLDEFAULTROOT must be defined\n";
@@ -263,9 +267,9 @@ let generate_conf_doc oc { defs; q_includes; r_includes } =
 
 let generate_conf_defs oc { defs; extra_args } =
   section oc "Extra variables.";
-  List.iter (fun (k,v) -> Printf.fprintf oc "%s = %s\n" k v) defs;
+  List.iter (forget_source > (fun (k,v) -> Printf.fprintf oc "%s = %s\n" k v)) defs;
   Printf.fprintf oc "COQMF_OTHERFLAGS = %s\n"
-    (String.concat " " extra_args)
+    (String.concat " " (List.map forget_source extra_args))
 
 let generate_conf oc project args  =
   fprintf oc "# This configuration file was generated by running:\n";
@@ -283,10 +287,10 @@ let ensure_root_dir
   ({ ml_includes; r_includes; q_includes;
      v_files; ml_files; mli_files; ml4_files;
      mllib_files; mlpack_files } as project)
-=
-  let open List in
+  =
+  let exists f = List.exists (forget_source > f) in
   let here = Sys.getcwd () in
-  let not_tops = List.for_all (fun s -> s <> Filename.basename s) in
+  let not_tops = List.for_all (fun s -> s.thing <> Filename.basename s.thing) in
   if exists (fun { canonical_path = x } -> x = here) ml_includes
   || exists (fun ({ canonical_path = x },_) -> is_prefix x here) r_includes
   || exists (fun ({ canonical_path = x },_) -> is_prefix x here) q_includes
@@ -296,10 +300,11 @@ let ensure_root_dir
   then
     project
   else
+    let source x = {thing=x; source=CmdLine} in
     let here_path = { path = "."; canonical_path = here } in
     { project with
-        ml_includes = here_path :: ml_includes;
-        r_includes = (here_path, "Top") :: r_includes }
+        ml_includes = source here_path :: ml_includes;
+        r_includes = source (here_path, "Top") :: r_includes }
 ;;
 
 let warn_install_at_root_directory 
@@ -310,15 +315,15 @@ let warn_install_at_root_directory
   let open CList in
   let inc_top_p =
     map_filter
-      (fun ({ path } ,ldir) -> if ldir = "" then Some path else None)
+      (fun {thing=({ path } ,ldir)} -> if ldir = "" then Some path else None)
       (r_includes @ q_includes) in
   let files =
     v_files @ mli_files @ ml4_files @ ml_files @ mllib_files @ mlpack_files in
-  let bad = filter (fun f -> mem (Filename.dirname f) inc_top_p) files in
+  let bad = filter (fun f -> mem (Filename.dirname f.thing) inc_top_p) files in
   if bad <> [] then begin
     eprintf "Warning: No file should be installed at the root of Coq's library.\n";
     eprintf "Warning: No logical path (-R, -Q) applies to these files:\n";
-    List.iter (fun x -> eprintf "Warning:  %s\n" x) bad;
+    List.iter (fun x -> eprintf "Warning:  %s\n" x.thing) bad;
     eprintf "\n";
   end
 ;;
@@ -327,10 +332,10 @@ let check_overlapping_include { q_includes; r_includes } =
   let pwd = Sys.getcwd () in
   let aux = function
     | [] -> ()
-    | ({ path; canonical_path }, _) :: l ->
+    | {thing = { path; canonical_path }, _} :: l ->
 	if not (is_prefix pwd canonical_path) then
 	  eprintf "Warning: %s (used in -R or -Q) is not a subdirectory of the current directory\n\n" path;
-	List.iter (fun ({ path = p; canonical_path = cp }, _) ->
+        List.iter (fun {thing={ path = p; canonical_path = cp }, _} ->
 	  if is_prefix canonical_path cp  || is_prefix cp canonical_path then
 	    eprintf "Warning: %s and %s overlap (used in -R or -Q)\n\n"
               path p) l
@@ -353,7 +358,7 @@ let destination_of { ml_includes; q_includes; r_includes; } file =
     clean_path (physical_dir_of_logical_dir logic ^ "/" ^
                 chop_prefix canonical_path file_dir ^ "/") in
   let candidates =
-    CList.map_filter (fun ({ canonical_path }, logic) ->
+    CList.map_filter (fun {thing={ canonical_path }, logic} ->
       if is_prefix canonical_path file_dir then
         Some(mk_destination logic canonical_path)
       else None) includes
@@ -363,10 +368,10 @@ let destination_of { ml_includes; q_includes; r_includes; } file =
      (* BACKWARD COMPATIBILITY: -I into the only logical root *)
      begin match
         r_includes,
-        List.find (fun { canonical_path = p } -> is_prefix p file_dir)
+        List.find (fun {thing={ canonical_path = p }} -> is_prefix p file_dir)
           ml_includes
      with
-        | [{ canonical_path }, logic], { canonical_path = p } ->
+        | [{thing={ canonical_path }, logic}], {thing={ canonical_path = p }} ->
             let destination =
               clean_path (physical_dir_of_logical_dir logic ^ "/" ^
                           chop_prefix p file_dir ^ "/") in
diff --git a/tools/coqdep.ml b/tools/coqdep.ml
index 4569994b4..26a2b2696 100644
--- a/tools/coqdep.ml
+++ b/tools/coqdep.ml
@@ -464,7 +464,7 @@ let split_period = Str.split (Str.regexp (Str.quote "."))
 let treat_coqproject f =
   let open CoqProject_file in
   let project = read_project_file f in
-  List.iter (treat_file None) project.v_files
+  List.iter (fun f -> treat_file None f.thing) project.v_files
 
 let rec parse = function
   | "-c" :: ll -> option_c := true; parse ll