diff options
Diffstat (limited to 'scripts')
| -rw-r--r-- | scripts/coqc.ml4 | 7 | ||||
| -rw-r--r-- | scripts/coqmktop.ml | 17 |
2 files changed, 11 insertions, 13 deletions
diff --git a/scripts/coqc.ml4 b/scripts/coqc.ml4 index c4d6468dd7..d0ef0c5ebc 100644 --- a/scripts/coqc.ml4 +++ b/scripts/coqc.ml4 @@ -18,6 +18,7 @@ let environment = Unix.environment () let bindir = ref Coq_config.bindir +let binary = ref "coqtop.byte" (* the $COQBIN environment variable has priority over the Coq_config value *) let _ = @@ -114,6 +115,8 @@ let parse_args () = bindir := d ; parse (cfiles,args) rem | "-bindir" :: [] -> usage () + | "-opt" :: rem -> + binary := "coqtop.opt"; parse (cfiles,args) rem | ("-?"|"-h"|"-H"|"-help"|"--help") :: _ -> usage () | ("-image"|"-libdir"|"-I"|"-R"|"-include"|"-outputstate"|"-inputstate" |"-is"|"-load-vernac-source"|"-load-vernac-object"|"-load-ml-source" @@ -125,7 +128,7 @@ let parse_args () = | [] -> usage () end | ("-notactics"|"-debug"|"-db"|"-debugger"|"-nolib"|"-batch"|"-nois" - |"-q"|"-opt"|"-full"|"-profile"|"-just-parsing"|"-echo" as o) :: rem -> + |"-q"|"-full"|"-profile"|"-just-parsing"|"-echo" as o) :: rem -> parse (cfiles,o::args) rem | f :: rem -> if Sys.file_exists f then @@ -150,7 +153,7 @@ let main () = prerr_endline "coqc: too few arguments" ; usage () end; - let coqtopname = Filename.concat !bindir "coqtop.byte" in + let coqtopname = Filename.concat !bindir !binary in List.iter (compile coqtopname args) cfiles let _ = Printexc.print main (); exit 0 diff --git a/scripts/coqmktop.ml b/scripts/coqmktop.ml index a148c7695c..e087271aef 100644 --- a/scripts/coqmktop.ml +++ b/scripts/coqmktop.ml @@ -49,15 +49,11 @@ let notopobjs = gramobjs (* 5. High-level tactics objects *) let hightactics = split_cmo Tolink.hightactics -let cmotacsobjs = [ - "prolog.cmo"; "equality.cmo"; "inv.cmo"; "leminv.cmo"; - "point.cmo"; "progmach.cmo"; "program.cmo"; "propre.cmo"; - "tauto.cmo"; "gelim.cmo"; "eqdecide.cmo"] (* environment *) let src_coqtop = ref Coq_config.coqtop -let notactics = ref false let opt = ref false +let full = ref false let top = ref false let searchisos = ref false let echo = ref false @@ -98,10 +94,9 @@ let module_of_file name = let files_to_link userfiles = let dyn_objs = if not !opt then dynobjs else [] in let command_objs = if !searchisos then coqsearch else [] in - let tactic_objs = if !notactics then [] else hightactics in let toplevel_objs = if !top then topobjs else if !opt then notopobjs else [] in - let objs = core_objs @ dyn_objs @ toplevel @ command_objs @ tactic_objs @ + let objs = core_objs @ dyn_objs @ toplevel @ command_objs @ hightactics @ toplevel_objs in let tolink = if !opt then @@ -142,11 +137,11 @@ let usage () = prerr_endline "Usage: coqmktop <options> <ocaml options> files Options are: -srcdir dir Specify where the Coq source files are - -notactics Do not link high level tactics -o exec-file Specify the name of the resulting toplevel -opt Compile in native code + -full Link high level tactics -top Build Coq on a ocaml toplevel (incompatible with -opt) - -searchisos Build a toplevel for SearchIsos (implies -notactics) + -searchisos Build a toplevel for SearchIsos -R dir Specify recursively directories for Ocaml\n"; exit 1 @@ -156,11 +151,11 @@ let parse_args () = | [] -> List.rev op, List.rev fl | "-srcdir" :: d :: rem -> src_coqtop := d ; parse (op,fl) rem | "-srcdir" :: _ -> usage () - | "-notactics" :: rem -> notactics := true ; parse (op,fl) rem | "-opt" :: rem -> opt := true ; parse (op,fl) rem + | "-full" :: rem -> full := true ; parse (op,fl) rem | "-top" :: rem -> top := true ; parse (op,fl) rem | "-searchisos" :: rem -> - searchisos := true; notactics := true; parse (op,fl) rem + searchisos := true; parse (op,fl) rem | "-echo" :: rem -> echo := true ; parse (op,fl) rem | ("-cclib"|"-ccopt"|"-I"|"-o" as o) :: rem' -> begin |