diff options
Diffstat (limited to 'tools/coq_makefile.ml')
| -rw-r--r-- | tools/coq_makefile.ml | 393 |
1 files changed, 250 insertions, 143 deletions
diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml index 478cf887..eab909f5 100644 --- a/tools/coq_makefile.ml +++ b/tools/coq_makefile.ml @@ -27,8 +27,9 @@ 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 rec print_prefix_list sep = function + | x :: l -> print sep; print x; print_prefix_list sep l + | [] -> () let section s = let l = String.length s in @@ -43,6 +44,17 @@ let section s = print_com (String.make (l+2) '#'); print "\n" +(* These are the Coq library directories that are used for + * plugin development + *) +let lib_dirs = + ["kernel"; "lib"; "library"; "parsing"; + "pretyping"; "interp"; "printing"; "intf"; + "proofs"; "tactics"; "tools"; "ltacprof"; + "toplevel"; "stm"; "grammar"; "config"; + "ltac"; "engine"] + + let usage () = output_string stderr "Usage summary: @@ -93,17 +105,28 @@ 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 let l2 = String.length dir2 in - dir1 = dir2 || (l1 < l2 && String.sub dir2 0 l1 = dir1 && dir2.[l1] = '/') + let sep = Filename.dir_sep in + if dir1 = dir2 then true + else if l1 + String.length sep <= l2 then + let dir1' = String.sub dir2 0 l1 in + let sep' = String.sub dir2 l1 (String.length sep) in + dir1' = dir1 && sep' = sep + else false 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; @@ -118,62 +141,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_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_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) 0 [] l + in (Some varq, other) let install_include_by_root perms = let install_dir for_i (pdir,pdir',vars) = @@ -249,33 +284,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 @@ -290,7 +330,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; @@ -300,10 +340,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"; @@ -322,11 +362,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"; @@ -355,7 +398,7 @@ let clean sds sps = 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 'OCAMLFIND =\t$(OCAMLFIND)'\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 () = () @@ -363,48 +406,78 @@ 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$(OCAMLDEP) -slash $(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$(OCAMLDEP) -slash $(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$(OCAMLDEP) -slash $(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"; - print "$(VFILES:.v=.vio): %.vio: %.v\n\t$(COQC) -quick $(COQDEBUG) $(COQFLAGS) $*\n\n"; + print "$(VOFILES): %.vo: %.v\n"; + print "\t$(SHOW)COQC $<\n"; + print "\t$(HIDE)$(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" + print "\t$(SHOW)'COQDEP $<'\n"; + print "\t$(HIDE)$(COQDEP) $(COQLIBS) \"$<\" > \"$@\" || ( RV=$$?; rm -f \"$@\"; exit $${RV} )\n\n"; + print "$(addsuffix .beautified,$(VFILES)): %.v.beautified:\n\t$(COQC) $(COQDEBUG) $(COQFLAGS) -beautify $*.v\n\n" in if !some_mlifile then mli_rules (); if !some_ml4file then ml4_rules (); @@ -446,26 +519,24 @@ let variables is_install opt (args,defs) = 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)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\""; + print "COQSRCLIBS?=" ; + List.iter (fun c -> print "-I \"$(COQLIB)"; print c ; print "\" \\\n") lib_dirs ; List.iter (fun c -> print " \\ -I \"$(COQLIB)/"; print c; print "\"") Coq_config.plugins_dirs; print "\n"; print "ZFLAGS=$(OCAMLLIBS) $(COQSRCLIBS) -I $(CAMLP4LIB)\n\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 "CAMLC?=$(OCAMLFIND) ocamlc -c -rectypes -thread\n"; + 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) -CAMLP4EXTEND=pa_extend.cmo q_MLast.cmo pa_macro.cmo unix.cma threads.cma +CAMLP4EXTEND=pa_extend.cmo q_MLast.cmo pa_macro.cmo else -CAMLP4EXTEND=threads.cma +CAMLP4EXTEND= endif\n"; - print "PP?=-pp '$(CAMLP4O) -I $(CAMLLIB) -I $(CAMLLIB)threads/ $(COQSRCLIBS) compat5.cmo \\ + print "PP?=-pp '$(CAMLP4O) -I $(CAMLLIB) -I $(COQLIB)/grammar compat5.cmo \\ $(CAMLP4EXTEND) $(GRAMMARS) $(CAMLP4OPTIONS) -impl'\n\n"; end; match is_install with @@ -502,39 +573,50 @@ 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"; print "$(call includecmdwithout@,$(COQBIN)coqtop -config)\n\n"; - print "TIMED=\nTIMECMD=\nSTDTIME?=/usr/bin/time -f \"$* (user: %U mem: %M ko)\"\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 include_dirs (inc_ml,inc_q,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 includes = + List.map (fun (p,l,_) -> + let l' = if l = "" then "\"\"" else l in + " \"" ^ p ^ "\" " ^ 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_ml; print "\n"; - end; - if !some_vfile || !some_mllibfile || !some_mlpackfile then begin - 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 + section "Libraries definitions."; + if !some_ml4file || !some_mlfile || !some_mlifile then begin + print "OCAMLLIBS?="; print_list "\\\n " str_ml; print "\n"; + end; + if !some_vfile || !some_mllibfile || !some_mlpackfile then begin + print "COQLIBS?="; + print_prefix_list "\\\n -Q" (includes inc_q); + print_prefix_list "\\\n -R" (includes inc_r); + print_prefix_list "\\\n " str_ml; + print "\n"; + end; + if !some_vfile then begin + print "COQCHKLIBS?="; + print_prefix_list "\\\n -R" (includes inc_q); + print_prefix_list "\\\n -R" (includes inc_r); + print "\n"; + print "COQDOCLIBS?="; + print_prefix_list "\\\n -R" (includes inc_q); + print_prefix_list "\\\n -R" (includes inc_r); + print "\n"; + end; + print "\n" let double_colon = ["clean"; "cleanall"; "archclean"] @@ -565,10 +647,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 = @@ -682,9 +767,9 @@ let main_targets vfiles (mlifiles,ml4files,mlfiles,mllibfiles,mlpackfiles) other begin print "mlihtml: $(MLIFILES:.mli=.cmi)\n"; print "\t mkdir $@ || rm -rf $@/*\n"; - print "\t$(OCAMLDOC) -html -rectypes -d $@ -m A $(ZDEBUG) $(ZFLAGS) $(^:.cmi=.mli)\n\n"; + print "\t$(OCAMLFIND) ocamldoc -html -rectypes -d $@ -m A $(ZDEBUG) $(ZFLAGS) $(^:.cmi=.mli)\n\n"; print "all-mli.tex: $(MLIFILES:.mli=.cmi)\n"; - print "\t$(OCAMLDOC) -latex -rectypes -o $@ -m A $(ZDEBUG) $(ZFLAGS) $(^:.cmi=.mli)\n\n"; + print "\t$(OCAMLFIND) ocamldoc -latex -rectypes -o $@ -m A $(ZDEBUG) $(ZFLAGS) $(^:.cmi=.mli)\n\n"; end; if !some_vfile then begin @@ -707,7 +792,7 @@ let main_targets vfiles (mlifiles,ml4files,mlfiles,mllibfiles,mlpackfiles) other print "all-gal.pdf: $(VFILES)\n"; print "\t$(COQDOC) -toc $(COQDOCFLAGS) -pdf -g $(COQDOCLIBS) -o $@ `$(COQDEP) -sort -suffix .v $^`\n\n"; print "validate: $(VOFILES)\n"; - print "\t$(COQCHK) $(COQCHKFLAGS) $(COQLIBS) $(notdir $(^:.vo=))\n\n"; + print "\t$(COQCHK) $(COQCHKFLAGS) $(COQCHKLIBS) $(notdir $(^:.vo=))\n\n"; print "beautify: $(VFILES:=.beautified)\n"; print "\tfor file in $^; do mv $${file%.beautified} $${file%beautified}old && mv $${file} $${file%.beautified}; done\n"; print "\t@echo \'Do not do \"make clean\" until you are sure that everything went well!\'\n"; @@ -760,22 +845,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" @@ -793,12 +880,29 @@ let check_overlapping_include (_,inc_i,inc_r) = Printf.eprintf "Warning: in options -R/-Q, %s and %s overlap\n" pdir pdir') l; in aux (inc_i@inc_r) +(* Generate a .merlin file that references the standard library and + * any -I included paths. + *) +let merlin targets (ml_inc,_,_) = + print ".merlin:\n"; + print "\t@echo 'FLG -rectypes' > .merlin\n" ; + List.iter (fun c -> + printf "\t@echo \"B $(COQLIB)%s\" >> .merlin\n" c) + lib_dirs ; + List.iter (fun (_,c) -> + printf "\t@echo \"B %s\" >> .merlin\n" c; + printf "\t@echo \"S %s\" >> .merlin\n" c) + ml_inc; + print "\n" + let do_makefile args = let has_file var = function |[] -> 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 @@ -822,7 +926,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 (); @@ -835,6 +941,7 @@ let do_makefile args = section "Special targets."; standard opt; install targets inc is_install; + merlin targets inc; clean sds sps; make_makefile sds; implicit (); |