From 97fefe1fcca363a1317e066e7f4b99b9c1e9987b Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Thu, 12 Jan 2012 16:02:20 +0100 Subject: Imported Upstream version 8.4~beta --- scripts/coqc.ml | 15 +++---- scripts/coqmktop.ml | 113 +++++++++++++++++++++++----------------------------- 2 files changed, 56 insertions(+), 72 deletions(-) (limited to 'scripts') diff --git a/scripts/coqc.ml b/scripts/coqc.ml index d5544b94..dfcb9c18 100644 --- a/scripts/coqc.ml +++ b/scripts/coqc.ml @@ -1,13 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* usage () | ("-outputstate"|"-inputstate"|"-is" |"-load-vernac-source"|"-l"|"-load-vernac-object" - |"-load-ml-source"|"-require"|"-load-ml-object"|"-user" + |"-load-ml-source"|"-require"|"-load-ml-object" |"-init-file"|"-dump-glob"|"-compat"|"-coqlib" as o) :: rem -> begin match rem with @@ -153,12 +151,11 @@ let parse_args () = | "-R" :: s :: t :: rem -> parse (cfiles,t::s::"-R"::args) rem | ("-notactics"|"-debug"|"-nolib" - |"-debugVM"|"-alltransp"|"-VMno" |"-batch"|"-nois"|"-noglob"|"-no-glob" |"-q"|"-full"|"-profile"|"-just-parsing"|"-echo" |"-unsafe"|"-quiet" |"-silent"|"-m"|"-xml"|"-v7"|"-v8"|"-beautify"|"-strict-implicit" - |"-dont-load-proofs"|"-impredicative-set"|"-vm" - |"-unboxed-values"|"-unboxed-definitions"|"-draw-vm-instr" as o) :: rem -> + |"-dont-load-proofs"|"-load-proofs"|"-force-load-proofs" + |"-impredicative-set"|"-vm" as o) :: rem -> parse (cfiles,o::args) rem | ("-where") :: _ -> @@ -169,7 +166,7 @@ let parse_args () = | ("-config" | "--config") :: _ -> Usage.print_config (); exit 0 | ("-v"|"--version") :: _ -> - Usage.version () + Usage.version 0 | f :: rem -> if Sys.file_exists f then parse (f::cfiles,args) rem @@ -195,7 +192,7 @@ let main () = end; let coqtopname = if !image <> "" then !image - else Filename.concat (Envars.coqbin ()) (!binary ^ Coq_config.exec_extension) + else Filename.concat Envars.coqbin (!binary ^ Coq_config.exec_extension) in (* List.iter (compile coqtopname args) cfiles*) Unix.handle_unix_error (compile coqtopname args) cfiles diff --git a/scripts/coqmktop.ml b/scripts/coqmktop.ml index c7596d83..7dcfbab1 100644 --- a/scripts/coqmktop.ml +++ b/scripts/coqmktop.ml @@ -1,13 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* "-I" :: ("\"" ^ List.fold_left Filename.concat coqlib d ^ "\"") :: l) (src_dirs ()) (["-I"; "\"" ^ camlp4lib ^ "\""] @ - ["-I"; "\"" ^ coqlib ^ "\""] @ - (if !coqide then ["-thread"; "-I"; "+lablgtk2"] else [])) + ["-I"; "\"" ^ coqlib ^ "\""]) (* Transform bytecode object file names in native object file names *) let native_suffix f = @@ -89,18 +88,10 @@ let files_to_link userfiles = if not !opt || Coq_config.has_natdynlink then dynobjs else [] in let toplevel_objs = if !top then topobjs else if !opt then notopobjs else [] in - let ide_objs = - if !coqide then "Threads"::"Lablgtk"::"GtkThread"::ide else [] - in - let ide_libs = - if !coqide then - ["threads.cma" ; "lablgtk.cma" ; "gtkThread.cmo" ; "ide/ide.cma" ] - else [] - in - let objs = dyn_objs @ libobjs @ core_objs @ toplevel_objs @ ide_objs in + let objs = dyn_objs @ libobjs @ core_objs @ toplevel_objs in let modules = List.map module_of_file (objs @ userfiles) in - let libs = dyn_objs @ libobjs @ core_libs @ toplevel_objs @ ide_libs in + let libs = dyn_objs @ libobjs @ core_libs @ toplevel_objs in let libstolink = (if !opt then List.map native_suffix libs else libs) @ userfiles in @@ -132,20 +123,19 @@ let all_subdirs dir = (* usage *) let usage () = - prerr_endline "Usage: coqmktop files -Flags are: - -coqlib dir Specify where the Coq object files are - -camlbin dir Specify where the OCaml binaries are - -camlp4bin dir Specify where the CAmp4/5 binaries are - -o exec-file Specify the name of the resulting toplevel - -boot Run in boot mode - -echo Print calls to external commands - -ide Build a toplevel for the Coq IDE - -full Link high level tactics - -opt Compile in native code - -searchisos Build a toplevel for SearchIsos - -top Build Coq on a OCaml toplevel (incompatible with -opt) - -R dir Specify recursively directories for Ocaml\n"; + prerr_endline "Usage: coqmktop files\ +\nFlags are:\ +\n -coqlib dir Specify where the Coq object files are\ +\n -camlbin dir Specify where the OCaml binaries are\ +\n -camlp4bin dir Specify where the Camlp4/5 binaries are\ +\n -o exec-file Specify the name of the resulting toplevel\ +\n -boot Run in boot mode\ +\n -echo Print calls to external commands\ +\n -full Link high level tactics\ +\n -opt Compile in native code\ +\n -top Build Coq on a OCaml toplevel (incompatible with -opt)\ +\n -R dir Add recursively dir to OCaml search path\ +\n"; exit 1 (* parsing of the command line *) @@ -165,8 +155,6 @@ let parse_args () = | "-opt" :: rem -> opt := true ; parse (op,fl) rem | "-full" :: rem -> full := true ; parse (op,fl) rem | "-top" :: rem -> top := true ; parse (op,fl) rem - | "-ide" :: rem -> - coqide := true; parse (op,fl) rem | "-v8" :: rem -> Printf.eprintf "warning: option -v8 deprecated"; parse (op,fl) rem @@ -184,12 +172,14 @@ let parse_args () = | ("-noassert"|"-compact"|"-g"|"-p"|"-thread"|"-dtypes" as o) :: rem -> parse (o::op,fl) rem | ("-h"|"--help") :: _ -> usage () + | ("-no-start") :: rem -> no_start:=true; parse (op, fl) rem | f :: rem -> if Filename.check_suffix f ".ml" or Filename.check_suffix f ".cmx" or Filename.check_suffix f ".cmo" or Filename.check_suffix f ".cmxa" - or Filename.check_suffix f ".cma" then + or Filename.check_suffix f ".cma" + or Filename.check_suffix f ".c" then parse (op,f::fl) rem else begin prerr_endline ("Don't know what to do with " ^ f); @@ -220,23 +210,24 @@ let declare_loading_string () = if not !top then "Mltop.remove ();;" else - "begin try - (* Enable rectypes in the toplevel if it has the directive #rectypes *) - begin match Hashtbl.find Toploop.directive_table \"rectypes\" with - | Toploop.Directive_none f -> f () - | _ -> () - end - with - | Not_found -> () - end;; - - let ppf = Format.std_formatter;; - Mltop.set_top - {Mltop.load_obj= - (fun f -> if not (Topdirs.load_file ppf f) then Util.error (\"Could not load plugin \"^f));\ - Mltop.use_file=Topdirs.dir_use ppf; - Mltop.add_dir=Topdirs.dir_directory; - Mltop.ml_loop=(fun () -> Toploop.loop ppf) };;\n" + "begin try\ +\n (* Enable rectypes in the toplevel if it has the directive #rectypes *)\ +\n begin match Hashtbl.find Toploop.directive_table \"rectypes\" with\ +\n | Toploop.Directive_none f -> f ()\ +\n | _ -> ()\ +\n end\ +\n with\ +\n | Not_found -> ()\ +\n end;;\ +\n\ +\n let ppf = Format.std_formatter;;\ +\n Mltop.set_top\ +\n {Mltop.load_obj=\ +\n (fun f -> if not (Topdirs.load_file ppf f) then Util.error (\"Could not load plugin \"^f));\ +\n Mltop.use_file=Topdirs.dir_use ppf;\ +\n Mltop.add_dir=Topdirs.dir_directory;\ +\n Mltop.ml_loop=(fun () -> Toploop.loop ppf) };;\ +\n" (* create a temporary main file to link *) let create_tmp_main_file modules = @@ -249,13 +240,9 @@ let create_tmp_main_file modules = output_string oc "\"];;\n"; (* Initializes the kind of loading *) output_string oc (declare_loading_string()); - (* Start the right toplevel loop: Coq or Coq_searchisos *) - if !searchisos then - output_string oc "Cmd_searchisos_line.start();;\n" - else if !coqide then - output_string oc "Coqide.start();;\n" - else - output_string oc "Coqtop.start();;\n"; + (* Start the toplevel loop *) + if not !no_start then + output_string oc "Coqtop.start();;\n"; close_out oc; main_name with e -> -- cgit v1.2.3