From aad9936c225ef5b4f463b4af9ce1fa267bab337b Mon Sep 17 00:00:00 2001 From: pboutill Date: Thu, 1 Sep 2011 09:50:51 +0000 Subject: Creation of ide/project_file.ml4 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14433 85f007b7-540e-0410-9357-904b9bb8a0f7 --- Makefile.build | 2 +- ide/ide.mllib | 1 + ide/minilib.ml | 28 ++ ide/minilib.mli | 3 + ide/project_file.ml4 | 121 ++++++++ tools/coq_makefile.ml | 610 ++++++++++++++++++++++++++++++++++++++++ tools/coq_makefile.ml4 | 733 ------------------------------------------------- 7 files changed, 764 insertions(+), 734 deletions(-) create mode 100644 ide/project_file.ml4 create mode 100644 tools/coq_makefile.ml delete mode 100644 tools/coq_makefile.ml4 diff --git a/Makefile.build b/Makefile.build index 91d73ae25..efebb57df 100644 --- a/Makefile.build +++ b/Makefile.build @@ -492,7 +492,7 @@ $(GALLINA): $(addsuffix $(BESTOBJ), tools/gallina_lexer tools/gallina) $(SHOW)'OCAMLBEST -o $@' $(HIDE)$(call bestocaml,,) -$(COQMAKEFILE): $(addsuffix $(BESTOBJ), config/coq_config tools/coq_makefile) +$(COQMAKEFILE): $(addsuffix $(BESTOBJ),config/coq_config ide/minilib ide/project_file tools/coq_makefile) $(SHOW)'OCAMLBEST -o $@' $(HIDE)$(call bestocaml,,str) diff --git a/ide/ide.mllib b/ide/ide.mllib index 8d3260510..8f3a6c353 100644 --- a/ide/ide.mllib +++ b/ide/ide.mllib @@ -22,4 +22,5 @@ Coq Coq_commands Command_windows Coqide_ui +Project_file Coqide diff --git a/ide/minilib.ml b/ide/minilib.ml index dcadc81f5..71956cf8f 100644 --- a/ide/minilib.ml +++ b/ide/minilib.ml @@ -74,3 +74,31 @@ let home = let coqlib = ref "" let coqtop_path = ref "" + +(* Hints to partially detects if two paths refer to the same repertory *) +let rec remove_path_dot p = + let curdir = Filename.concat Filename.current_dir_name "" in (* Unix: "./" *) + let n = String.length curdir in + if String.length p > n && String.sub p 0 n = curdir then + remove_path_dot (String.sub p n (String.length p - n)) + else + p + +let strip_path p = + let cwd = Filename.concat (Sys.getcwd ()) "" in (* Unix: "`pwd`/" *) + let n = String.length cwd in + if String.length p > n && String.sub p 0 n = cwd then + remove_path_dot (String.sub p n (String.length p - n)) + else + remove_path_dot p + +let canonical_path_name p = + let current = Sys.getcwd () in + try + Sys.chdir p; + let p' = Sys.getcwd () in + Sys.chdir current; + p' + with Sys_error _ -> + (* We give up to find a canonical name and just simplify it... *) + strip_path p diff --git a/ide/minilib.mli b/ide/minilib.mli index 1daa60e1a..2128b7d86 100644 --- a/ide/minilib.mli +++ b/ide/minilib.mli @@ -25,3 +25,6 @@ val home : string val coqlib : string ref val coqtop_path : string ref + +val strip_path : string -> string +val canonical_path_name : string -> string diff --git a/ide/project_file.ml4 b/ide/project_file.ml4 new file mode 100644 index 000000000..ef39b904c --- /dev/null +++ b/ide/project_file.ml4 @@ -0,0 +1,121 @@ +type target = + | ML of string (* ML file : foo.ml -> (ML "foo.ml") *) + | MLI of string (* MLI file : foo.mli -> (MLI "foo.mli") *) + | ML4 of string (* ML4 file : foo.ml4 -> (ML4 "foo.ml4") *) + | MLLIB of string (* MLLIB file : foo.mllib -> (MLLIB "foo.mllib") *) + | V of string (* V file : foo.v -> (V "foo") *) + | Arg of string + | Special of string * string * string (* file, dependencies, command *) + | Subdir of string + | Def of string * string (* X=foo -> Def ("X","foo") *) + | Include of string + | RInclude of string * string (* -R physicalpath logicalpath *) + + +exception Parsing_error +let rec parse_string = parser + | [< '' ' | '\n' | '\t' >] -> "" + | [< 'c; s >] -> (String.make 1 c)^(parse_string s) + | [< >] -> "" +and parse_string2 = parser + | [< ''"' >] -> "" + | [< 'c; s >] -> (String.make 1 c)^(parse_string2 s) +and parse_skip_comment = parser + | [< ''\n'; s >] -> s + | [< 'c; s >] -> parse_skip_comment s + | [< >] -> [< >] +and parse_args = parser + | [< '' ' | '\n' | '\t'; s >] -> parse_args s + | [< ''#'; s >] -> parse_args (parse_skip_comment s) + | [< ''"'; str = parse_string2; s >] -> ("" ^ str) :: parse_args s + | [< 'c; str = parse_string; s >] -> ((String.make 1 c) ^ str) :: (parse_args s) + | [< >] -> [] + + +let parse f = + let c = open_in f in + let res = parse_args (Stream.of_channel c) in + close_in c; + res + +let rec process_cmd_line ((project_file,makefile,install,opt) as opts) l = function + | [] -> opts,List.rev l + | ("-h"|"--help") :: _ -> + raise Parsing_error + | ("-no-opt"|"-byte") :: r -> + process_cmd_line (project_file,makefile,install,false) l r + | ("-full"|"-opt") :: r -> + process_cmd_line (project_file,makefile,install,true) l r + | "-impredicative-set" :: r -> + prerr_string "Please now use \"-arg -impredicative-set\" instead of \"-impredicative-set\" alone to be more uniform.\n"; + process_cmd_line opts (Arg "-impredicative_set" :: l) r + | "-no-install" :: r -> + if not install then prerr_string "Warning: -no-install sets more than once.\n"; + process_cmd_line (project_file,makefile,false,opt) l r + | "-custom" :: com :: dependencies :: file :: r -> + process_cmd_line opts (Special (file,dependencies,com) :: l) r + | "-I" :: d :: r -> + process_cmd_line opts (Include d :: l) r + | "-R" :: p :: lp :: r -> + process_cmd_line opts (RInclude (p,lp) :: l) r + | ("-I"|"-custom") :: _ -> + raise Parsing_error + | "-f" :: file :: r -> + let () = match project_file with + | None -> () + | Some _ -> prerr_string + "Warning: Several features will not work with multiple project files.\n" + in process_cmd_line (Some file,makefile,install,opt) l ((parse file)@r) + | ["-f"] -> + raise Parsing_error + | "-o" :: file :: r -> + let () = match makefile with + |None -> () + |Some f -> + prerr_string "Warning: Only one output file in genererated. "; + prerr_string f; prerr_string " will not.\n" + in process_cmd_line (project_file,Some file,install,opt) l r + | v :: "=" :: def :: r -> + process_cmd_line opts (Def (v,def) :: l) r + | "-arg" :: a :: r -> + process_cmd_line opts (Arg a :: l) r + | f :: r -> + process_cmd_line opts (( + if Filename.check_suffix f ".v" then V f + else if (Filename.check_suffix f ".ml") then ML f + else if (Filename.check_suffix f ".ml4") then ML4 f + else if (Filename.check_suffix f ".mli") then MLI f + else if (Filename.check_suffix f ".mllib") then MLLIB f + else Subdir f) :: l) r + +let rec post_canonize f = + if Filename.basename f = Filename.current_dir_name + then let dir = Filename.dirname f in + if dir = Filename.current_dir_name then f else post_canonize dir + else f + +(* Return: ((v,(mli,ml4,ml,mllib),special,subdir),(i_inc,r_inc),(args,defs)) *) +let rec split_arguments = function + | V n :: r -> + let (v,m,o,s),i,d = split_arguments r in ((Minilib.strip_path n::v,m,o,s),i,d) + | ML n :: r -> + let (v,(mli,ml4,ml,mllib),o,s),i,d = split_arguments r in ((v,(mli,ml4,Minilib.strip_path n::ml,mllib),o,s),i,d) + | MLI n :: r -> + let (v,(mli,ml4,ml,mllib),o,s),i,d = split_arguments r in ((v,(Minilib.strip_path n::mli,ml4,ml,mllib),o,s),i,d) + | ML4 n :: r -> + let (v,(mli,ml4,ml,mllib),o,s),i,d = split_arguments r in ((v,(mli,Minilib.strip_path n::ml4,ml,mllib),o,s),i,d) + | MLLIB n :: r -> + let (v,(mli,ml4,ml,mllib),o,s),i,d = split_arguments r in ((v,(mli,ml4,ml,Minilib.strip_path n::mllib),o,s),i,d) + | Special (n,dep,c) :: r -> + let (v,m,o,s),i,d = split_arguments r in ((v,m,(n,dep,c)::o,s),i,d) + | Subdir n :: r -> + let (v,m,o,s),i,d = split_arguments r in ((v,m,o,n::s),i,d) + | Include p :: r -> + let t,(i,r),d = split_arguments r in (t,((post_canonize p,Minilib.canonical_path_name p)::i,r),d) + | RInclude (p,l) :: r -> + let t,(i,r),d = split_arguments r in (t,(i,(post_canonize p,l,Minilib.canonical_path_name p)::r),d) + | Def (v,def) :: r -> + let t,i,(args,defs) = split_arguments r in (t,i,(args,(v,def)::defs)) + | Arg a :: r -> + let t,i,(args,defs) = split_arguments r in (t,i,(a::args,defs)) + | [] -> ([],([],[],[],[]),[],[]),([],[]),([],[]) diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml new file mode 100644 index 000000000..ca31a2bd0 --- /dev/null +++ b/tools/coq_makefile.ml @@ -0,0 +1,610 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* print x + | 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 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; + print "# "; print s; print " #\n"; + print sep2; + print sep; + 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] + +[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 +[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\" +[-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\". +[VARIABLE = value]: Add the variable definition \"VARIABLE=value\" +[-byte]: compile with byte-code version of coq +[-opt]: compile with native-code version of coq +[-arg opt]: send option \"opt\" to coqc +[-no-install]: build a makefile with no install target +[-f file]: take the contents of file as arguments +[-o file]: output should go in file file +[-h]: print this usage summary +[--help]: equivalent to [-h]\n"; + exit 1 + +let is_genrule r = + let genrule = Str.regexp("%") in + Str.string_match genrule r 0 + +let absolute_dir dir = + let current = Sys.getcwd () in + Sys.chdir dir; + let dir' = Sys.getcwd () in + Sys.chdir current; + dir' + +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 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] = '/') + +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 + for i = 0 to le - 1 do + if pdir.[i] = '.' then pdir.[i] <- '/'; + done; + pdir + +let standard opt = + print "byte:\n"; + print "\t$(MAKE) all \"OPT:=-byte\"\n\n"; + print "opt:\n"; + if not opt then print "\t@echo \"WARNING: opt is disabled\"\n"; + print "\t$(MAKE) all \"OPT:="; print (if opt then "-opt" else "-byte"); + print "\"\n\n" + +let is_prefix_of_file dir f = + is_prefix dir (absolute_dir (Filename.dirname f)) + +let classify_files_by_root var files (inc_i,inc_r) = + if not (List.exists (fun (pdir,_,_) -> pdir = ".") inc_r) then + begin + (* Files in the scope of a -R option (assuming they are disjoint) *) + list_iter_i (fun i (pdir,ldir,abspdir) -> + if List.exists (is_prefix_of_file abspdir) files then + printf "%s%d:=$(patsubst %s/%%,%%,$(filter %s/%%,$(%s)))\n" + var i pdir pdir var) + inc_r; + (* Files not in the scope of a -R option *) + let pat_of_dir (pdir,_,_) = pdir^"/%" in + let pdir_patterns = String.concat " " (List.map pat_of_dir inc_r) in + printf "%s0:=$(filter-out %s,$(%s))\n" var pdir_patterns var + end + +let install_include_by_root path_var files_var files (_,inc_r) = + 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.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)$(%s)user-contrib/%s/$$i`; \\\n\t install $$i $(DSTROOT)$(%s)user-contrib/%s/$$i; \\\n" path_var pdir path_var pdir; + printf "\tdone\n" + with Not_found -> + (* Files in the scope of a -R option (assuming they are disjoint) *) + list_iter_i (fun i (pdir,ldir,abspdir) -> + if List.exists (is_prefix_of_file abspdir) files then + begin + let pdir' = physical_dir_of_logical_dir ldir in + printf "\tcd %s; for i in $(%s%d); do \\\n" pdir files_var i; + printf "\t install -d `dirname $(DSTROOT)$(%s)user-contrib/%s/$$i`; \\\n\t install $$i $(DSTROOT)$(%s)user-contrib/%s/$$i; \\\n" path_var pdir' path_var pdir'; + printf "\tdone\n" + end) inc_r; + (* Files not in the scope of a -R option *) + printf "\tfor i in $(%s0); do \\\n" files_var; + printf "\t install -d `dirname $(DSTROOT)$(%s)user-contrib/$(INSTALLDEFAULTROOT)/$$i`; \\\n\t install $$i $(DSTROOT)$(%s)user-contrib/$(INSTALLDEFAULTROOT)/$$i; \\\n" path_var path_var; + printf "\tdone\n" + +let install_doc some_vfiles some_mlifiles (_,inc_r) = + let install_one_kind kind dir = + printf "\tinstall -d $(DSTROOT)$(DOCDIR)user-contrib/%s/%s\n" dir kind; + printf "\tfor i in %s/*; do \\\n" kind; + printf "\t install $$i $(DSTROOT)$(DOCDIR)user-contrib/%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"; + if some_vfiles then install_one_kind "html" "$(INSTALLDEFAULTROOT)"; + if some_mlifiles then install_one_kind "mlihtml" "$(INSTALLDEFAULTROOT)"; + end in + print "\n" + +let install (vfiles,(mlifiles,ml4files,mlfiles,mllibfiles),_,sds) inc = + let not_empty = function |[] -> false |_::_ -> true in + let cmfiles = mlfiles@ml4files in + let allcmfiles = cmfiles@mllibfiles in + if (not_empty allcmfiles) then begin + print "install-natdynlink:\n"; + install_include_by_root "COQLIB" "CMXSFILES" allcmfiles inc; + print "\n"; + end; + print "install:"; + if (not_empty allcmfiles) then print "$(if ifeq '$(HASNATDYNLINK)' 'true',install-natdynlink)"; + print "\n"; + if not_empty vfiles then install_include_by_root "COQLIB" "VOFILES" vfiles inc; + if (not_empty cmfiles) then begin + install_include_by_root "COQLIB" "CMOFILES" cmfiles inc; + install_include_by_root "COQLIB" "CMIFILES" cmfiles inc; + end; + if (not_empty mllibfiles) then + install_include_by_root "COQLIB" "CMAFILES" mllibfiles inc; + List.iter + (fun 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 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"; + List.iter + (fun x -> print "\t(cd "; print x; print " ; $(MAKE) Makefile)\n") + sds; + print "\n"; + end + +let clean sds sps = + print "clean:\n"; + print "\trm -f *~ Makefile-localvars.gen\n"; + if !some_mlfile || !some_mlifile || !some_ml4file || !some_mllibfile then begin + print "\trm -f $(CMOFILES) $(CMIFILES) $(CMXFILES) $(CMAFILES) $(CMXAFILES) $(CMXSFILES) $(OFILES)\n"; + print "\trm -f $(MLFILES:.ml=.ml.d) $(MLIFILES:.mli=.mli.d) $(ML4FILES:.ml4=.ml4.d) $(MLLIBFILES:.mllib=.mllib.d)\n"; + end; + if !some_vfile then + print "\trm -f $(VOFILES) $(VIFILES) $(GFILES) $(VFILES:.v=.v.d)\n"; + 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"; + List.iter + (fun (file,_,_) -> + if not (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") + 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") + sds; + print "\n\n"; + print "printenv: Makefile-localvars.gen\n\t@cat $^\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\n" + +let header_includes () = () + +let footer_includes () = + if !some_vfile then print "-include $(VFILES:.v=.v.d)\n.SECONDARY: $(VFILES:.v=.v.d)\n\n"; + if !some_mlfile then print "-include $(MLFILES:.ml=.ml.d)\n.SECONDARY: $(MLFILES:.ml=.ml.d)\n\n"; + if !some_mlifile then print "-include $(MLIFILES:.mli=.mli.d)\n.SECONDARY: $(MLIFILES:.mli=.mli.d)\n\n"; + if !some_ml4file then print "-include $(ML4FILES:.ml4=.ml4.d)\n.SECONDARY: $(ML4FILES:.ml4=.ml4.d)\n\n"; + if !some_mllibfile then print "-include $(MLLIBFILES:.mllib=.mllib.d)\n.SECONDARY: $(MLLIBFILES:.mllib=.mllib.d)\n\n" + +let implicit () = + let mli_rules () = + print "%.cmi: %.mli\n\t$(CAMLC) $(ZDEBUG) $(ZFLAGS) $<\n\n"; + print "%.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$(OCAMLDEP) -slash $(OCAMLLIBS) $(PP) -impl \"$<\" > \"$@\" || ( 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 "\t$(OCAMLDEP) -slash $(OCAMLLIBS) \"$<\" > \"$@\" || ( RV=$$?; rm -f \"$@\"; exit $${RV} )\n\n" in + let cmxs_rules () = + print "%.cmxs: %.cmx\n\t$(CAMLOPTLINK) $(ZDEBUG) $(ZFLAGS) -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 "%.cmxs: %.cmxa\n\t$(CAMLOPTLINK) $(ZDEBUG) $(ZFLAGS) -linkall -shared -o $@ $<\n\n"; + print "%.mllib.d: %.mllib\n"; + print "\t$(COQDEP) -slash $(COQLIBS) -c \"$<\" > \"$@\" || ( 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) -latex $< -o $@\n\n"; + print "%.html: %.v %.glob\n\t$(COQDOC) -html $< -o $@\n\n"; + print "%.g.tex: %.v\n\t$(COQDOC) -latex -g $< -o $@\n\n"; + print "%.g.html: %.v %.glob\n\t$(COQDOC) -html -g $< -o $@\n\n"; + print "%.v.d: %.v\n"; + print "\t$(COQDEP) -slash $(COQLIBS) \"$<\" > \"$@\" || ( RV=$$?; rm -f \"$@\"; exit $${RV} )\n\n" + in + if !some_mlifile then mli_rules (); + if !some_ml4file then ml4_rules (); + if !some_mlfile then ml_rules (); + if !some_mlfile || !some_ml4file then cmxs_rules (); + if !some_mllibfile then mllib_rules (); + if !some_vfile then v_rules () + +let variables opt (args,defs) = + let var_aux (v,def) = print v; print "="; print def; print "\n" in + section "Variables definitions."; + List.iter var_aux defs; + print "\n"; + print "ZFLAGS=$(OCAMLLIBS) $(COQSRCLIBS) -I $(CAMLP4LIB)\n"; + if not opt then + print "override OPT:=-byte\n" + else + print "OPT?=\n"; + begin + match args with + |[] -> () + |h::t -> print "OTHERFLAGS="; + print h; + List.iter (fun s -> print " ";print s) t; + print "\n"; + end; + (* Coq executables and relative variables *) + print "COQFLAGS?=-q $(OPT) $(COQLIBS) $(OTHERFLAGS) $(COQ_XML)\n"; + print "COQC?=$(COQBIN)coqc\n"; + print "COQDEP?=$(COQBIN)coqdep -c\n"; + print "GALLINA?=$(COQBIN)gallina\n"; + print "COQDOC?=$(COQBIN)coqdoc\n"; + (* Caml executables and relative variables *) + print "CAMLC?=$(OCAMLC) -c -rectypes\n"; + print "CAMLOPTC?=$(OCAMLOPT) -c -rectypes\n"; + print "CAMLLINK?=$(OCAMLC) -rectypes\n"; + print "CAMLOPTLINK?=$(OCAMLOPT) -rectypes\n"; + print "GRAMMARS?=grammar.cma\n"; + print "CAMLP4EXTEND?=pa_extend.cmo pa_macro.cmo q_MLast.cmo\n"; + print "CAMLP4OPTIONS?=\n"; + print "PP?=-pp \"$(CAMLP4BIN)$(CAMLP4)o -I $(CAMLLIB) -I . $(COQSRCLIBS) $(CAMLP4EXTEND) $(GRAMMARS) $(CAMLP4OPTIONS) -impl\"\n"; + print "\n" + +let parameters () = + print "NOARG: all\n\n# \n"; + print "# This Makefile may take COQBIN as argument passed as environment variables:\n"; + print "# to specify the directory where Coq binaries resides;\n"; + print "Makefile-localvars.gen:\n\t$(COQBIN)coqtop -config > $@\n\n"; + print "-include Makefile-localvars.gen\n.SECONDARY: Makefile-localvars.gen\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 + 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."; + print "OCAMLLIBS?="; print_list "\\\n " str_i; print "\n"; + 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"; + List.iter (fun c -> print " \\ + -I $(COQLIB)plugins/"; print c) Coq_config.plugins_dirs; print "\n"; + 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" + +let custom sps = + let pr_path (file,dependencies,com) = + print file; print ": "; print dependencies; print "\n"; + if com <> "" then (print "\t"; print com); print "\n\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" + in + if sds <> [] then section "Subdirectories."; + List.iter pr_subdir sds; + section "Special targets."; + print ".PHONY: "; + print_list " " + ("NOARG" :: "all" :: "opt" :: "byte" :: "archclean" :: "clean" :: "install" + :: "depend" :: "html" :: sds); + print "\n\n" + +let main_targets vfiles (mlifiles,ml4files,mlfiles,mllibfiles) other_targets inc = + begin match vfiles with + |[] -> () + |l -> + print "VFILES:="; print_list "\\\n " l; print "\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" + end; + let mlsfiles = match ml4files,mlfiles with + |[],[] -> [] + |[],ml -> + print "MLFILES:="; print_list "\\\n " ml; print "\n"; + print "CMOFILES:=$(MLFILES:.ml=.cmo)\n"; + ml + |ml4,[] -> + print "ML4FILES:="; print_list "\\\n " ml4; print "\n"; + print "CMOFILES:=$(ML4FILES:.ml4=.cmo)\n"; + ml4 + |ml4,ml -> + print "ML4FILES:="; print_list "\\\n " ml4; print "\n"; + print "MLFILES:="; print_list "\\\n " ml; print "\n"; + print "CMOFILES:=$(ML4FILES:.ml4=.cmo) $(MLFILES:.ml=.cmo)\n"; + ml@ml4 in + begin match mlsfiles with + |[] -> () + |l -> + classify_files_by_root "CMOFILES" l inc; + print "CMXFILES:=$(CMOFILES:.cmo=.cmx)\n"; + print "OFILES:=$(CMXFILES:.cmx=.o)\n"; + end; + begin match mllibfiles with + |[] -> () + |l -> + print "MLLIBFILES:="; print_list "\\\n " l; print "\n"; + print "CMAFILES:=$(MLLIBFILES:.mllib=.cma)\n"; + print "CMXAFILES:=$(CMAFILES:.cma=.cmxa)\n"; + end; + begin match mlifiles with + |[] -> () + |l -> + print "MLIFILES:="; print_list "\\\n " l; print "\n"; + end; + begin match mlifiles,mlfiles with + |[],[] -> () + |l,[] -> + print "CMIFILES:=$(MLIFILES:.mli=.cmi)\n"; + classify_files_by_root "CMIFILES" l inc; + |[],l -> + print "CMIFILES:=$(CMOFILES:.cmo=.cmi)\n"; + classify_files_by_root "CMIFILES" l inc; + |l1,l2 -> + print "CMIFILES:=$(sort $(CMOFILES:.cmo=.cmi) $(MLIFILES:.mli=.cmi))\n"; + classify_files_by_root "CMIFILES" (l1@l2) inc; + end; + begin match mllibfiles,mlsfiles with + |[],[] -> () + |l,[] -> + print "CMXSFILES:=$(CMXAFILES:.cmxa=.cmxs)\n"; + classify_files_by_root "CMXSFILES" l inc; + |[],l -> + print "CMXSFILES:=$(CMXFILES:.cmx=.cmxs)\n"; + classify_files_by_root "CMXSFILES" l inc; + |l1,l2 -> + print "CMXSFILES:=$(CMXFILES:.cmx=.cmxs) $(CMXAFILES:.cmxa=.cmxs)\n"; + classify_files_by_root "CMXSFILES" (l1@l2) inc; + end; + print "\nall: "; + if !some_vfile then print "$(VOFILES) "; + if !some_mlfile || !some_ml4file then print "$(CMOFILES) "; + if !some_mllibfile then print "$(CMAFILES) "; + if !some_mlfile || !some_ml4file || !some_mllibfile then print "$(if ifeq '$(HASNATDYNLINK)' 'true',$(CMXSFILES)) "; + print_list "\\\n " other_targets; print "\n\n"; + if !some_mlifile then + 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 "all-mli.tex: $(MLIFILES:.mli=.cmi)\n"; + print "\t$(OCAMLDOC) -latex -rectypes -o $@ -m A $(ZDEBUG) $(ZFLAGS) $(^:.cmi=.mli)\n\n"; + end; + if !some_vfile then + begin + print "spec: $(VIFILES)\n\n"; + print "gallina: $(GFILES)\n\n"; + print "html: $(GLOBFILES) $(VFILES)\n"; + print "\t- mkdir -p html\n"; + print "\t$(COQDOC) -toc -html $(COQDOCLIBS) -d html $(VFILES)\n\n"; + print "gallinahtml: $(GLOBFILES) $(VFILES)\n"; + print "\t- mkdir -p html\n"; + print "\t$(COQDOC) -toc -html -g $(COQDOCLIBS) -d html $(VFILES)\n\n"; + print "all.ps: $(VFILES)\n"; + print "\t$(COQDOC) -toc -ps $(COQDOCLIBS) -o $@ `$(COQDEP) -sort -suffix .v $(VFILES)`\n\n"; + print "all-gal.ps: $(VFILES)\n"; + print "\t$(COQDOC) -toc -ps -g $(COQDOCLIBS) -o $@ `$(COQDEP) -sort -suffix .v $(VFILES)`\n\n"; + print "all.pdf: $(VFILES)\n"; + print "\t$(COQDOC) -toc -pdf $(COQDOCLIBS) -o $@ `$(COQDEP) -sort -suffix .v $(VFILES)`\n\n"; + print "all-gal.pdf: $(VFILES)\n"; + print "\t$(COQDOC) -toc -pdf -g $(COQDOCLIBS) -o $@ `$(COQDEP) -sort -suffix .v $(VFILES)`\n\n"; + print "\n" + end + +let all_target (vfiles, 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 + section "Definition of the \"all\" target."; + main_targets vfiles mlfiles other_targets inc; + custom sps; + subdirs sds + +let banner () = + print (Printf.sprintf +"############################################################################# +## v # The Coq Proof Assistant ## +## print x; print " ") l + +let command_line args = + print "#\n# This Makefile was generated by the command line :\n"; + print "# coq_makefile "; + print_list args; + print "\n#\n\n" + +let ensure_root_dir (v,(mli,ml4,ml,mllib),_,_) ((i_inc,r_inc) as l) = + let here = absolute_dir "." 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 && not_tops mllib) then + l + else + ((".",here)::i_inc,r_inc) + +let warn_install_at_root_directory (vfiles,(mlifiles,ml4files,mlfiles,mllibfiles),_,_) (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 @ List.map fst inc_i in + let files = vfiles @ mlifiles @ ml4files @ mlfiles @ mllibfiles in + if List.exists (fun f -> List.mem (Filename.dirname f) inc_top) 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 ") + +let check_overlapping_include (_,inc_r) = + let pwd = Sys.getcwd () in + let rec 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 + Printf.eprintf "Warning: in options -R, %s and %s overlap\n" pdir pdir') l; + in aux inc_r + +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 (None,None,true,true) [] args + with Project_file.Parsing_error -> usage () in + let (v_f,(mli_f,ml4_f,ml_f,mllib_f),sps,sds as targets), inc, defs = + Project_file.split_arguments l in + + let () = match project_file with |None -> () |Some f -> make_name := f in + let () = match makefile with + |None -> () + |Some f -> makefile_name := f; output_channel := open_out f in + has_file some_vfile v_f; has_file some_mlifile mli_f; has_file some_mlfile ml_f; + has_file some_ml4file ml4_f; has_file some_mllibfile mllib_f; + let check_dep f = + if Filename.check_suffix f ".v" then some_vfile := true + else if (Filename.check_suffix f ".mli") then some_mlifile := true + else if (Filename.check_suffix f ".ml4") then some_ml4file := true + else if (Filename.check_suffix f ".ml") then some_mlfile := true + else if (Filename.check_suffix f ".mllib") then some_mllibfile := true + in + List.iter (fun (_,dependencies,_) -> + List.iter check_dep (Str.split (Str.regexp "[ \t]+") dependencies)) sps; + + let inc = ensure_root_dir targets inc in + if is_install then warn_install_at_root_directory targets inc; + check_overlapping_include inc; + banner (); + header_includes (); + warning (); + command_line args; + parameters (); + include_dirs inc; + variables opt defs; + all_target targets inc; + implicit (); + standard opt; + if is_install then install targets inc; + clean sds sps; + make_makefile sds; + footer_includes (); + warning (); + if not (makefile = None) then close_out !output_channel; + exit 0 + +let main () = + let args = + if Array.length Sys.argv = 1 then usage (); + List.tl (Array.to_list Sys.argv) + in + do_makefile args + +let _ = Printexc.catch main () diff --git a/tools/coq_makefile.ml4 b/tools/coq_makefile.ml4 deleted file mode 100644 index edbe22e73..000000000 --- a/tools/coq_makefile.ml4 +++ /dev/null @@ -1,733 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* (ML "foo.ml") *) - | MLI of string (* MLI file : foo.mli -> (MLI "foo.mli") *) - | ML4 of string (* ML4 file : foo.ml4 -> (ML4 "foo.ml4") *) - | MLLIB of string (* MLLIB file : foo.mllib -> (MLLIB "foo.mllib") *) - | V of string (* V file : foo.v -> (V "foo") *) - | Arg of string - | Special of string * string * string (* file, dependencies, command *) - | Subdir of string - | Def of string * string (* X=foo -> Def ("X","foo") *) - | Include of string - | RInclude of string * string (* -R physicalpath logicalpath *) - -let output_channel = ref stdout -let makefile_name = ref "Makefile" -let make_name = ref "" - -let some_vfile = ref false -let some_mlfile = ref false -let some_mlifile = ref false -let some_ml4file = ref false -let some_mllibfile = ref false - -let print x = output_string !output_channel x -let printf x = Printf.fprintf !output_channel x - -let rec print_list sep = function - | [ x ] -> print x - | 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 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; - print "# "; print s; print " #\n"; - print sep2; - print sep; - 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] - -[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 -[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\" -[-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\". -[VARIABLE = value]: Add the variable definition \"VARIABLE=value\" -[-byte]: compile with byte-code version of coq -[-opt]: compile with native-code version of coq -[-arg opt]: send option \"opt\" to coqc -[-no-install]: build a makefile with no install target -[-f file]: take the contents of file as arguments -[-o file]: output should go in file file -[-h]: print this usage summary -[--help]: equivalent to [-h]\n"; - exit 1 - -let is_genrule r = - let genrule = Str.regexp("%") in - Str.string_match genrule r 0 - -let absolute_dir dir = - let current = Sys.getcwd () in - Sys.chdir dir; - let dir' = Sys.getcwd () in - Sys.chdir current; - dir' - -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 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] = '/') - -let pre_canonize f = - let l = String.length f in - if l > 2 && f.[0] = '.' && f.[1] = '/' then - let n = let i = ref 2 in while !i < l && f.[!i] = '/' do incr i done; !i in - String.sub f n (l-n) - else f - -let post_canonize f = - let n = 1 + let i = ref (String.length f - 1) in while !i >= 0 && f.[!i] = '/' do decr i done; !i in - String.sub f 0 n - -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 - for i = 0 to le - 1 do - if pdir.[i] = '.' then pdir.[i] <- '/'; - done; - pdir - -let standard opt = - print "byte:\n"; - print "\t$(MAKE) all \"OPT:=-byte\"\n\n"; - print "opt:\n"; - if not opt then print "\t@echo \"WARNING: opt is disabled\"\n"; - print "\t$(MAKE) all \"OPT:="; print (if opt then "-opt" else "-byte"); - print "\"\n\n" - -let is_prefix_of_file dir f = - is_prefix dir (absolute_dir (Filename.dirname f)) - -let classify_files_by_root var files (inc_i,inc_r) = - if not (List.exists (fun (pdir,_,_) -> pdir = ".") inc_r) then - begin - (* Files in the scope of a -R option (assuming they are disjoint) *) - list_iter_i (fun i (pdir,ldir,abspdir) -> - if List.exists (is_prefix_of_file abspdir) files then - printf "%s%d:=$(patsubst %s/%%,%%,$(filter %s/%%,$(%s)))\n" - var i pdir pdir var) - inc_r; - (* Files not in the scope of a -R option *) - let pat_of_dir (pdir,_,_) = pdir^"/%" in - let pdir_patterns = String.concat " " (List.map pat_of_dir inc_r) in - printf "%s0:=$(filter-out %s,$(%s))\n" var pdir_patterns var - end - -let install_include_by_root path_var files_var files (_,inc_r) = - 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.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)$(%s)user-contrib/%s/$$i`; \\\n\t install $$i $(DSTROOT)$(%s)user-contrib/%s/$$i; \\\n" path_var pdir path_var pdir; - printf "\tdone\n" - with Not_found -> - (* Files in the scope of a -R option (assuming they are disjoint) *) - list_iter_i (fun i (pdir,ldir,abspdir) -> - if List.exists (is_prefix_of_file abspdir) files then - begin - let pdir' = physical_dir_of_logical_dir ldir in - printf "\tcd %s; for i in $(%s%d); do \\\n" pdir files_var i; - printf "\t install -d `dirname $(DSTROOT)$(%s)user-contrib/%s/$$i`; \\\n\t install $$i $(DSTROOT)$(%s)user-contrib/%s/$$i; \\\n" path_var pdir' path_var pdir'; - printf "\tdone\n" - end) inc_r; - (* Files not in the scope of a -R option *) - printf "\tfor i in $(%s0); do \\\n" files_var; - printf "\t install -d `dirname $(DSTROOT)$(%s)user-contrib/$(INSTALLDEFAULTROOT)/$$i`; \\\n\t install $$i $(DSTROOT)$(%s)user-contrib/$(INSTALLDEFAULTROOT)/$$i; \\\n" path_var path_var; - printf "\tdone\n" - -let install_doc some_vfiles some_mlifiles (_,inc_r) = - let install_one_kind kind dir = - printf "\tinstall -d $(DSTROOT)$(DOCDIR)user-contrib/%s/%s\n" dir kind; - printf "\tfor i in %s/*; do \\\n" kind; - printf "\t install $$i $(DSTROOT)$(DOCDIR)user-contrib/%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"; - if some_vfiles then install_one_kind "html" "$(INSTALLDEFAULTROOT)"; - if some_mlifiles then install_one_kind "mlihtml" "$(INSTALLDEFAULTROOT)"; - end in - print "\n" - -let install (vfiles,(mlifiles,ml4files,mlfiles,mllibfiles),_,sds) inc = - let not_empty = function |[] -> false |_::_ -> true in - let cmfiles = mlfiles@ml4files in - let allcmfiles = cmfiles@mllibfiles in - if (not_empty allcmfiles) then begin - print "install-natdynlink:\n"; - install_include_by_root "COQLIB" "CMXSFILES" allcmfiles inc; - print "\n"; - end; - print "install:"; - if (not_empty allcmfiles) then print "$(if ifeq '$(HASNATDYNLINK)' 'true',install-natdynlink)"; - print "\n"; - if not_empty vfiles then install_include_by_root "COQLIB" "VOFILES" vfiles inc; - if (not_empty cmfiles) then begin - install_include_by_root "COQLIB" "CMOFILES" cmfiles inc; - install_include_by_root "COQLIB" "CMIFILES" cmfiles inc; - end; - if (not_empty mllibfiles) then - install_include_by_root "COQLIB" "CMAFILES" mllibfiles inc; - List.iter - (fun 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 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"; - List.iter - (fun x -> print "\t(cd "; print x; print " ; $(MAKE) Makefile)\n") - sds; - print "\n"; - end - -let clean sds sps = - print "clean:\n"; - print "\trm -f *~ Makefile-localvars.gen\n"; - if !some_mlfile || !some_mlifile || !some_ml4file || !some_mllibfile then begin - print "\trm -f $(CMOFILES) $(CMIFILES) $(CMXFILES) $(CMAFILES) $(CMXAFILES) $(CMXSFILES) $(OFILES)\n"; - print "\trm -f $(MLFILES:.ml=.ml.d) $(MLIFILES:.mli=.mli.d) $(ML4FILES:.ml4=.ml4.d) $(MLLIBFILES:.mllib=.mllib.d)\n"; - end; - if !some_vfile then - print "\trm -f $(VOFILES) $(VIFILES) $(GFILES) $(VFILES:.v=.v.d)\n"; - 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"; - List.iter - (fun (file,_,_) -> - if not (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") - 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") - sds; - print "\n\n"; - print "printenv: Makefile-localvars.gen\n\t@cat $^\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\n" - -let header_includes () = () - -let footer_includes () = - if !some_vfile then print "-include $(VFILES:.v=.v.d)\n.SECONDARY: $(VFILES:.v=.v.d)\n\n"; - if !some_mlfile then print "-include $(MLFILES:.ml=.ml.d)\n.SECONDARY: $(MLFILES:.ml=.ml.d)\n\n"; - if !some_mlifile then print "-include $(MLIFILES:.mli=.mli.d)\n.SECONDARY: $(MLIFILES:.mli=.mli.d)\n\n"; - if !some_ml4file then print "-include $(ML4FILES:.ml4=.ml4.d)\n.SECONDARY: $(ML4FILES:.ml4=.ml4.d)\n\n"; - if !some_mllibfile then print "-include $(MLLIBFILES:.mllib=.mllib.d)\n.SECONDARY: $(MLLIBFILES:.mllib=.mllib.d)\n\n" - -let implicit () = - let mli_rules () = - print "%.cmi: %.mli\n\t$(CAMLC) $(ZDEBUG) $(ZFLAGS) $<\n\n"; - print "%.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$(OCAMLDEP) -slash $(OCAMLLIBS) $(PP) -impl \"$<\" > \"$@\" || ( 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 "\t$(OCAMLDEP) -slash $(OCAMLLIBS) \"$<\" > \"$@\" || ( RV=$$?; rm -f \"$@\"; exit $${RV} )\n\n" in - let cmxs_rules () = - print "%.cmxs: %.cmx\n\t$(CAMLOPTLINK) $(ZDEBUG) $(ZFLAGS) -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 "%.cmxs: %.cmxa\n\t$(CAMLOPTLINK) $(ZDEBUG) $(ZFLAGS) -linkall -shared -o $@ $<\n\n"; - print "%.mllib.d: %.mllib\n"; - print "\t$(COQDEP) -slash $(COQLIBS) -c \"$<\" > \"$@\" || ( 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) -latex $< -o $@\n\n"; - print "%.html: %.v %.glob\n\t$(COQDOC) -html $< -o $@\n\n"; - print "%.g.tex: %.v\n\t$(COQDOC) -latex -g $< -o $@\n\n"; - print "%.g.html: %.v %.glob\n\t$(COQDOC) -html -g $< -o $@\n\n"; - print "%.v.d: %.v\n"; - print "\t$(COQDEP) -slash $(COQLIBS) \"$<\" > \"$@\" || ( RV=$$?; rm -f \"$@\"; exit $${RV} )\n\n" - in - if !some_mlifile then mli_rules (); - if !some_ml4file then ml4_rules (); - if !some_mlfile then ml_rules (); - if !some_mlfile || !some_ml4file then cmxs_rules (); - if !some_mllibfile then mllib_rules (); - if !some_vfile then v_rules () - -let variables opt (args,defs) = - let var_aux (v,def) = print v; print "="; print def; print "\n" in - section "Variables definitions."; - List.iter var_aux defs; - print "\n"; - print "ZFLAGS=$(OCAMLLIBS) $(COQSRCLIBS) -I $(CAMLP4LIB)\n"; - if not opt then - print "override OPT:=-byte\n" - else - print "OPT?=\n"; - begin - match args with - |[] -> () - |h::t -> print "OTHERFLAGS="; - print h; - List.iter (fun s -> print " ";print s) t; - print "\n"; - end; - (* Coq executables and relative variables *) - print "COQFLAGS?=-q $(OPT) $(COQLIBS) $(OTHERFLAGS) $(COQ_XML)\n"; - print "COQC?=$(COQBIN)coqc\n"; - print "COQDEP?=$(COQBIN)coqdep -c\n"; - print "GALLINA?=$(COQBIN)gallina\n"; - print "COQDOC?=$(COQBIN)coqdoc\n"; - (* Caml executables and relative variables *) - print "CAMLC?=$(OCAMLC) -c -rectypes\n"; - print "CAMLOPTC?=$(OCAMLOPT) -c -rectypes\n"; - print "CAMLLINK?=$(OCAMLC) -rectypes\n"; - print "CAMLOPTLINK?=$(OCAMLOPT) -rectypes\n"; - print "GRAMMARS?=grammar.cma\n"; - print "CAMLP4EXTEND?=pa_extend.cmo pa_macro.cmo q_MLast.cmo\n"; - print "CAMLP4OPTIONS?=\n"; - print "PP?=-pp \"$(CAMLP4BIN)$(CAMLP4)o -I $(CAMLLIB) -I . $(COQSRCLIBS) $(CAMLP4EXTEND) $(GRAMMARS) $(CAMLP4OPTIONS) -impl\"\n"; - print "\n" - -let parameters () = - print "NOARG: all\n\n# \n"; - print "# This Makefile may take COQBIN as argument passed as environment variables:\n"; - print "# to specify the directory where Coq binaries resides;\n"; - print "Makefile-localvars.gen:\n\t$(COQBIN)coqtop -config > $@\n\n"; - print "-include Makefile-localvars.gen\n.SECONDARY: Makefile-localvars.gen\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 - 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."; - print "OCAMLLIBS?="; print_list "\\\n " str_i; print "\n"; - 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"; - List.iter (fun c -> print " \\ - -I $(COQLIB)plugins/"; print c) Coq_config.plugins_dirs; print "\n"; - 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" - -let custom sps = - let pr_path (file,dependencies,com) = - print file; print ": "; print dependencies; print "\n"; - if com <> "" then (print "\t"; print com); print "\n\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" - in - if sds <> [] then section "Subdirectories."; - List.iter pr_subdir sds; - section "Special targets."; - print ".PHONY: "; - print_list " " - ("NOARG" :: "all" :: "opt" :: "byte" :: "archclean" :: "clean" :: "install" - :: "depend" :: "html" :: sds); - print "\n\n" - -(* Return: ((v,(mli,ml4,ml,mllib),special,subdir),(i_inc,r_inc),(args,defs)) *) -let rec split_arguments = function - | V n :: r -> - let (v,m,o,s),i,d = split_arguments r in ((pre_canonize n::v,m,o,s),i,d) - | ML n :: r -> - let (v,(mli,ml4,ml,mllib),o,s),i,d = split_arguments r in ((v,(mli,ml4,pre_canonize n::ml,mllib),o,s),i,d) - | MLI n :: r -> - let (v,(mli,ml4,ml,mllib),o,s),i,d = split_arguments r in ((v,(pre_canonize n::mli,ml4,ml,mllib),o,s),i,d) - | ML4 n :: r -> - let (v,(mli,ml4,ml,mllib),o,s),i,d = split_arguments r in ((v,(mli,pre_canonize n::ml4,ml,mllib),o,s),i,d) - | MLLIB n :: r -> - let (v,(mli,ml4,ml,mllib),o,s),i,d = split_arguments r in ((v,(mli,ml4,ml,pre_canonize n::mllib),o,s),i,d) - | Special (n,dep,c) :: r -> - let (v,m,o,s),i,d = split_arguments r in ((v,m,(n,dep,c)::o,s),i,d) - | Subdir n :: r -> - let (v,m,o,s),i,d = split_arguments r in ((v,m,o,n::s),i,d) - | Include p :: r -> - let t,(i,r),d = split_arguments r in (t,((post_canonize p,absolute_dir p)::i,r),d) - | RInclude (p,l) :: r -> - let t,(i,r),d = split_arguments r in (t,(i,(post_canonize p,l,absolute_dir p)::r),d) - | Def (v,def) :: r -> - let t,i,(args,defs) = split_arguments r in (t,i,(args,(v,def)::defs)) - | Arg a :: r -> - let t,i,(args,defs) = split_arguments r in (t,i,(a::args,defs)) - | [] -> ([],([],[],[],[]),[],[]),([],[]),([],[]) - -let main_targets vfiles (mlifiles,ml4files,mlfiles,mllibfiles) other_targets inc = - begin match vfiles with - |[] -> () - |l -> - print "VFILES:="; print_list "\\\n " l; print "\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" - end; - let mlsfiles = match ml4files,mlfiles with - |[],[] -> [] - |[],ml -> - print "MLFILES:="; print_list "\\\n " ml; print "\n"; - print "CMOFILES:=$(MLFILES:.ml=.cmo)\n"; - ml - |ml4,[] -> - print "ML4FILES:="; print_list "\\\n " ml4; print "\n"; - print "CMOFILES:=$(ML4FILES:.ml4=.cmo)\n"; - ml4 - |ml4,ml -> - print "ML4FILES:="; print_list "\\\n " ml4; print "\n"; - print "MLFILES:="; print_list "\\\n " ml; print "\n"; - print "CMOFILES:=$(ML4FILES:.ml4=.cmo) $(MLFILES:.ml=.cmo)\n"; - ml@ml4 in - begin match mlsfiles with - |[] -> () - |l -> - classify_files_by_root "CMOFILES" l inc; - print "CMXFILES:=$(CMOFILES:.cmo=.cmx)\n"; - print "OFILES:=$(CMXFILES:.cmx=.o)\n"; - end; - begin match mllibfiles with - |[] -> () - |l -> - print "MLLIBFILES:="; print_list "\\\n " l; print "\n"; - print "CMAFILES:=$(MLLIBFILES:.mllib=.cma)\n"; - print "CMXAFILES:=$(CMAFILES:.cma=.cmxa)\n"; - end; - begin match mlifiles with - |[] -> () - |l -> - print "MLIFILES:="; print_list "\\\n " l; print "\n"; - end; - begin match mlifiles,mlfiles with - |[],[] -> () - |l,[] -> - print "CMIFILES:=$(MLIFILES:.mli=.cmi)\n"; - classify_files_by_root "CMIFILES" l inc; - |[],l -> - print "CMIFILES:=$(CMOFILES:.cmo=.cmi)\n"; - classify_files_by_root "CMIFILES" l inc; - |l1,l2 -> - print "CMIFILES:=$(sort $(CMOFILES:.cmo=.cmi) $(MLIFILES:.mli=.cmi))\n"; - classify_files_by_root "CMIFILES" (l1@l2) inc; - end; - begin match mllibfiles,mlsfiles with - |[],[] -> () - |l,[] -> - print "CMXSFILES:=$(CMXAFILES:.cmxa=.cmxs)\n"; - classify_files_by_root "CMXSFILES" l inc; - |[],l -> - print "CMXSFILES:=$(CMXFILES:.cmx=.cmxs)\n"; - classify_files_by_root "CMXSFILES" l inc; - |l1,l2 -> - print "CMXSFILES:=$(CMXFILES:.cmx=.cmxs) $(CMXAFILES:.cmxa=.cmxs)\n"; - classify_files_by_root "CMXSFILES" (l1@l2) inc; - end; - print "\nall: "; - if !some_vfile then print "$(VOFILES) "; - if !some_mlfile || !some_ml4file then print "$(CMOFILES) "; - if !some_mllibfile then print "$(CMAFILES) "; - if !some_mlfile || !some_ml4file || !some_mllibfile then print "$(if ifeq '$(HASNATDYNLINK)' 'true',$(CMXSFILES)) "; - print_list "\\\n " other_targets; print "\n\n"; - if !some_mlifile then - 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 "all-mli.tex: $(MLIFILES:.mli=.cmi)\n"; - print "\t$(OCAMLDOC) -latex -rectypes -o $@ -m A $(ZDEBUG) $(ZFLAGS) $(^:.cmi=.mli)\n\n"; - end; - if !some_vfile then - begin - print "spec: $(VIFILES)\n\n"; - print "gallina: $(GFILES)\n\n"; - print "html: $(GLOBFILES) $(VFILES)\n"; - print "\t- mkdir -p html\n"; - print "\t$(COQDOC) -toc -html $(COQDOCLIBS) -d html $(VFILES)\n\n"; - print "gallinahtml: $(GLOBFILES) $(VFILES)\n"; - print "\t- mkdir -p html\n"; - print "\t$(COQDOC) -toc -html -g $(COQDOCLIBS) -d html $(VFILES)\n\n"; - print "all.ps: $(VFILES)\n"; - print "\t$(COQDOC) -toc -ps $(COQDOCLIBS) -o $@ `$(COQDEP) -sort -suffix .v $(VFILES)`\n\n"; - print "all-gal.ps: $(VFILES)\n"; - print "\t$(COQDOC) -toc -ps -g $(COQDOCLIBS) -o $@ `$(COQDEP) -sort -suffix .v $(VFILES)`\n\n"; - print "all.pdf: $(VFILES)\n"; - print "\t$(COQDOC) -toc -pdf $(COQDOCLIBS) -o $@ `$(COQDEP) -sort -suffix .v $(VFILES)`\n\n"; - print "all-gal.pdf: $(VFILES)\n"; - print "\t$(COQDOC) -toc -pdf -g $(COQDOCLIBS) -o $@ `$(COQDEP) -sort -suffix .v $(VFILES)`\n\n"; - print "\n" - end - -let all_target (vfiles, 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 - section "Definition of the \"all\" target."; - main_targets vfiles mlfiles other_targets inc; - custom sps; - subdirs sds - -let parse f = - let rec string = parser - | [< '' ' | '\n' | '\t' >] -> "" - | [< 'c; s >] -> (String.make 1 c)^(string s) - | [< >] -> "" - and string2 = parser - | [< ''"' >] -> "" - | [< 'c; s >] -> (String.make 1 c)^(string2 s) - and skip_comment = parser - | [< ''\n'; s >] -> s - | [< 'c; s >] -> skip_comment s - | [< >] -> [< >] - and args = parser - | [< '' ' | '\n' | '\t'; s >] -> args s - | [< ''#'; s >] -> args (skip_comment s) - | [< ''"'; str = string2; s >] -> ("" ^ str) :: args s - | [< 'c; str = string; s >] -> ((String.make 1 c) ^ str) :: (args s) - | [< >] -> [] - in - let c = open_in f in - let res = args (Stream.of_channel c) in - close_in c; - res - -let rec process_cmd_line ((project_file,makefile,install,opt) as opts) l = function - | [] -> opts,List.rev l - | ("-h"|"--help") :: _ -> - usage () - | ("-no-opt"|"-byte") :: r -> - process_cmd_line (project_file,makefile,install,false) l r - | ("-full"|"-opt") :: r -> - process_cmd_line (project_file,makefile,install,true) l r - | "-impredicative-set" :: r -> - prerr_string "Please now use \"-arg -impredicative-set\" instead of \"-impredicative-set\" alone to be more uniform.\n"; - process_cmd_line opts (Arg "-impredicative_set" :: l) r - | "-no-install" :: r -> - if not install then prerr_string "Warning: -no-install sets more than once.\n"; - process_cmd_line (project_file,makefile,false,opt) l r - | "-custom" :: com :: dependencies :: file :: r -> - process_cmd_line opts (Special (file,dependencies,com) :: l) r - | "-I" :: d :: r -> - process_cmd_line opts (Include d :: l) r - | "-R" :: p :: lp :: r -> - process_cmd_line opts (RInclude (p,lp) :: l) r - | ("-I"|"-custom") :: _ -> - usage () - | "-f" :: file :: r -> - let () = match project_file with - | None -> () - | Some _ -> prerr_string - "Warning: Several features will not work with multiple project files.\n" - in process_cmd_line (Some file,makefile,install,opt) l ((parse file)@r) - | ["-f"] -> - usage () - | "-o" :: file :: r -> - let () = match makefile with - |None -> () - |Some f -> - prerr_string "Warning: Only one output file in genererated. "; - prerr_string f; prerr_string " will not.\n" - in process_cmd_line (project_file,Some file,install,opt) l r - | v :: "=" :: def :: r -> - process_cmd_line opts (Def (v,def) :: l) r - | "-arg" :: a :: r -> - process_cmd_line opts (Arg a :: l) r - | f :: r -> - process_cmd_line opts (( - if Filename.check_suffix f ".v" then V f - else if (Filename.check_suffix f ".ml") then ML f - else if (Filename.check_suffix f ".ml4") then ML4 f - else if (Filename.check_suffix f ".mli") then MLI f - else if (Filename.check_suffix f ".mllib") then MLLIB f - else Subdir f) :: l) r - -let banner () = - print (Printf.sprintf -"############################################################################# -## v # The Coq Proof Assistant ## -## print x; print " ") l - -let command_line args = - print "#\n# This Makefile was generated by the command line :\n"; - print "# coq_makefile "; - print_list args; - print "\n#\n\n" - -let ensure_root_dir (v,(mli,ml4,ml,mllib),_,_) ((i_inc,r_inc) as l) = - let here = absolute_dir "." 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 && not_tops mllib) then - l - else - ((".",here)::i_inc,r_inc) - -let warn_install_at_root_directory (vfiles,(mlifiles,ml4files,mlfiles,mllibfiles),_,_) (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 @ List.map fst inc_i in - let files = vfiles @ mlifiles @ ml4files @ mlfiles @ mllibfiles in - if List.exists (fun f -> List.mem (Filename.dirname f) inc_top) 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 ") - -let check_overlapping_include (_,inc_r) = - let pwd = Sys.getcwd () in - let rec 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 - Printf.eprintf "Warning: in options -R, %s and %s overlap\n" pdir pdir') l; - in aux inc_r - -let do_makefile args = - let has_file var = function - |[] -> var := false - |_::_ -> var := true in - let (project_file,makefile,is_install,opt),l = - process_cmd_line (None,None,true,true) [] args in - let (v_f,(mli_f,ml4_f,ml_f,mllib_f),sps,sds as targets), inc, defs = - split_arguments l in - - let () = match project_file with |None -> () |Some f -> make_name := f in - let () = match makefile with - |None -> () - |Some f -> makefile_name := f; output_channel := open_out f in - has_file some_vfile v_f; has_file some_mlifile mli_f; has_file some_mlfile ml_f; - has_file some_ml4file ml4_f; has_file some_mllibfile mllib_f; - let check_dep f = - if Filename.check_suffix f ".v" then some_vfile := true - else if (Filename.check_suffix f ".mli") then some_mlifile := true - else if (Filename.check_suffix f ".ml4") then some_ml4file := true - else if (Filename.check_suffix f ".ml") then some_mlfile := true - else if (Filename.check_suffix f ".mllib") then some_mllibfile := true - in - List.iter (fun (_,dependencies,_) -> - List.iter check_dep (Str.split (Str.regexp "[ \t]+") dependencies)) sps; - - let inc = ensure_root_dir targets inc in - if is_install then warn_install_at_root_directory targets inc; - check_overlapping_include inc; - banner (); - header_includes (); - warning (); - command_line args; - parameters (); - include_dirs inc; - variables opt defs; - all_target targets inc; - implicit (); - standard opt; - if is_install then install targets inc; - clean sds sps; - make_makefile sds; - footer_includes (); - warning (); - if not (makefile = None) then close_out !output_channel; - exit 0 - -let main () = - let args = - if Array.length Sys.argv = 1 then usage (); - List.tl (Array.to_list Sys.argv) - in - do_makefile args - -let _ = Printexc.catch main () -- cgit v1.2.3