From 6b649aba925b6f7462da07599fe67ebb12a3460e Mon Sep 17 00:00:00 2001 From: Samuel Mimram Date: Wed, 28 Jul 2004 21:54:47 +0000 Subject: Imported Upstream version 8.0pl1 --- tools/coq_makefile.ml4 | 454 +++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 454 insertions(+) create mode 100644 tools/coq_makefile.ml4 (limited to 'tools/coq_makefile.ml4') diff --git a/tools/coq_makefile.ml4 b/tools/coq_makefile.ml4 new file mode 100644 index 00000000..4879e97d --- /dev/null +++ b/tools/coq_makefile.ml4 @@ -0,0 +1,454 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* (ML "foo") *) + | V of string (* V file : foo.v -> (V "foo") *) + | 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_file = ref false +let some_vfile = ref false +let some_mlfile = ref false + +let opt = ref "-opt" +let impredicative_set = 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 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] ... [-custom + command dependencies file] ... [-I dir] ... [-R physicalpath logicalpath] + ... [VARIABLE = value] ... [-opt|-byte] [-f file] [-o file] [-h] [--help] + +[file.v]: Coq file to be compiled +[file.ml]: ML file to be compiled +[subdirectory] : subdirectory that should be \"made\" +[-custom command dependencies file]: add target \"file\" with command + \"command\" and dependencies \"dependencies\" +[-I dir]: look for dependencies in \"dir\" +[-R physicalpath logicalpath]: look for 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 +[-impredicative-set]: compile with option -impredicative-set of coq +[-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 = + print "byte:\n"; + print "\t$(MAKE) all \"OPT=\"\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"; + if !some_file then print "include .depend\n\n"; + print ".depend depend:\n"; + if !some_file then begin + print "\trm -f .depend\n"; + print "\t$(COQDEP) -i $(COQLIBS) *.v *.ml *.mli >.depend\n"; + print "\t$(COQDEP) $(COQLIBS) -suffix .html *.v >>.depend\n"; + end; + List.iter + (fun x -> print "\t(cd "; print x; print " ; $(MAKE) depend)\n") + sds; + print "\n"; + print "install:\n"; + print "\tmkdir -p `$(COQC) -where`/user-contrib\n"; + if !some_vfile then print "\tcp -f *.vo `$(COQC) -where`/user-contrib\n"; + if !some_mlfile then print "\tcp -f *.cmo `$(COQC) -where`/user-contrib\n"; + List.iter + (fun x -> print "\t(cd "; print x; print " ; $(MAKE) install)\n") + sds; + print "\n"; + if !make_name <> "" then begin + printf "%s: %s\n" !makefile_name !make_name; + printf "\tmv -f %s %s.bak\n" !makefile_name !makefile_name; + printf "\t$(COQBIN)coq_makefile -f %s -o %s\n" !make_name !makefile_name; + print "\n"; + List.iter + (fun x -> print "\t(cd "; print x; print " ; $(MAKE) Makefile)\n") + sds; + print "\n"; + end; + print "clean:\n"; + print "\trm -f *.cmo *.cmi *.cmx *.o *.vo *.vi *.g *~\n"; + print "\trm -f all.ps all-gal.ps $(HTMLFILES) $(GHTMLFILES)\n"; + 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"; + print "html:\n"; + List.iter + (fun x -> print "\t(cd "; print x; print " ; $(MAKE) html)\n") + sds; + print "\n" + +let implicit () = + let ml_rules () = + print ".mli.cmi:\n\t$(CAMLC) $(ZDEBUG) $(ZFLAGS) $<\n\n"; + print ".ml.cmo:\n\t$(CAMLC) $(ZDEBUG) $(ZFLAGS) $(PP) $<\n\n"; + print ".ml.cmx:\n\t$(CAMLOPTC) $(ZDEBUG) $(ZFLAGS) $(PP) $<\n\n"; + and v_rule () = + print ".v.vo:\n\t$(COQC) $(COQDEBUG) $(COQFLAGS) $*\n\n"; + print ".v.vi:\n\t$(COQC) -i $(COQDEBUG) $(COQFLAGS) $*\n\n"; + print ".v.g:\n\t$(GALLINA) $<\n\n"; + print ".v.tex:\n\t$(COQDOC) -latex $< -o $@\n\n"; + print ".v.html:\n\t$(COQDOC) -html $< -o $@\n\n"; + print ".v.g.tex:\n\t$(COQDOC) -latex -g $< -o $@\n\n"; + print ".v.g.html:\n\t$(COQDOC) -html -g $< -o $@\n\n" + and ml_suffixes = + if !some_mlfile then + [ ".mli"; ".ml"; ".cmo"; ".cmi"; ".cmx" ] + else + [] + and v_suffixes = + if !some_vfile then + [ ".v"; ".vo"; ".vi"; ".g"; ".html"; ".tex"; ".g.tex"; ".g.html" ] + else + [] + in + let suffixes = ml_suffixes @ v_suffixes in + if suffixes <> [] then begin + print ".SUFFIXES: "; print_list " " suffixes; + print "\n\n" + end; + 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 + section "Variables definitions."; + print "CAMLP4LIB=`camlp4 -where`\n"; +(* print "MAKE=make \"COQBIN=$(COQBIN)\" \"OPT=$(OPT)\"\n"; *) + print "COQSRC=-I $(COQTOP)/kernel -I $(COQTOP)/lib \\ + -I $(COQTOP)/library -I $(COQTOP)/parsing \\ + -I $(COQTOP)/pretyping -I $(COQTOP)/interp \\ + -I $(COQTOP)/proofs -I $(COQTOP)/syntax -I $(COQTOP)/tactics \\ + -I $(COQTOP)/toplevel -I $(COQTOP)/contrib/correctness \\ + -I $(COQTOP)/contrib/extraction -I $(COQTOP)/contrib/field \\ + -I $(COQTOP)/contrib/fourier -I $(COQTOP)/contrib/graphs \\ + -I $(COQTOP)/contrib/interface -I $(COQTOP)/contrib/jprover \\ + -I $(COQTOP)/contrib/omega -I $(COQTOP)/contrib/romega \\ + -I $(COQTOP)/contrib/ring -I $(COQTOP)/contrib/xml \\ + -I $(CAMLP4LIB)\n"; + print "ZFLAGS=$(OCAMLLIBS) $(COQSRC)\n"; + if !opt = "-byte" then + print "override OPT=-byte\n" + else + print "OPT=\n"; + if !impredicative_set = true then print "OTHERFLAGS=-impredicative-set\n"; + print "COQFLAGS=-q $(OPT) $(COQLIBS) $(OTHERFLAGS) $(COQ_XML)\n"; + print "COQC=$(COQBIN)coqc\n"; + print "GALLINA=gallina\n"; + print "COQDOC=coqdoc\n"; + print "CAMLC=ocamlc -c\n"; + print "CAMLOPTC=ocamlopt -c\n"; + print "CAMLLINK=ocamlc\n"; + print "CAMLOPTLINK=ocamlopt\n"; + print "COQDEP=$(COQBIN)coqdep -c\n"; + print "GRAMMARS=grammar.cma\n"; + print "CAMLP4EXTEND=pa_extend.cmo pa_ifdef.cmo q_MLast.cmo\n"; + print "PP=-pp \"camlp4o -I . -I $(COQTOP)/parsing $(CAMLP4EXTEND) $(GRAMMARS) -impl\"\n"; + var_aux l; + print "\n" + +let include_dirs l = + let include_aux' includeR = + let rec include_aux = function + | [] -> [] + | Include x :: r -> ("-I " ^ x) :: (include_aux r) + | RInclude (p,l) :: r when includeR -> + let l' = if l = "" then "\"\"" else l in + ("-R " ^ p ^ " " ^ l') :: (include_aux r) + | _ :: r -> include_aux r + in + include_aux + in + let i_ocaml = "-I ." :: (include_aux' false l) in + let i_coq = "-I ." :: (include_aux' true l) in + section "Libraries definition."; + print "OCAMLLIBS="; print_list "\\\n " i_ocaml; print "\n"; + print "COQLIBS="; print_list "\\\n " i_coq; print "\n\n" + +let special l = + let pr_sp (file,dependencies,com) = + print file; print ": "; print dependencies; print "\n"; + print "\t"; print com; print "\n\n" + in + let rec sp_aux = function + | [] -> [] + | Special (file,deps,com) :: r -> (file,deps,com) :: (sp_aux r) + | _ :: r -> sp_aux r + in + let sps = sp_aux l in + 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 = + 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."; + print ".PHONY: "; + print_list " " + ("all" :: "opt" :: "byte" :: "archclean" :: "clean" :: "install" + :: "depend" :: "html" :: sds); + print "\n\n"; + sds + +(* Extract gallina/html filenames (foo.v) from the list of all targets *) + +let rec other_files suff = function + | V n :: r -> + let f = (Filename.chop_suffix n ".vo") ^ suff in + f :: (other_files suff r) + | _ :: r -> + other_files suff r + | [] -> + [] + +let vfiles = other_files ".v" +let gfiles = other_files ".g" +let hfiles = other_files ".html" +let tfiles = other_files ".tex" +let vifiles = other_files ".vi" +let gtfiles l = List.map (fun f -> f ^ ".tex") (gfiles l) +let ghfiles l = List.map (fun f -> f ^ ".html") (gfiles l) +let vofiles = other_files ".vo" + +let all_target l = + let rec fnames = function + | ML n :: r -> n :: (fnames r) + | Subdir n :: r -> n :: (fnames r) + | V n :: r -> n :: (fnames r) + | Special (n,_,_) :: r -> n :: (fnames r) + | Include _ :: r -> fnames r + | RInclude _ :: r -> fnames r + | Def _ :: r -> fnames r + | [] -> [] + in + section "Definition of the \"all\" target."; + print "VFILES="; print_list "\\\n " (vfiles l); print "\n"; + print "VOFILES=$(VFILES:.v=.vo)\n"; + print "VIFILES=$(VFILES:.v=.vi)\n"; + print "GFILES=$(VFILES:.v=.g)\n"; + print "HTMLFILES=$(VFILES:.v=.html)\n"; + print "GHTMLFILES=$(VFILES:.v=.g.html)\n"; + print "\n"; + print "all: "; print_list "\\\n " (fnames l); + print "\n\n"; + if !some_vfile then begin + print "spec: $(VIFILES)\n\n"; + print "gallina: $(GFILES)\n\n"; + print "html: $(HTMLFILES)\n\n"; + print "gallinahtml: $(GHTMLFILES)\n\n"; + print "all.ps: $(VFILES)\n"; + print "\t$(COQDOC) -ps -o $@ `$(COQDEP) -sort -suffix .v $(VFILES)`\n\n"; + print "all-gal.ps: $(VFILES)\n"; + print "\t$(COQDOC) -ps -g -o $@ `$(COQDEP) -sort -suffix .v $(VFILES)`\n\n"; + print "\n\n" + end + +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 = function + | [] -> + some_file := !some_file or !some_mlfile or !some_vfile; [] + | ("-h"|"--help") :: _ -> + usage () + | ("-no-opt"|"-byte") :: r -> + opt := "-byte"; process_cmd_line r + | ("-full"|"-opt") :: r -> + opt := "-opt"; process_cmd_line r + | "-impredicative-set" :: r -> + impredicative_set := true; process_cmd_line r + | "-custom" :: com :: dependencies :: file :: r -> + some_file := true; + Special (file,dependencies,com) :: (process_cmd_line r) + | "-I" :: d :: r -> + Include d :: (process_cmd_line r) + | "-R" :: p :: l :: r -> + RInclude (p,l) :: (process_cmd_line r) + | ("-I"|"-custom") :: _ -> + usage () + | "-f" :: file :: r -> + make_name := file; + process_cmd_line ((parse file)@r) + | ["-f"] -> + usage () + | "-o" :: file :: r -> + makefile_name := file; + output_channel := (open_out file); + (process_cmd_line r) + | v :: "=" :: def :: r -> + Def (v,def) :: (process_cmd_line r) + | f :: r -> + if Filename.check_suffix f ".v" then begin + some_vfile := true; + V (f^"o") :: (process_cmd_line r) + end else if Filename.check_suffix f ".ml" then begin + some_mlfile := true; + ML ((Filename.chop_suffix f "ml")^"cmo") :: (process_cmd_line r) + end else + Subdir f :: (process_cmd_line r) + +let banner () = + print +"############################################################################## +## The Calculus of Inductive Constructions ## +## ## +## Projet Coq ## +## ## +## INRIA ENS-CNRS ## +## Rocquencourt Lyon ## +## ## +## Coq V7 ## +## ## +## ## +############################################################################## + +" + +let warning () = + print "# WARNING\n#\n"; + print "# This Makefile has been automagically generated by coq_makefile\n"; + print "# Edit at your own risks !\n"; + print "#\n# END OF WARNING\n\n" + +let print_list l = List.iter (fun x -> 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 directories_deps l = + let print_dep f dep = + if dep <> [] then begin print f; print ": "; print_list dep; print "\n" end + in + let rec iter ((dirs,before) as acc) = function + | [] -> + () + | (Subdir d) :: l -> + print_dep d before; iter (d :: dirs, d :: before) l + | (ML f) :: l -> + print_dep f dirs; iter (dirs, f :: before) l + | (V f) :: l -> + print_dep f dirs; iter (dirs, f :: before) l + | (Special (f,_,_)) :: l -> + print_dep f dirs; iter (dirs, f :: before) l + | _ :: l -> + iter acc l + in + iter ([],[]) l + +let do_makefile args = + let l = process_cmd_line args in + banner (); + warning (); + command_line args; + variables l; + include_dirs l; + all_target l; + special l; + let sds = subdirs l in + implicit (); + standard sds; + (* TEST directories_deps l; *) + warning (); + if not (!output_channel == stdout) 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