diff options
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/coqargs.ml | 4 | ||||
| -rw-r--r-- | toplevel/coqloop.ml | 55 | ||||
| -rw-r--r-- | toplevel/coqloop.mli | 2 | ||||
| -rw-r--r-- | toplevel/coqtop.ml | 148 | ||||
| -rw-r--r-- | toplevel/coqtop.mli | 3 |
5 files changed, 132 insertions, 80 deletions
diff --git a/toplevel/coqargs.ml b/toplevel/coqargs.ml index a1a07fce87..17e848c5af 100644 --- a/toplevel/coqargs.ml +++ b/toplevel/coqargs.ml @@ -10,8 +10,8 @@ let warning s = Flags.(with_option warn Feedback.msg_warning (Pp.strbrk s)) -let fatal_error ?extra exn = - Topfmt.print_err_exn ?extra exn; +let fatal_error exn = + Topfmt.print_err_exn Topfmt.ParsingCommandLine exn; let exit_code = if CErrors.(is_anomaly exn || not (handled exn)) then 129 else 1 in exit exit_code diff --git a/toplevel/coqloop.ml b/toplevel/coqloop.ml index d0989cfcc2..da91695144 100644 --- a/toplevel/coqloop.ml +++ b/toplevel/coqloop.ml @@ -150,29 +150,28 @@ let print_highlight_location ib loc = let valid_buffer_loc ib loc = let (b,e) = Loc.unloc loc in b-ib.start >= 0 && e-ib.start < ib.len && b<=e - (* Toplevel error explanation. *) -let error_info_for_buffer ?loc buf = - Option.map (fun loc -> +let error_info_for_buffer ?loc phase buf = + match loc with + | None -> Topfmt.pr_phase ?loc phase + | Some loc -> let fname = loc.Loc.fname in - let hl, loc = (* We are in the toplevel *) - match fname with - | Loc.ToplevelInput -> - let nloc = adjust_loc_buf buf loc in - if valid_buffer_loc buf loc then - (fnl () ++ print_highlight_location buf nloc, nloc) - (* in the toplevel, but not a valid buffer *) - else (mt (), nloc) - (* we are in batch mode, don't adjust location *) - | Loc.InFile _ -> - (mt (), loc) - in Topfmt.pr_loc loc ++ hl - ) loc + match fname with + | Loc.ToplevelInput -> + let nloc = adjust_loc_buf buf loc in + if valid_buffer_loc buf loc then + match Topfmt.pr_phase ~loc:nloc phase with + | None -> None + | Some hd -> Some (hd ++ fnl () ++ print_highlight_location buf nloc) + (* in the toplevel, but not a valid buffer *) + else Topfmt.pr_phase ~loc phase + (* we are in batch mode, don't adjust location *) + | Loc.InFile _ -> Topfmt.pr_phase ~loc phase (* Actual printing routine *) -let print_error_for_buffer ?loc lvl msg buf = - let pre_hdr = error_info_for_buffer ?loc buf in +let print_error_for_buffer ?loc phase lvl msg buf = + let pre_hdr = error_info_for_buffer ?loc phase buf in if !print_emacs then Topfmt.emacs_logger ?pre_hdr lvl msg else Topfmt.std_logger ?pre_hdr lvl msg @@ -272,8 +271,17 @@ let read_sentence ~state input = (* TopErr.print_toplevel_parse_error reraise top_buffer; *) Exninfo.iraise reraise +let extract_default_loc loc doc_id sid : Loc.t option = + match loc with + | Some _ -> loc + | None -> + try + let doc = Stm.get_doc doc_id in + Option.cata fst None Stm.(get_ast ~doc sid) + with _ -> loc + (** Coqloop Console feedback handler *) -let coqloop_feed (fb : Feedback.feedback) = let open Feedback in +let coqloop_feed phase (fb : Feedback.feedback) = let open Feedback in match fb.contents with | Processed -> () | Incomplete -> () @@ -290,8 +298,11 @@ let coqloop_feed (fb : Feedback.feedback) = let open Feedback in (* Re-enable when we switch back to feedback-based error printing *) | Message (Error,loc,msg) -> () (* TopErr.print_error_for_buffer ?loc lvl msg top_buffer *) + | Message (Warning,loc,msg) -> + let loc = extract_default_loc loc fb.doc_id fb.span_id in + TopErr.print_error_for_buffer ?loc phase Warning msg top_buffer | Message (lvl,loc,msg) -> - TopErr.print_error_for_buffer ?loc lvl msg top_buffer + TopErr.print_error_for_buffer ?loc phase lvl msg top_buffer (** Main coq loop : read vernacular expressions until Drop is entered. Ctrl-C is handled internally as Sys.Break instead of aborting Coq. @@ -341,7 +352,7 @@ let top_goal_print oldp newp = let (e, info) = CErrors.push exn in let loc = Loc.get_loc info in let msg = CErrors.iprint (e, info) in - TopErr.print_error_for_buffer ?loc Feedback.Error msg top_buffer + TopErr.print_error_for_buffer ?loc Topfmt.InteractiveLoop Feedback.Error msg top_buffer (* Careful to keep this loop tail-rec *) let rec vernac_loop ~state = @@ -383,7 +394,7 @@ let rec vernac_loop ~state = let (e, info) = CErrors.push any in let loc = Loc.get_loc info in let msg = CErrors.iprint (e, info) in - TopErr.print_error_for_buffer ?loc Feedback.Error msg top_buffer; + TopErr.print_error_for_buffer ?loc Topfmt.InteractiveLoop Feedback.Error msg top_buffer; vernac_loop ~state let rec loop ~state = diff --git a/toplevel/coqloop.mli b/toplevel/coqloop.mli index 39a9de4f83..6d9867fb97 100644 --- a/toplevel/coqloop.mli +++ b/toplevel/coqloop.mli @@ -30,7 +30,7 @@ val top_buffer : input_buffer val set_prompt : (unit -> string) -> unit (** Toplevel feedback printer. *) -val coqloop_feed : Feedback.feedback -> unit +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 diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index a08cfa9f48..809490166c 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -35,12 +35,16 @@ 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 +let coqtop_init_feed = Coqloop.coqloop_feed Topfmt.Initialization + +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 in + 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 () @@ -101,9 +105,16 @@ let load_vernacular opts ~state = 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 ~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 +158,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 +205,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 +229,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; time = opts.time } in - let state = load_init_vernaculars opts ~state 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) @@ -265,13 +281,18 @@ 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; time = opts.time } in - let state = load_init_vernaculars opts ~state 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 ~echo ~check:false ~interactive:false ~state long_f_dot_v in let doc = Stm.finish ~doc:state.doc in @@ -288,21 +309,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:None) f_in + (fun f_in -> compile cur_feeder opts ~echo ~f_in ~f_out) f_in else - compile opts ~echo ~f_in ~f_out:None + 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 *) @@ -315,16 +337,24 @@ let check_vio_tasks opts = (* vio files *) let schedule_vio opts = - (* We must add update the loadpath here as the scheduling process - happens outside of the STM *) - let iload_path = build_load_path opts in - List.iter Mltop.add_coq_path iload_path; - if opts.vio_checking then Vio_checking.schedule_vio_checking opts.vio_files_j opts.vio_files else Vio_checking.schedule_vio_compilation opts.vio_files_j opts.vio_files +let do_vio opts = + (* We must initialize the loadpath here as the vio scheduling + process happens outside of the STM *) + if opts.vio_files <> [] || opts.vio_tasks <> [] then + let iload_path = build_load_path opts in + List.iter Mltop.add_coq_path iload_path; + + (* Vio compile pass *) + if opts.vio_files <> [] then schedule_vio opts; + (* Vio task pass *) + if opts.vio_tasks <> [] then check_vio_tasks opts + + (******************************************************************************) (* Color Options *) (******************************************************************************) @@ -360,7 +390,7 @@ let init_color color_mode = let toploop_init = ref begin fun opts x -> let () = init_color opts.color in let () = CoqworkmgrApi.init !WorkerLoop.async_proofs_worker_priority in - x + opts, x end let print_style_tags opts = @@ -412,7 +442,7 @@ let init_toplevel arglist = 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: @@ -427,14 +457,26 @@ 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 = !toploop_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"; @@ -469,35 +511,33 @@ 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; time = opts.time } 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; - (* Vio compile pass *) - if opts.vio_files <> [] then schedule_vio opts; - (* Vio task pass *) - check_vio_tasks 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 () = diff --git a/toplevel/coqtop.mli b/toplevel/coqtop.mli index 056279bbd0..fcc569ca07 100644 --- a/toplevel/coqtop.mli +++ b/toplevel/coqtop.mli @@ -18,5 +18,6 @@ val init_toplevel : string list -> Vernac.State.t option * Coqargs.coq_cmdopts val start : unit -> unit (* For other toploops *) -val toploop_init : (Coqargs.coq_cmdopts -> string list -> string list) ref +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 |