diff options
Diffstat (limited to 'tools/coq_makefile.ml')
| -rw-r--r-- | tools/coq_makefile.ml | 543 |
1 files changed, 326 insertions, 217 deletions
diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml index 74266925..d660f420 100644 --- a/tools/coq_makefile.ml +++ b/tools/coq_makefile.ml @@ -1,12 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* créer un Makefile pour un développement Coq automatiquement *) +(* Coq_makefile: automatically create a Makefile for a Coq development *) let output_channel = ref stdout let makefile_name = ref "Makefile" @@ -32,38 +32,47 @@ let list_iter_i f = let section s = let l = String.length s in - let sep = String.make (l+5) '#' - and sep2 = String.make (l+5) ' ' in - String.set sep (l+4) '\n'; - String.set sep2 0 '#'; - String.set sep2 (l+3) '#'; - String.set sep2 (l+4) '\n'; - print sep; - print sep2; + let print_com s = + print "#"; + print s; + print "#\n" in + print_com (String.make (l+2) '#'); + print_com (String.make (l+2) ' '); print "# "; print s; print " #\n"; - print sep2; - print sep; + print_com (String.make (l+2) ' '); + print_com (String.make (l+2) '#'); print "\n" let usage () = output_string stderr "Usage summary: -coq_makefile [subdirectory] .... [file.v] ... [file.ml[i4]?] ... [file.mllib] - ... [-custom command dependencies file] ... [-I dir] ... [-R physicalpath - logicalpath] ... [VARIABLE = value] ... [-arg opt] ... [-opt|-byte] - [-no-install] [-f file] [-o file] [-h] [--help] +coq_makefile [subdirectory] .... [file.v] ... [file.ml[i4]?] ... + [file.ml{lib,pack}] ... [-extra[-phony] result dependencies command] + ... [-I dir] ... [-R physicalpath logicalpath] ... [VARIABLE = value] + ... [-arg opt] ... [-opt|-byte] [-no-install] [-f file] [-o file] + [-h] [--help] [file.v]: Coq file to be compiled [file.ml[i4]?]: Objective Caml file to be compiled -[file.mllib]: ocamlbuild file that describes a Objective Caml library +[file.ml{lib,pack}]: ocamlbuild file that describes a Objective Caml + library/module [subdirectory] : subdirectory that should be \"made\" and has a Makefile itself to do so. -[-custom command dependencies file]: add target \"file\" with command - \"command\" and dependencies \"dependencies\" +[-extra result dependencies command]: add target \"result\" with command + \"command\" and dependencies \"dependencies\". If \"result\" is not + generic (do not contains a %), \"result\" is built by _make all_ and + deleted by _make clean_. +[-extra-phony result dependencies command]: add a PHONY target \"result\" + with command \"command\" and dependencies \"dependencies\". Note that + _-extra-phony foo bar \"\"_ is a regular way to add the target \"bar\" as + as a dependencies of an already defined target \"foo\". [-I dir]: look for Objective Caml dependencies in \"dir\" [-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 @@ -78,7 +87,7 @@ coq_makefile [subdirectory] .... [file.v] ... [file.ml[i4]?] ... [file.mllib] [--help]: equivalent to [-h]\n"; exit 1 -let is_genrule r = +let is_genrule r = (* generic rule (like bar%foo: ...) *) let genrule = Str.regexp("%") in Str.string_match genrule r 0 @@ -89,11 +98,11 @@ let string_prefix a b = let is_prefix dir1 dir2 = let l1 = String.length dir1 in let l2 = String.length dir2 in - dir1 = dir2 or (l1 < l2 & String.sub dir2 0 l1 = dir1 & dir2.[l1] = '/') + dir1 = dir2 || (l1 < l2 && String.sub dir2 0 l1 = dir1 && dir2.[l1] = '/') let physical_dir_of_logical_dir ldir = let le = String.length ldir - 1 in - let pdir = if 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; @@ -107,14 +116,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 -> Minilib.canonical_path_name (Filename.dirname x)) + (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; @@ -123,128 +133,188 @@ 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) *) - list_iter_i (fun i (pdir,ldir,abspdir) -> + list_iter_i (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_r; + (inc_i@inc_r); end -let install_include_by_root files_var files (inc_i,inc_r) = - try +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 ldir = match inc_r with - |[(".",t,_)] -> t - |l -> let out = List.assoc "." (List.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 - let pdir = physical_dir_of_logical_dir ldir in - printf "\tfor i in $(%s); do \\\n" files_var; - printf "\t install -d `dirname $(DSTROOT)$(COQLIBINSTALL)/%s/$$i`; \\\n" pdir; - printf "\t install -m 0644 $$i $(DSTROOT)$(COQLIBINSTALL)/%s/$$i; \\\n" pdir; - printf "\tdone\n" - with Not_found -> - let absdir_of_files = List.rev_map - (fun x -> Minilib.canonical_path_name (Filename.dirname x)) - files in - let has_inc_i_files = - List.exists (fun (_,a) -> List.mem a absdir_of_files) inc_i in - let install_inc_i d = - printf "\tinstall -d $(DSTROOT)$(COQLIBINSTALL)/%s; \\\n" d; - printf "\tfor i in $(%sINC); do \\\n" files_var; - printf "\t install -m 0644 $$i $(DSTROOT)$(COQLIBINSTALL)/%s/`basename $$i`; \\\n" d; + 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 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 install_include_by_root perms = + let install_dir for_i (pdir,pdir',vars) = + let b = vars <> [] in + if b then begin + printf "\tcd \"%s\" && for i in " pdir; + print_list " " (List.rev_map (Format.sprintf "$(%s)") vars); + print "; do \\\n"; + printf "\t install -d \"`dirname \"$(DSTROOT)\"$(COQLIBINSTALL)/%s/$$i`\"; \\\n" pdir'; + printf "\t install -m %s $$i \"$(DSTROOT)\"$(COQLIBINSTALL)/%s/$$i; \\\n" perms pdir'; + printf "\tdone\n"; + end; + for_i b pdir' in + let install_i = function + |[] -> fun _ _ -> () + |l -> fun b d -> + if not b then printf "\tinstall -d \"$(DSTROOT)\"$(COQLIBINSTALL)/%s; \\\n" d; + print "\tfor i in "; + print_list " " (List.rev_map (Format.sprintf "$(%sINC)") l); + print "; do \\\n"; + printf "\t install -m %s $$i \"$(DSTROOT)\"$(COQLIBINSTALL)/%s/`basename $$i`; \\\n" perms d; printf "\tdone\n" - in - if inc_r = [] then - if has_inc_i_files then - begin - (* Files in the scope of a -I option *) - install_inc_i "$(INSTALLDEFAULTROOT)"; - end else () + in function + |None,l -> List.iter (install_dir (fun _ _ -> ())) l + |Some v_i,l -> List.iter (install_dir (install_i v_i)) l + +let uninstall_by_root = + let uninstall_dir for_i (pdir,pdir',vars) = + printf "\tprintf 'cd \"$${DSTROOT}\"$(COQLIBINSTALL)/%s" pdir'; + if vars <> [] then begin + print " && rm -f "; + print_list " " (List.rev_map (Format.sprintf "$(%s)") vars); + end; + for_i (); + print " && find . -type d -and -empty -delete\\n"; + print "cd \"$${DSTROOT}\"$(COQLIBINSTALL) && "; + printf "find \"%s\" -maxdepth 0 -and -empty -exec rmdir -p \\{\\} \\;\\n' >> \"$@\"\n" pdir' +in + let uninstall_i = function + |[] -> () + |l -> + print " && \\\\\\nfor i in "; + print_list " " (List.rev_map (Format.sprintf "$(%sINC)") l); + print "; do rm -f \"`basename \"$$i\"`\"; done" + in function + |None,l -> List.iter (uninstall_dir (fun _ -> ())) l + |Some v_i,l -> List.iter (uninstall_dir (fun () -> uninstall_i v_i)) l + +let where_put_doc = function + |_,[],[] -> "$(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_i) + || pr.[String.length pr - 1] = '.') + then + physical_dir_of_logical_dir pr else - (* Files in the scope of a -R option (assuming they are disjoint) *) - list_iter_i (fun i (pdir,ldir,abspdir) -> - let has_inc_r_files = List.exists (is_prefix abspdir) absdir_of_files in - let pdir' = physical_dir_of_logical_dir ldir in - if has_inc_r_files then - begin - printf "\tcd %s; for i in $(%s%d); do \\\n" pdir files_var i; - printf "\t install -d `dirname $(DSTROOT)$(COQLIBINSTALL)/%s/$$i`; \\\n" pdir'; - printf "\t install -m 0644 $$i $(DSTROOT)$(COQLIBINSTALL)/%s/$$i; \\\n" pdir'; - printf "\tdone\n"; - end; - if has_inc_i_files then install_inc_i pdir' - ) inc_r - -let install_doc some_vfiles some_mlifiles (_,inc_r) = - let install_one_kind kind dir = - printf "\tinstall -d $(DSTROOT)$(COQDOCINSTALL)/%s/%s\n" dir kind; - printf "\tfor i in %s/*; do \\\n" kind; - printf "\t install -m 0644 $$i $(DSTROOT)$(COQDOCINSTALL)/%s/$$i;\\\n" dir; - print "\tdone\n" in - print "install-doc:\n"; - let () = match inc_r with - |[] -> - if some_vfiles then install_one_kind "html" "$(INSTALLDEFAULTROOT)"; - if some_mlifiles then install_one_kind "mlihtml" "$(INSTALLDEFAULTROOT)"; - |(_,lp,_)::q -> - 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] = '.') - then begin - let rt = physical_dir_of_logical_dir pr in - if some_vfiles then install_one_kind "html" rt; - if some_mlifiles then install_one_kind "mlihtml" rt; - end else begin - prerr_string "Warning: -R options don't have a correct common prefix, - install-doc will put anything in $INSTALLDEFAULTROOT\n"; - if some_vfiles then install_one_kind "html" "$(INSTALLDEFAULTROOT)"; - if some_mlifiles then install_one_kind "mlihtml" "$(INSTALLDEFAULTROOT)"; - end in - print "\n" + 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)" let install (vfiles,(mlifiles,ml4files,mlfiles,mllibfiles,mlpackfiles),_,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 where_what_oth = vars_to_put_by_root + [("VOFILES",vfiles);("VFILES",vfiles);("GLOBFILES",vfiles);("NATIVEFILES",vfiles);("CMOFILES",cmofiles);("CMIFILES",cmifiles);("CMAFILES",mllibfiles)] + 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 - let not_empty = function |[] -> false |_::_ -> true in - let cmofiles = mlpackfiles@mlfiles@ml4files in - let cmifiles = mlifiles@cmofiles in - let cmxsfiles = cmofiles@mllibfiles in if (not_empty cmxsfiles) then begin print "install-natdynlink:\n"; - install_include_by_root "CMXSFILES" cmxsfiles inc; + install_include_by_root "0755" where_what_cmxs; + print "\n"; + end; + if (not_empty cmxsfiles) 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)"; print "\n"; - if not_empty vfiles then install_include_by_root "VOFILES" vfiles inc; - if (not_empty cmofiles) then - install_include_by_root "CMOFILES" cmofiles inc; - if (not_empty cmifiles) then - install_include_by_root "CMIFILES" cmifiles inc; - if (not_empty mllibfiles) then - install_include_by_root "CMAFILES" mllibfiles inc; + install_include_by_root "0644" where_what_oth; List.iter (fun x -> - printf "\t(cd %s; $(MAKE) DSTROOT=$(DSTROOT) INSTALLDEFAULTROOT=$(INSTALLDEFAULTROOT)/%s install)\n" x x) + printf "\t+cd %s && $(MAKE) DSTROOT=\"$(DSTROOT)\" INSTALLDEFAULTROOT=\"$(INSTALLDEFAULTROOT)/%s\" install\n" x x) sds; print "\n"; - install_doc (not_empty vfiles) (not_empty mlifiles) inc + let install_one_kind kind dir = + printf "\tinstall -d \"$(DSTROOT)\"$(COQDOCINSTALL)/%s/%s\n" dir kind; + printf "\tfor i in %s/*; do \\\n" kind; + printf "\t install -m 0644 $$i \"$(DSTROOT)\"$(COQDOCINSTALL)/%s/$$i;\\\n" dir; + 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; + print "\n"; + let uninstall_one_kind kind dir = + printf "\tprintf 'cd \"$${DSTROOT}\"$(COQDOCINSTALL)/%s \\\\\\n' >> \"$@\"\n" dir; + printf "\tprintf '&& rm -f $(shell find \"%s\" -maxdepth 1 -and -type f -print)\\n' >> \"$@\"\n" kind; + print "\tprintf 'cd \"$${DSTROOT}\"$(COQDOCINSTALL) && "; + printf "find %s/%s -maxdepth 0 -and -empty -exec rmdir -p \\{\\} \\;\\n' >> \"$@\"\n" dir kind + in + print "uninstall_me.sh:\n"; + print "\techo '#!/bin/sh' > $@ \n"; + if (not_empty cmxsfiles) 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; + print "\tchmod +x $@\n"; + print "\n"; + print "uninstall: uninstall_me.sh\n"; + print "\tsh $<\n\n" let make_makefile sds = if !make_name <> "" then begin printf "%s: %s\n" !makefile_name !make_name; print "\tmv -f $@ $@.bak\n"; - print "\t$(COQBIN)coq_makefile -f $< -o $@\n\n"; + print "\t\"$(COQBIN)coq_makefile\" -f $< -o $@\n\n"; List.iter - (fun x -> print "\t(cd "; print x; print " ; $(MAKE) Makefile)\n") + (fun x -> print "\t+cd "; print x; print " && $(MAKE) Makefile\n") sds; print "\n"; end @@ -257,71 +327,78 @@ let clean sds sps = print "\trm -f $(addsuffix .d,$(MLFILES) $(MLIFILES) $(ML4FILES) $(MLLIBFILES) $(MLPACKFILES))\n"; end; if !some_vfile then - print "\trm -f $(VOFILES) $(VIFILES) $(GFILES) $(VFILES:.v=.v.d) $(VFILES:=.beautified) $(VFILES:=.old)\n"; + begin + print "\trm -f $(OBJFILES) $(OBJFILES:.o=.native) $(NATIVEFILES)\n"; + print "\trm -f $(VOFILES) $(VOFILES:.vo=.vio) $(GFILES) $(VFILES:.v=.v.d) $(VFILES:=.beautified) $(VFILES:=.old)\n" + end; print "\trm -f all.ps all-gal.ps all.pdf all-gal.pdf all.glob $(VFILES:.v=.glob) $(VFILES:.v=.tex) $(VFILES:.v=.g.tex) all-mli.tex\n"; - print "\t- rm -rf html mlihtml\n"; + print "\t- rm -rf html mlihtml uninstall_me.sh\n"; List.iter - (fun (file,_,_) -> - if not (is_genrule file) then + (fun (file,_,is_phony,_) -> + if not (is_phony || is_genrule file) then (print "\t- rm -rf "; print file; print "\n")) sps; List.iter - (fun x -> print "\t(cd "; print x; print " ; $(MAKE) clean)\n") + (fun x -> print "\t+cd "; print x; print " && $(MAKE) clean\n") sds; print "\n"; print "archclean:\n"; print "\trm -f *.cmx *.o\n"; List.iter - (fun x -> print "\t(cd "; print x; print " ; $(MAKE) archclean)\n") + (fun x -> print "\t+cd "; print x; print " && $(MAKE) archclean\n") sds; print "\n"; - print "printenv:\n\t@$(COQBIN)coqtop -config\n"; - print "\t@echo CAMLC =\t$(CAMLC)\n\t@echo CAMLOPTC =\t$(CAMLOPTC)\n\t@echo PP =\t$(PP)\n\t@echo COQFLAGS =\t$(COQFLAGS)\n"; - print "\t@echo COQLIBINSTALL =\t$(COQLIBINSTALL)\n\t@echo COQDOCINSTALL =\t$(COQDOCINSTALL)\n\n" + print "printenv:\n\t@\"$(COQBIN)coqtop\" -config\n"; + print "\t@echo 'CAMLC =\t$(CAMLC)'\n\t@echo 'CAMLOPTC =\t$(CAMLOPTC)'\n\t@echo 'PP =\t$(PP)'\n\t@echo 'COQFLAGS =\t$(COQFLAGS)'\n"; + print "\t@echo 'COQLIBINSTALL =\t$(COQLIBINSTALL)'\n\t@echo 'COQDOCINSTALL =\t$(COQDOCINSTALL)'\n\n" let header_includes () = () let implicit () = section "Implicit rules."; let mli_rules () = - print "%.cmi: %.mli\n\t$(CAMLC) $(ZDEBUG) $(ZFLAGS) $<\n\n"; - print "%.mli.d: %.mli\n"; + print "$(MLIFILES:.mli=.cmi): %.cmi: %.mli\n\t$(CAMLC) $(ZDEBUG) $(ZFLAGS) $<\n\n"; + print "$(addsuffix .d,$(MLIFILES)): %.mli.d: %.mli\n"; print "\t$(OCAMLDEP) -slash $(OCAMLLIBS) \"$<\" > \"$@\" || ( RV=$$?; rm -f \"$@\"; exit $${RV} )\n\n" in let ml4_rules () = - 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) -slash $(OCAMLLIBS) \"$<\" > \"$@\" || ( RV=$$?; rm -f \"$@\"; exit $${RV} )\n\n" in + 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$(COQDEP) $(OCAMLLIBS) \"$<\" > \"$@\" || ( 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"; - print "%.ml.d: %.ml\n"; + 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$(OCAMLDEP) -slash $(OCAMLLIBS) \"$<\" > \"$@\" || ( RV=$$?; rm -f \"$@\"; exit $${RV} )\n\n" in - let cmxs_rules () = - print "%.cmxs: %.cmxa\n\t$(CAMLOPTLINK) $(ZDEBUG) $(ZFLAGS) -linkall -shared -o $@ $<\n\n"; - print "%.cmxs: %.cmx\n\t$(CAMLOPTLINK) $(ZDEBUG) $(ZFLAGS) -shared -o $@ $<\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 let mllib_rules () = - 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) -slash $(COQLIBS) -c \"$<\" > \"$@\" || ( RV=$$?; rm -f \"$@\"; exit $${RV} )\n\n" in + 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 "$(addsuffix .d,$(MLLIBFILES)): %.mllib.d: %.mllib\n"; + print "\t$(COQDEP) $(OCAMLLIBS) \"$<\" > \"$@\" || ( 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) -slash $(COQLIBS) -c \"$<\" > \"$@\" || ( RV=$$?; rm -f \"$@\"; exit $${RV} )\n\n"; + 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 "$(addsuffix .d,$(MLPACKFILES)): %.mlpack.d: %.mlpack\n"; + print "\t$(COQDEP) $(OCAMLLIBS) \"$<\" > \"$@\" || ( RV=$$?; rm -f \"$@\"; exit $${RV} )\n\n"; in let v_rules () = - print "%.vo %.glob: %.v\n\t$(COQC) $(COQDEBUG) $(COQFLAGS) $*\n\n"; - print "%.vi: %.v\n\t$(COQC) -i $(COQDEBUG) $(COQFLAGS) $*\n\n"; - print "%.g: %.v\n\t$(GALLINA) $<\n\n"; - print "%.tex: %.v\n\t$(COQDOC) $(COQDOCFLAGS) -latex $< -o $@\n\n"; - print "%.html: %.v %.glob\n\t$(COQDOC) $(COQDOCFLAGS) -html $< -o $@\n\n"; - print "%.g.tex: %.v\n\t$(COQDOC) $(COQDOCFLAGS) -latex -g $< -o $@\n\n"; - print "%.g.html: %.v %.glob\n\t$(COQDOC)$(COQDOCFLAGS) -html -g $< -o $@\n\n"; - print "%.v.d: %.v\n"; - print "\t$(COQDEP) -slash $(COQLIBS) \"$<\" > \"$@\" || ( RV=$$?; rm -f \"$@\"; exit $${RV} )\n\n"; - print "%.v.beautified:\n\t$(COQC) $(COQDEBUG) $(COQFLAGS) -beautify $*\n\n" + print "$(VOFILES): %.vo: %.v\n\t$(COQC) $(COQDEBUG) $(COQFLAGS) $*\n\n"; + print "$(GLOBFILES): %.glob: %.v\n\t$(COQC) $(COQDEBUG) $(COQFLAGS) $*\n\n"; + print "$(VFILES:.v=.vio): %.vio: %.v\n\t$(COQC) -quick $(COQDEBUG) $(COQFLAGS) $*\n\n"; + print "$(GFILES): %.g: %.v\n\t$(GALLINA) $<\n\n"; + print "$(VFILES:.v=.tex): %.tex: %.v\n\t$(COQDOC) $(COQDOCFLAGS) -latex $< -o $@\n\n"; + print "$(HTMLFILES): %.html: %.v %.glob\n\t$(COQDOC) $(COQDOCFLAGS) -html $< -o $@\n\n"; + print "$(VFILES:.v=.g.tex): %.g.tex: %.v\n\t$(COQDOC) $(COQDOCFLAGS) -latex -g $< -o $@\n\n"; + print "$(GHTMLFILES): %.g.html: %.v %.glob\n\t$(COQDOC) $(COQDOCFLAGS) -html -g $< -o $@\n\n"; + print "$(addsuffix .d,$(VFILES)): %.v.d: %.v\n"; + print "\t$(COQDEP) $(COQLIBS) \"$<\" > \"$@\" || ( RV=$$?; rm -f \"$@\"; exit $${RV} )\n\n"; + print "$(addsuffix .beautified,$(VFILES)): %.v.beautified:\n\t$(COQC) $(COQDEBUG) $(COQFLAGS) -beautify $*\n\n" in if !some_mlifile then mli_rules (); if !some_ml4file then ml4_rules (); @@ -350,100 +427,121 @@ let variables is_install opt (args,defs) = end; (* Coq executables and relative variables *) if !some_vfile || !some_mlpackfile || !some_mllibfile then - print "COQDEP?=$(COQBIN)coqdep -c\n"; + print "COQDEP?=\"$(COQBIN)coqdep\" -c\n"; if !some_vfile then begin print "COQFLAGS?=-q $(OPT) $(COQLIBS) $(OTHERFLAGS) $(COQ_XML)\n"; print "COQCHKFLAGS?=-silent -o\n"; print "COQDOCFLAGS?=-interpolate -utf8\n"; - print "COQC?=$(COQBIN)coqc\n"; - print "GALLINA?=$(COQBIN)gallina\n"; - print "COQDOC?=$(COQBIN)coqdoc\n"; - print "COQCHK?=$(COQBIN)coqchk\n\n"; + print "COQC?=$(TIMER) \"$(COQBIN)coqc\"\n"; + print "GALLINA?=\"$(COQBIN)gallina\"\n"; + print "COQDOC?=\"$(COQBIN)coqdoc\"\n"; + print "COQCHK?=\"$(COQBIN)coqchk\"\n"; + print "COQMKTOP?=\"$(COQBIN)coqmktop\"\n\n"; end; (* Caml executables and relative variables *) if !some_ml4file || !some_mlfile || !some_mlifile then begin - print "COQSRCLIBS?=-I $(COQLIB)kernel -I $(COQLIB)lib \\ - -I $(COQLIB)library -I $(COQLIB)parsing \\ - -I $(COQLIB)pretyping -I $(COQLIB)interp \\ - -I $(COQLIB)proofs -I $(COQLIB)tactics \\ - -I $(COQLIB)toplevel"; + print "COQSRCLIBS?=-I \"$(COQLIB)kernel\" -I \"$(COQLIB)lib\" \\ + -I \"$(COQLIB)library\" -I \"$(COQLIB)parsing\" -I \"$(COQLIB)pretyping\" \\ + -I \"$(COQLIB)interp\" -I \"$(COQLIB)printing\" -I \"$(COQLIB)intf\" \\ + -I \"$(COQLIB)proofs\" -I \"$(COQLIB)tactics\" -I \"$(COQLIB)tools\" \\ + -I \"$(COQLIB)toplevel\" -I \"$(COQLIB)stm\" -I \"$(COQLIB)grammar\" \\ + -I \"$(COQLIB)config\""; List.iter (fun c -> print " \\ - -I $(COQLIB)plugins/"; print c) 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"; - print "CAMLLINK?=$(OCAMLC) -rectypes\n"; - print "CAMLOPTLINK?=$(OCAMLOPT) -rectypes\n"; + print "CAMLC?=$(OCAMLC) -c -rectypes -thread\n"; + print "CAMLOPTC?=$(OCAMLOPT) -c -rectypes -thread\n"; + print "CAMLLINK?=$(OCAMLC) -rectypes -thread\n"; + print "CAMLOPTLINK?=$(OCAMLOPT) -rectypes -thread\n"; print "GRAMMARS?=grammar.cma\n"; - print "CAMLP4EXTEND?=pa_extend.cmo pa_macro.cmo q_MLast.cmo\n"; - print "CAMLP4OPTIONS?=-loc loc\n"; - print "PP?=-pp \"$(CAMLP4BIN)$(CAMLP4)o -I $(CAMLLIB) -I . $(COQSRCLIBS) $(CAMLP4EXTEND) $(GRAMMARS) $(CAMLP4OPTIONS) -impl\"\n\n"; + print "ifeq ($(CAMLP4),camlp5) +CAMLP4EXTEND=pa_extend.cmo q_MLast.cmo pa_macro.cmo unix.cma threads.cma +else +CAMLP4EXTEND= +endif\n"; + print "PP?=-pp '$(CAMLP4O) -I $(CAMLLIB) -I $(CAMLLIB)threads/ $(COQSRCLIBS) compat5.cmo \\ + $(CAMLP4EXTEND) $(GRAMMARS) $(CAMLP4OPTIONS) -impl'\n\n"; end; match is_install with | Project_file.NoInstall -> () | Project_file.UnspecInstall -> section "Install Paths."; print "ifdef USERINSTALL\n"; - print "XDG_DATA_HOME?=$(HOME)/.local/share\n"; + print "XDG_DATA_HOME?=\"$(HOME)/.local/share\"\n"; print "COQLIBINSTALL=$(XDG_DATA_HOME)/coq\n"; print "COQDOCINSTALL=$(XDG_DATA_HOME)/doc/coq\n"; print "else\n"; - print "COQLIBINSTALL=${COQLIB}user-contrib\n"; - print "COQDOCINSTALL=${DOCDIR}user-contrib\n"; + print "COQLIBINSTALL=\"${COQLIB}user-contrib\"\n"; + print "COQDOCINSTALL=\"${DOCDIR}user-contrib\"\n"; + print "COQTOPINSTALL=\"${COQLIB}toploop\"\n"; print "endif\n\n" | Project_file.TraditionalInstall -> section "Install Paths."; - print "COQLIBINSTALL=${COQLIB}user-contrib\n"; - print "COQDOCINSTALL=${DOCDIR}user-contrib\n"; + print "COQLIBINSTALL=\"${COQLIB}user-contrib\"\n"; + print "COQDOCINSTALL=\"${DOCDIR}user-contrib\"\n"; + print "COQTOPINSTALL=\"${COQLIB}toploop\"\n"; print "\n" | Project_file.UserInstall -> section "Install Paths."; - print "XDG_DATA_HOME?=$(HOME)/.local/share\n"; + print "XDG_DATA_HOME?=\"$(HOME)/.local/share\"\n"; print "COQLIBINSTALL=$(XDG_DATA_HOME)/coq\n"; print "COQDOCINSTALL=$(XDG_DATA_HOME)/doc/coq\n"; + print "COQTOPINSTALL=$(XDG_DATA_HOME)/coq/toploop\n"; print "\n" let parameters () = print ".DEFAULT_GOAL := all\n\n# \n"; print "# This Makefile may take arguments passed as environment variables:\n"; print "# COQBIN to specify the directory where Coq binaries resides;\n"; + 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 "# 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"; - print "$(call includecmdwithout@,$(COQBIN)coqtop -config)\n\n" - -let include_dirs (inc_i,inc_r) = - let parse_includes l = List.map (fun (x,_) -> "-I " ^ x) 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 inc_i' = List.filter (fun (_,i) -> not (List.exists (fun (_,_,i') -> is_prefix i' i) inc_r)) inc_i in + print "$(call includecmdwithout@,$(COQBIN)coqtop -config)\n\n"; + print "TIMED=\nTIMECMD=\nSTDTIME?=/usr/bin/time -f \"$* (user: %U mem: %M ko)\"\n"; + print "TIMER=$(if $(TIMED), $(STDTIME), $(TIMECMD))\n\n"; + print "vo_to_obj = $(addsuffix .o,\\\n"; + print " $(filter-out Warning: Error:,\\\n"; + print " $(shell $(COQBIN)coqtop -q -noinit -batch -quiet -print-mod-uid $(1))))\n\n" + +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,_) -> + let l' = if l = "" then "\"\"" else l in + "-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_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 = - let pr_path (file,dependencies,com) = + let pr_path (file,dependencies,is_phony,com) = print file; print ": "; print dependencies; print "\n"; - if com <> "" then (print "\t"; print com); print "\n\n" + if com <> "" then (print "\t"; print com; print "\n"); + print "\n" in if sps <> [] then section "Custom targets."; List.iter pr_path sps let subdirs sds = let pr_subdir s = - print s; print ":\n\tcd "; print s; print " ; $(MAKE) all\n\n" + print s; print ":\n\t+cd \""; print s; print "\" && $(MAKE) all\n\n" in if sds <> [] then section "Subdirectories."; List.iter pr_subdir sds @@ -470,13 +568,17 @@ let main_targets vfiles (mlifiles,ml4files,mlfiles,mllibfiles,mlpackfiles) other begin match vfiles with |[] -> () |l -> - print "VOFILES:=$(VFILES:.v=.vo)\n"; + print "VO=vo\n"; + print "VOFILES:=$(VFILES:.v=.$(VO))\n"; classify_files_by_root "VOFILES" l inc; print "GLOBFILES:=$(VFILES:.v=.glob)\n"; - print "VIFILES:=$(VFILES:.v=.vi)\n"; print "GFILES:=$(VFILES:.v=.g)\n"; print "HTMLFILES:=$(VFILES:.v=.html)\n"; - print "GHTMLFILES:=$(VFILES:.v=.g.html)\n" + print "GHTMLFILES:=$(VFILES:.v=.g.html)\n"; + print "OBJFILES=$(call vo_to_obj,$(VOFILES))\n"; + print "ALLNATIVEFILES=$(OBJFILES:.o=.cmi) $(OBJFILES:.o=.cmo) $(OBJFILES:.o=.cmx) $(OBJFILES:.o=.cmxs)\n"; + print "NATIVEFILES=$(foreach f, $(ALLNATIVEFILES), $(wildcard $f))\n"; + classify_files_by_root "NATIVEFILES" l inc end; decl_var "ML4FILES" ml4files; decl_var "MLFILES" mlfiles; @@ -566,7 +668,9 @@ let main_targets vfiles (mlifiles,ml4files,mlfiles,mllibfiles,mlpackfiles) other end; if !some_vfile then begin - print "spec: $(VIFILES)\n\n"; + print "quick: $(VOFILES:.vo=.vio)\n\n"; + print "vio2vo:\n\t$(COQC) $(COQDEBUG) $(COQFLAGS) -schedule-vio2vo $(J) $(VOFILES:%.vo=%.vio)\n"; + print "checkproofs:\n\t$(COQC) $(COQDEBUG) $(COQFLAGS) -schedule-vio-checking $(J) $(VOFILES:%.vo=%.vio)\n"; print "gallina: $(GFILES)\n\n"; print "html: $(GLOBFILES) $(VFILES)\n"; print "\t- mkdir -p html\n"; @@ -591,13 +695,18 @@ let main_targets vfiles (mlifiles,ml4files,mlfiles,mllibfiles,mlpackfiles) other end let all_target (vfiles, (_,_,_,_,mlpackfiles as mlfiles), sps, sds) inc = - let special_targets = List.filter (fun (n,_,_) -> not (is_genrule n)) sps in - let other_targets = List.map (function x,_,_ -> x) special_targets @ sds in + let other_targets = CList.map_filter + (fun (n,_,is_phony,_) -> if not (is_phony || is_genrule n) then Some n else None) + sps @ sds in main_targets vfiles mlfiles other_targets inc; print ".PHONY: "; print_list " " - ("all" :: "opt" :: "byte" :: "archclean" :: "clean" :: "install" - :: "userinstall" :: "depend" :: "html" :: "validate" :: sds); + ("all" :: "opt" :: "byte" :: "archclean" :: "clean" :: "install" :: + "uninstall_me.sh" :: "uninstall" :: "userinstall" :: "depend" :: + "html" :: "validate" :: + (sds@(CList.map_filter + (fun (n,_,is_phony,_) -> + if is_phony then Some n else None) sps))); print "\n\n"; custom sps; subdirs sds; @@ -628,38 +737,38 @@ 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 - or List.exists (fun (_,_,x) -> is_prefix x here) r_inc - or (not_tops v && not_tops mli && not_tops ml4 && not_tops ml + 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) = - let inc_r_top = List.filter (fun (_,ldir,_) -> ldir = "") inc_r in - let inc_top = List.map (fun (p,_,_) -> p) inc_r_top in + (vfiles,(mlifiles,ml4files,mlfiles,mllibfiles,mlpackfiles),_,_) (inc_ml,inc_i,inc_r) = + 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 - if inc_r = [] || List.exists (fun f -> List.mem (Filename.dirname f) inc_top) files + 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 %sis recommended\n" - (if inc_r_top = [] then "" else "with non trivial logical root ") + 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" + (if inc_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 rec aux = function + let aux = function | [] -> () | (pdir,_,abspdir)::l -> if not (is_prefix pwd abspdir) then Printf.eprintf "Warning: in option -R, %s is not a subdirectory of the current directory\n" pdir; List.iter (fun (pdir',_,abspdir') -> - if is_prefix abspdir abspdir' or is_prefix abspdir' abspdir then + 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 @@ -686,7 +795,7 @@ let do_makefile args = else if (Filename.check_suffix f ".mllib") then some_mllibfile := true else if (Filename.check_suffix f ".mlpack") then some_mlpackfile := true in - List.iter (fun (_,dependencies,_) -> + List.iter (fun (_,dependencies,_,_) -> List.iter check_dep (Str.split (Str.regexp "[ \t]+") dependencies)) sps; let inc = ensure_root_dir targets inc in |