diff options
Diffstat (limited to 'toplevel/coqtop.ml')
| -rw-r--r-- | toplevel/coqtop.ml | 982 |
1 files changed, 418 insertions, 564 deletions
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index d9f8ed88..943b66f6 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -1,19 +1,15 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Pp -open CErrors -open Util -open Flags -open Names -open Libnames -open States -open Coqinit +open Coqargs let () = at_exit flush_all @@ -34,64 +30,31 @@ let print_header () = Feedback.msg_notice (str "Welcome to Coq " ++ str ver ++ str " (" ++ str rev ++ str ")"); flush_all () -let warning s = with_option Flags.warn Feedback.msg_warning (strbrk s) +let warning s = Flags.(with_option warn Feedback.msg_warning (strbrk s)) -let toploop = ref None +(* 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 color : [`ON | `AUTO | `OFF] ref = ref `AUTO -let set_color = function -| "yes" | "on" -> color := `ON -| "no" | "off" -> color := `OFF -| "auto" -> color := `AUTO -| _ -> prerr_endline ("Error: on/off/auto expected after option color"); exit 1 - -let init_color () = - let has_color = match !color with - | `OFF -> false - | `ON -> true - | `AUTO -> - Terminal.has_style Unix.stdout && - Terminal.has_style Unix.stderr && - (* emacs compilation buffer does not support colors by default, - 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 *) - Feedback.init_color_output () - | Some "" -> - (** No color output *) - () - | Some s -> - (** Overwrite all colors *) - Ppstyle.clear_styles (); - Ppstyle.parse_config s; - Feedback.init_color_output () - end - -let toploop_init = ref begin fun x -> - let () = init_color () in - let () = CoqworkmgrApi.(init !Flags.async_proofs_worker_priority) in - x - end - -let toploop_run = ref (fun () -> +(* 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 - if_verbose warning "Dumpglob cannot be used in interactive mode."; + Flags.if_verbose warning "Dumpglob cannot be used in interactive mode."; Dumpglob.noglob () end; - Coqloop.loop(); + let _ = Coqloop.loop ~time:opts.time ~state in (* Initialise and launch the Ocaml toplevel *) Coqinit.init_ocaml_path(); - Mltop.ocaml_toploop()) + Mltop.ocaml_toploop(); + (* We let the feeder in place for users of Drop *) + Feedback.del_feeder tl_feed -let output_context = ref false +let toploop_run = ref console_toploop_run let memory_stat = ref false - let print_memory_stat () = begin (* -m|--memory from the command-line *) if !memory_stat then @@ -111,151 +74,319 @@ let print_memory_stat () = let _ = at_exit print_memory_stat -let impredicative_set = ref Declarations.PredicativeSet -let set_impredicative_set c = impredicative_set := Declarations.ImpredicativeSet -let set_type_in_type () = - let typing_flags = Environ.typing_flags (Global.env ()) in - Global.set_typing_flags { typing_flags with Declarations.check_universes = false } -let engage () = - Global.set_engagement !impredicative_set - -let set_batch_mode () = batch_mode := true - -let toplevel_default_name = DirPath.make [Id.of_string "Top"] -let toplevel_name = ref (Some toplevel_default_name) -let set_toplevel_name dir = - if DirPath.is_empty dir then error "Need a non empty toplevel module name"; - toplevel_name := Some dir -let unset_toplevel_name () = toplevel_name := None - -let remove_top_ml () = Mltop.remove () - -let warn_deprecated_inputstate = - CWarnings.create ~name:"deprecated-inputstate" ~category:"deprecated" - (fun () -> strbrk "The inputstate option is deprecated and discouraged.") - -let inputstate = ref "" -let set_inputstate s = - warn_deprecated_inputstate (); - inputstate:=s -let inputstate () = - if not (String.is_empty !inputstate) then - let fname = Loadpath.locate_file (CUnix.make_suffix !inputstate ".coq") in - intern_state fname - -let warn_deprecated_outputstate = - CWarnings.create ~name:"deprecated-outputstate" ~category:"deprecated" - (fun () -> - strbrk "The outputstate option is deprecated and discouraged.") - -let outputstate = ref "" -let set_outputstate s = - warn_deprecated_outputstate (); - outputstate:=s -let outputstate () = - if not (String.is_empty !outputstate) then - let fname = CUnix.make_suffix !outputstate ".coq" in - extern_state fname - -let set_include d p implicit = - let p = dirpath_of_string p in - push_include d p implicit - -let load_vernacular_list = ref ([] : (string * bool) list) -let add_load_vernacular verb s = - load_vernacular_list := ((CUnix.make_suffix s ".v"),verb) :: !load_vernacular_list -let load_vernacular () = - List.iter - (fun (s,b) -> - let s = Loadpath.locate_file s in - if !Flags.beautify then - with_option beautify_file (Vernac.load_vernac b) s - else - Vernac.load_vernac b s) - (List.rev !load_vernacular_list) - -let load_vernacular_obj = ref ([] : string list) -let add_vernac_obj s = load_vernacular_obj := s :: !load_vernacular_obj -let load_vernac_obj () = - let map dir = Qualid (Loc.ghost, qualid_of_string dir) in - Vernacentries.vernac_require None None (List.rev_map map !load_vernacular_obj) - -let require_prelude () = - let vo = Envars.coqlib () / "theories/Init/Prelude.vo" in - let vio = Envars.coqlib () / "theories/Init/Prelude.vio" in - let m = - if Sys.file_exists vo then vo else - if Sys.file_exists vio then vio else vo in - Library.require_library_from_dirpath [Coqlib.prelude_module,m] (Some true) - -let require_list = ref ([] : string list) -let add_require s = require_list := s :: !require_list -let require () = - let () = if !load_init then silently require_prelude () in - let map dir = Qualid (Loc.ghost, qualid_of_string dir) in - Vernacentries.vernac_require None (Some false) (List.rev_map map !require_list) - -let add_compat_require v = - match v with - | Flags.V8_4 -> add_require "Coq.Compat.Coq84" - | Flags.V8_5 -> add_require "Coq.Compat.Coq85" - | _ -> () - -let compile_list = ref ([] : (bool * string) list) - -let glob_opt = ref false - -let add_compile verbose s = - set_batch_mode (); - Flags.make_silent true; - if not !glob_opt then Dumpglob.dump_to_dotglob (); - (** make the file name explicit; needed not to break up Coq loadpath stuff. *) - let s = - let open Filename in - if is_implicit s - then concat current_dir_name s - else s +(******************************************************************************) +(* Input/Output State *) +(******************************************************************************) +let inputstate opts = + Option.iter (fun istate_file -> + let fname = Loadpath.locate_file (CUnix.make_suffix istate_file ".coq") in + States.intern_state fname) opts.inputstate + +let outputstate opts = + Option.iter (fun ostate_file -> + let fname = CUnix.make_suffix ostate_file ".coq" in + States.extern_state fname) opts.outputstate + +(******************************************************************************) +(* Interactive Load File Simulation *) +(******************************************************************************) +let load_vernacular opts ~state = + List.fold_left + (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 + 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 + else begin + Flags.if_verbose Feedback.msg_info (str"Skipping rcfile loading."); + state + end in + + load_vernacular opts ~state + +(******************************************************************************) +(* Startup LoadPath and Modules *) +(******************************************************************************) +(* prelude_data == From Coq Require Export Prelude. *) +let prelude_data = "Prelude", Some "Coq", Some true + +let require_libs opts = + if opts.load_init then prelude_data :: opts.vo_requires else opts.vo_requires + +let cmdline_load_path opts = + let open Mltop in + (* loadpaths given by options -Q and -R *) + List.map + (fun (unix_path, coq_path, implicit) -> + { recursive = true; + path_spec = VoPath { unix_path; coq_path; has_ml = Mltop.AddNoML; implicit } }) + (List.rev opts.vo_includes) @ + + (* additional ml directories, given with option -I *) + List.map (fun s -> {recursive = false; path_spec = MlPath s}) (List.rev opts.ml_includes) + +let build_load_path opts = + Coqinit.libs_init_load_path ~load_init:opts.load_init @ + cmdline_load_path opts + +(******************************************************************************) +(* Fatal Errors *) +(******************************************************************************) + +(** Prints info which is either an error or an anomaly and then exits + with the appropriate error code *) +let fatal_error msg = + Topfmt.std_logger Feedback.Error msg; + flush_all (); + exit 1 + +let fatal_error_exn ?extra exn = + Topfmt.print_err_exn ?extra exn; + flush_all (); + let exit_code = + if CErrors.(is_anomaly exn || not (handled exn)) then 129 else 1 in - compile_list := (verbose,s) :: !compile_list + exit exit_code + +(******************************************************************************) +(* File Compilation *) +(******************************************************************************) +let warn_file_no_extension = + CWarnings.create ~name:"file-no-extension" ~category:"filesystem" + (fun (f,ext) -> + str "File \"" ++ str f ++ + strbrk "\" has been implicitly expanded to \"" ++ + str f ++ str ext ++ str "\"") + +let ensure_ext ext f = + if Filename.check_suffix f ext then f + else begin + warn_file_no_extension (f,ext); + f ^ ext + end -let compile_file (v,f) = +let chop_extension f = + try Filename.chop_extension f with _ -> f + +let ensure_bname src tgt = + let src, tgt = Filename.basename src, Filename.basename tgt in + let src, tgt = chop_extension src, chop_extension tgt in + if src <> tgt then + fatal_error (str "Source and target file names must coincide, directories can differ" ++ fnl () ++ + str "Source: " ++ str src ++ fnl () ++ + str "Target: " ++ str tgt) + +let ensure ext src tgt = ensure_bname src tgt; ensure_ext ext tgt + +let ensure_v v = ensure ".v" v v +let ensure_vo v vo = ensure ".vo" v vo +let ensure_vio v vio = ensure ".vio" v vio + +let ensure_exists f = + if not (Sys.file_exists f) then + 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 open Vernac.State in + let check_pending_proofs () = + let pfs = Proof_global.get_all_proof_names () in + if not (CList.is_empty pfs) then + fatal_error (str "There are pending proofs: " + ++ (pfs + |> List.rev + |> prlist_with_sep pr_comma Names.Id.print) + ++ str ".") + in + let iload_path = build_load_path opts in + let require_libs = require_libs opts in + let stm_options = opts.stm_flags in + match opts.compilation_mode with + | BuildVo -> + Flags.record_aux_file := true; + let long_f_dot_v = ensure_v f_in in + ensure_exists long_f_dot_v; + let long_f_dot_vo = + match f_out with + | None -> long_f_dot_v ^ "o" + | Some f -> ensure_vo long_f_dot_v f in + + let doc, sid = Stm.(new_doc + { doc_type = VoDoc long_f_dot_vo; + iload_path; require_libs; stm_options; + }) in + + let state = { doc; sid; proof = None } in + let state = load_init_vernaculars 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) + ~v_file:long_f_dot_v); + 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 _doc = Stm.join ~doc:state.doc in + let wall_clock2 = Unix.gettimeofday () in + check_pending_proofs (); + Library.save_library_to ldir long_f_dot_vo (Global.opaque_tables ()); + Aux_file.record_in_aux_at "vo_compile_time" + (Printf.sprintf "%.3f" (wall_clock2 -. wall_clock1)); + Aux_file.stop_aux_file (); + Dumpglob.end_dump_glob () + + | BuildVio -> + Flags.record_aux_file := false; + Dumpglob.noglob (); + + let long_f_dot_v = ensure_v f_in in + ensure_exists long_f_dot_v; + + let long_f_dot_vio = + match f_out with + | None -> long_f_dot_v ^ "io" + | Some f -> ensure_vio long_f_dot_v f in + + (* We need to disable error resiliency, otherwise some errors + will be ignored in batch mode. c.f. #6707 + + This is not necessary in the vo case as it fully checks the + document anyways. *) + let stm_options = let open Stm.AsyncOpts in + { stm_options with + async_proofs_cmd_error_resilience = false; + async_proofs_tac_error_resilience = `None; + } in + + let doc, sid = Stm.(new_doc + { doc_type = VioDoc long_f_dot_vio; + iload_path; require_libs; stm_options; + }) in + + let state = { doc; sid; proof = None } in + let state = load_init_vernaculars 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 doc = Stm.finish ~doc:state.doc in + check_pending_proofs (); + let _doc = Stm.snapshot_vio ~doc ldir long_f_dot_vio in + Stm.reset_task_queue () + + | Vio2Vo -> + let open Filename in + Flags.record_aux_file := false; + Dumpglob.noglob (); + let f = if check_suffix f_in ".vio" then chop_extension f_in else f_in in + let lfdv, sum, lib, univs, disch, tasks, proofs = Library.load_library_todo f in + 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 = + ignore(CoqworkmgrApi.get 1); + compile opts ~echo ~f_in ~f_out; + CoqworkmgrApi.giveback 1 + +let compile_file opts (f_in, echo) = + let f_out = opts.compilation_output_name in if !Flags.beautify then - with_option beautify_file (Vernac.compile v) f + Flags.with_option Flags.beautify_file + (fun f_in -> compile opts ~echo ~f_in ~f_out) f_in else - Vernac.compile v f + compile opts ~echo ~f_in ~f_out -let compile_files () = - if !compile_list == [] then () - else - let init_state = States.freeze ~marshallable:`No in - Feedback.(add_feeder debug_feeder); - List.iter (fun vf -> - States.unfreeze init_state; - compile_file vf) - (List.rev !compile_list) +let compile_files opts = + let compile_list = List.rev opts.compile_list in + List.iter (compile_file opts) compile_list -(** Options for proof general *) - -let set_emacs () = - if not (Option.is_empty !toploop) then - error "Flag -emacs is incompatible with a custom toplevel loop"; - Flags.print_emacs := true; - Feedback.(set_logger emacs_logger); - Vernacentries.qed_display_script := false; - color := `OFF - -(** Options for CoqIDE *) +(******************************************************************************) +(* VIO Dispatching *) +(******************************************************************************) +let check_vio_tasks opts = + let rc = + List.fold_left (fun acc t -> Vio_checking.check_vio t && acc) + true (List.rev opts.vio_tasks) in + if not rc then fatal_error Pp.(str "VIO Task Check failed") -let set_ideslave () = - if !Flags.print_emacs then error "Flags -ideslave and -emacs are incompatible"; - toploop := Some "coqidetop"; - Flags.ide_slave := true +(* vio files *) +let schedule_vio opts = + 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 *) +(******************************************************************************) +let init_color color_mode = + let has_color = match color_mode with + | `OFF -> false + | `ON -> true + | `AUTO -> + Terminal.has_style Unix.stdout && + Terminal.has_style Unix.stderr && + (* emacs compilation buffer does not support colors by default, + 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 -(** Options for slaves *) +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 set_toploop name = - if !Flags.print_emacs then error "Flags -toploop and -emacs are incompatible"; - toploop := Some name +let print_style_tags opts = + let () = init_color opts.color in + let tags = Topfmt.dump_tags () in + let iter (t, st) = + let opt = Terminal.eval st ^ t ^ Terminal.reset ^ "\n" in + print_string opt + in + let make (t, st) = + let tags = List.map string_of_int (Terminal.repr st) in + (t ^ "=" ^ String.concat ";" tags) + in + let repr = List.map make tags in + let () = Printf.printf "COQ_COLORS=\"%s\"\n" (String.concat ":" repr) in + let () = List.iter iter tags in + flush_all () (** GC tweaking *) @@ -282,389 +413,112 @@ let init_gc () = Gc.minor_heap_size = 33554432; (** 4M *) Gc.space_overhead = 120} -(*s Parsing of the command line. - We no longer use [Arg.parse], in order to use share [Usage.print_usage] - between coqtop and coqc. *) - -let usage () = - Envars.set_coqlib CErrors.error; - init_load_path (); - if !batch_mode 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 - -let print_style_tags () = - let () = init_color () in - let tags = Ppstyle.dump () in - let iter (t, st) = - let st = match st with Some st -> st | None -> Terminal.make () in - let opt = - Terminal.eval st ^ - String.concat "." (Ppstyle.repr t) ^ - Terminal.reset ^ "\n" - in - print_string opt - in - let make (t, st) = match st with - | None -> None - | Some st -> - let tags = List.map string_of_int (Terminal.repr st) in - let t = String.concat "." (Ppstyle.repr t) in - Some (t ^ "=" ^ String.concat ";" tags) - in - let repr = List.map_filter make tags in - let () = Printf.printf "COQ_COLORS=\"%s\"\n" (String.concat ":" repr) in - let () = List.iter iter tags in - flush_all () - -let error_missing_arg s = - prerr_endline ("Error: extra argument expected after option "^s); - prerr_endline "See -help for the syntax of supported options"; - exit 1 - -let filter_opts = ref false -let exitcode () = if !filter_opts then 2 else 0 - -let print_where = ref false -let print_config = ref false -let print_tags = ref false - -let get_priority opt s = - try Flags.priority_of_string s - with Invalid_argument _ -> - prerr_endline ("Error: low/high expected after "^opt); exit 1 - -let get_async_proofs_mode opt = function - | "no" | "off" -> Flags.APoff - | "yes" | "on" -> Flags.APon - | "lazy" -> Flags.APonLazy - | _ -> prerr_endline ("Error: on/off/lazy expected after "^opt); exit 1 - -let get_cache opt = function - | "force" -> Some Flags.Force - | _ -> prerr_endline ("Error: force expected after "^opt); exit 1 - - -let set_worker_id opt s = - assert (s <> "master"); - Flags.async_proofs_worker_id := s - -let get_bool opt = function - | "yes" | "on" -> true - | "no" | "off" -> false - | _ -> prerr_endline ("Error: yes/no expected after option "^opt); exit 1 - -let get_int opt n = - try int_of_string n - with Failure _ -> - prerr_endline ("Error: integer expected after option "^opt); exit 1 - -let get_float opt n = - try float_of_string n - with Failure _ -> - prerr_endline ("Error: float expected after option "^opt); exit 1 - -let get_host_port opt s = - match CString.split ':' s with - | [host; portr; portw] -> - Some (Spawned.Socket(host, int_of_string portr, int_of_string portw)) - | ["stdfds"] -> Some Spawned.AnonPipe - | _ -> - prerr_endline ("Error: host:portr:portw or stdfds expected after option "^opt); - exit 1 - -let get_error_resilience opt = function - | "on" | "all" | "yes" -> `All - | "off" | "no" -> `None - | s -> `Only (String.split ',' s) - -let get_task_list s = List.map int_of_string (Str.split (Str.regexp ",") s) - -let vio_tasks = ref [] - -let add_vio_task f = - set_batch_mode (); - Flags.make_silent true; - vio_tasks := f :: !vio_tasks - -let check_vio_tasks () = - let rc = - List.fold_left (fun acc t -> Vio_checking.check_vio t && acc) - true (List.rev !vio_tasks) in - if not rc then exit 1 - -let vio_files = ref [] -let vio_files_j = ref 0 -let vio_checking = ref false -let add_vio_file f = - set_batch_mode (); - Flags.make_silent true; - vio_files := f :: !vio_files - -let set_vio_checking_j opt j = - try vio_files_j := int_of_string j - with Failure _ -> - prerr_endline ("The first argument of " ^ opt ^ " must the number"); - prerr_endline "of concurrent workers to be used (a positive integer)."; - prerr_endline "Makefiles generated by coq_makefile should be called"; - prerr_endline "setting the J variable like in 'make vio2vo J=3'"; - exit 1 - -let is_not_dash_option = function - | Some f when String.length f > 0 && f.[0] <> '-' -> true - | _ -> false - -let schedule_vio_checking () = - if !vio_files <> [] && !vio_checking then - Vio_checking.schedule_vio_checking !vio_files_j !vio_files -let schedule_vio_compilation () = - if !vio_files <> [] && not !vio_checking then - Vio_checking.schedule_vio_compilation !vio_files_j !vio_files - -let get_native_name s = - (* We ignore even critical errors because this mode has to be super silent *) - try - String.concat "/" [Filename.dirname s; - Nativelib.output_dir; Library.native_name_from_filename s] - with _ -> "" - -let parse_args arglist = - let args = ref arglist in - let extras = ref [] in - let rec parse () = match !args with - | [] -> List.rev !extras - | opt :: rem -> - args := rem; - let next () = match !args with - | x::rem -> args := rem; x - | [] -> error_missing_arg opt - in - let peek_next () = match !args with - | x::_ -> Some x - | [] -> None - in - begin match opt with - - (* Complex options with many args *) - |"-I"|"-include" -> - begin match rem with - | d :: rem -> push_ml_include d; args := rem - | [] -> error_missing_arg opt - end - |"-Q" -> - begin match rem with - | d :: p :: rem -> set_include d p false; args := rem - | _ -> error_missing_arg opt - end - |"-R" -> - begin match rem with - | d :: p :: rem -> set_include d p true; args := rem - | _ -> error_missing_arg opt - end - - (* Options with two arg *) - |"-check-vio-tasks" -> - let tno = get_task_list (next ()) in - let tfile = next () in - add_vio_task (tno,tfile) - |"-schedule-vio-checking" -> - vio_checking := true; - set_vio_checking_j opt (next ()); - add_vio_file (next ()); - while is_not_dash_option (peek_next ()) do add_vio_file (next ()); done - |"-schedule-vio2vo" -> - set_vio_checking_j opt (next ()); - add_vio_file (next ()); - while is_not_dash_option (peek_next ()) do add_vio_file (next ()); done - - (* Options with one arg *) - |"-coqlib" -> Flags.coqlib_spec:=true; Flags.coqlib:=(next ()) - |"-async-proofs" -> - Flags.async_proofs_mode := get_async_proofs_mode opt (next()) - |"-async-proofs-j" -> - Flags.async_proofs_n_workers := (get_int opt (next ())) - |"-async-proofs-cache" -> - Flags.async_proofs_cache := get_cache opt (next ()) - |"-async-proofs-tac-j" -> - Flags.async_proofs_n_tacworkers := (get_int opt (next ())) - |"-async-proofs-worker-priority" -> - Flags.async_proofs_worker_priority := get_priority opt (next ()) - |"-async-proofs-private-flags" -> - Flags.async_proofs_private_flags := Some (next ()); - |"-async-proofs-tactic-error-resilience" -> - Flags.async_proofs_tac_error_resilience := get_error_resilience opt (next ()) - |"-async-proofs-command-error-resilience" -> - Flags.async_proofs_cmd_error_resilience := get_bool opt (next ()) - |"-async-proofs-delegation-threshold" -> - Flags.async_proofs_delegation_threshold:= get_float opt (next ()) - |"-worker-id" -> set_worker_id opt (next ()) - |"-compat" -> let v = get_compat_version (next ()) in Flags.compat_version := v; add_compat_require v - |"-compile" -> add_compile false (next ()) - |"-compile-verbose" -> add_compile true (next ()) - |"-dump-glob" -> Dumpglob.dump_into_file (next ()); glob_opt := true - |"-feedback-glob" -> Dumpglob.feedback_glob () - |"-exclude-dir" -> System.exclude_directory (next ()) - |"-init-file" -> set_rcfile (next ()) - |"-inputstate"|"-is" -> set_inputstate (next ()) - |"-load-ml-object" -> Mltop.dir_ml_load (next ()) - |"-load-ml-source" -> Mltop.dir_ml_use (next ()) - |"-load-vernac-object" -> add_vernac_obj (next ()) - |"-load-vernac-source"|"-l" -> add_load_vernacular false (next ()) - |"-load-vernac-source-verbose"|"-lv" -> add_load_vernacular true (next ()) - |"-outputstate" -> set_outputstate (next ()) - |"-print-mod-uid" -> let s = String.concat " " (List.map get_native_name rem) in print_endline s; exit 0 - |"-profile-ltac-cutoff" -> Flags.profile_ltac := true; Flags.profile_ltac_cutoff := get_float opt (next ()) - |"-require" -> add_require (next ()) - |"-top" -> set_toplevel_name (dirpath_of_string (next ())) - |"-with-geoproof" -> Coq_config.with_geoproof := get_bool opt (next ()) - |"-main-channel" -> Spawned.main_channel := get_host_port opt (next()) - |"-control-channel" -> Spawned.control_channel := get_host_port opt (next()) - |"-vio2vo" -> add_compile false (next ()); Flags.compilation_mode := Vio2Vo - |"-toploop" -> set_toploop (next ()) - |"-w" | "-W" -> CWarnings.set_flags (CWarnings.normalize_flags_string (next ())) - |"-o" -> Flags.compilation_output_name := Some (next()) - - (* Options with zero arg *) - |"-async-queries-always-delegate" - |"-async-proofs-always-delegate" - |"-async-proofs-full" -> - Flags.async_proofs_full := true; - |"-async-proofs-never-reopen-branch" -> - Flags.async_proofs_never_reopen_branch := true; - |"-batch" -> set_batch_mode () - |"-test-mode" -> test_mode := true - |"-beautify" -> beautify := true - |"-boot" -> boot := true; no_load_rc () - |"-bt" -> Backtrace.record_backtrace true - |"-color" -> set_color (next ()) - |"-config"|"--config" -> print_config := true - |"-debug" -> set_debug () - |"-emacs" -> set_emacs () - |"-filteropts" -> filter_opts := true - |"-h"|"-H"|"-?"|"-help"|"--help" -> usage () - |"-ideslave" -> set_ideslave () - |"-impredicative-set" -> set_impredicative_set () - |"-indices-matter" -> Indtypes.enforce_indices_matter () - |"-just-parsing" -> warning "-just-parsing option has been removed in 8.6" - |"-m"|"--memory" -> memory_stat := true - |"-noinit"|"-nois" -> load_init := false - |"-no-glob"|"-noglob" -> Dumpglob.noglob (); glob_opt := true - |"-native-compiler" -> - if Coq_config.no_native_compiler then - warning "Native compilation was disabled at configure time." - else native_compiler := true - |"-notop" -> unset_toplevel_name () - |"-output-context" -> output_context := true - |"-profile-ltac" -> Flags.profile_ltac := true - |"-q" -> no_load_rc () - |"-quiet"|"-silent" -> Flags.make_silent true; Flags.make_warn false - |"-quick" -> Flags.compilation_mode := BuildVio - |"-list-tags" -> print_tags := true - |"-time" -> Flags.time := true - |"-type-in-type" -> set_type_in_type () - |"-unicode" -> add_require "Utf8_core" - |"-v"|"--version" -> Usage.version (exitcode ()) - |"--print-version" -> Usage.machine_readable_version (exitcode ()) - |"-where" -> print_where := true - |"-xml" -> Flags.xml_export := true - - (* Deprecated options *) - |"-byte" -> warning "option -byte deprecated, call with .byte suffix" - |"-opt" -> warning "option -opt deprecated, call with .opt suffix" - |"-full" -> warning "option -full deprecated" - |"-notactics" -> warning "Obsolete option \"-notactics\"."; remove_top_ml () - |"-emacs-U" -> - warning "Obsolete option \"-emacs-U\", use -emacs instead."; set_emacs () - |"-v7" -> error "This version of Coq does not support v7 syntax" - |"-v8" -> warning "Obsolete option \"-v8\"." - |"-lazy-load-proofs" -> warning "Obsolete option \"-lazy-load-proofs\"." - |"-dont-load-proofs" -> warning "Obsolete option \"-dont-load-proofs\"." - |"-force-load-proofs" -> warning "Obsolete option \"-force-load-proofs\"." - |"-unsafe" -> warning "Obsolete option \"-unsafe\"."; ignore (next ()) - |"-quality" -> warning "Obsolete option \"-quality\"." - - (* Unknown option *) - | s -> extras := s :: !extras - end; - parse () - in - try - parse () - with - | UserError(_, s) as e -> - if is_empty s then exit 1 - else fatal_error (CErrors.print e) false - | any -> fatal_error (CErrors.print any) (CErrors.is_anomaly any) - +(** Main init routine *) let init_toplevel 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 Lib.init(); - (* Default Proofb Mode starts with an alternative default. *) - Goptions.set_string_option_value ["Default";"Proof";"Mode"] "Classic"; - begin + + (* Coq's init process, phase 2: + Basic Coq environment, load-path, plugins. + *) + let res = begin try - let extras = parse_args arglist in + let opts,extras = parse_args arglist in + memory_stat := opts.memory_stat; + (* If we have been spawned by the Spawn module, this has to be done * early since the master waits us to connect back *) Spawned.init_channels (); - Envars.set_coqlib CErrors.error; - if !print_where then (print_endline(Envars.coqlib ()); exit(exitcode ())); - if !print_config then (Usage.print_config (); exit (exitcode ())); - if !print_tags then (print_style_tags (); exit (exitcode ())); - if !filter_opts then (print_string (String.concat "\n" extras); exit 0); - init_load_path (); - Option.iter Mltop.load_ml_object_raw !toploop; - let extras = !toploop_init extras in - if not (List.is_empty extras) then begin + 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); + 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 + 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; - if_verbose print_header (); - inputstate (); + Flags.if_verbose print_header (); Mltop.init_known_plugins (); - engage (); - if (not !batch_mode || List.is_empty !compile_list) - && Global.env_is_initial () - then Option.iter Declaremods.start_library !toplevel_name; - init_library_roots (); - load_vernac_obj (); - require (); - Stm.init (); - load_rcfile(); - load_vernacular (); - compile_files (); - schedule_vio_checking (); - schedule_vio_compilation (); - check_vio_tasks (); - outputstate () + Global.set_engagement opts.impredicative_set; + + (* Allow the user to load an arbitrary state here *) + inputstate opts; + + (* This state will be shared by all the documents *) + Stm.init_core (); + + (* Coq init process, phase 3: Stm initialization, backtracking state. + + It is essential that the module system is in a consistent + state before we take the first snapshot. This was not + guaranteed in the past, but now is thanks to the STM API. + + We split the codepath here depending whether coqtop is called + in interactive mode or not. *) + + (* The condition for starting the interactive mode is a bit + convoluted, we should really refactor batch/compilation_mode + more. *) + if (not opts.batch_mode + || CList.(is_empty opts.compile_list && is_empty opts.vio_files && is_empty opts.vio_tasks)) + (* Interactive *) + then begin + 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 + (* 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 + end; with any -> - let any = CErrors.push any in flush_all(); - let msg = - if !batch_mode then mt () - else str "Error during initialization:" ++ fnl () - in - let is_anomaly e = CErrors.is_anomaly e || not (CErrors.handled e) in - fatal_error (msg ++ Coqloop.print_toplevel_error any) (is_anomaly (fst any)) - end; - if !batch_mode then begin - flush_all(); - if !output_context then - Feedback.msg_notice (with_option raw_print Prettyp.print_full_pure_context () ++ fnl ()); - Profile.print_profile (); - exit 0 - end + let extra = Some (str "Error during initialization: ") in + fatal_error_exn ?extra any + end in + Feedback.del_feeder init_feeder; + res let start () = - let () = init_toplevel (List.tl (Array.to_list Sys.argv)) in - (* In batch mode, Coqtop has already exited at this point. In interactive one, - dump glob is nothing but garbage ... *) - !toploop_run (); - exit 1 - -(* [Coqtop.start] will be called by the code produced by coqmktop *) + match init_toplevel (List.tl (Array.to_list Sys.argv)) with + (* Batch mode *) + | Some state, opts when not opts.batch_mode -> + !toploop_run opts ~state; + exit 1 + | _ , opts -> + flush_all(); + if opts.output_context then begin + let sigma, env = Pfedit.get_current_context () in + Feedback.msg_notice (Flags.(with_option raw_print (Prettyp.print_full_pure_context env) sigma) ++ fnl ()) + end; + CProfile.print_profile (); + exit 0 |