aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--ide/project_file.ml448
-rw-r--r--tools/coq_makefile.ml101
2 files changed, 92 insertions, 57 deletions
diff --git a/ide/project_file.ml4 b/ide/project_file.ml4
index 28df1fca3..41dc1befa 100644
--- a/ide/project_file.ml4
+++ b/ide/project_file.ml4
@@ -10,7 +10,8 @@ type target =
(* file, dependencies, is_phony, command *)
| Subdir of string
| Def of string * string (* X=foo -> Def ("X","foo") *)
- | Include of string
+ | MLInclude of string (* -I physicalpath *)
+ | Include of string * string (* -Q physicalpath logicalpath *)
| RInclude of string * string (* -R physicalpath logicalpath *)
type install =
@@ -80,11 +81,14 @@ let rec process_cmd_line orig_dir ((project_file,makefile,install,opt) as opts)
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
+ | "-Q" :: d :: lp :: r ->
+ process_cmd_line orig_dir opts ((Include (CUnix.correct_path d orig_dir, lp)) :: l) r
| "-I" :: d :: r ->
- process_cmd_line orig_dir opts ((Include (CUnix.correct_path d orig_dir)) :: l) r
+ process_cmd_line orig_dir opts ((MLInclude (CUnix.correct_path d orig_dir)) :: l) r
+ | "-R" :: p :: "-as" :: lp :: r
| "-R" :: p :: lp :: r ->
process_cmd_line orig_dir opts (RInclude (CUnix.correct_path p orig_dir,lp) :: l) r
- | ("-R"|"-I"|"-custom"|"-extra"|"-extra-phony") :: _ ->
+ | ("-Q"|"-R"|"-I"|"-custom"|"-extra"|"-extra-phony") :: _ ->
raise Parsing_error
| "-f" :: file :: r ->
let file = CUnix.remove_path_dot (CUnix.correct_path file orig_dir) in
@@ -129,7 +133,7 @@ let rec post_canonize f =
if dir = Filename.current_dir_name then f else post_canonize dir
else f
-(* Return: ((v,(mli,ml4,ml,mllib,mlpack),special,subdir),(i_inc,r_inc),(args,defs)) *)
+(* Return: ((v,(mli,ml4,ml,mllib,mlpack),special,subdir),(ml_inc,q_inc,r_inc),(args,defs)) *)
let split_arguments =
let rec aux = function
| V n :: r ->
@@ -153,17 +157,24 @@ let split_arguments =
let (v,m,o,s),i,d = aux r in ((v,m,(n,dep,is_phony,c)::o,s),i,d)
| Subdir n :: r ->
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 = aux r in (t,((CUnix.remove_path_dot (post_canonize p),
- CUnix.canonical_path_name p)::i,r),d)
+ | MLInclude p :: r ->
+ let t,(ml,q,r),d = aux r in (t,((CUnix.remove_path_dot (post_canonize p),
+ CUnix.canonical_path_name p)::ml,q,r),d)
+ | Include (p,l) :: r ->
+ let t,(ml,i,r),d = aux r in
+ let i_new = (CUnix.remove_path_dot (post_canonize p),l,
+ CUnix.canonical_path_name p) in
+ (t,(ml,i_new::i,r),d)
| RInclude (p,l) :: r ->
- let t,(i,r),d = aux r in (t,(i,(CUnix.remove_path_dot (post_canonize p),l,
- CUnix.canonical_path_name p)::r),d)
+ let t,(ml,i,r),d = aux r in
+ let r_new = (CUnix.remove_path_dot (post_canonize p),l,
+ CUnix.canonical_path_name p) in
+ (t,(ml,i,r_new::r),d)
| Def (v,def) :: r ->
let t,i,(args,defs) = aux r in (t,i,(args,(v,def)::defs))
| Arg a :: r ->
let t,i,(args,defs) = aux r in (t,i,(a::args,defs))
- | [] -> ([],([],[],[],[],[]),[],[]),([],[]),([],[])
+ | [] -> ([],([],[],[],[],[]),[],[]),([],[],[]),([],[])
in aux
let read_project_file f =
@@ -175,21 +186,22 @@ let args_from_project file project_files default_name =
let contains_file dir =
List.exists (fun x -> is_f (CUnix.correct_path x dir))
in
- let build_cmd_line i_inc r_inc args =
- List.fold_right (fun (_,i) o -> "-I" :: i :: 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 []))
+ 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 (_,(_,(i_inc,r_inc),(args,_))) =
+ let (_,(_,(ml_inc,i_inc,r_inc),(args,_))) =
List.find (fun (dir,((v_files,_,_,_),_,_)) ->
contains_file dir v_files) project_files in
- build_cmd_line i_inc r_inc args
+ build_cmd_line ml_inc i_inc r_inc args
with Not_found ->
let rec find_project_file dir = try
- let ((v_files,_,_,_),(i_inc,r_inc),(args,_)) =
+ let ((v_files,_,_,_),(ml_inc,i_inc,r_inc),(args,_)) =
read_project_file (Filename.concat dir default_name) in
if contains_file dir v_files
- then build_cmd_line i_inc r_inc args
+ then build_cmd_line ml_inc i_inc r_inc args
else let newdir = Filename.dirname dir in
if dir = newdir then [] else find_project_file newdir
with Sys_error s ->
diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml
index 9aac367b0..e6da7320a 100644
--- a/tools/coq_makefile.ml
+++ b/tools/coq_makefile.ml
@@ -72,6 +72,9 @@ coq_makefile [subdirectory] .... [file.v] ... [file.ml[i4]?] ...
[-R physicalpath logicalpath]: look for Coq dependencies resursively
starting from \"physicalpath\". The logical path associated to the
physical path is \"logicalpath\".
+[-Q physicalpath logicalpath]: look for Coq dependencies starting from
+ \"physicalpath\". The logical path associated to the physical path
+ is \"logicalpath\".
[VARIABLE = value]: Add the variable definition \"VARIABLE=value\"
[-byte]: compile with byte-code version of coq
[-opt]: compile with native-code version of coq
@@ -115,14 +118,15 @@ let standard opt =
print "\t$(MAKE) all \"OPT:="; print (if opt then "-opt" else "-byte");
print "\"\n\n"
-let classify_files_by_root var files (inc_i,inc_r) =
- if not (List.exists (fun (pdir,_,_) -> pdir = ".") inc_r) then
+let classify_files_by_root var files (inc_ml,inc_i,inc_r) =
+ if not (List.exists (fun (pdir,_,_) -> pdir = ".") inc_r)
+ && not (List.exists (fun (pdir,_,_) -> pdir = ".") inc_i) then
begin
let absdir_of_files = List.rev_map
(fun x -> CUnix.canonical_path_name (Filename.dirname x))
files in
(* files in scope of a -I option (assuming they are no overlapping) *)
- let has_inc_i = List.exists (fun (_,a) -> List.mem a absdir_of_files) inc_i in
+ let has_inc_i = List.exists (fun (_,a) -> List.mem a absdir_of_files) inc_ml in
if has_inc_i then
begin
printf "%sINC=" var;
@@ -131,7 +135,7 @@ let classify_files_by_root var files (inc_i,inc_r) =
then printf
"$(filter $(wildcard %s/*),$(%s)) "
pdir var
- ) inc_i;
+ ) inc_ml;
printf "\n";
end;
(* Files in the scope of a -R option (assuming they are disjoint) *)
@@ -139,38 +143,38 @@ let classify_files_by_root var files (inc_i,inc_r) =
if List.exists (is_prefix abspdir) absdir_of_files then
printf "%s%d=$(patsubst %s/%%,%%,$(filter %s/%%,$(%s)))\n"
var i pdir pdir var)
- inc_r;
+ (inc_i@inc_r);
end
-let vars_to_put_by_root var_x_files_l (inc_i,inc_r) =
+let vars_to_put_by_root var_x_files_l (inc_ml,inc_i,inc_r) =
let var_x_absdirs_l = List.rev_map
(fun (v,l) -> (v,List.rev_map (fun x -> CUnix.canonical_path_name (Filename.dirname x)) l))
var_x_files_l in
let var_filter f g = List.fold_left (fun acc (var,dirs) ->
if f dirs
then (g var)::acc else acc) [] var_x_absdirs_l in
- try
(* All files caught by a -R . option (assuming it is the only one) *)
- let ldir = match inc_r with
- |[(".",t,_)] -> t
- |l -> let out = List.assoc "." (List.rev_map (fun (p,l,_) -> (p,l)) inc_r) in
- let () = prerr_string "Warning: install rule assumes that -R . _ is the only -R option" in
- out in
- (None,[".",physical_dir_of_logical_dir ldir,List.rev_map fst var_x_files_l])
- with Not_found ->
- (
- (* vars for -I options *)
- Some (var_filter (fun l -> List.exists (fun (_,a) -> List.mem a l) inc_i) (fun x -> x)),
+ match inc_i@inc_r with
+ |[(".",t,_)] -> (None,[".",physical_dir_of_logical_dir t,List.rev_map fst var_x_files_l])
+ |l ->
+ try
+ let out = List.assoc "." (List.rev_map (fun (p,l,_) -> (p,l)) l) in
+ let () = prerr_string "Warning: install rule assumes that -R/-Q . _ is the only -R/-Q option" in
+ (None,[".",physical_dir_of_logical_dir out,List.rev_map fst var_x_files_l])
+ with Not_found ->
+ (
+ (* vars for -Q options *)
+ Some (var_filter (fun l -> List.exists (fun (_,a) -> List.mem a l) inc_ml) (fun x -> x)),
(* (physical dir, physical dir of logical path,vars) for -R options
(assuming physical dirs are disjoint) *)
- if inc_r = [] then
+ if l = [] then
[".","$(INSTALLDEFAULTROOT)",[]]
else
Util.List.fold_left_i (fun i out (pdir,ldir,abspdir) ->
let vars_r = var_filter (List.exists (is_prefix abspdir)) (fun x -> x^string_of_int i) in
let pdir' = physical_dir_of_logical_dir ldir in
- (pdir,pdir',vars_r)::out) 1 [] inc_r
- )
+ (pdir,pdir',vars_r)::out) 1 [] l
+ )
let install_include_by_root =
let install_dir for_i (pdir,pdir',vars) =
@@ -220,15 +224,29 @@ in
|Some v_i,l -> List.iter (uninstall_dir (fun () -> uninstall_i v_i)) l
let where_put_doc = function
- |_,[] -> "$(INSTALLDEFAULTROOT)";
- |_,((_,lp,_)::q as inc_r) ->
+ |_,[],[] -> "$(INSTALLDEFAULTROOT)";
+ |_,((_,lp,_)::q as inc_i),[] ->
let pr = List.fold_left (fun a (_,b,_) -> string_prefix a b) lp q in
if (pr <> "") &&
- ((List.exists (fun(_,b,_) -> b = pr) inc_r) || pr.[String.length pr - 1] = '.')
+ ((List.exists (fun(_,b,_) -> b = pr) inc_i)
+ || pr.[String.length pr - 1] = '.')
then
physical_dir_of_logical_dir pr
else
- let () = prerr_string "Warning: -R options don't have a correct common prefix,
+ let () = prerr_string "Warning: -Q options don't have a correct common prefix,
+ install-doc will put anything in $INSTALLDEFAULTROOT\n" in
+ "$(INSTALLDEFAULTROOT)"
+ |_,inc_i,((_,lp,_)::q as inc_r) ->
+ let pr = List.fold_left (fun a (_,b,_) -> string_prefix a b) lp q in
+ let pr = List.fold_left (fun a (_,b,_) -> string_prefix a b) pr inc_i in
+ if (pr <> "") &&
+ ((List.exists (fun(_,b,_) -> b = pr) inc_r)
+ || (List.exists (fun(_,b,_) -> b = pr) inc_i)
+ || pr.[String.length pr - 1] = '.')
+ then
+ physical_dir_of_logical_dir pr
+ else
+ let () = prerr_string "Warning: -R/-Q options don't have a correct common prefix,
install-doc will put anything in $INSTALLDEFAULTROOT\n" in
"$(INSTALLDEFAULTROOT)"
@@ -339,7 +357,7 @@ let implicit () =
print "%.cmo: %.ml4\n\t$(CAMLC) $(ZDEBUG) $(ZFLAGS) $(PP) -impl $<\n\n";
print "%.cmx: %.ml4\n\t$(CAMLOPTC) $(ZDEBUG) $(ZFLAGS) $(PP) -impl $<\n\n";
print "%.ml4.d: %.ml4\n";
- print "\t$(COQDEP) $(OCAMLLIBS) \"$<\" > \"$@\" || ( RV=$$?; rm -f \"$@\"; exit $${RV} )\n\n" in
+ print "\t$(COQDEP) $(OCAMLLIBS) -c \"$<\" > \"$@\" || ( RV=$$?; rm -f \"$@\"; exit $${RV} )\n\n" in
let ml_rules () =
print "%.cmo: %.ml\n\t$(CAMLC) $(ZDEBUG) $(ZFLAGS) $<\n\n";
print "%.cmx: %.ml\n\t$(CAMLOPTC) $(ZDEBUG) $(ZFLAGS) $<\n\n";
@@ -352,12 +370,12 @@ let implicit () =
print "%.cma: | %.mllib\n\t$(CAMLLINK) $(ZDEBUG) $(ZFLAGS) -a -o $@ $^\n\n";
print "%.cmxa: | %.mllib\n\t$(CAMLOPTLINK) $(ZDEBUG) $(ZFLAGS) -a -o $@ $^\n\n";
print "%.mllib.d: %.mllib\n";
- print "\t$(COQDEP) $(COQLIBS) -c \"$<\" > \"$@\" || ( RV=$$?; rm -f \"$@\"; exit $${RV} )\n\n" in
+ print "\t$(COQDEP) $(OCAMLLIBS) -c \"$<\" > \"$@\" || ( RV=$$?; rm -f \"$@\"; exit $${RV} )\n\n" in
let mlpack_rules () =
print "%.cmo: | %.mlpack\n\t$(CAMLLINK) $(ZDEBUG) $(ZFLAGS) -pack -o $@ $^\n\n";
print "%.cmx: | %.mlpack\n\t$(CAMLOPTLINK) $(ZDEBUG) $(ZFLAGS) -pack -o $@ $^\n\n";
print "%.mlpack.d: %.mlpack\n";
- print "\t$(COQDEP) $(COQLIBS) -c \"$<\" > \"$@\" || ( RV=$$?; rm -f \"$@\"; exit $${RV} )\n\n";
+ print "\t$(COQDEP) $(OCAMLLIBS) -c \"$<\" > \"$@\" || ( RV=$$?; rm -f \"$@\"; exit $${RV} )\n\n";
in
let v_rules () =
print "%.vo %.glob: %.v\n\t$(COQC) $(COQDEBUG) $(COQFLAGS) $*\n\n";
@@ -417,7 +435,7 @@ let variables is_install opt (args,defs) =
-I \"$(COQLIB)proofs\" -I \"$(COQLIB)tactics\" -I \"$(COQLIB)tools\" \\
-I \"$(COQLIB)toplevel\" -I \"$(COQLIB)stm\" -I \"$(COQLIB)grammar\"";
List.iter (fun c -> print " \\
- -I \"$(COQLIB)/"; print c; print "\"") Coq_config.plugins_dirs; print "\n";
+ -I \"$(COQLIB)/"; print c; print "\"") Coq_config.plugins_dirs; print "\n";
print "ZFLAGS=$(OCAMLLIBS) $(COQSRCLIBS) -I $(CAMLP4LIB)\n\n";
print "CAMLC?=$(OCAMLC) -c -rectypes\n";
print "CAMLOPTC?=$(OCAMLOPT) -c -rectypes\n";
@@ -471,21 +489,26 @@ let parameters () =
print "TIMED=\nTIMECMD=\nSTDTIME?=/usr/bin/time -f \"$* (user: %U mem: %M ko)\"\n";
print "TIMER=$(if $(TIMED), $(STDTIME), $(TIMECMD))\n\n"
-let include_dirs (inc_i,inc_r) =
- let parse_includes l = List.map (fun (x,_) -> "-I " ^ x) l in
+let include_dirs (inc_ml,inc_i,inc_r) =
+ let parse_ml_includes l = List.map (fun (x,_) -> "-I " ^ x) l in
+ let parse_includes l = List.map (fun (x,l,_) -> "-Q " ^ x ^ " " ^ l) l in
let parse_rec_includes l =
List.map (fun (p,l,_) ->
let l' = if l = "" then "\"\"" else l in "-R " ^ p ^ " " ^ l')
l in
+ let str_ml = parse_ml_includes inc_ml in
let str_i = parse_includes inc_i in
let str_r = parse_rec_includes inc_r in
section "Libraries definitions.";
if !some_ml4file || !some_mlfile || !some_mlifile then begin
- print "OCAMLLIBS?="; print_list "\\\n " str_i; print "\n";
+ print "OCAMLLIBS?="; print_list "\\\n " str_ml; print "\n";
end;
if !some_vfile || !some_mllibfile || !some_mlpackfile then begin
- print "COQLIBS?="; print_list "\\\n " str_i; print " "; print_list "\\\n " str_r; print "\n";
- print "COQDOCLIBS?="; print_list "\\\n " str_r; print "\n\n";
+ print "COQLIBS?="; print_list "\\\n " str_i;
+ List.iter (fun x -> print "\\\n "; print x) str_r;
+ List.iter (fun x -> print "\\\n "; print x) str_ml; print "\n";
+ print "COQDOCLIBS?="; print_list "\\\n " str_i;
+ List.iter (fun x -> print "\\\n "; print x) str_r; print "\n\n";
end
let custom sps =
@@ -691,19 +714,19 @@ let command_line args =
print_list args;
print "\n#\n\n"
-let ensure_root_dir (v,(mli,ml4,ml,mllib,mlpack),_,_) ((i_inc,r_inc) as l) =
+let ensure_root_dir (v,(mli,ml4,ml,mllib,mlpack),_,_) ((ml_inc,i_inc,r_inc) as l) =
let here = Sys.getcwd () in
let not_tops =List.for_all (fun s -> s <> Filename.basename s) in
- if List.exists (fun (_,x) -> x = here) i_inc
+ if List.exists (fun (_,_,x) -> x = here) i_inc
|| List.exists (fun (_,_,x) -> is_prefix x here) r_inc
|| (not_tops v && not_tops mli && not_tops ml4 && not_tops ml
&& not_tops mllib && not_tops mlpack) then
l
else
- ((".",here)::i_inc,r_inc)
+ ((".",here)::ml_inc,(".","Top",here)::i_inc,r_inc)
let warn_install_at_root_directory
- (vfiles,(mlifiles,ml4files,mlfiles,mllibfiles,mlpackfiles),_,_) (inc_i,inc_r) =
+ (vfiles,(mlifiles,ml4files,mlfiles,mllibfiles,mlpackfiles),_,_) (inc_ml,inc_i,inc_r) =
let inc_r_top = List.filter (fun (_,ldir,_) -> ldir = "") inc_r in
let inc_top = List.map (fun (p,_,_) -> p) inc_r_top in
let files = vfiles @ mlifiles @ ml4files @ mlfiles @ mllibfiles @ mlpackfiles in
@@ -712,7 +735,7 @@ let warn_install_at_root_directory
Printf.eprintf "Warning: install target will copy files at the first level of the coq contributions installation directory; option -R %sis recommended\n"
(if inc_r_top = [] then "" else "with non trivial logical root ")
-let check_overlapping_include (_,inc_r) =
+let check_overlapping_include (_,inc_i,inc_r) =
let pwd = Sys.getcwd () in
let aux = function
| [] -> ()
@@ -722,7 +745,7 @@ let check_overlapping_include (_,inc_r) =
List.iter (fun (pdir',_,abspdir') ->
if is_prefix abspdir abspdir' || is_prefix abspdir' abspdir then
Printf.eprintf "Warning: in options -R, %s and %s overlap\n" pdir pdir') l;
- in aux inc_r
+ in aux (inc_i@inc_r)
let do_makefile args =
let has_file var = function
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-02 23:47:55 +0000