diff options
Diffstat (limited to 'toplevel/coqtop.ml')
| -rw-r--r-- | toplevel/coqtop.ml | 220 |
1 files changed, 118 insertions, 102 deletions
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index 943b66f6..09ecb7ec 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -30,29 +30,14 @@ 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 *) -let coqtop_init_feed = Coqloop.coqloop_feed - -(* 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 in - if Dumpglob.dump () then begin - Flags.if_verbose warning "Dumpglob cannot be used in interactive mode."; - Dumpglob.noglob () - end; - let _ = Coqloop.loop ~time:opts.time ~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 coqtop_init_feed = Coqloop.coqloop_feed Topfmt.Initialization -let toploop_run = ref console_toploop_run +let coqtop_doc_feed = Coqloop.coqloop_feed Topfmt.LoadingPrelude + +let coqtop_rcfile_feed = Coqloop.coqloop_feed Topfmt.LoadingRcFile let memory_stat = ref false let print_memory_stat () = @@ -95,15 +80,22 @@ let load_vernacular opts ~state = (fun state (f_in, echo) -> let s = Loadpath.locate_file f_in in (* Should make the beautify logic clearer *) - let load_vernac f = Vernac.load_vernac ~time:opts.time ~echo ~interactive:false ~check:true ~state f in + let load_vernac f = Vernac.load_vernac ~echo ~interactive:false ~check:true ~state f in if !Flags.beautify then Flags.with_option Flags.beautify_file load_vernac f_in else load_vernac s ) state (List.rev opts.load_vernacular_list) -let load_init_vernaculars opts ~state = - let state = if opts.load_rcfile then - Coqinit.load_rcfile ~rcfile:opts.rcfile ~time:opts.time ~state +let load_init_vernaculars cur_feeder opts ~state = + let state = + if opts.load_rcfile then begin + Feedback.del_feeder !cur_feeder; + let rc_feeder = Feedback.add_feeder coqtop_rcfile_feed in + let state = Coqinit.load_rcfile ~rcfile:opts.rcfile ~state in + Feedback.del_feeder rc_feeder; + cur_feeder := Feedback.add_feeder coqtop_init_feed; + state + end else begin Flags.if_verbose Feedback.msg_info (str"Skipping rcfile loading."); state @@ -147,8 +139,8 @@ let fatal_error msg = flush_all (); exit 1 -let fatal_error_exn ?extra exn = - Topfmt.print_err_exn ?extra exn; +let fatal_error_exn exn = + Topfmt.print_err_exn Topfmt.Initialization exn; flush_all (); let exit_code = if CErrors.(is_anomaly exn || not (handled exn)) then 129 else 1 @@ -194,7 +186,7 @@ let ensure_exists f = fatal_error (hov 0 (str "Can't find file" ++ spc () ++ str f)) (* Compile a vernac file *) -let compile opts ~echo ~f_in ~f_out = +let compile cur_feeder opts ~echo ~f_in ~f_out = let open Vernac.State in let check_pending_proofs () = let pfs = Proof_global.get_all_proof_names () in @@ -218,13 +210,18 @@ let compile opts ~echo ~f_in ~f_out = | None -> long_f_dot_v ^ "o" | Some f -> ensure_vo long_f_dot_v f in - let doc, sid = Stm.(new_doc + Feedback.del_feeder !cur_feeder; + let doc_feeder = Feedback.add_feeder coqtop_doc_feed in + let doc, sid = + Stm.(new_doc { doc_type = VoDoc long_f_dot_vo; iload_path; require_libs; stm_options; }) in + Feedback.del_feeder doc_feeder; + cur_feeder := Feedback.add_feeder coqtop_init_feed; - let state = { doc; sid; proof = None } in - let state = load_init_vernaculars opts ~state in + let state = { doc; sid; proof = None; time = opts.time } in + let state = load_init_vernaculars cur_feeder opts ~state in let ldir = Stm.get_ldir ~doc:state.doc in Aux_file.(start_aux_file ~aux_file:(aux_file_name_for long_f_dot_vo) @@ -232,7 +229,7 @@ let compile opts ~echo ~f_in ~f_out = Dumpglob.start_dump_glob ~vfile:long_f_dot_v ~vofile:long_f_dot_vo; Dumpglob.dump_string ("F" ^ Names.DirPath.to_string ldir ^ "\n"); let wall_clock1 = Unix.gettimeofday () in - let state = Vernac.load_vernac ~time:opts.time ~echo ~check:true ~interactive:false ~state long_f_dot_v in + let state = Vernac.load_vernac ~echo ~check:true ~interactive:false ~state long_f_dot_v in let _doc = Stm.join ~doc:state.doc in let wall_clock2 = Unix.gettimeofday () in check_pending_proofs (); @@ -265,15 +262,20 @@ let compile opts ~echo ~f_in ~f_out = async_proofs_tac_error_resilience = `None; } in - let doc, sid = Stm.(new_doc + Feedback.del_feeder !cur_feeder; + let doc_feeder = Feedback.add_feeder coqtop_doc_feed in + let doc, sid = + Stm.(new_doc { doc_type = VioDoc long_f_dot_vio; iload_path; require_libs; stm_options; }) in + Feedback.del_feeder doc_feeder; + cur_feeder := Feedback.add_feeder coqtop_init_feed; - let state = { doc; sid; proof = None } in - let state = load_init_vernaculars opts ~state in + let state = { doc; sid; proof = None; time = opts.time } in + let state = load_init_vernaculars cur_feeder opts ~state in let ldir = Stm.get_ldir ~doc:state.doc in - let state = Vernac.load_vernac ~time:opts.time ~echo ~check:false ~interactive:false ~state long_f_dot_v in + let state = Vernac.load_vernac ~echo ~check:false ~interactive:false ~state long_f_dot_v in let doc = Stm.finish ~doc:state.doc in check_pending_proofs (); let _doc = Stm.snapshot_vio ~doc ldir long_f_dot_vio in @@ -288,22 +290,22 @@ let compile opts ~echo ~f_in ~f_out = let univs, proofs = Stm.finish_tasks lfdv univs disch proofs tasks in Library.save_library_raw lfdv sum lib univs proofs -let compile opts ~echo ~f_in ~f_out = +let compile cur_feeder opts ~echo ~f_in ~f_out = ignore(CoqworkmgrApi.get 1); - compile opts ~echo ~f_in ~f_out; + compile cur_feeder opts ~echo ~f_in ~f_out; CoqworkmgrApi.giveback 1 -let compile_file opts (f_in, echo) = +let compile_file cur_feeder opts (f_in, echo) = let f_out = opts.compilation_output_name in if !Flags.beautify then Flags.with_option Flags.beautify_file - (fun f_in -> compile opts ~echo ~f_in ~f_out) f_in + (fun f_in -> compile cur_feeder opts ~echo ~f_in ~f_out) f_in else - compile opts ~echo ~f_in ~f_out + compile cur_feeder opts ~echo ~f_in ~f_out -let compile_files opts = +let compile_files cur_feeder opts = let compile_list = List.rev opts.compile_list in - List.iter (compile_file opts) compile_list + List.iter (compile_file cur_feeder opts) compile_list (******************************************************************************) (* VIO Dispatching *) @@ -337,8 +339,8 @@ let do_vio opts = (******************************************************************************) (* Color Options *) (******************************************************************************) -let init_color color_mode = - let has_color = match color_mode with +let init_color opts = + let has_color = match opts.color with | `OFF -> false | `ON -> true | `AUTO -> @@ -348,32 +350,23 @@ let init_color color_mode = its TERM variable is set to "dumb". *) try Sys.getenv "TERM" <> "dumb" with Not_found -> false in - if has_color then begin - let colors = try Some (Sys.getenv "COQ_COLORS") with Not_found -> None in - match colors with - | None -> - (** Default colors *) - Topfmt.default_styles (); - Topfmt.init_terminal_output ~color:true - | Some "" -> - (** No color output *) - Topfmt.init_terminal_output ~color:false - | Some s -> - (** Overwrite all colors *) - Topfmt.parse_color_config s; - Topfmt.init_terminal_output ~color:true - end - 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 - x - end + let term_color = + if has_color then begin + let colors = try Some (Sys.getenv "COQ_COLORS") with Not_found -> None in + match colors with + | None -> Topfmt.default_styles (); true (** Default colors *) + | Some "" -> false (** No color output *) + | Some s -> Topfmt.parse_color_config s; true (** Overwrite all colors *) + end + else + false + in + if Proof_diffs.show_diffs () && not term_color && not opts.batch_mode then + (prerr_endline "Error: -diffs requires enabling -color"; exit 1); + Topfmt.init_terminal_output ~color:term_color let print_style_tags opts = - let () = init_color opts.color in + let () = init_color opts in let tags = Topfmt.dump_tags () in let iter (t, st) = let opt = Terminal.eval st ^ t ^ Terminal.reset ^ "\n" in @@ -391,7 +384,7 @@ let print_style_tags opts = (** GC tweaking *) (** Coq is a heavy user of persistent data structures and symbolic ASTs, so the - minor heap is heavily sollicited. Unfortunately, the default size is far too + minor heap is heavily solicited. Unfortunately, the default size is far too small, so we enlarge it a lot (128 times larger). To better handle huge memory consumers, we also augment the default major @@ -414,14 +407,14 @@ 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 *) CProfile.init_profile (); init_gc (); Sys.catch_break false; (* Ctrl-C is fatal during the initialisation *) - let init_feeder = Feedback.add_feeder coqtop_init_feed in + let init_feeder = ref (Feedback.add_feeder coqtop_init_feed) in Lib.init(); (* Coq's init process, phase 2: @@ -436,20 +429,30 @@ let init_toplevel arglist = * early since the master waits us to connect back *) Spawned.init_channels (); Envars.set_coqlib ~fail:(fun msg -> CErrors.user_err Pp.(str msg)); - if opts.print_where then (print_endline(Envars.coqlib ()); exit(exitcode opts)); - if opts.print_config then (Envars.print_config stdout Coq_config.all_src_dirs; exit (exitcode opts)); - if opts.print_tags then (print_style_tags opts; exit (exitcode opts)); - if opts.filter_opts then (print_string (String.concat "\n" extras); exit 0); + if opts.print_where then begin + print_endline (Envars.coqlib ()); + exit (exitcode opts) + end; + if opts.print_config then begin + Envars.print_config stdout Coq_config.all_src_dirs; + exit (exitcode opts) + end; + if opts.print_tags then begin + print_style_tags opts; + exit (exitcode opts) + end; + if opts.filter_opts then begin + print_string (String.concat "\n" extras); + exit 0; + 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 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"; exit 1 end; - Flags.if_verbose print_header (); Mltop.init_known_plugins (); Global.set_engagement opts.impredicative_set; @@ -478,41 +481,54 @@ let init_toplevel arglist = let iload_path = build_load_path opts in let require_libs = require_libs opts in let stm_options = opts.stm_flags in - try - let open Vernac.State in - let doc, sid = - Stm.(new_doc - { doc_type = Interactive opts.toplevel_name; - iload_path; require_libs; stm_options; - }) in - let state = { doc; sid; proof = None } in - Some (load_init_vernaculars opts ~state), opts - with any -> flush_all(); fatal_error_exn any + let open Vernac.State in + Feedback.del_feeder !init_feeder; + let doc_feeder = Feedback.add_feeder coqtop_doc_feed in + let doc, sid = + Stm.(new_doc + { doc_type = Interactive opts.toplevel_name; + iload_path; require_libs; stm_options; + }) in + Feedback.del_feeder doc_feeder; + init_feeder := Feedback.add_feeder coqtop_init_feed; + let state = { doc; sid; proof = None; time = opts.time } in + Some (load_init_vernaculars init_feeder opts ~state), opts (* Non interactive: we perform a sequence of compilation steps *) end else begin - try - compile_files opts; - (* Careful this will modify the load-path and state so after - this point some stuff may not be safe anymore. *) - do_vio opts; - (* Allow the user to output an arbitrary state *) - outputstate opts; - None, opts - with any -> flush_all(); fatal_error_exn any + compile_files init_feeder opts; + (* Careful this will modify the load-path and state so after + this point some stuff may not be safe anymore. *) + do_vio opts; + (* Allow the user to output an arbitrary state *) + outputstate opts; + None, opts end; with any -> flush_all(); - let extra = Some (str "Error during initialization: ") in - fatal_error_exn ?extra any + fatal_error_exn any end in - Feedback.del_feeder init_feeder; + 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; + CoqworkmgrApi.(init !async_proofs_worker_priority); + if CList.is_empty extra then + Flags.if_verbose print_header (); + 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(); |