diff options
author | 2011-09-01 09:50:16 +0000 | |
---|---|---|
committer | 2011-09-01 09:50:16 +0000 | |
commit | dacd20ee007fd8f690ffc0ae1f264d61c12fcd8d (patch) | |
tree | f9943269dea1786cc9529eca91e9406c8cac681d | |
parent | cb039d900f3a70ca2e6fb765251b2a424af0e0b3 (diff) |
Coq_makefile: New option -arg to specify a compiler option.
Consequently, option -impredicative-set is deprecated.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14428 85f007b7-540e-0410-9357-904b9bb8a0f7
-rw-r--r-- | tools/coq_makefile.ml4 | 30 |
1 files changed, 21 insertions, 9 deletions
diff --git a/tools/coq_makefile.ml4 b/tools/coq_makefile.ml4 index f1ee4f175..69c5456d6 100644 --- a/tools/coq_makefile.ml4 +++ b/tools/coq_makefile.ml4 @@ -14,6 +14,7 @@ type target = | 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") *) @@ -31,7 +32,6 @@ let some_ml4file = ref false let some_mllibfile = ref false let opt = ref "-opt" -let impredicative_set = ref false let no_install = ref false let print x = output_string !output_channel x @@ -65,7 +65,7 @@ let usage () = coq_makefile [subdirectory] .... [file.v] ... [file.ml[i4]?] ... [file.mllib] ... [-custom command dependencies file] ... [-I dir] ... [-R physicalpath - logicalpath] ... [VARIABLE = value] ... [-opt|-byte] [-impredicative-set] + logicalpath] ... [VARIABLE = value] ... [-arg opt] ... [-opt|-byte] [-no-install] [-f file] [-o file] [-h] [--help] [file.v]: Coq file to be compiled @@ -82,7 +82,7 @@ coq_makefile [subdirectory] .... [file.v] ... [file.ml[i4]?] ... [file.mllib] [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 +[-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 @@ -336,7 +336,7 @@ let implicit () = if !some_mllibfile then mllib_rules (); if !some_vfile then v_rules () -let variables defs = +let variables (args,defs) = let var_aux (v,def) = print v; print "="; print def; print "\n" in section "Variables definitions."; List.iter var_aux defs; @@ -346,7 +346,14 @@ let variables defs = print "override OPT:=-byte\n" else print "OPT?=\n"; - if !impredicative_set = true then print "OTHERFLAGS=-impredicative-set\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"; @@ -358,7 +365,6 @@ let variables defs = 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"; @@ -421,6 +427,7 @@ let subdirs sds = :: "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) @@ -441,8 +448,10 @@ let rec split_arguments = function | 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,d = split_arguments r in (t,i,(v,def)::d) - | [] -> ([],([],[],[],[]),[],[]),([],[]),[] + 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 @@ -591,7 +600,8 @@ let rec process_cmd_line = function | ("-full"|"-opt") :: r -> opt := "-opt"; process_cmd_line r | "-impredicative-set" :: r -> - impredicative_set := true; process_cmd_line r + prerr_string "Please now use \"-arg -impredicative-set\" instead of \"-impredicative-set\" alone to be more uniform.\n"; + Arg "-impredicative_set" :: process_cmd_line r | "-no-install" :: r -> no_install := true; process_cmd_line r | "-custom" :: com :: dependencies :: file :: r -> @@ -620,6 +630,8 @@ let rec process_cmd_line = function (process_cmd_line r) | v :: "=" :: def :: r -> Def (v,def) :: (process_cmd_line r) + | "-arg" :: a :: r -> + Arg a :: (process_cmd_line r) | f :: r -> if Filename.check_suffix f ".v" then begin some_vfile := true; |