From 382ee49700c4b4ee78ba95b2e86866ebd3b35d74 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Wed, 7 Mar 2018 01:33:17 +0100 Subject: [stm] Make toplevels standalone executables. We turn coqtop "plugins" into standalone executables, which will be installed in `COQBIN` and located using the standard `PATH` mechanism. Using dynamic linking for `coqtop` customization didn't make a lot of sense, given that only one of such "plugins" could be loaded at a time. This cleans up some code and solves two problems: - `coqtop` needing to locate plugins, - dependency issues as plugins in `stm` depended on files in `toplevel`. In order to implement this, we do some minor cleanup of the toplevel API, making it functional, and implement uniform build rules. In particular: - `stm` and `toplevel` have become library-only directories, - a new directory, `topbin`, contains the new executables, - 4 new binaries have been introduced, for coqide and the stm. - we provide a common and cleaned up way to locate toplevels. --- toplevel/coqargs.ml | 34 ++++++++++---------------------- toplevel/coqargs.mli | 3 ++- toplevel/coqinit.ml | 8 ++------ toplevel/coqloop.ml | 22 +++++++++++++++++++++ toplevel/coqloop.mli | 10 ++++------ toplevel/coqtop.ml | 48 ++++++++++++++++----------------------------- toplevel/coqtop.mli | 25 +++++++++++++---------- toplevel/coqtop_byte_bin.ml | 34 -------------------------------- toplevel/coqtop_opt_bin.ml | 16 --------------- toplevel/toplevel.mllib | 5 +++-- toplevel/workerLoop.ml | 29 +++++++++++++++++++++++++++ toplevel/workerLoop.mli | 14 +++++++++++++ 12 files changed, 118 insertions(+), 130 deletions(-) delete mode 100644 toplevel/coqtop_byte_bin.ml delete mode 100644 toplevel/coqtop_opt_bin.ml create mode 100644 toplevel/workerLoop.ml create mode 100644 toplevel/workerLoop.mli (limited to 'toplevel') diff --git a/toplevel/coqargs.ml b/toplevel/coqargs.ml index 17e848c5a..5c1ffd784 100644 --- a/toplevel/coqargs.ml +++ b/toplevel/coqargs.ml @@ -52,7 +52,6 @@ type coq_cmdopts = { compilation_mode : compilation_mode; toplevel_name : Names.DirPath.t; - toploop : string option; compile_list: (string * bool) list; (* bool is verbosity *) compilation_output_name : string option; @@ -81,6 +80,8 @@ type coq_cmdopts = { print_config: bool; output_context : bool; + print_emacs : bool; + inputstate : string option; outputstate : string option; @@ -100,7 +101,6 @@ let init_args = { compilation_mode = BuildVo; toplevel_name = Names.(DirPath.make [Id.of_string "Top"]); - toploop = None; compile_list = []; compilation_output_name = None; @@ -129,6 +129,8 @@ let init_args = { print_config = false; output_context = false; + print_emacs = false; + inputstate = None; outputstate = None; } @@ -191,11 +193,8 @@ let set_vio_checking_j opts opt j = (** Options for proof general *) let set_emacs opts = - if not (Option.is_empty opts.toploop) then - CErrors.user_err Pp.(str "Flag -emacs is incompatible with a custom toplevel loop"); - Coqloop.print_emacs := true; Printer.enable_goal_tags_printing := true; - { opts with color = `OFF } + { opts with color = `OFF; print_emacs = true } let set_color opts = function | "yes" | "on" -> { opts with color = `ON } @@ -310,12 +309,9 @@ let usage batch = let lp = Coqinit.toplevel_init_load_path () in (* Necessary for finding the toplevels below *) List.iter Mltop.add_coq_path lp; - if batch then Usage.print_usage_coqc () - else begin - Mltop.load_ml_objects_raw_rex - (Str.regexp (if Mltop.is_native then "^.*top.cmxs$" else "^.*top.cma$")); - Usage.print_usage_coqtop () - end + if batch + then Usage.print_usage_coqc () + else Usage.print_usage_coqtop () (* Main parsing routine *) let parse_args arglist : coq_cmdopts * string list = @@ -401,7 +397,7 @@ let parse_args arglist : coq_cmdopts * string list = }} |"-async-proofs-worker-priority" -> - WorkerLoop.async_proofs_worker_priority := get_priority opt (next ()); + CoqworkmgrApi.async_proofs_worker_priority := get_priority opt (next ()); oval |"-async-proofs-private-flags" -> @@ -500,11 +496,6 @@ let parse_args arglist : coq_cmdopts * string list = let oval = add_compile oval false (next ()) in { oval with compilation_mode = Vio2Vo } - |"-toploop" -> - if !Coqloop.print_emacs then - CErrors.user_err Pp.(str "Flags -toploop and -emacs are incompatible"); - { oval with toploop = Some (next ()) } - |"-w" | "-W" -> let w = next () in if w = "none" then @@ -538,12 +529,7 @@ let parse_args arglist : coq_cmdopts * string list = |"-stm-debug" -> Stm.stm_debug := true; oval |"-emacs" -> set_emacs oval |"-filteropts" -> { oval with filter_opts = true } - |"-ideslave" -> - if !Coqloop.print_emacs then - CErrors.user_err Pp.(str "Flags -ideslave and -emacs are incompatible"); - Flags.ide_slave := true; - { oval with toploop = Some "coqidetop" } - + |"-ideslave" -> Flags.ide_slave := true; oval |"-impredicative-set" -> { oval with impredicative_set = Declarations.ImpredicativeSet } |"-indices-matter" -> Indtypes.enforce_indices_matter (); oval diff --git a/toplevel/coqargs.mli b/toplevel/coqargs.mli index de9b6a682..9fb6219a6 100644 --- a/toplevel/coqargs.mli +++ b/toplevel/coqargs.mli @@ -27,7 +27,6 @@ type coq_cmdopts = { compilation_mode : compilation_mode; toplevel_name : Names.DirPath.t; - toploop : string option; compile_list: (string * bool) list; (* bool is verbosity *) compilation_output_name : string option; @@ -56,6 +55,8 @@ type coq_cmdopts = { print_config: bool; output_context : bool; + print_emacs : bool; + inputstate : string option; outputstate : string option; diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml index 3e7a83085..e61f830f3 100644 --- a/toplevel/coqinit.ml +++ b/toplevel/coqinit.ml @@ -75,16 +75,12 @@ let ml_path_if c p = let f x = { recursive = false; path_spec = MlPath x } in if c then List.map f p else [] -(* LoadPath for toploop toplevels *) +(* LoadPath for developers *) let toplevel_init_load_path () = let coqlib = Envars.coqlib () in (* NOTE: These directories are searched from last to first *) (* first, developer specific directory to open *) - ml_path_if Coq_config.local [coqlib/"dev"] @ - - (* main loops *) - ml_path_if (Coq_config.local || !Flags.boot) [coqlib/"stm"; coqlib/"ide"] @ - ml_path_if (System.exists_dir (coqlib/"toploop")) [coqlib/"toploop"] + ml_path_if Coq_config.local [coqlib/"dev"] (* LoadPath for Coq user libraries *) let libs_init_load_path ~load_init = diff --git a/toplevel/coqloop.ml b/toplevel/coqloop.ml index da9169514..d7ede1c2e 100644 --- a/toplevel/coqloop.ml +++ b/toplevel/coqloop.ml @@ -410,3 +410,25 @@ let rec loop ~state = str (Printexc.to_string any)) ++ spc () ++ hov 0 (str "Please report at " ++ str Coq_config.wwwbugtracker ++ str ".")); loop ~state + +(* Default toplevel loop *) +let warning s = Flags.(with_option warn Feedback.msg_warning (strbrk s)) + +let drop_args = ref None +let loop ~opts ~state = + drop_args := Some opts; + let open Coqargs in + print_emacs := opts.print_emacs; + (* We initialize the console only if we run the toploop_run *) + let tl_feed = Feedback.add_feeder (coqloop_feed Topfmt.InteractiveLoop) in + if Dumpglob.dump () then begin + Flags.if_verbose warning "Dumpglob cannot be used in interactive mode."; + Dumpglob.noglob () + end; + let _ = loop ~state in + (* Initialise and launch the Ocaml toplevel *) + Coqinit.init_ocaml_path(); + Mltop.ocaml_toploop(); + (* We delete the feeder after the OCaml toploop has ended so users + of Drop can see the feedback. *) + Feedback.del_feeder tl_feed diff --git a/toplevel/coqloop.mli b/toplevel/coqloop.mli index 6d9867fb9..5c07a8bf3 100644 --- a/toplevel/coqloop.mli +++ b/toplevel/coqloop.mli @@ -10,9 +10,6 @@ (** The Coq toplevel loop. *) -(** -emacs option: printing includes emacs tags. *) -val print_emacs : bool ref - (** A buffer for the character read from a channel. We store the command * entered to be able to report errors without pretty-printing. *) @@ -32,8 +29,9 @@ val set_prompt : (unit -> string) -> unit (** Toplevel feedback printer. *) val coqloop_feed : Topfmt.execution_phase -> Feedback.feedback -> unit -(** Main entry point of Coq: read and execute vernac commands. *) -val loop : state:Vernac.State.t -> Vernac.State.t - (** Last document seen after `Drop` *) val drop_last_doc : Vernac.State.t option ref +val drop_args : Coqargs.coq_cmdopts option ref + +(** Main entry point of Coq: read and execute vernac commands. *) +val loop : opts:Coqargs.coq_cmdopts -> state:Vernac.State.t -> unit diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index 809490166..e979d0e54 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -30,8 +30,6 @@ let print_header () = Feedback.msg_notice (str "Welcome to Coq " ++ str ver ++ str " (" ++ str rev ++ str ")"); flush_all () -let warning s = Flags.(with_option warn Feedback.msg_warning (strbrk s)) - (* Feedback received in the init stage, this is different as the STM will not be generally be initialized, thus stateid, etc... may be bogus. For now we just print to the console too *) @@ -41,23 +39,6 @@ let coqtop_doc_feed = Coqloop.coqloop_feed Topfmt.LoadingPrelude let coqtop_rcfile_feed = Coqloop.coqloop_feed Topfmt.LoadingRcFile -(* Default toplevel loop *) -let console_toploop_run opts ~state = - (* We initialize the console only if we run the toploop_run *) - let tl_feed = Feedback.add_feeder (Coqloop.coqloop_feed Topfmt.InteractiveLoop) in - if Dumpglob.dump () then begin - Flags.if_verbose warning "Dumpglob cannot be used in interactive mode."; - Dumpglob.noglob () - end; - let _ = Coqloop.loop ~state in - (* Initialise and launch the Ocaml toplevel *) - Coqinit.init_ocaml_path(); - Mltop.ocaml_toploop(); - (* We let the feeder in place for users of Drop *) - Feedback.del_feeder tl_feed - -let toploop_run = ref console_toploop_run - let memory_stat = ref false let print_memory_stat () = begin (* -m|--memory from the command-line *) @@ -387,12 +368,6 @@ let init_color color_mode = else Topfmt.init_terminal_output ~color:false -let toploop_init = ref begin fun opts x -> - let () = init_color opts.color in - let () = CoqworkmgrApi.init !WorkerLoop.async_proofs_worker_priority in - opts, x - end - let print_style_tags opts = let () = init_color opts.color in let tags = Topfmt.dump_tags () in @@ -435,7 +410,7 @@ let init_gc () = Gc.space_overhead = 120} (** Main init routine *) -let init_toplevel arglist = +let init_toplevel custom_init arglist = (* Coq's init process, phase 1: OCaml parameters, basic structures, and IO *) @@ -475,8 +450,7 @@ let init_toplevel arglist = end; let top_lp = Coqinit.toplevel_init_load_path () in List.iter Mltop.add_coq_path top_lp; - Option.iter Mltop.load_ml_object_raw opts.toploop; - let opts, extras = !toploop_init opts extras in + let opts, extras = custom_init ~opts extras in if not (CList.is_empty extras) then begin prerr_endline ("Don't know what to do with "^String.concat " " extras); prerr_endline "See -help for the list of supported options"; @@ -540,11 +514,23 @@ let init_toplevel arglist = Feedback.del_feeder !init_feeder; res -let start () = - match init_toplevel (List.tl (Array.to_list Sys.argv)) with +type custom_toplevel = { + init : opts:coq_cmdopts -> string list -> coq_cmdopts * string list; + run : opts:coq_cmdopts -> state:Vernac.State.t -> unit; +} + +let coqtop_init ~opts extra = + init_color opts.color; + CoqworkmgrApi.(init !async_proofs_worker_priority); + opts, extra + +let coqtop_toplevel = { init = coqtop_init; run = Coqloop.loop; } + +let start_coq custom = + match init_toplevel custom.init (List.tl (Array.to_list Sys.argv)) with (* Batch mode *) | Some state, opts when not opts.batch_mode -> - !toploop_run opts ~state; + custom.run ~opts ~state; exit 1 | _ , opts -> flush_all(); diff --git a/toplevel/coqtop.mli b/toplevel/coqtop.mli index fcc569ca0..641448f10 100644 --- a/toplevel/coqtop.mli +++ b/toplevel/coqtop.mli @@ -8,16 +8,21 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) -(** The Coq main module. The following function [start] will parse the - command line, print the banner, initialize the load path, load the input - state, load the files given on the command line, load the resource file, - produce the output state if any, and finally will launch [Coqloop.loop]. *) +(** Definition of custom toplevels. + [init] is used to do custom command line argument parsing. + [run] launches a custom toplevel. +*) +type custom_toplevel = { + init : opts:Coqargs.coq_cmdopts -> string list -> Coqargs.coq_cmdopts * string list; + run : opts:Coqargs.coq_cmdopts -> state:Vernac.State.t -> unit; +} -val init_toplevel : string list -> Vernac.State.t option * Coqargs.coq_cmdopts +val coqtop_toplevel : custom_toplevel -val start : unit -> unit +(** The Coq main module. [start custom] will parse the command line, + print the banner, initialize the load path, load the input state, + load the files given on the command line, load the resource file, + produce the output state if any, and finally will launch + [custom.run]. *) -(* For other toploops *) -val toploop_init : - (Coqargs.coq_cmdopts -> string list -> Coqargs.coq_cmdopts * string list) ref -val toploop_run : (Coqargs.coq_cmdopts -> state:Vernac.State.t -> unit) ref +val start_coq : custom_toplevel -> unit diff --git a/toplevel/coqtop_byte_bin.ml b/toplevel/coqtop_byte_bin.ml deleted file mode 100644 index 0b65cebbb..000000000 --- a/toplevel/coqtop_byte_bin.ml +++ /dev/null @@ -1,34 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(* f () - | _ -> () - end - with - | Not_found -> () - end; - let ppf = Format.std_formatter in - Mltop.(set_top - { load_obj = (fun f -> if not (Topdirs.load_file ppf f) - then CErrors.user_err Pp.(str ("Could not load plugin "^f)) - ); - use_file = Topdirs.dir_use ppf; - add_dir = Topdirs.dir_directory; - ml_loop = (fun () -> Toploop.loop ppf); - }) - -(* Main coqtop initialization *) -let _ = - drop_setup (); - Coqtop.start() diff --git a/toplevel/coqtop_opt_bin.ml b/toplevel/coqtop_opt_bin.ml deleted file mode 100644 index ea4c0ea52..000000000 --- a/toplevel/coqtop_opt_bin.ml +++ /dev/null @@ -1,16 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(* parse rest + | x :: rest -> x :: parse rest + | [] -> [] + +let arg_init init ~opts extra_args = + let extra_args = parse extra_args in + Flags.quiet := true; + init (); + CoqworkmgrApi.(init !async_proofs_worker_priority); + opts, extra_args + +let start ~init ~loop = + let open Coqtop in + let custom = { + init = arg_init init; + run = (fun ~opts:_ ~state:_ -> loop ()); + } in + start_coq custom diff --git a/toplevel/workerLoop.mli b/toplevel/workerLoop.mli new file mode 100644 index 000000000..e497dee6d --- /dev/null +++ b/toplevel/workerLoop.mli @@ -0,0 +1,14 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* unit) -> + loop:(unit -> unit) -> unit -- cgit v1.2.3