Merge branch 'v8.5'

5 files changed, 53 insertions, 24 deletions

diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index a04678a1b9..c92c8fff76 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -94,9 +94,21 @@ 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
 
@@ -111,10 +123,15 @@ let set_hierarchy () = if !type_in_type then Global.set_type_in_type ()
 
 let set_batch_mode () = batch_mode := true
 
-let set_warning = function
-| "all" -> make_warn true
-| "none" -> make_warn false
-| _ -> prerr_endline ("Error: all/none expected after option w"); exit 1
+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)
@@ -630,6 +647,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
 
diff --git a/toplevel/obligations.ml b/toplevel/obligations.ml
index 523134b50f..9df5a411ba 100644
--- a/toplevel/obligations.ml
+++ b/toplevel/obligations.ml
@@ -306,7 +306,7 @@ type fixpoint_kind =
 
 type notations = (Vernacexpr.lstring * Constrexpr.constr_expr * Notation_term.scope_name option) list
 
-type program_info = {
+type program_info_aux = {
   prg_name: Id.t;
   prg_body: constr;
   prg_type: constr;
@@ -322,6 +322,13 @@ type program_info = {
   prg_opaque : bool;
 }
 
+type program_info = program_info_aux Ephemeron.key
+
+let get_info x =
+  try Ephemeron.get x
+  with Ephemeron.InvalidKey ->
+    Errors.anomaly Pp.(str "Program obligation can't be accessed by a worker")
+
 let assumption_message = Declare.assumption_message
 
 let (set_default_tactic, get_default_tactic, print_default_tactic) = 
@@ -452,7 +459,7 @@ let subst_deps_obl obls obl =
 
 module ProgMap = Map.Make(Id)
 
-let map_replace k v m = ProgMap.add k v (ProgMap.remove k m)
+let map_replace k v m = ProgMap.add k (Ephemeron.create v) (ProgMap.remove k m)
 
 let map_keys m = ProgMap.fold (fun k _ l -> k :: l) m []
 
@@ -674,13 +681,13 @@ let get_prog name =
   let prg_infos = !from_prg in
     match name with
 	Some n ->
-	  (try ProgMap.find n prg_infos
+	  (try get_info (ProgMap.find n prg_infos)
 	   with Not_found -> raise (NoObligations (Some n)))
       | None ->
 	  (let n = map_cardinal prg_infos in
 	     match n with
 		 0 -> raise (NoObligations None)
-	       | 1 -> map_first prg_infos
+	       | 1 -> get_info (map_first prg_infos)
 	       | _ -> 
                    error ("More than one program with unsolved obligations: "^
                     String.concat ", " 
@@ -690,7 +697,7 @@ let get_prog name =
 let get_any_prog () =
   let prg_infos = !from_prg in
   let n = map_cardinal prg_infos in
-  if n > 0 then map_first prg_infos
+  if n > 0 then get_info (map_first prg_infos)
   else raise (NoObligations None)
 
 let get_prog_err n =
@@ -730,7 +737,7 @@ let update_obls prg obls rem =
 	    progmap_remove prg';
 	    Defined kn
       | l ->
-	  let progs = List.map (fun x -> ProgMap.find x !from_prg) prg'.prg_deps in
+	  let progs = List.map (fun x -> get_info (ProgMap.find x !from_prg)) prg'.prg_deps in
 	    if List.for_all (fun x -> obligations_solved x) progs then
 	      let kn = declare_mutual_definition progs in
 		Defined (ConstRef kn)
@@ -929,7 +936,7 @@ and solve_obligations n tac =
     solve_prg_obligations prg tac
 
 and solve_all_obligations tac =
-  ProgMap.iter (fun k v -> ignore(solve_prg_obligations v tac)) !from_prg
+  ProgMap.iter (fun k v -> ignore(solve_prg_obligations (get_info v) tac)) !from_prg
 
 and try_solve_obligation n prg tac =
   let prg = get_prog prg in
@@ -970,7 +977,7 @@ let show_obligations ?(msg=true) n =
     | Some n ->
 	try [ProgMap.find n !from_prg]
 	with Not_found -> raise (NoObligations (Some n))
-  in List.iter (show_obligations_of_prg ~msg) progs
+  in List.iter (fun x -> show_obligations_of_prg ~msg (get_info x)) progs
 
 let show_term n =
   let prg = get_prog_err n in
@@ -991,7 +998,7 @@ let add_definition n ?term t ctx ?(implicits=[]) ?(kind=Global,false,Definition)
   else (
     let len = Array.length obls in
     let _ = Flags.if_verbose msg_info (info ++ str ", generating " ++ int len ++ str " obligation(s)") in
-      progmap_add n prg;
+      progmap_add n (Ephemeron.create prg);
       let res = auto_solve_obligations (Some n) tactic in
 	match res with
 	| Remain rem -> Flags.if_verbose (fun () -> show_obligations ~msg:false (Some n)) (); res
@@ -1004,7 +1011,7 @@ let add_mutual_definitions l ctx ?tactic ?(kind=Global,false,Definition) ?(reduc
     (fun  (n, b, t, imps, obls) ->
      let prg = init_prog_info ~opaque n (Some b) t ctx deps (Some fixkind)
        notations obls imps kind reduce hook 
-     in progmap_add n prg) l;
+     in progmap_add n (Ephemeron.create prg)) l;
     let _defined =
       List.fold_left (fun finished x ->
 	if finished then finished
diff --git a/toplevel/usage.ml b/toplevel/usage.ml
index c7d77de8cc..281fb7ef72 100644
--- a/toplevel/usage.ml
+++ b/toplevel/usage.ml
@@ -52,7 +52,7 @@ let print_usage_channel co command =
 \n                         proofs in each fi.vio\
 \n\
 \n  -where                 print Coq's standard library location and exit\
-\n  -config                print Coq's configuration information and exit\
+\n  -config, --config      print Coq's configuration information and exit\
 \n  -v                     print Coq version and exit\
 \n  -list-tags             print highlight color tags known by Coq and exit\
 \n\
@@ -74,8 +74,12 @@ let print_usage_channel co command =
 \n  -indices-matter        levels of indices (and nonuniform parameters) contribute to the level of inductives\
 \n  -type-in-type          disable universe consistency checking\
 \n  -time                  display the time taken by each command\
+\n  -m, --memory           display total heap size at program exit\
+\n                         (use environment variable\
+\n                          OCAML_GC_STATS=\"/tmp/gclog.txt\"\
+\n                          for full Gc stats dump)
 \n  -native-compiler       precompile files for the native_compute machinery\
-\n  -h, -help              print this list of options\
+\n  -h, -help, --help      print this list of options\
 \n";
   List.iter (fun (name, text) ->
     output_string co
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index 7d84ecf6ca..bc8aa2fffa 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -344,10 +344,10 @@ let compile verbosely f =
       let open Library in
       Dumpglob.noglob ();
       let f = if check_suffix f ".vio" then chop_extension f else f in
-      let lfdv, lib, univs, disch, tasks, proofs = load_library_todo f in
+      let lfdv, sum, lib, univs, disch, tasks, proofs = load_library_todo f in
       Stm.set_compilation_hints lfdv;
       let univs, proofs = Stm.finish_tasks lfdv univs disch proofs tasks in
-      Library.save_library_raw lfdv lib univs proofs
+      Library.save_library_raw lfdv sum lib univs proofs
 
 let compile v f = 
   ignore(CoqworkmgrApi.get 1);
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 80fe26a817..8d9f8f52c8 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -1435,10 +1435,10 @@ let _ =
   declare_bool_option
     { optsync  = true;
       optdepr  = false;
-      optname  = "printing of universes";
-      optkey   = ["Printing";"Universes"];
-      optread  = (fun () -> !Constrextern.print_universes);
-      optwrite = (fun b -> Constrextern.print_universes:=b) }
+      optname  = "dumping bytecode after compilation";
+      optkey   = ["Dump";"Bytecode"];
+      optread  = Flags.get_dump_bytecode;
+      optwrite = Flags.set_dump_bytecode }
 
 let vernac_debug b =
   set_debug (if b then Tactic_debug.DebugOn 0 else Tactic_debug.DebugOff)