Imported Upstream version 8.5~beta3+dfsg

1 files changed, 77 insertions, 48 deletions

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