diff options
Diffstat (limited to 'scripts/coqmktop.ml')
| -rw-r--r-- | scripts/coqmktop.ml | 113 |
1 files changed, 50 insertions, 63 deletions
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 *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: coqmktop.ml 14641 2011-11-06 11:59:10Z herbelin $ *) - (* coqmktop is a script to link Coq, analogous to ocamlmktop. The command line contains options specific to coqmktop, options for the Ocaml linker and files to link (in addition to the default Coq files). *) @@ -19,7 +17,8 @@ open Unix (* 1. Core objects *) let ocamlobjs = ["str.cma";"unix.cma";"nums.cma"] let dynobjs = ["dynlink.cma"] -let camlp4objs = ["gramlib.cma"] +let camlp4objs = + if Coq_config.camlp4 = "camlp5" then ["gramlib.cma"] else ["camlp4lib.cma"] let libobjs = ocamlobjs @ camlp4objs let spaces = Str.regexp "[ \t\n]+" @@ -28,14 +27,17 @@ let split_list l = Str.split spaces l let copts = split_list Tolink.copts let core_objs = split_list Tolink.core_objs let core_libs = split_list Tolink.core_libs -let ide = split_list Tolink.ide (* 3. Toplevel objects *) let camlp4topobjs = if Coq_config.camlp4 = "camlp5" then ["camlp5_top.cma"; "pa_o.cmo"; "pa_extend.cmo"] else - ["camlp4_top.cma"; "pa_o.cmo"; "pa_op.cmo"; "pa_extend.cmo"] + [ "Camlp4Top.cmo"; + "Camlp4Parsers/Camlp4OCamlRevisedParser.cmo"; + "Camlp4Parsers/Camlp4OCamlParser.cmo"; + "Camlp4Parsers/Camlp4GrammarParser.cmo"; + "q_util.cmo"; "q_coqast.cmo" ] let topobjs = camlp4topobjs let gramobjs = [] @@ -47,13 +49,11 @@ let notopobjs = gramobjs let opt = ref false let full = ref false let top = ref false -let searchisos = ref false -let coqide = ref false let echo = ref false +let no_start = ref false let src_dirs () = - [ []; ["kernel";"byterun"]; [ "config" ]; [ "toplevel" ] ] @ - if !coqide then [[ "ide" ]] else [] + [ []; ["kernel";"byterun"]; [ "config" ]; [ "toplevel" ] ] let includes () = let coqlib = Envars.coqlib () in @@ -62,8 +62,7 @@ let includes () = (fun d l -> "-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 <options> <ocaml options> 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 <options> <ocaml options> 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 -> |