diff options
Diffstat (limited to 'toplevel/coqtop.ml')
| -rw-r--r-- | toplevel/coqtop.ml | 183 |
1 files changed, 100 insertions, 83 deletions
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index afd4ef40..d9f8ed88 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -7,9 +7,8 @@ (************************************************************************) open Pp -open Errors +open CErrors open Util -open System open Flags open Names open Libnames @@ -27,15 +26,15 @@ let get_version_date () = let rev = input_line ch in let () = close_in ch in (ver,rev) - with e when Errors.noncritical e -> + with e when CErrors.noncritical e -> (Coq_config.version,Coq_config.date) let print_header () = let (ver,rev) = get_version_date () in - ppnl (str "Welcome to Coq " ++ str ver ++ str " (" ++ str rev ++ str ")"); - pp_flush () + Feedback.msg_notice (str "Welcome to Coq " ++ str ver ++ str " (" ++ str rev ++ str ")"); + flush_all () -let warning s = msg_warning (strbrk s) +let warning s = with_option Flags.warn Feedback.msg_warning (strbrk s) let toploop = ref None @@ -55,14 +54,14 @@ let init_color () = Terminal.has_style Unix.stderr && (* emacs compilation buffer does not support colors by default, its TERM variable is set to "dumb". *) - Unix.getenv "TERM" <> "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 *) - Ppstyle.init_color_output () + Feedback.init_color_output () | Some "" -> (** No color output *) () @@ -70,7 +69,7 @@ let init_color () = (** Overwrite all colors *) Ppstyle.clear_styles (); Ppstyle.parse_config s; - Ppstyle.init_color_output () + Feedback.init_color_output () end let toploop_init = ref begin fun x -> @@ -96,8 +95,8 @@ let memory_stat = ref false let print_memory_stat () = begin (* -m|--memory from the command-line *) if !memory_stat then - ppnl - (str "total heap size = " ++ int (CObj.heap_size_kb ()) ++ str " kbytes"); + Feedback.msg_notice + (str "total heap size = " ++ int (CObj.heap_size_kb ()) ++ str " kbytes" ++ fnl ()); end; begin (* operf-macro interface: @@ -114,23 +113,14 @@ let _ = at_exit print_memory_stat let impredicative_set = ref Declarations.PredicativeSet let set_impredicative_set c = impredicative_set := Declarations.ImpredicativeSet -let type_in_type = ref Declarations.StratifiedType -let set_type_in_type () = type_in_type := Declarations.TypeInType +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,!type_in_type) + Global.set_engagement !impredicative_set let set_batch_mode () = batch_mode := true -let user_warning = ref false -(** User explicitly set warning *) - -let set_warning p = - let () = user_warning := true in - match p with - | "all" -> make_warn true - | "none" -> make_warn false - | _ -> prerr_endline ("Error: all/none expected after option w"); exit 1 - let toplevel_default_name = DirPath.make [Id.of_string "Top"] let toplevel_name = ref (Some toplevel_default_name) let set_toplevel_name dir = @@ -140,18 +130,27 @@ 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 = - let () = msg_warning (str "The inputstate option is deprecated and discouraged.") in + 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 = - let () = msg_warning (str "The outputstate option is deprecated and discouraged.") in + warn_deprecated_outputstate (); outputstate:=s let outputstate () = if not (String.is_empty !outputstate) then @@ -169,7 +168,7 @@ let load_vernacular () = List.iter (fun (s,b) -> let s = Loadpath.locate_file s in - if Flags.do_beautify () then + if !Flags.beautify then with_option beautify_file (Vernac.load_vernac b) s else Vernac.load_vernac b s) @@ -199,6 +198,7 @@ let require () = 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) @@ -219,33 +219,44 @@ let add_compile verbose s = compile_list := (verbose,s) :: !compile_list let compile_file (v,f) = - if Flags.do_beautify () then + if !Flags.beautify then with_option beautify_file (Vernac.compile v) f else Vernac.compile v f let compile_files () = - match !compile_list with - | [] -> () - | [vf] -> compile_file vf (* One compilation : no need to save init state *) - | l -> - let init_state = States.freeze ~marshallable:`No in - let coqdoc_init_state = Lexer.location_table () in - List.iter - (fun vf -> - States.unfreeze init_state; - Lexer.restore_location_table coqdoc_init_state; - compile_file vf) - (List.rev l) + 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) (** 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; - Pp.make_pp_emacs (); + Feedback.(set_logger emacs_logger); Vernacentries.qed_display_script := false; color := `OFF +(** Options for CoqIDE *) + +let set_ideslave () = + if !Flags.print_emacs then error "Flags -ideslave and -emacs are incompatible"; + toploop := Some "coqidetop"; + Flags.ide_slave := true + +(** Options for slaves *) + +let set_toploop name = + if !Flags.print_emacs then error "Flags -toploop and -emacs are incompatible"; + toploop := Some name + (** GC tweaking *) (** Coq is a heavy user of persistent data structures and symbolic ASTs, so the @@ -257,25 +268,26 @@ let set_emacs () = *) let init_gc () = - let param = - try ignore (Sys.getenv "OCAMLRUNPARAM"); true - with Not_found -> false - in - let control = Gc.get () in - let tweaked_control = { control with - Gc.minor_heap_size = 33554432; (** 4M *) -(* Gc.major_heap_increment = 268435456; (** 32M *) *) - Gc.space_overhead = 120; - } in - if param then () - else Gc.set tweaked_control + try + (* OCAMLRUNPARAM environment variable is set. + * In that case, we let ocamlrun to use the values provided by the user. + *) + ignore (Sys.getenv "OCAMLRUNPARAM") + + with Not_found -> + (* OCAMLRUNPARAM environment variable is not set. + * In this case, we put in place our preferred configuration. + *) + Gc.set { (Gc.get ()) with + 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 Errors.error; + Envars.set_coqlib CErrors.error; init_load_path (); if !batch_mode then Usage.print_usage_coqc () else begin @@ -316,9 +328,6 @@ let error_missing_arg s = let filter_opts = ref false let exitcode () = if !filter_opts then 2 else 0 -let verb_compat_ntn = ref false -let no_compat_ntn = ref false - let print_where = ref false let print_config = ref false let print_tags = ref false @@ -353,15 +362,25 @@ let get_int opt 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:port or stdfds expected after option "^opt); + 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 [] @@ -442,10 +461,6 @@ let parse_args arglist = end |"-R" -> begin match rem with - | d :: "-as" :: [] -> error_missing_arg opt - | d :: "-as" :: p :: rem -> - warning "option -R * -as * deprecated, remove the -as"; - set_include d p true; args := rem | d :: p :: rem -> set_include d p true; args := rem | _ -> error_missing_arg opt end @@ -479,13 +494,19 @@ let parse_args arglist = 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" -> exclude_search_in_dirname (next ()) + |"-exclude-dir" -> System.exclude_directory (next ()) |"-init-file" -> set_rcfile (next ()) |"-inputstate"|"-is" -> set_inputstate (next ()) |"-load-ml-object" -> Mltop.dir_ml_load (next ()) @@ -495,14 +516,16 @@ let parse_args arglist = |"-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" -> toploop := Some (next ()) - |"-w" -> set_warning (next ()) + |"-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" @@ -513,7 +536,7 @@ let parse_args arglist = Flags.async_proofs_never_reopen_branch := true; |"-batch" -> set_batch_mode () |"-test-mode" -> test_mode := true - |"-beautify" -> make_beautify true + |"-beautify" -> beautify := true |"-boot" -> boot := true; no_load_rc () |"-bt" -> Backtrace.record_backtrace true |"-color" -> set_color (next ()) @@ -522,13 +545,12 @@ let parse_args arglist = |"-emacs" -> set_emacs () |"-filteropts" -> filter_opts := true |"-h"|"-H"|"-?"|"-help"|"--help" -> usage () - |"-ideslave" -> toploop := Some "coqidetop"; Flags.ide_slave := true + |"-ideslave" -> set_ideslave () |"-impredicative-set" -> set_impredicative_set () |"-indices-matter" -> Indtypes.enforce_indices_matter () - |"-just-parsing" -> Vernac.just_parsing := true + |"-just-parsing" -> warning "-just-parsing option has been removed in 8.6" |"-m"|"--memory" -> memory_stat := true |"-noinit"|"-nois" -> load_init := false - |"-no-compat-notations" -> no_compat_ntn := true |"-no-glob"|"-noglob" -> Dumpglob.noglob (); glob_opt := true |"-native-compiler" -> if Coq_config.no_native_compiler then @@ -536,6 +558,7 @@ let parse_args arglist = 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 @@ -544,7 +567,7 @@ let parse_args arglist = |"-type-in-type" -> set_type_in_type () |"-unicode" -> add_require "Utf8_core" |"-v"|"--version" -> Usage.version (exitcode ()) - |"-verbose-compat-notations" -> verb_compat_ntn := true + |"--print-version" -> Usage.machine_readable_version (exitcode ()) |"-where" -> print_where := true |"-xml" -> Flags.xml_export := true @@ -573,10 +596,10 @@ let parse_args arglist = with | UserError(_, s) as e -> if is_empty s then exit 1 - else fatal_error (Errors.print e) false - | any -> fatal_error (Errors.print any) (Errors.is_anomaly any) + else fatal_error (CErrors.print e) false + | any -> fatal_error (CErrors.print any) (CErrors.is_anomaly any) -let init arglist = +let init_toplevel arglist = init_gc (); Sys.catch_break false; (* Ctrl-C is fatal during the initialisation *) Lib.init(); @@ -588,7 +611,7 @@ let init arglist = (* 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 Errors.error; + 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 ())); @@ -605,9 +628,6 @@ let init arglist = inputstate (); Mltop.init_known_plugins (); engage (); - (* Be careful to set these variables after the inputstate *) - Syntax_def.set_verbose_compat_notations !verb_compat_ntn; - Syntax_def.set_compat_notations (not !no_compat_ntn); if (not !batch_mode || List.is_empty !compile_list) && Global.env_is_initial () then Option.iter Declaremods.start_library !toplevel_name; @@ -623,30 +643,27 @@ let init arglist = check_vio_tasks (); outputstate () with any -> - let any = Errors.push any in + 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 = Errors.is_anomaly e || not (Errors.handled e) 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 - Pp.ppnl (with_option raw_print Prettyp.print_full_pure_context ()); + Feedback.msg_notice (with_option raw_print Prettyp.print_full_pure_context () ++ fnl ()); Profile.print_profile (); exit 0 end -let init_toplevel = init - 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 ... *) - if not !user_warning then make_warn true; !toploop_run (); exit 1 |