From cfbfe13f5b515ae2e3c6cdd97e2ccee03bc26e56 Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Sun, 1 Feb 2009 00:54:40 +0100 Subject: Imported Upstream version 8.2~rc2+dfsg --- tools/coq_makefile.ml4 | 441 +++++++++++++++++++++++++++++++------------------ 1 file changed, 284 insertions(+), 157 deletions(-) (limited to 'tools/coq_makefile.ml4') diff --git a/tools/coq_makefile.ml4 b/tools/coq_makefile.ml4 index d1d0d854..3fbf71dd 100644 --- a/tools/coq_makefile.ml4 +++ b/tools/coq_makefile.ml4 @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: coq_makefile.ml4 11255 2008-07-24 16:57:13Z notin $ *) +(* $Id: coq_makefile.ml4 11771 2009-01-09 18:00:56Z notin $ *) (* créer un Makefile pour un développement Coq automatiquement *) @@ -29,6 +29,7 @@ let some_mlfile = ref false let opt = ref "-opt" let impredicative_set = ref false +let no_install = ref false let print x = output_string !output_channel x let printf x = Printf.fprintf !output_channel x @@ -38,6 +39,14 @@ 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 best_ocamlc = + if Coq_config.best = "opt" then "ocamlc.opt" else "ocamlc" +let best_ocamlopt = + if Coq_config.best = "opt" then "ocamlopt.opt" else "ocamlopt" + let section s = let l = String.length s in let sep = String.make (l+5) '#' @@ -58,10 +67,11 @@ let usage () = coq_makefile [subdirectory] .... [file.v] ... [file.ml] ... [-custom command dependencies file] ... [-I dir] ... [-R physicalpath logicalpath] - ... [VARIABLE = value] ... [-opt|-byte] [-f file] [-o file] [-h] [--help] + ... [VARIABLE = value] ... [-opt|-byte] [-impredicative-set] [-no-install] + [-f file] [-o file] [-h] [--help] [file.v]: Coq file to be compiled -[file.ml]: ML file to be compiled +[file.ml]: Objective Caml file to be compiled [subdirectory] : subdirectory that should be \"made\" [-custom command dependencies file]: add target \"file\" with command \"command\" and dependencies \"dependencies\" @@ -73,26 +83,118 @@ coq_makefile [subdirectory] .... [file.v] ... [file.ml] ... [-custom [-byte]: compile with byte-code version of coq [-opt]: compile with native-code version of coq [-impredicative-set]: compile with option -impredicative-set of coq +[-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 standard sds sps = +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 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 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 is_absolute_prefix dir dir' = + is_prefix (absolute_dir dir) (absolute_dir dir') + +let is_included dir = function + | RInclude (dir',_) -> is_absolute_prefix dir' dir + | Include dir' -> absolute_dir dir = absolute_dir dir' + | _ -> false + +let has_top_file = function + | ML s | V s -> s = Filename.basename s + | _ -> false + +let physical_dir_of_logical_dir ldir = + let pdir = String.copy ldir in + for i = 0 to String.length ldir - 1 do + if pdir.[i] = '.' then pdir.[i] <- '/'; + done; + pdir + +let standard ()= print "byte:\n"; print "\t$(MAKE) all \"OPT:=-byte\"\n\n"; print "opt:\n"; if !opt = "" then print "\t@echo \"WARNING: opt is disabled\"\n"; - print "\t$(MAKE) all \"OPT:="; print !opt; print "\"\n\n"; + print "\t$(MAKE) all \"OPT:="; print !opt; 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 var files (_,inc_r) = + try + (* All files caught by a -R . option (assuming it is the only one) *) + let ldir = List.assoc "." (List.map (fun (p,l,_) -> (p,l)) inc_r) in + let pdir = physical_dir_of_logical_dir ldir in + printf "\t(for i in $(%s); do \\\n" var; + printf "\t install -D $$i $(COQLIB)/user-contrib/%s/$$i; \\\n" pdir; + printf "\t done)\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 "\t(cd %s; for i in $(%s%d); do \\\n" pdir var i; + printf "\t install -D $$i $(COQLIB)/user-contrib/%s/$$i; \\\n" pdir'; + printf "\t done)\n" + end) inc_r; + (* Files not in the scope of a -R option *) + printf "\t(for i in $(%s0); do \\\n" var; + printf "\t install -D $$i $(COQLIB)/user-contrib/$(INSTALLDEFAULTROOT)/$$i; \\\n"; + printf "\t done)\n" + +let install (vfiles,mlfiles,_,sds) inc = print "install:\n"; - print "\tmkdir -p `$(COQC) -where`/user-contrib\n"; - if !some_vfile then print "\tcp -f $(VOFILES) `$(COQC) -where`/user-contrib\n"; - if !some_mlfile then print "\tcp -f *.cmo `$(COQC) -where`/user-contrib\n"; + print "\tmkdir -p $(COQLIB)/user-contrib\n"; + if !some_vfile then install_include_by_root "VOFILES" vfiles inc; + if !some_mlfile then install_include_by_root "CMOFILES" mlfiles inc; + if !some_mlfile then install_include_by_root "CMIFILES" mlfiles inc; + if Coq_config.has_natdynlink && !some_mlfile then + install_include_by_root "CMXSFILES" mlfiles inc; List.iter - (fun x -> print "\t(cd "; print x; print " ; $(MAKE) install)\n") + (fun x -> + printf "\t(cd %s; $(MAKE) INSTALLDEFAULTROOT=$(INSTALLDEFAULTROOT)/%s install)\n" x x) sds; - print "\n"; + print "\n" + +let make_makefile sds = if !make_name <> "" then begin printf "%s: %s\n" !makefile_name !make_name; printf "\tmv -f %s %s.bak\n" !makefile_name !makefile_name; @@ -102,16 +204,22 @@ let standard sds sps = (fun x -> print "\t(cd "; print x; print " ; $(MAKE) Makefile)\n") sds; print "\n"; - end; + end + +let clean sds sps = print "clean:\n"; - print "\trm -f *.cmo *.cmi *.cmx *.o $(VOFILES) $(VIFILES) $(GFILES) *~\n"; - print "\trm -f all.ps all-gal.ps all.glob $(VFILES:.v=.glob) $(HTMLFILES) \ + print "\trm -f $(VOFILES) $(VIFILES) $(GFILES) *~\n"; + print "\trm -f all.ps all-gal.ps all.pdf all-gal.pdf all.glob $(VFILES:.v=.glob) $(HTMLFILES) \ $(GHTMLFILES) $(VFILES:.v=.tex) $(VFILES:.v=.g.tex) $(VFILES:.v=.v.d)\n"; if !some_mlfile then print "\trm -f $(CMOFILES) $(MLFILES:.ml=.cmi) $(MLFILES:.ml=.ml.d)\n"; + if Coq_config.has_natdynlink && !some_mlfile then + print "\trm -f $(CMXSFILES) $(CMXSFILES:.cmxs=.o)\n"; print "\t- rm -rf html\n"; List.iter - (fun (file,_,_) -> print "\t- rm -f "; print file; print "\n") + (fun (file,_,_) -> + if not (is_genrule file) then + (print "\t- rm -f "; print file; print "\n")) sps; List.iter (fun x -> print "\t(cd "; print x; print " ; $(MAKE) clean)\n") @@ -122,19 +230,26 @@ let standard sds sps = List.iter (fun x -> print "\t(cd "; print x; print " ; $(MAKE) archclean)\n") sds; - print "\n\n" + print "\n\n"; + print "printenv: \n\t@echo CAMLC =\t$(CAMLC)\n\t@echo CAMLOPTC =\t$(CAMLOPTC)\n"; + print "\t@echo CAMLP4LIB =\t$(CAMLP4LIB)\n\n" -let includes () = +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" let implicit () = let ml_rules () = print "%.cmi: %.mli\n\t$(CAMLC) $(ZDEBUG) $(ZFLAGS) $<\n\n"; - print "%.cmo: %.ml\n\t$(CAMLC) $(ZDEBUG) $(ZFLAGS) $(PP) $<\n\n"; - print "%.cmx: %.ml\n\t$(CAMLOPTC) $(ZDEBUG) $(ZFLAGS) $(PP) $<\n\n"; + print "%.cmo: %.ml\n\t$(CAMLC) $(ZDEBUG) $(ZFLAGS) -c $(PP) $<\n\n"; + print "%.cmx: %.ml\n\t$(CAMLOPTC) $(ZDEBUG) $(ZFLAGS) -c $(PP) $<\n\n"; + print "%.cmxs: %.ml\n\t$(CAMLOPTC) $(ZDEBUG) $(ZFLAGS) -shared -o $@ $(PP) $<\n\n"; + 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 "%.ml.d: %.ml\n"; - print "\t$(CAMLBIN)ocamldep -slash $(ZFLAGS) $(PP) \"$<\" > \"$@\"\n\n" + print "\t$(CAMLBIN)ocamldep -slash $(COQSRCLIBS) $(PP) \"$<\" > \"$@\"\n\n" and v_rule () = print "%.vo %.glob: %.v\n\t$(COQC) -dump-glob $*.glob $(COQDEBUG) $(COQFLAGS) $*\n\n"; print "%.vi: %.v\n\t$(COQC) -i $(COQDEBUG) $(COQFLAGS) $*\n\n"; @@ -149,34 +264,10 @@ let implicit () = if !some_mlfile then ml_rules (); if !some_vfile then v_rule () -let variables l = - let rec var_aux = function - | [] -> () - | Def(v,def) :: r -> print v; print "="; print def; print "\n"; var_aux r - | _ :: r -> var_aux r - in +let variables defs = + let var_aux (v,def) = print v; print "="; print def; print "\n" in section "Variables definitions."; - print "CAMLP4:=$(notdir $(CAMLP4LIB))\n"; - if Coq_config.local then - (print "COQSRC:=$(COQTOP)\n"; - print "COQSRCLIBS:=-I $(COQTOP)/kernel -I $(COQTOP)/lib \\ - -I $(COQTOP)/library -I $(COQTOP)/parsing \\ - -I $(COQTOP)/pretyping -I $(COQTOP)/interp \\ - -I $(COQTOP)/proofs -I $(COQTOP)/tactics \\ - -I $(COQTOP)/toplevel -I $(COQTOP)/contrib/cc \\ - -I $(COQTOP)/contrib/dp -I $(COQTOP)/contrib/extraction \\ - -I $(COQTOP)/contrib/field -I $(COQTOP)/contrib/firstorder \\ - -I $(COQTOP)/contrib/fourier -I $(COQTOP)/contrib/funind \\ - -I $(COQTOP)/contrib/interface -I $(COQTOP)/contrib/jprover \\ - -I $(COQTOP)/contrib/micromega -I $(COQTOP)/contrib/omega \\ - -I $(COQTOP)/contrib/ring -I $(COQTOP)/contrib/romega \\ - -I $(COQTOP)/contrib/rtauto -I $(COQTOP)/contrib/setoid_ring \\ - -I $(COQTOP)/contrib/subtac -I $(COQTOP)/contrib/xml \\ - -I $(CAMLP4LIB)\n") - else - (print "COQSRC:=$(shell $(COQBIN)coqc -where)\n"; - print "COQSRCLIBS:=-I $(COQSRC)\n"); - print "ZFLAGS:=$(OCAMLLIBS) $(COQSRCLIBS)\n"; + print "ZFLAGS=$(OCAMLLIBS) $(COQSRCLIBS) -I $(CAMLP4LIB)\n"; if !opt = "-byte" then print "override OPT:=-byte\n" else @@ -184,81 +275,62 @@ let variables l = if !impredicative_set = true then print "OTHERFLAGS=-impredicative-set\n"; (* Coq executables and relative variables *) print "COQFLAGS:=-q $(OPT) $(COQLIBS) $(OTHERFLAGS) $(COQ_XML)\n"; + print "ifdef CAMLBIN\n COQMKTOPFLAGS:=-camlbin $(CAMLBIN) -camlp4bin $(CAMLP4BIN)\nendif\n"; print "COQC:=$(COQBIN)coqc\n"; print "COQDEP:=$(COQBIN)coqdep -c\n"; print "GALLINA:=$(COQBIN)gallina\n"; print "COQDOC:=$(COQBIN)coqdoc\n"; + print "COQMKTOP:=$(COQBIN)coqmktop\n"; (* Caml executables and relative variables *) - printf "CAMLC:=$(CAMLBIN)ocamlc -rectypes -c\n"; - printf "CAMLOPTC:=$(CAMLBIN)ocamlopt -rectypes -c\n"; - printf "CAMLLINK:=$(CAMLBIN)ocamlc -rectypes\n"; - printf "CAMLOPTLINK:=$(CAMLBIN)ocamlopt -rectypes\n"; + printf "CAMLC:=$(CAMLBIN)%s -rectypes\n" best_ocamlc; + printf "CAMLOPTC:=$(CAMLBIN)%s -rectypes\n" best_ocamlopt; + printf "CAMLLINK:=$(CAMLBIN)%s -rectypes\n" best_ocamlc; + printf "CAMLOPTLINK:=$(CAMLBIN)%s -rectypes\n" best_ocamlopt; print "GRAMMARS:=grammar.cma\n"; print "CAMLP4EXTEND:=pa_extend.cmo pa_macro.cmo q_MLast.cmo\n"; - - (if Coq_config.local then - print "PP:=-pp \"$(CAMLBIN)$(CAMLP4)o -I . -I $(COQTOP)/parsing $(CAMLP4EXTEND) $(GRAMMARS) -impl\"\n" - else - print "PP:=-pp \"$(CAMLBIN)$(CAMLP4)o -I . -I $(COQSRC) $(CAMLP4EXTEND) $(GRAMMARS) -impl\"\n"); - var_aux l; + print "CAMLP4OPTIONS:=\n"; + List.iter var_aux defs; + print "PP:=-pp \"$(CAMLP4BIN)$(CAMLP4)o -I . $(COQSRCLIBS) $(CAMLP4EXTEND) $(GRAMMARS) $(CAMLP4OPTIONS) -impl\"\n"; print "\n" -let absolute_dir dir = - let current = Sys.getcwd () in - Sys.chdir dir; - let dir' = Sys.getcwd () in - Sys.chdir current; - dir' - -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 parameters () = + print "# \n"; + print "# This Makefile may take 3 arguments passed as environment variables:\n"; + print "# - COQBIN to specify the directory where Coq binaries resides;\n"; + print "# - CAMLBIN and CAMLP4BIN to give the path for the OCaml and Camlp4/5 binaries.\n"; + print "COQLIB:=$(shell $(COQBIN)coqtop -where | sed -e 's/\\\\/\\\\\\\\/g')\n"; + print "CAMLP4:=\"$(shell $(COQBIN)coqtop -config | awk -F = '/CAMLP4=/{print $$2}')\"\n"; + print "ifndef CAMLP4BIN\n CAMLP4BIN:=$(CAMLBIN)\nendif\n\n"; + print "CAMLP4LIB:=$(shell $(CAMLP4BIN)$(CAMLP4) -where)\n\n" -let is_included dir = function - | RInclude (dir',_) -> is_prefix (absolute_dir dir') (absolute_dir dir) - | Include dir' -> absolute_dir dir = absolute_dir dir' - | _ -> false - -let dir_of_target t = - match t with - | RInclude (dir,_) -> dir - | Include dir -> dir - | _ -> assert false - -let include_dirs l = - let rec split_includes l = - match l with - | [] -> [], [] - | Include _ as i :: rem -> - let ri, rr = split_includes rem in - (i :: ri), rr - | RInclude _ as r :: rem -> - let ri, rr = split_includes rem in - ri, (r :: rr) - | _ :: rem -> split_includes rem - in - let rec parse_includes l = - match l with - | [] -> [] - | Include x :: rem -> ("-I " ^ x) :: parse_includes rem - | RInclude (p,l) :: rem -> - let l' = if l = "" then "\"\"" else l in - ("-R " ^ p ^ " " ^ l') :: parse_includes rem - | _ :: rem -> parse_includes rem - in - let l' = if List.exists (is_included ".") l then l else Include "." :: l in - let inc_i, inc_r = split_includes l' in - let inc_i' = List.filter (fun i -> not (List.exists (fun i' -> is_included (dir_of_target i) i') inc_r)) inc_i in +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_absolute_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_includes inc_r in - section "Libraries definition."; - print "CAMLP4LIB:=$(shell $(CAMLBIN)camlp5 -where 2> /dev/null || $(CAMLBIN)camlp4 -where)\n"; + let str_r = parse_rec_includes inc_r in + section "Libraries definitions."; print "OCAMLLIBS:=-I $(CAMLP4LIB) "; 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 -I $(COQLIB)/contrib/cc -I $(COQLIB)/contrib/dp \\ + -I $(COQLIB)/contrib/extraction -I $(COQLIB)/contrib/field \\ + -I $(COQLIB)/contrib/firstorder -I $(COQLIB)/contrib/fourier \\ + -I $(COQLIB)/contrib/funind -I $(COQLIB)/contrib/interface \\ + -I $(COQLIB)/contrib/micromega -I $(COQLIB)/contrib/omega \\ + -I $(COQLIB)/contrib/ring -I $(COQLIB)/contrib/romega \\ + -I $(COQLIB)/contrib/rtauto -I $(COQLIB)/contrib/setoid_ring \\ + -I $(COQLIB)/contrib/subtac -I $(COQLIB)/contrib/xml\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 rec special = function | [] -> [] | Special (file,deps,com) :: r -> (file,deps,com) :: (special r) @@ -272,15 +344,10 @@ let custom sps = if sps <> [] then section "Custom targets."; List.iter pr_sp sps -let subdirs l = - let rec subdirs_aux = function - | [] -> [] - | Subdir x :: r -> x :: (subdirs_aux r) - | _ :: r -> subdirs_aux r - and pr_subdir s = +let subdirs sds = + let pr_subdir s = print s; print ":\n\tcd "; print s; print " ; $(MAKE) all\n\n" in - let sds = subdirs_aux l in if sds <> [] then section "Subdirectories."; List.iter pr_subdir sds; section "Special targets."; @@ -288,30 +355,31 @@ let subdirs l = print_list " " ("all" :: "opt" :: "byte" :: "archclean" :: "clean" :: "install" :: "depend" :: "html" :: sds); - print "\n\n"; - sds - - -let all_target l = - let rec parse_arguments l = - match l with - | ML n :: r -> let v,m,o = parse_arguments r in (v,n::m,o) - | Subdir n :: r -> let v,m,o = parse_arguments r in (v,m,n::o) - | V n :: r -> let v,m,o = parse_arguments r in (n::v,m,o) - | Special (n,_,_) :: r -> let v,m,o = parse_arguments r in (v,m,n::o) - | Include _ :: r -> parse_arguments r - | RInclude _ :: r -> parse_arguments r - | Def _ :: r -> parse_arguments r - | [] -> [],[],[] - in - let - vfiles, mlfiles, other_targets = parse_arguments l - in - section "Definition of the \"all\" target."; + print "\n\n" + +let rec split_arguments = function + | V n :: r -> + let (v,m,o,s),i,d = split_arguments r in ((canonize n::v,m,o,s),i,d) + | ML n :: r -> + let (v,m,o,s),i,d = split_arguments r in ((v,canonize n::m,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,((p,absolute_dir p)::i,r),d) + | RInclude (p,l) :: r -> + let t,(i,r),d = split_arguments r in (t,(i,(p,l,absolute_dir p)::r),d) + | Def (v,def) :: r -> + let t,i,d = split_arguments r in (t,i,(v,def)::d) + | [] -> ([],[],[],[]),([],[]),[] + +let main_targets vfiles mlfiles other_targets inc = if !some_vfile then begin print "VFILES:="; print_list "\\\n " vfiles; print "\n"; print "VOFILES:=$(VFILES:.v=.vo)\n"; + classify_files_by_root "VOFILES" vfiles inc; print "GLOBFILES:=$(VFILES:.v=.glob)\n"; print "VIFILES:=$(VFILES:.v=.vi)\n"; print "GFILES:=$(VFILES:.v=.g)\n"; @@ -322,10 +390,18 @@ let all_target l = begin print "MLFILES:="; print_list "\\\n " mlfiles; print "\n"; print "CMOFILES:=$(MLFILES:.ml=.cmo)\n"; + classify_files_by_root "CMOFILES" mlfiles inc; + print "CMIFILES:=$(MLFILES:.ml=.cmi)\n"; + classify_files_by_root "CMIFILES" mlfiles inc; + print "CMXFILES:=$(MLFILES:.ml=.cmx)\n"; + print "CMXSFILES:=$(MLFILES:.ml=.cmxs)\n"; + classify_files_by_root "CMXSFILES" mlfiles inc; + print "OFILES:=$(MLFILES:.ml=.o)\n"; end; print "\nall: "; if !some_vfile then print "$(VOFILES) "; if !some_mlfile then print "$(CMOFILES) "; + if Coq_config.has_natdynlink && !some_mlfile then print "$(CMXSFILES) "; print_list "\\\n " other_targets; print "\n"; if !some_vfile then begin @@ -341,8 +417,20 @@ let all_target l = 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\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 (fun 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 @@ -379,14 +467,14 @@ let rec process_cmd_line = function opt := "-opt"; process_cmd_line r | "-impredicative-set" :: r -> impredicative_set := true; process_cmd_line r + | "-no-install" :: r -> + no_install := true; process_cmd_line r | "-custom" :: com :: dependencies :: file :: r -> let check_dep f = if Filename.check_suffix f ".v" then some_vfile := true - else if Filename.check_suffix f ".ml" then + else if (Filename.check_suffix f ".ml") || (Filename.check_suffix f ".ml4") then some_mlfile := true - else - () in List.iter check_dep (Str.split (Str.regexp "[ \t]+") dependencies); Special (file,dependencies,com) :: (process_cmd_line r) @@ -411,11 +499,14 @@ let rec process_cmd_line = function if Filename.check_suffix f ".v" then begin some_vfile := true; V f :: (process_cmd_line r) - end else if Filename.check_suffix f ".ml" then begin - some_mlfile := true; - ML f :: (process_cmd_line r) - end else - Subdir f :: (process_cmd_line r) + end else if (Filename.check_suffix f ".ml") || (Filename.check_suffix f ".ml4") then begin + some_mlfile := true; + ML f :: (process_cmd_line r) + end else if (Filename.check_suffix f ".mli") then begin + Printf.eprintf "Warning: no need for .mli files, skipped %s\n" f; + process_cmd_line r + end else + Subdir f :: (process_cmd_line r) let banner () = print @@ -462,24 +553,61 @@ let directories_deps l = in iter ([],[]) l +let ensure_root_dir l = + if List.exists (is_included ".") l or not (List.exists has_top_file l) then + l + else + Include "." :: l + +let warn_install_at_root_directory (vfiles,mlfiles,_,_) (inc_i,inc_r) = + let inc_r_top = List.filter (fun (_,ldir,_) -> ldir = "") inc_r in + let inc_top = List.map (fun (p,_,a) -> (p,a)) inc_r_top @ inc_i in + let files = vfiles @ mlfiles in + if not !no_install && + List.exists (fun f -> List.mem_assoc (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_i,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 subdirectoty 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; + List.iter (fun (pdir',abspdir') -> + if is_prefix abspdir abspdir' or is_prefix abspdir' abspdir then + Printf.eprintf "Warning: in option -I, %s overlap with %s in option -R\n" pdir' pdir) inc_i + in aux inc_r + let do_makefile args = let l = process_cmd_line args in - banner (); - warning (); - command_line args; - include_dirs l; - variables l; - all_target l; - let sps = special l in - custom sps; - let sds = subdirs l in - implicit (); - standard sds sps; - (* TEST directories_deps l; *) - includes (); - warning (); - if not (!output_channel == stdout) then close_out !output_channel; - exit 0 + let l = ensure_root_dir l in + let (_,_,sps,sds as targets), inc, defs = split_arguments l in + warn_install_at_root_directory targets inc; + check_overlapping_include inc; + banner (); + header_includes (); + warning (); + command_line args; + parameters (); + include_dirs inc; + variables defs; + all_target targets inc; + implicit (); + standard (); + if not !no_install then install targets inc; + clean sds sps; + make_makefile sds; + (* TEST directories_deps l; *) + footer_includes (); + warning (); + if not (!output_channel == stdout) then close_out !output_channel; + exit 0 let main () = let args = @@ -489,4 +617,3 @@ let main () = do_makefile args let _ = Printexc.catch main () - -- cgit v1.2.3