From 2280477a96e19ba5060de2d48dcc8fd7c8079d22 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 13 Nov 2015 11:31:34 +0100 Subject: Imported Upstream version 8.5~beta3+dfsg --- toplevel/coqtop.ml | 125 +++++++++++++++++++++++++++++++++-------------------- 1 file changed, 77 insertions(+), 48 deletions(-) (limited to 'toplevel/coqtop.ml') diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index e9e86953..72966a4a 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -20,12 +20,6 @@ let () = at_exit flush_all let ( / ) = Filename.concat -let fatal_error info anomaly = - let msg = info ++ fnl () in - pp_with ~pp_tag:Ppstyle.pp_tag !Pp_control.err_ft msg; - flush_all (); - exit (if anomaly then 129 else 1) - let get_version_date () = try let ch = open_in (Envars.coqlib () / "revision") in @@ -38,7 +32,7 @@ let get_version_date () = let print_header () = let (ver,rev) = get_version_date () in - ppnl (str ("Welcome to Coq "^ver^" ("^rev^")")); + ppnl (str "Welcome to Coq " ++ str ver ++ str " (" ++ str rev ++ str ")"); pp_flush () let warning s = msg_warning (strbrk s) @@ -47,8 +41,8 @@ let toploop = ref None let color : [`ON | `AUTO | `OFF] ref = ref `AUTO let set_color = function -| "on" -> color := `ON -| "off" -> color := `OFF +| "yes" | "on" -> color := `ON +| "no" | "off" -> color := `OFF | "auto" -> color := `AUTO | _ -> prerr_endline ("Error: on/off/auto expected after option color"); exit 1 @@ -58,7 +52,10 @@ let init_color () = | `ON -> true | `AUTO -> Terminal.has_style Unix.stdout && - Terminal.has_style Unix.stderr + 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" in if has_color then begin let colors = try Some (Sys.getenv "COQ_COLORS") with Not_found -> None in @@ -97,23 +94,43 @@ let output_context = ref false let memory_stat = ref false let print_memory_stat () = - if !memory_stat then + begin (* -m|--memory from the command-line *) + if !memory_stat then ppnl - (str "total heap size = " ++ int (CObj.heap_size_kb ()) ++ str " kbytes") + (str "total heap size = " ++ int (CObj.heap_size_kb ()) ++ str " kbytes"); + end; + begin + (* operf-macro interface: + https://github.com/OCamlPro/operf-macro *) + try + let fn = Sys.getenv "OCAML_GC_STATS" in + let oc = open_out fn in + Gc.print_stat oc; + close_out oc + with _ -> () + end let _ = at_exit print_memory_stat -let engagement = ref None -let set_engagement c = engagement := Some c +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 engage () = - match !engagement with Some c -> Global.set_engagement c | None -> () - -let type_in_type = ref false -let set_type_in_type () = type_in_type := true -let set_hierarchy () = if !type_in_type then Global.set_type_in_type () + Global.set_engagement (!impredicative_set,!type_in_type) 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 = @@ -127,13 +144,19 @@ let inputstate = ref "" let set_inputstate s = let () = msg_warning (str "The inputstate option is deprecated and discouraged.") in inputstate:=s -let inputstate () = if not (String.is_empty !inputstate) then intern_state !inputstate +let inputstate () = + if not (String.is_empty !inputstate) then + let fname = Loadpath.locate_file (CUnix.make_suffix !inputstate ".coq") in + intern_state fname let outputstate = ref "" let set_outputstate s = let () = msg_warning (str "The outputstate option is deprecated and discouraged.") in outputstate:=s -let outputstate () = if not (String.is_empty !outputstate) then extern_state !outputstate +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 @@ -145,6 +168,7 @@ let add_load_vernacular verb s = let load_vernacular () = List.iter (fun (s,b) -> + let s = Loadpath.locate_file s in if Flags.do_beautify () then with_option beautify_file (Vernac.load_vernac b) s else @@ -154,8 +178,8 @@ let load_vernacular () = let load_vernacular_obj = ref ([] : string list) let add_vernac_obj s = load_vernacular_obj := s :: !load_vernacular_obj let load_vernac_obj () = - List.iter (fun f -> Library.require_library_from_file None f None) - (List.rev !load_vernacular_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 @@ -168,9 +192,9 @@ let require_prelude () = let require_list = ref ([] : string list) let add_require s = require_list := s :: !require_list let require () = - if !load_init then silently require_prelude (); - List.iter (fun s -> Library.require_library_from_file None s (Some false)) - (List.rev !require_list) + 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 compile_list = ref ([] : (bool * string) list) @@ -209,15 +233,6 @@ let compile_files () = compile_file vf) (List.rev l) -(*s options for the virtual machine *) - -let boxed_val = ref false -let use_vm = ref false - -let set_vm_opt () = - Vm.set_transp_values (not !boxed_val); - Vconv.set_use_vm !use_vm - (** Options for proof general *) let set_emacs () = @@ -276,7 +291,16 @@ let print_style_tags () = in print_string opt in - List.iter iter tags; + 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 = @@ -300,8 +324,8 @@ let get_priority opt s = prerr_endline ("Error: low/high expected after "^opt); exit 1 let get_async_proofs_mode opt = function - | "off" -> Flags.APoff - | "on" -> Flags.APon + | "no" | "off" -> Flags.APoff + | "yes" | "on" -> Flags.APon | "lazy" -> Flags.APonLazy | _ -> prerr_endline ("Error: on/off/lazy expected after "^opt); exit 1 @@ -315,8 +339,8 @@ let set_worker_id opt s = Flags.async_proofs_worker_id := s let get_bool opt = function - | "yes" -> true - | "no" -> false + | "yes" | "on" -> true + | "no" | "off" -> false | _ -> prerr_endline ("Error: yes/no expected after option "^opt); exit 1 let get_int opt n = @@ -326,7 +350,8 @@ let get_int opt n = let get_host_port opt s = match CString.split ':' s with - | [host; port] -> Some (Spawned.Socket(host, int_of_string port)) + | [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); @@ -472,6 +497,7 @@ let parse_args arglist = |"-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 ()) (* Options with zero arg *) |"-async-queries-always-delegate" @@ -481,6 +507,7 @@ let parse_args arglist = |"-async-proofs-never-reopen-branch" -> Flags.async_proofs_never_reopen_branch := true; |"-batch" -> set_batch_mode () + |"-test-mode" -> test_mode := true |"-beautify" -> make_beautify true |"-boot" -> boot := true; no_load_rc () |"-bt" -> Backtrace.record_backtrace true @@ -491,18 +518,21 @@ let parse_args arglist = |"-filteropts" -> filter_opts := true |"-h"|"-H"|"-?"|"-help"|"--help" -> usage () |"-ideslave" -> toploop := Some "coqidetop"; Flags.ide_slave := true - |"-impredicative-set" -> set_engagement Declarations.ImpredicativeSet + |"-impredicative-set" -> set_impredicative_set () |"-indices-matter" -> Indtypes.enforce_indices_matter () |"-just-parsing" -> Vernac.just_parsing := true |"-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 - |"-no-native-compiler" -> no_native_compiler := 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 |"-q" -> no_load_rc () - |"-quiet"|"-silent" -> Flags.make_silent true + |"-quiet"|"-silent" -> Flags.make_silent true; Flags.make_warn false |"-quick" -> Flags.compilation_mode := BuildVio |"-list-tags" -> print_tags := true |"-time" -> Flags.time := true @@ -510,7 +540,6 @@ let parse_args arglist = |"-unicode" -> add_require "Utf8_core" |"-v"|"--version" -> Usage.version (exitcode ()) |"-verbose-compat-notations" -> verb_compat_ntn := true - |"-vm" -> use_vm := true |"-where" -> print_where := true (* Deprecated options *) @@ -570,9 +599,7 @@ let init arglist = if_verbose print_header (); inputstate (); Mltop.init_known_plugins (); - set_vm_opt (); engage (); - set_hierarchy (); (* 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); @@ -597,7 +624,8 @@ let init arglist = if !batch_mode then mt () else str "Error during initialization:" ++ fnl () in - fatal_error (msg ++ Coqloop.print_toplevel_error any) (Errors.is_anomaly (fst any)) + let is_anomaly e = Errors.is_anomaly e || not (Errors.handled e) in + fatal_error (msg ++ Coqloop.print_toplevel_error any) (is_anomaly (fst any)) end; if !batch_mode then begin flush_all(); @@ -613,6 +641,7 @@ 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 -- cgit v1.2.3