From d14df293d2696f00a8de137bea9fe3a89e0bdeb0 Mon Sep 17 00:00:00 2001 From: letouzey Date: Wed, 19 Dec 2001 11:42:11 +0000 Subject: reparation du make depend et du .depend git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2334 85f007b7-540e-0410-9357-904b9bb8a0f7 --- tools/coq-tex.ml | 274 ------------------------------- tools/coq-tex.ml4 | 274 +++++++++++++++++++++++++++++++ tools/coq_makefile.ml | 430 ------------------------------------------------- tools/coq_makefile.ml4 | 430 +++++++++++++++++++++++++++++++++++++++++++++++++ 4 files changed, 704 insertions(+), 704 deletions(-) delete mode 100644 tools/coq-tex.ml create mode 100644 tools/coq-tex.ml4 delete mode 100644 tools/coq_makefile.ml create mode 100644 tools/coq_makefile.ml4 (limited to 'tools') diff --git a/tools/coq-tex.ml b/tools/coq-tex.ml deleted file mode 100644 index 541777d6e4..0000000000 --- a/tools/coq-tex.ml +++ /dev/null @@ -1,274 +0,0 @@ -(***********************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* () - | _ -> begin - print_string "This program only runs under Unix !\n"; - flush stdout; - exit 1 - end - -let linelen = ref 72 -let output = ref "" -let output_specified = ref false -let image = ref "" -let cut_at_blanks = ref false -let verbose = ref false -let slanted = ref false -let hrule = ref false -let small = ref false - -let coq_prompt = Str.regexp "Coq < " -let any_prompt = Str.regexp "^[A-Z0-9a-z_\$']* < " - -let remove_prompt s = Str.replace_first any_prompt "" s - -(* First pass: extract the Coq phrases to evaluate from [texfile] - * and put them into the file [inputv] *) - -let begin_coq = Str.regexp "\\\\begin{coq_\(example\|example\*\|example\#\|eval\)}[ \t]*$" -let end_coq = Str.regexp "\\\\end{coq_\(example\|example\*\|example\#\|eval\)}[ \t]*$" - -let extract texfile inputv = - let chan_in = open_in texfile in - let chan_out = open_out inputv in - let rec inside () = - let s = input_line chan_in in - if Str.string_match end_coq s 0 then - outside () - else begin - output_string chan_out (s ^ "\n"); - inside () - end - and outside () = - let s = input_line chan_in in - if Str.string_match begin_coq s 0 then - inside () - else - outside () - in - try - outside () - with End_of_file -> - begin close_in chan_in; close_out chan_out end - -(* Second pass: insert the answers of Coq from [coq_output] into the - * TeX file [texfile]. The result goes in file [result]. *) - -let begin_coq_example = - Str.regexp "\\\\begin{coq_\(example\|example\*\|example\#\)}[ \t]*$" -let begin_coq_eval = Str.regexp "\\\\begin{coq_eval}[ \t]*$" -let end_coq_example = Str.regexp "\\\\end{coq_\(example\|example\*\|example\#\)}[ \t]*$" -let end_coq_eval = Str.regexp "\\\\end{coq_eval}[ \t]*$" -let dot_end_line = Str.regexp "\\.[ \t]*$" - -let has_match r s = - try let _ = Str.search_forward r s 0 in true with Not_found -> false - -let percent = Str.regexp "%" -let bang = Str.regexp "!" -let expos = Str.regexp "^" - -let tex_escaped s = - let rec trans = parser - | [< s1 = (parser - | [< ''_'|'$'|'{'|'}'|'&'|'%'|'#' as c >] -> - "\\" ^ (String.make 1 c) - | [< ''\\' >] -> "\\char'134" - | [< ''^' >] -> "\\char'136" - | [< ''~' >] -> "\\char'176" - | [< '' ' >] -> "~" - | [< ''<' >] -> "{<}" - | [< ''>' >] -> "{>}" - | [< 'c >] -> String.make 1 c); - s2 = trans >] -> s1 ^ s2 - | [< >] -> "" - in - trans (Stream.of_string s) - -let encapsule sl c_out s = - if sl then - Printf.fprintf c_out "\\texttt{\\textit{%s}}\\\\\n" (tex_escaped s) - else - Printf.fprintf c_out "\\texttt{%s}\\\\\n" (tex_escaped s) - -let print_block c_out bl = - List.iter (fun s -> if s="" then () else encapsule !slanted c_out s) bl - -let insert texfile coq_output result = - let c_tex = open_in texfile in - let c_coq = open_in coq_output in - let c_out = open_out result in - (* next_block k : this function reads the next block of Coq output - * removing the k leading prompts. - * it returns the block as a list of string) *) - let last_read = ref "" in - let next_block k = - if !last_read = "" then last_read := input_line c_coq; - (* skip k prompts *) - for i = 1 to k do - last_read := remove_prompt !last_read; - done; - (* read and return the following lines until a prompt is found *) - let rec read_lines () = - let s = input_line c_coq in - if Str.string_match any_prompt s 0 then begin - last_read := s; [] - end else - s :: (read_lines ()) - in - let first = !last_read in first :: (read_lines ()) - in - (* we are outside of a \begin{coq_...} ... \end{coq_...} block *) - let rec outside () = - let s = input_line c_tex in - if Str.string_match begin_coq_example s 0 then begin - if !small then output_string c_out "\\begin{small}\n"; - output_string c_out "\\begin{flushleft}\n"; - if !hrule then output_string c_out "\\hrulefill\\\\\n"; - inside (Str.matched_group 1 s <> "example*") - (Str.matched_group 1 s <> "example#") 0 true - end else if Str.string_match begin_coq_eval s 0 then - eval 0 - else begin - output_string c_out (s ^ "\n"); - outside () - end - (* we are inside a \begin{coq_example?} ... \end{coq_example?} block - * show_answers tells what kind of block it is - * k is the number of lines read until now *) - and inside show_answers show_questions k first_block = - let s = input_line c_tex in - if Str.string_match end_coq_example s 0 then begin - if !hrule then output_string c_out "\\hrulefill\\\\\n"; - output_string c_out "\\end{flushleft}\n"; - if !small then output_string c_out "\\end{small}\n"; - outside () - end else begin - if !verbose then Printf.printf "Coq < %s\n" s; - if (not first_block) & k=0 then output_string c_out "\\medskip\n"; - if show_questions then encapsule false c_out ("Coq < " ^ s); - if has_match dot_end_line s then begin - let bl = next_block (succ k) in - if !verbose then List.iter print_endline bl; - if show_answers then print_block c_out bl; - inside show_answers show_questions 0 false - end else - inside show_answers show_questions (succ k) first_block - end - (* we are inside a \begin{coq_eval} ... \end{coq_eval} block - * k is the number of lines read until now *) - and eval k = - let s = input_line c_tex in - if Str.string_match end_coq_eval s 0 then - outside () - else begin - if !verbose then Printf.printf "Coq < %s\n" s; - if has_match dot_end_line s then - let bl = next_block (succ k) in - if !verbose then List.iter print_endline bl; - eval 0 - else - eval (succ k) - end - in - try - let _ = next_block 0 in (* to skip the Coq banner *) - outside () - with End_of_file -> begin - close_in c_tex; - close_in c_coq; - close_out c_out - end - -(* Process of one TeX file *) - -let rm f = try Sys.remove f with _ -> () - -let one_file texfile = - let inputv = Filename.temp_file "coq_tex" ".v" in - let coq_output = Filename.temp_file "coq_tex" ".coq_output"in - let result = - if !output_specified then - !output - else if Filename.check_suffix texfile ".tex" then - (Filename.chop_suffix texfile ".tex") ^ ".v.tex" - else - texfile ^ ".v.tex" - in - try - (* 1. extract Coq phrases *) - extract texfile inputv; - (* 2. run Coq on input *) - let _ = Sys.command (Printf.sprintf "%s < %s > %s 2>&1" !image inputv - coq_output) - in - (* 3. insert Coq output into original file *) - insert texfile coq_output result; - (* 4. clean up *) - rm inputv; rm coq_output - with e -> begin - rm inputv; rm coq_output; - raise e - end - -(* Parsing of the command line, check of the Coq command and process - * of all the files in the command line, one by one *) - -let files = ref [] - -let parse_cl () = - Arg.parse - [ "-o", Arg.String (fun s -> output_specified := true; output := s), - "output-file Specifiy the resulting LaTeX file"; - "-n", Arg.Int (fun n -> linelen := n), - "line-width Set the line width"; - "-image", Arg.String (fun s -> image := s), - "coq-image Use coq-image as Coq command"; - "-w", Arg.Set cut_at_blanks, - " Try to cut lines at blanks"; - "-v", Arg.Set verbose, - " Verbose mode (show Coq answers on stdout)"; - "-sl", Arg.Set slanted, - " Coq answers in slanted font (only with LaTeX2e)"; - "-hrule", Arg.Set hrule, - " Coq parts are written between 2 horizontal lines"; - "-small", Arg.Set small, - " Coq parts are written in small font" - ] - (fun s -> files := s :: !files) - "coq-tex [options] file ..." - -let main () = - parse_cl (); - if !image = "" then begin - Printf.printf "Warning: preprocessing with default image \"coqtop\"\n"; - image := "coqtop" - end; - if Sys.command (!image ^ " -batch > /dev/null 2>&1") <> 0 then begin - Printf.printf "Error: "; - let _ = Sys.command (!image ^ " -batch") in - exit 1 - end else begin - Printf.printf "Your version of coqtop seems OK\n"; - flush stdout - end; - List.iter one_file (List.rev !files) - -let _ = Printexc.catch main () diff --git a/tools/coq-tex.ml4 b/tools/coq-tex.ml4 new file mode 100644 index 0000000000..541777d6e4 --- /dev/null +++ b/tools/coq-tex.ml4 @@ -0,0 +1,274 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* () + | _ -> begin + print_string "This program only runs under Unix !\n"; + flush stdout; + exit 1 + end + +let linelen = ref 72 +let output = ref "" +let output_specified = ref false +let image = ref "" +let cut_at_blanks = ref false +let verbose = ref false +let slanted = ref false +let hrule = ref false +let small = ref false + +let coq_prompt = Str.regexp "Coq < " +let any_prompt = Str.regexp "^[A-Z0-9a-z_\$']* < " + +let remove_prompt s = Str.replace_first any_prompt "" s + +(* First pass: extract the Coq phrases to evaluate from [texfile] + * and put them into the file [inputv] *) + +let begin_coq = Str.regexp "\\\\begin{coq_\(example\|example\*\|example\#\|eval\)}[ \t]*$" +let end_coq = Str.regexp "\\\\end{coq_\(example\|example\*\|example\#\|eval\)}[ \t]*$" + +let extract texfile inputv = + let chan_in = open_in texfile in + let chan_out = open_out inputv in + let rec inside () = + let s = input_line chan_in in + if Str.string_match end_coq s 0 then + outside () + else begin + output_string chan_out (s ^ "\n"); + inside () + end + and outside () = + let s = input_line chan_in in + if Str.string_match begin_coq s 0 then + inside () + else + outside () + in + try + outside () + with End_of_file -> + begin close_in chan_in; close_out chan_out end + +(* Second pass: insert the answers of Coq from [coq_output] into the + * TeX file [texfile]. The result goes in file [result]. *) + +let begin_coq_example = + Str.regexp "\\\\begin{coq_\(example\|example\*\|example\#\)}[ \t]*$" +let begin_coq_eval = Str.regexp "\\\\begin{coq_eval}[ \t]*$" +let end_coq_example = Str.regexp "\\\\end{coq_\(example\|example\*\|example\#\)}[ \t]*$" +let end_coq_eval = Str.regexp "\\\\end{coq_eval}[ \t]*$" +let dot_end_line = Str.regexp "\\.[ \t]*$" + +let has_match r s = + try let _ = Str.search_forward r s 0 in true with Not_found -> false + +let percent = Str.regexp "%" +let bang = Str.regexp "!" +let expos = Str.regexp "^" + +let tex_escaped s = + let rec trans = parser + | [< s1 = (parser + | [< ''_'|'$'|'{'|'}'|'&'|'%'|'#' as c >] -> + "\\" ^ (String.make 1 c) + | [< ''\\' >] -> "\\char'134" + | [< ''^' >] -> "\\char'136" + | [< ''~' >] -> "\\char'176" + | [< '' ' >] -> "~" + | [< ''<' >] -> "{<}" + | [< ''>' >] -> "{>}" + | [< 'c >] -> String.make 1 c); + s2 = trans >] -> s1 ^ s2 + | [< >] -> "" + in + trans (Stream.of_string s) + +let encapsule sl c_out s = + if sl then + Printf.fprintf c_out "\\texttt{\\textit{%s}}\\\\\n" (tex_escaped s) + else + Printf.fprintf c_out "\\texttt{%s}\\\\\n" (tex_escaped s) + +let print_block c_out bl = + List.iter (fun s -> if s="" then () else encapsule !slanted c_out s) bl + +let insert texfile coq_output result = + let c_tex = open_in texfile in + let c_coq = open_in coq_output in + let c_out = open_out result in + (* next_block k : this function reads the next block of Coq output + * removing the k leading prompts. + * it returns the block as a list of string) *) + let last_read = ref "" in + let next_block k = + if !last_read = "" then last_read := input_line c_coq; + (* skip k prompts *) + for i = 1 to k do + last_read := remove_prompt !last_read; + done; + (* read and return the following lines until a prompt is found *) + let rec read_lines () = + let s = input_line c_coq in + if Str.string_match any_prompt s 0 then begin + last_read := s; [] + end else + s :: (read_lines ()) + in + let first = !last_read in first :: (read_lines ()) + in + (* we are outside of a \begin{coq_...} ... \end{coq_...} block *) + let rec outside () = + let s = input_line c_tex in + if Str.string_match begin_coq_example s 0 then begin + if !small then output_string c_out "\\begin{small}\n"; + output_string c_out "\\begin{flushleft}\n"; + if !hrule then output_string c_out "\\hrulefill\\\\\n"; + inside (Str.matched_group 1 s <> "example*") + (Str.matched_group 1 s <> "example#") 0 true + end else if Str.string_match begin_coq_eval s 0 then + eval 0 + else begin + output_string c_out (s ^ "\n"); + outside () + end + (* we are inside a \begin{coq_example?} ... \end{coq_example?} block + * show_answers tells what kind of block it is + * k is the number of lines read until now *) + and inside show_answers show_questions k first_block = + let s = input_line c_tex in + if Str.string_match end_coq_example s 0 then begin + if !hrule then output_string c_out "\\hrulefill\\\\\n"; + output_string c_out "\\end{flushleft}\n"; + if !small then output_string c_out "\\end{small}\n"; + outside () + end else begin + if !verbose then Printf.printf "Coq < %s\n" s; + if (not first_block) & k=0 then output_string c_out "\\medskip\n"; + if show_questions then encapsule false c_out ("Coq < " ^ s); + if has_match dot_end_line s then begin + let bl = next_block (succ k) in + if !verbose then List.iter print_endline bl; + if show_answers then print_block c_out bl; + inside show_answers show_questions 0 false + end else + inside show_answers show_questions (succ k) first_block + end + (* we are inside a \begin{coq_eval} ... \end{coq_eval} block + * k is the number of lines read until now *) + and eval k = + let s = input_line c_tex in + if Str.string_match end_coq_eval s 0 then + outside () + else begin + if !verbose then Printf.printf "Coq < %s\n" s; + if has_match dot_end_line s then + let bl = next_block (succ k) in + if !verbose then List.iter print_endline bl; + eval 0 + else + eval (succ k) + end + in + try + let _ = next_block 0 in (* to skip the Coq banner *) + outside () + with End_of_file -> begin + close_in c_tex; + close_in c_coq; + close_out c_out + end + +(* Process of one TeX file *) + +let rm f = try Sys.remove f with _ -> () + +let one_file texfile = + let inputv = Filename.temp_file "coq_tex" ".v" in + let coq_output = Filename.temp_file "coq_tex" ".coq_output"in + let result = + if !output_specified then + !output + else if Filename.check_suffix texfile ".tex" then + (Filename.chop_suffix texfile ".tex") ^ ".v.tex" + else + texfile ^ ".v.tex" + in + try + (* 1. extract Coq phrases *) + extract texfile inputv; + (* 2. run Coq on input *) + let _ = Sys.command (Printf.sprintf "%s < %s > %s 2>&1" !image inputv + coq_output) + in + (* 3. insert Coq output into original file *) + insert texfile coq_output result; + (* 4. clean up *) + rm inputv; rm coq_output + with e -> begin + rm inputv; rm coq_output; + raise e + end + +(* Parsing of the command line, check of the Coq command and process + * of all the files in the command line, one by one *) + +let files = ref [] + +let parse_cl () = + Arg.parse + [ "-o", Arg.String (fun s -> output_specified := true; output := s), + "output-file Specifiy the resulting LaTeX file"; + "-n", Arg.Int (fun n -> linelen := n), + "line-width Set the line width"; + "-image", Arg.String (fun s -> image := s), + "coq-image Use coq-image as Coq command"; + "-w", Arg.Set cut_at_blanks, + " Try to cut lines at blanks"; + "-v", Arg.Set verbose, + " Verbose mode (show Coq answers on stdout)"; + "-sl", Arg.Set slanted, + " Coq answers in slanted font (only with LaTeX2e)"; + "-hrule", Arg.Set hrule, + " Coq parts are written between 2 horizontal lines"; + "-small", Arg.Set small, + " Coq parts are written in small font" + ] + (fun s -> files := s :: !files) + "coq-tex [options] file ..." + +let main () = + parse_cl (); + if !image = "" then begin + Printf.printf "Warning: preprocessing with default image \"coqtop\"\n"; + image := "coqtop" + end; + if Sys.command (!image ^ " -batch > /dev/null 2>&1") <> 0 then begin + Printf.printf "Error: "; + let _ = Sys.command (!image ^ " -batch") in + exit 1 + end else begin + Printf.printf "Your version of coqtop seems OK\n"; + flush stdout + end; + List.iter one_file (List.rev !files) + +let _ = Printexc.catch main () diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml deleted file mode 100644 index 613257c685..0000000000 --- a/tools/coq_makefile.ml +++ /dev/null @@ -1,430 +0,0 @@ -(***********************************************************************) -(* 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 some_file = ref false -let some_vfile = ref false -let some_mlfile = ref false - -let opt = ref "-opt" - -let print x = output_string !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 -[-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:\n"; - if !some_file then begin - print "\trm .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 "xml::\n"; - List.iter - (fun x -> print "\t(cd "; print x; print " ; $(MAKE) xml)\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"; - print "Makefile: Make\n"; - print "\tmv -f Makefile Makefile.bak\n"; - print "\t$(COQBIN)coq_makefile -f Make -o Makefile\n"; - print "\n"; - 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" - -let implicit () = - let ml_rules () = - print ".mli.cmi:\n\t$(CAMLC) $(ZDEBUG) $(ZFLAGS) $<\n\n"; - print ".ml.cmo:\n\t$(CAMLC) $(ZDEBUG) $(ZFLAGS) $<\n\n"; - print ".ml.cmx:\n\t$(CAMLOPTC) $(ZDEBUG) $(ZFLAGS) $<\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$(COQWEB) $< -o $@\n\n"; - print ".v.html:\n\t$(COQWEB) -html $< -o $@\n\n"; - print ".g.g.tex:\n\t$(COQWEB) $< -o $@\n\n"; - print ".g.g.html:\n\t$(COQWEB) -html $< -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)/proofs -I $(COQTOP)/syntax -I $(COQTOP)/tactics \\ - -I $(COQTOP)/toplevel -I $(CAMLP4LIB)\n"; - print "ZFLAGS=$(OCAMLLIBS) $(COQSRC)\n"; - print "OPT="; if !opt = "-byte" then print "-byte"; print "\n"; - print "COQFLAGS=-q $(OPT) $(COQLIBS)\n"; - print "COQC=$(COQBIN)coqc\n"; - print "GALLINA=gallina\n"; - print "COQWEB=coqweb\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 "COQVO2XML=coq_vo2xml\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" :: "xml" :: 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$(COQWEB) -ps -o $@ `$(COQDEP) -sort -suffix .v $(VFILES)`\n\n"; - print "all-gal.ps: $(GFILES)\n"; - print "\t$(COQWEB) -ps -o $@ `$(COQDEP) -sort -suffix .g $(VFILES)`\n\n"; - print "xml:: .xml_time_stamp\n"; - print ".xml_time_stamp: "; print_list "\\\n " (vofiles l); - print "\n\t$(COQVO2XML) $(COQFLAGS) $(?:%.o=%)\n"; - print "\ttouch .xml_time_stamp"; - 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 - | "-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" | "-h" | "--help" | "-custom") :: _ -> - usage () - | "-f"::file::r -> - process_cmd_line ((parse file)@r) - | ["-f"] -> - usage () - | "-o" :: file :: r -> - 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 () - diff --git a/tools/coq_makefile.ml4 b/tools/coq_makefile.ml4 new file mode 100644 index 0000000000..613257c685 --- /dev/null +++ b/tools/coq_makefile.ml4 @@ -0,0 +1,430 @@ +(***********************************************************************) +(* 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 some_file = ref false +let some_vfile = ref false +let some_mlfile = ref false + +let opt = ref "-opt" + +let print x = output_string !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 +[-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:\n"; + if !some_file then begin + print "\trm .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 "xml::\n"; + List.iter + (fun x -> print "\t(cd "; print x; print " ; $(MAKE) xml)\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"; + print "Makefile: Make\n"; + print "\tmv -f Makefile Makefile.bak\n"; + print "\t$(COQBIN)coq_makefile -f Make -o Makefile\n"; + print "\n"; + 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" + +let implicit () = + let ml_rules () = + print ".mli.cmi:\n\t$(CAMLC) $(ZDEBUG) $(ZFLAGS) $<\n\n"; + print ".ml.cmo:\n\t$(CAMLC) $(ZDEBUG) $(ZFLAGS) $<\n\n"; + print ".ml.cmx:\n\t$(CAMLOPTC) $(ZDEBUG) $(ZFLAGS) $<\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$(COQWEB) $< -o $@\n\n"; + print ".v.html:\n\t$(COQWEB) -html $< -o $@\n\n"; + print ".g.g.tex:\n\t$(COQWEB) $< -o $@\n\n"; + print ".g.g.html:\n\t$(COQWEB) -html $< -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)/proofs -I $(COQTOP)/syntax -I $(COQTOP)/tactics \\ + -I $(COQTOP)/toplevel -I $(CAMLP4LIB)\n"; + print "ZFLAGS=$(OCAMLLIBS) $(COQSRC)\n"; + print "OPT="; if !opt = "-byte" then print "-byte"; print "\n"; + print "COQFLAGS=-q $(OPT) $(COQLIBS)\n"; + print "COQC=$(COQBIN)coqc\n"; + print "GALLINA=gallina\n"; + print "COQWEB=coqweb\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 "COQVO2XML=coq_vo2xml\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" :: "xml" :: 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$(COQWEB) -ps -o $@ `$(COQDEP) -sort -suffix .v $(VFILES)`\n\n"; + print "all-gal.ps: $(GFILES)\n"; + print "\t$(COQWEB) -ps -o $@ `$(COQDEP) -sort -suffix .g $(VFILES)`\n\n"; + print "xml:: .xml_time_stamp\n"; + print ".xml_time_stamp: "; print_list "\\\n " (vofiles l); + print "\n\t$(COQVO2XML) $(COQFLAGS) $(?:%.o=%)\n"; + print "\ttouch .xml_time_stamp"; + 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 + | "-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" | "-h" | "--help" | "-custom") :: _ -> + usage () + | "-f"::file::r -> + process_cmd_line ((parse file)@r) + | ["-f"] -> + usage () + | "-o" :: file :: r -> + 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