From af6b36dd24651f1324e7babb982a345fde7d4b58 Mon Sep 17 00:00:00 2001 From: Pierre Letouzey Date: Thu, 2 Jun 2016 04:36:10 +0200 Subject: coq_makefile: add some -ml-synonym to the ocamldep rules Without this, dependencies upon a .ml4 (or a .mlpack) won't be handled correctly. --- tools/coq_makefile.ml | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml index 7b76514e4..3a85d1133 100644 --- a/tools/coq_makefile.ml +++ b/tools/coq_makefile.ml @@ -381,19 +381,19 @@ let implicit () = let mli_rules () = print "$(MLIFILES:.mli=.cmi): %.cmi: %.mli\n\t$(CAMLC) $(ZDEBUG) $(ZFLAGS) $<\n\n"; print "$(addsuffix .d,$(MLIFILES)): %.mli.d: %.mli\n"; - print "\t$(OCAMLFIND) ocamldep -slash $(OCAMLLIBS) \"$<\" > \"$@\" || ( RV=$$?; rm -f \"$@\"; exit $${RV} )\n\n" in + print "\t$(CAMLDEP) $(OCAMLLIBS) \"$<\" > \"$@\" || ( RV=$$?; rm -f \"$@\"; exit $${RV} )\n\n" in let ml4_rules () = print "$(ML4FILES:.ml4=.cmo): %.cmo: %.ml4\n\t$(CAMLC) $(ZDEBUG) $(ZFLAGS) $(PP) -impl $<\n\n"; print "$(filter-out $(addsuffix .cmx,$(foreach lib,$(MLPACKFILES:.mlpack=_MLPACK_DEPENDENCIES),$($(lib)))),$(ML4FILES:.ml4=.cmx)): %.cmx: %.ml4\n"; print "\t$(CAMLOPTC) $(ZDEBUG) $(ZFLAGS) $(PP) -impl $<\n\n"; print "$(addsuffix .d,$(ML4FILES)): %.ml4.d: %.ml4\n"; - print "\t$(OCAMLFIND) ocamldep -slash $(OCAMLLIBS) $(PP) -impl \"$<\" > \"$@\" || ( RV=$$?; rm -f \"$@\"; exit $${RV} )\n\n" in + print "\t$(CAMLDEP) $(OCAMLLIBS) $(PP) -impl \"$<\" > \"$@\" || ( RV=$$?; rm -f \"$@\"; exit $${RV} )\n\n" in let ml_rules () = print "$(MLFILES:.ml=.cmo): %.cmo: %.ml\n\t$(CAMLC) $(ZDEBUG) $(ZFLAGS) $<\n\n"; print "$(filter-out $(addsuffix .cmx,$(foreach lib,$(MLPACKFILES:.mlpack=_MLPACK_DEPENDENCIES),$($(lib)))),$(MLFILES:.ml=.cmx)): %.cmx: %.ml\n"; print "\t$(CAMLOPTC) $(ZDEBUG) $(ZFLAGS) $<\n\n"; print "$(addsuffix .d,$(MLFILES)): %.ml.d: %.ml\n"; - print "\t$(OCAMLFIND) ocamldep -slash $(OCAMLLIBS) \"$<\" > \"$@\" || ( RV=$$?; rm -f \"$@\"; exit $${RV} )\n\n" in + print "\t$(CAMLDEP) $(OCAMLLIBS) \"$<\" > \"$@\" || ( RV=$$?; rm -f \"$@\"; exit $${RV} )\n\n" in let cmxs_rules () = (* order is important here when there is foo.ml and foo.mllib *) print "$(filter-out $(MLLIBFILES:.mllib=.cmxs),$(MLFILES:.ml=.cmxs) $(ML4FILES:.ml4=.cmxs) $(MLPACKFILES:.mlpack=.cmxs)): %.cmxs: %.cmx \t$(CAMLOPTLINK) $(ZDEBUG) $(ZFLAGS) -shared -o $@ $<\n\n"; @@ -471,6 +471,7 @@ let variables is_install opt (args,defs) = print "CAMLOPTC?=$(OCAMLFIND) opt -c -rectypes -thread\n"; print "CAMLLINK?=$(OCAMLFIND) ocamlc -rectypes -thread\n"; print "CAMLOPTLINK?=$(OCAMLFIND) opt -rectypes -thread\n"; + print "CAMLDEP?=$(OCAMLFIND) ocamldep -slash -ml-synonym .ml4 -ml-synonym .mlpack\n"; print "CAMLLIB?=$(shell $(OCAMLFIND) printconf stdlib)\n"; print "GRAMMARS?=grammar.cma\n"; print "ifeq ($(CAMLP4),camlp5) -- cgit v1.2.3 From e9c57a3b6035278b0d4112da8c350a9cdd356259 Mon Sep 17 00:00:00 2001 From: Pierre Letouzey Date: Thu, 2 Jun 2016 05:01:35 +0200 Subject: coq_makefile : short display of commands executed by make This purely cosmetic effect is obtained by the same variables $(SHOW) and $(HIDE) as in the main Makefile of Coq. If you prefer the earlier raw output : make VERBOSE=1 --- tools/coq_makefile.ml | 76 +++++++++++++++++++++++++++++++++++++-------------- 1 file changed, 55 insertions(+), 21 deletions(-) diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml index 3a85d1133..4a94c38a4 100644 --- a/tools/coq_makefile.ml +++ b/tools/coq_makefile.ml @@ -379,36 +379,63 @@ let header_includes () = () let implicit () = section "Implicit rules."; let mli_rules () = - print "$(MLIFILES:.mli=.cmi): %.cmi: %.mli\n\t$(CAMLC) $(ZDEBUG) $(ZFLAGS) $<\n\n"; + print "$(MLIFILES:.mli=.cmi): %.cmi: %.mli\n"; + print "\t$(SHOW)'CAMLC -c $<'\n"; + print "\t$(HIDE)$(CAMLC) $(ZDEBUG) $(ZFLAGS) $<\n\n"; print "$(addsuffix .d,$(MLIFILES)): %.mli.d: %.mli\n"; - print "\t$(CAMLDEP) $(OCAMLLIBS) \"$<\" > \"$@\" || ( RV=$$?; rm -f \"$@\"; exit $${RV} )\n\n" in + print "\t$(SHOW)'CAMLDEP $<'\n"; + print "\t$(HIDE)$(CAMLDEP) $(OCAMLLIBS) \"$<\" > \"$@\" || ( RV=$$?; rm -f \"$@\"; exit $${RV} )\n\n" + in let ml4_rules () = - print "$(ML4FILES:.ml4=.cmo): %.cmo: %.ml4\n\t$(CAMLC) $(ZDEBUG) $(ZFLAGS) $(PP) -impl $<\n\n"; + print "$(ML4FILES:.ml4=.cmo): %.cmo: %.ml4\n"; + print "\t$(SHOW)'CAMLC -pp -c $<'\n"; + print "\t$(HIDE)$(CAMLC) $(ZDEBUG) $(ZFLAGS) $(PP) -impl $<\n\n"; print "$(filter-out $(addsuffix .cmx,$(foreach lib,$(MLPACKFILES:.mlpack=_MLPACK_DEPENDENCIES),$($(lib)))),$(ML4FILES:.ml4=.cmx)): %.cmx: %.ml4\n"; - print "\t$(CAMLOPTC) $(ZDEBUG) $(ZFLAGS) $(PP) -impl $<\n\n"; + print "\t$(SHOW)'CAMLOPT -pp -c $<'\n"; + print "\t$(HIDE)$(CAMLOPTC) $(ZDEBUG) $(ZFLAGS) $(PP) -impl $<\n\n"; print "$(addsuffix .d,$(ML4FILES)): %.ml4.d: %.ml4\n"; - print "\t$(CAMLDEP) $(OCAMLLIBS) $(PP) -impl \"$<\" > \"$@\" || ( RV=$$?; rm -f \"$@\"; exit $${RV} )\n\n" in + print "\t$(SHOW)'CAMLDEP -pp $<'\n"; + print "\t$(HIDE)$(CAMLDEP) $(OCAMLLIBS) $(PP) -impl \"$<\" > \"$@\" || ( RV=$$?; rm -f \"$@\"; exit $${RV} )\n\n" in let ml_rules () = - print "$(MLFILES:.ml=.cmo): %.cmo: %.ml\n\t$(CAMLC) $(ZDEBUG) $(ZFLAGS) $<\n\n"; + print "$(MLFILES:.ml=.cmo): %.cmo: %.ml\n"; + print "\t$(SHOW)'CAMLC -c $<'\n"; + print "\t$(HIDE)$(CAMLC) $(ZDEBUG) $(ZFLAGS) $<\n\n"; print "$(filter-out $(addsuffix .cmx,$(foreach lib,$(MLPACKFILES:.mlpack=_MLPACK_DEPENDENCIES),$($(lib)))),$(MLFILES:.ml=.cmx)): %.cmx: %.ml\n"; - print "\t$(CAMLOPTC) $(ZDEBUG) $(ZFLAGS) $<\n\n"; + print "\t$(SHOW)'CAMLOPT -c $<'\n"; + print "\t$(HIDE)$(CAMLOPTC) $(ZDEBUG) $(ZFLAGS) $<\n\n"; print "$(addsuffix .d,$(MLFILES)): %.ml.d: %.ml\n"; - print "\t$(CAMLDEP) $(OCAMLLIBS) \"$<\" > \"$@\" || ( RV=$$?; rm -f \"$@\"; exit $${RV} )\n\n" in + print "\t$(SHOW)'CAMLDEP $<'\n"; + print "\t$(HIDE)$(CAMLDEP) $(OCAMLLIBS) \"$<\" > \"$@\" || ( RV=$$?; rm -f \"$@\"; exit $${RV} )\n\n" in let cmxs_rules () = (* order is important here when there is foo.ml and foo.mllib *) - print "$(filter-out $(MLLIBFILES:.mllib=.cmxs),$(MLFILES:.ml=.cmxs) $(ML4FILES:.ml4=.cmxs) $(MLPACKFILES:.mlpack=.cmxs)): %.cmxs: %.cmx -\t$(CAMLOPTLINK) $(ZDEBUG) $(ZFLAGS) -shared -o $@ $<\n\n"; - print "$(MLLIBFILES:.mllib=.cmxs): %.cmxs: %.cmxa\n\t$(CAMLOPTLINK) $(ZDEBUG) $(ZFLAGS) -linkall -shared -o $@ $<\n\n" in + print "$(filter-out $(MLLIBFILES:.mllib=.cmxs),$(MLFILES:.ml=.cmxs) $(ML4FILES:.ml4=.cmxs) $(MLPACKFILES:.mlpack=.cmxs)): %.cmxs: %.cmx\n"; + print "\t$(SHOW)'CAMLOPT -shared -o $@'\n"; + print "\t$(HIDE)$(CAMLOPTLINK) $(ZDEBUG) $(ZFLAGS) -shared -o $@ $<\n\n"; + print "$(MLLIBFILES:.mllib=.cmxs): %.cmxs: %.cmxa\n"; + print "\t$(SHOW)'CAMLOPT -shared -o $@'\n"; + print "\t(HIDE)$(CAMLOPTLINK) $(ZDEBUG) $(ZFLAGS) -linkall -shared -o $@ $<\n\n" + in let mllib_rules () = - print "$(MLLIBFILES:.mllib=.cma): %.cma: | %.mllib\n\t$(CAMLLINK) $(ZDEBUG) $(ZFLAGS) -a -o $@ $^\n\n"; - print "$(MLLIBFILES:.mllib=.cmxa): %.cmxa: | %.mllib\n\t$(CAMLOPTLINK) $(ZDEBUG) $(ZFLAGS) -a -o $@ $^\n\n"; + print "$(MLLIBFILES:.mllib=.cma): %.cma: | %.mllib\n"; + print "\t$(SHOW)'CAMLC -a -o $@'\n"; + print "\t$(HIDE)$(CAMLLINK) $(ZDEBUG) $(ZFLAGS) -a -o $@ $^\n\n"; + print "$(MLLIBFILES:.mllib=.cmxa): %.cmxa: | %.mllib\n"; + print "\t$(SHOW)'CAMLOPT -a -o $@'\n"; + print "\t$(HIDE)$(CAMLOPTLINK) $(ZDEBUG) $(ZFLAGS) -a -o $@ $^\n\n"; print "$(addsuffix .d,$(MLLIBFILES)): %.mllib.d: %.mllib\n"; - print "\t$(COQDEP) $(OCAMLLIBS) -c \"$<\" > \"$@\" || ( RV=$$?; rm -f \"$@\"; exit $${RV} )\n\n" in + print "\t$(SHOW)'COQDEP $<'\n"; + print "\t$(HIDE)$(COQDEP) $(OCAMLLIBS) -c \"$<\" > \"$@\" || ( RV=$$?; rm -f \"$@\"; exit $${RV} )\n\n" + in let mlpack_rules () = - print "$(MLPACKFILES:.mlpack=.cmo): %.cmo: | %.mlpack\n\t$(CAMLLINK) $(ZDEBUG) $(ZFLAGS) -pack -o $@ $^\n\n"; - print "$(MLPACKFILES:.mlpack=.cmx): %.cmx: | %.mlpack\n\t$(CAMLOPTLINK) $(ZDEBUG) $(ZFLAGS) -pack -o $@ $^\n\n"; + print "$(MLPACKFILES:.mlpack=.cmo): %.cmo: | %.mlpack\n"; + print "\t$(SHOW)'CAMLC -pack -o $@'\n"; + print "\t$(HIDE)$(CAMLLINK) $(ZDEBUG) $(ZFLAGS) -pack -o $@ $^\n\n"; + print "$(MLPACKFILES:.mlpack=.cmx): %.cmx: | %.mlpack\n"; + print "\t$(SHOW)'CAMLOPT -pack -o $@'\n"; + print "\t$(HIDE)$(CAMLOPTLINK) $(ZDEBUG) $(ZFLAGS) -pack -o $@ $^\n\n"; print "$(addsuffix .d,$(MLPACKFILES)): %.mlpack.d: %.mlpack\n"; - print "\t$(COQDEP) $(OCAMLLIBS) -c \"$<\" > \"$@\" || ( RV=$$?; rm -f \"$@\"; exit $${RV} )\n\n"; -in + print "\t$(SHOW)'COQDEP $<'\n"; + print "\t$(HIDE)$(COQDEP) $(OCAMLLIBS) -c \"$<\" > \"$@\" || ( RV=$$?; rm -f \"$@\"; exit $${RV} )\n\n" + in let v_rules () = print "$(VOFILES): %.vo: %.v\n\t$(COQC) $(COQDEBUG) $(COQFLAGS) $*\n\n"; print "$(GLOBFILES): %.glob: %.v\n\t$(COQC) $(COQDEBUG) $(COQFLAGS) $*\n\n"; @@ -516,7 +543,11 @@ let parameters () = print "# TIMECMD set a command to log .v compilation time;\n"; print "# TIMED if non empty, use the default time command as TIMECMD;\n"; print "# ZDEBUG/COQDEBUG to specify debug flags for ocamlc&ocamlopt/coqc;\n"; - print "# DSTROOT to specify a prefix to install path.\n\n"; + print "# DSTROOT to specify a prefix to install path.\n"; + print "# VERBOSE to disable the short display of compilation rules.\n\n"; + print "VERBOSE?=\n"; + print "SHOW := $(if $(VERBOSE),@true \"\",@echo \"\")\n"; + print "HIDE := $(if $(VERBOSE),,@)\n\n"; print "# Here is a hack to make $(eval $(shell works:\n"; print "define donewline\n\n\nendef\n"; print "includecmdwithout@ = $(eval $(subst @,$(donewline),$(shell { $(1) | tr -d '\\r' | tr '\\n' '@'; })))\n"; @@ -579,10 +610,13 @@ let forpacks l = let () = if l <> [] then section "Ad-hoc implicit rules for mlpack." in List.iter (fun it -> let h = Filename.chop_extension it in + let pk = String.capitalize (Filename.basename h) in printf "$(addsuffix .cmx,$(filter $(basename $(MLFILES)),$(%s_MLPACK_DEPENDENCIES))): %%.cmx: %%.ml\n" h; - printf "\t$(CAMLOPTC) $(ZDEBUG) $(ZFLAGS) -for-pack %s $<\n\n" (String.capitalize (Filename.basename h)); + printf "\t$(SHOW)'CAMLOPT -c -for-pack %s $<'\n" pk; + printf "\t$(HIDE)$(CAMLOPTC) $(ZDEBUG) $(ZFLAGS) -for-pack %s $<\n\n" pk; printf "$(addsuffix .cmx,$(filter $(basename $(ML4FILES)),$(%s_MLPACK_DEPENDENCIES))): %%.cmx: %%.ml4\n" h; - printf "\t$(CAMLOPTC) $(ZDEBUG) $(ZFLAGS) -for-pack %s $(PP) -impl $<\n\n" (String.capitalize (Filename.basename h)) + printf "\t$(SHOW)'CAMLOPT -c -pp -for-pack %s $<'\n" pk; + printf "\t$(HIDE)$(CAMLOPTC) $(ZDEBUG) $(ZFLAGS) -for-pack %s $(PP) -impl $<\n\n" pk ) l let main_targets vfiles (mlifiles,ml4files,mlfiles,mllibfiles,mlpackfiles) other_targets inc = -- cgit v1.2.3 From 1826cf003fe564d751e8376cad69be6b59714596 Mon Sep 17 00:00:00 2001 From: Pierre Letouzey Date: Fri, 3 Jun 2016 11:11:26 +0200 Subject: coq_makefile: List.iteri is now standard since OCaml 4.00 --- tools/coq_makefile.ml | 5 +---- 1 file changed, 1 insertion(+), 4 deletions(-) diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml index 4a94c38a4..daa480677 100644 --- a/tools/coq_makefile.ml +++ b/tools/coq_makefile.ml @@ -27,9 +27,6 @@ let rec print_list sep = function | x :: l -> print x; print sep; print_list sep l | [] -> () -let list_iter_i f = - let rec aux i = function [] -> () | a::l -> f i a; aux (i+1) l in aux 1 - let section s = let l = String.length s in let print_com s = @@ -154,7 +151,7 @@ let classify_files_by_root var files (inc_ml,inc_i,inc_r) = printf "\n"; end; (* Files in the scope of a -R option (assuming they are disjoint) *) - list_iter_i (fun i (pdir,_,abspdir) -> + List.iteri (fun i (pdir,_,abspdir) -> if List.exists (is_prefix abspdir) absdir_of_files then printf "%s%d=$(patsubst %s/%%,%%,$(filter %s/%%,$(%s)))\n" var i pdir pdir var) -- cgit v1.2.3 From c3698ed4271658fc2edde3870394b3403d7489c9 Mon Sep 17 00:00:00 2001 From: Pierre Letouzey Date: Mon, 6 Jun 2016 13:35:30 +0200 Subject: Coq_makefile: code cleanup (less long lines, etc) --- tools/coq_makefile.ml | 183 +++++++++++++++++++++++++++++--------------------- 1 file changed, 107 insertions(+), 76 deletions(-) diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml index daa480677..ec039aae6 100644 --- a/tools/coq_makefile.ml +++ b/tools/coq_makefile.ml @@ -100,8 +100,10 @@ let is_genrule r = (* generic rule (like bar%foo: ...) *) Str.string_match genrule r 0 let string_prefix a b = - let rec aux i = try if a.[i] = b.[i] then aux (i+1) else i with |Invalid_argument _ -> i in - String.sub a 0 (aux 0) + let rec aux i = + try if a.[i] = b.[i] then aux (i+1) else i with Invalid_argument _ -> i + in + String.sub a 0 (aux 0) let is_prefix dir1 dir2 = let l1 = String.length dir1 in @@ -116,7 +118,10 @@ let is_prefix dir1 dir2 = let physical_dir_of_logical_dir ldir = let le = String.length ldir - 1 in - let pdir = if le >= 0 && ldir.[le] = '.' then String.sub ldir 0 (le - 1) else String.copy ldir in + let pdir = + if le >= 0 && ldir.[le] = '.' then String.sub ldir 0 (le - 1) + else String.copy ldir + in for i = 0 to le - 1 do if pdir.[i] = '.' then pdir.[i] <- '/'; done; @@ -131,62 +136,74 @@ let standard opt = print "\"\n\n" 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 + if List.exists (fun (pdir,_,_) -> pdir = ".") inc_r + || List.exists (fun (pdir,_,_) -> pdir = ".") inc_i + then () + else + 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_ml in - if has_inc_i then - begin - printf "%sINC=" var; - List.iter (fun (pdir,absdir) -> - if List.mem absdir absdir_of_files - then printf - "$(filter $(wildcard %s/*),$(%s)) " - pdir var - ) inc_ml; - printf "\n"; - end; - (* Files in the scope of a -R option (assuming they are disjoint) *) - List.iteri (fun i (pdir,_,abspdir) -> - 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_i@inc_r); - end + files + in + (* files in scope of a -I option (assuming they are no overlapping) *) + if List.exists (fun (_,a) -> List.mem a absdir_of_files) inc_ml then + begin + printf "%sINC=" var; + List.iter (fun (pdir,absdir) -> + if List.mem absdir absdir_of_files + then printf "$(filter $(wildcard %s/*),$(%s)) " pdir var) + inc_ml; + printf "\n"; + end; + (* Files in the scope of a -R option (assuming they are disjoint) *) + List.iteri (fun i (pdir,_,abspdir) -> + 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_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 - (* All files caught by a -R . option (assuming it is the only one) *) + 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 + (* All files caught by a -R . option (assuming it is the only one) *) match inc_i@inc_r with - |[(".",t,_)] -> (None,[".",physical_dir_of_logical_dir t,List.rev_map fst var_x_files_l]) + |[(".",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\n" in + let () = prerr_string "Warning: install rule assumes that -R/-Q . _ is the only -R/-Q option\n" + 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)), + let varq = var_filter + (fun l -> List.exists (fun (_,a) -> List.mem a l) inc_ml) + (fun x -> x) + in (* (physical dir, physical dir of logical path,vars) for -R options (assuming physical dirs are disjoint) *) - 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 [] l - ) + let other = + 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 [] l + in (Some varq, other) let install_include_by_root perms = let install_dir for_i (pdir,pdir',vars) = @@ -262,33 +279,38 @@ let where_put_doc = function install-doc will put anything in $INSTALLDEFAULTROOT\n" in "$(INSTALLDEFAULTROOT)" -let install (vfiles,(mlifiles,ml4files,mlfiles,mllibfiles,mlpackfiles),_,sds) inc = function +let install (vfiles,(mlis,ml4s,mls,mllibs,mlpacks),_,sds) inc = function |Project_file.NoInstall -> () |is_install -> let not_empty = function |[] -> false |_::_ -> true in - let cmofiles = List.rev_append mlpackfiles (List.rev_append mlfiles ml4files) in - let cmifiles = List.rev_append mlifiles cmofiles in - let cmxsfiles = List.rev_append cmofiles mllibfiles in - let where_what_cmxs = vars_to_put_by_root [("CMXSFILES",cmxsfiles)] inc in + let cmos = List.rev_append mlpacks (List.rev_append mls ml4s) in + let cmis = List.rev_append mlis cmos in + let cmxss = List.rev_append cmos mllibs in + let where_what_cmxs = vars_to_put_by_root [("CMXSFILES",cmxss)] inc in let where_what_oth = vars_to_put_by_root - [("VOFILES",vfiles);("VFILES",vfiles);("GLOBFILES",vfiles);("NATIVEFILES",vfiles);("CMOFILES",cmofiles);("CMIFILES",cmifiles);("CMAFILES",mllibfiles)] + [("VOFILES",vfiles);("VFILES",vfiles); + ("GLOBFILES",vfiles);("NATIVEFILES",vfiles); + ("CMOFILES",cmos);("CMIFILES",cmis);("CMAFILES",mllibs)] inc in let doc_dir = where_put_doc inc in - let () = if is_install = Project_file.UnspecInstall then - print "userinstall:\n\t+$(MAKE) USERINSTALL=true install\n\n" in - if (not_empty cmxsfiles) then begin + if is_install = Project_file.UnspecInstall then begin + print "userinstall:\n\t+$(MAKE) USERINSTALL=true install\n\n" + end; + if not_empty cmxss then begin print "install-natdynlink:\n"; install_include_by_root "0755" where_what_cmxs; print "\n"; end; - if (not_empty cmxsfiles) then begin + if not_empty cmxss then begin print "install-toploop: $(MLLIBFILES:.mllib=.cmxs)\n"; printf "\t install -d \"$(DSTROOT)\"$(COQTOPINSTALL)/\n"; printf "\t install -m 0755 $? \"$(DSTROOT)\"$(COQTOPINSTALL)/\n"; print "\n"; end; print "install:"; - if (not_empty cmxsfiles) then print "$(if $(HASNATDYNLINK_OR_EMPTY),install-natdynlink)"; + if not_empty cmxss then begin + print "$(if $(HASNATDYNLINK_OR_EMPTY),install-natdynlink)"; + end; print "\n"; install_include_by_root "0644" where_what_oth; List.iter @@ -303,7 +325,7 @@ let install (vfiles,(mlifiles,ml4files,mlfiles,mllibfiles,mlpackfiles),_,sds) in print "\tdone\n" in print "install-doc:\n"; if not_empty vfiles then install_one_kind "html" doc_dir; - if not_empty mlifiles then install_one_kind "mlihtml" doc_dir; + if not_empty mlis then install_one_kind "mlihtml" doc_dir; print "\n"; let uninstall_one_kind kind dir = printf "\tprintf 'cd \"$${DSTROOT}\"$(COQDOCINSTALL)/%s \\\\\\n' >> \"$@\"\n" dir; @@ -313,10 +335,10 @@ let install (vfiles,(mlifiles,ml4files,mlfiles,mllibfiles,mlpackfiles),_,sds) in in printf "uninstall_me.sh: %s\n" !makefile_name; print "\techo '#!/bin/sh' > $@\n"; - if (not_empty cmxsfiles) then uninstall_by_root where_what_cmxs; + if not_empty cmxss then uninstall_by_root where_what_cmxs; uninstall_by_root where_what_oth; if not_empty vfiles then uninstall_one_kind "html" doc_dir; - if not_empty mlifiles then uninstall_one_kind "mlihtml" doc_dir; + if not_empty mlis then uninstall_one_kind "mlihtml" doc_dir; print "\tchmod +x $@\n"; print "\n"; print "uninstall: uninstall_me.sh\n"; @@ -335,11 +357,14 @@ let make_makefile sds = let clean sds sps = print "clean::\n"; - if !some_mlfile || !some_mlifile || !some_ml4file || !some_mllibfile || !some_mlpackfile then begin - print "\trm -f $(ALLCMOFILES) $(CMIFILES) $(CMAFILES)\n"; - print "\trm -f $(ALLCMOFILES:.cmo=.cmx) $(CMXAFILES) $(CMXSFILES) $(ALLCMOFILES:.cmo=.o) $(CMXAFILES:.cmxa=.a)\n"; - print "\trm -f $(addsuffix .d,$(MLFILES) $(MLIFILES) $(ML4FILES) $(MLLIBFILES) $(MLPACKFILES))\n"; - end; + if !some_mlfile || !some_mlifile || !some_ml4file + || !some_mllibfile || !some_mlpackfile + then + begin + print "\trm -f $(ALLCMOFILES) $(CMIFILES) $(CMAFILES)\n"; + print "\trm -f $(ALLCMOFILES:.cmo=.cmx) $(CMXAFILES) $(CMXSFILES) $(ALLCMOFILES:.cmo=.o) $(CMXAFILES:.cmxa=.a)\n"; + print "\trm -f $(addsuffix .d,$(MLFILES) $(MLIFILES) $(ML4FILES) $(MLLIBFILES) $(MLPACKFILES))\n"; + end; if !some_vfile then begin print "\trm -f $(OBJFILES) $(OBJFILES:.o=.native) $(NATIVEFILES)\n"; @@ -805,22 +830,24 @@ let command_line args = print_list args; print "\n#\n\n" -let ensure_root_dir (v,(mli,ml4,ml,mllib,mlpack),_,_) ((ml_inc,i_inc,r_inc) as l) = +let ensure_root_dir (vfiles,(mlis,ml4s,mls,mllibs,mlpacks),_,_) inc = + let (ml_inc,i_inc,r_inc) = inc 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 <> Filename.basename s) in 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 + || (not_tops vfiles && not_tops mlis && not_tops ml4s && not_tops mls + && not_tops mllibs && not_tops mlpacks) + then + inc else ((".",here)::ml_inc,i_inc,(".","Top",here)::r_inc) -let warn_install_at_root_directory - (vfiles,(mlifiles,ml4files,mlfiles,mllibfiles,mlpackfiles),_,_) (inc_ml,inc_i,inc_r) = +let warn_install_at_root_directory (vfiles,(mlis,ml4s,mls,mllibs,mlpacks),_,_) inc = + let (inc_ml,inc_i,inc_r) = inc in let inc_top = List.filter (fun (_,ldir,_) -> ldir = "") (inc_r@inc_i) in let inc_top_p = List.map (fun (p,_,_) -> p) inc_top in - let files = vfiles @ mlifiles @ ml4files @ mlfiles @ mllibfiles @ mlpackfiles in + let files = vfiles @ mlis @ ml4s @ mls @ mllibs @ mlpacks in if List.exists (fun f -> List.mem (Filename.dirname f) inc_top_p) files then Printf.eprintf "Warning: install target will copy files at the first level of the coq contributions installation directory; option -R or -Q %sis recommended\n" @@ -858,7 +885,9 @@ 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,Project_file.UnspecInstall,true) [] args + try + Project_file.process_cmd_line Filename.current_dir_name + (None,None,Project_file.UnspecInstall,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 @@ -882,7 +911,9 @@ 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 <> Project_file.NoInstall then warn_install_at_root_directory targets inc; + if is_install <> Project_file.NoInstall then begin + warn_install_at_root_directory targets inc; + end; check_overlapping_include inc; banner (); header_includes (); -- cgit v1.2.3