From 2a5fd12d597d4337810ae367ea3a49720ee3d80c Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Tue, 21 Apr 2015 17:43:01 +0200
Subject: STM: print trace on "anomaly, no safe id attached"

---
 lib/errors.ml  | 2 ++
 lib/errors.mli | 1 +
 2 files changed, 3 insertions(+)

(limited to 'lib')

diff --git a/lib/errors.ml b/lib/errors.ml
index a4ec357ee4..13f3916477 100644
--- a/lib/errors.ml
+++ b/lib/errors.ml
@@ -99,6 +99,8 @@ let iprint (e, info) = print ~info e
 (** Same as [print], except that the "Please report" part of an anomaly
     isn't printed (used in Ltac debugging). *)
 let print_no_report e = print_gen (print_anomaly false) !handle_stack e
+let iprint_no_report (e, info) =
+  print_gen (print_anomaly false) !handle_stack e ++ print_backtrace info
 
 (** Predefined handlers **)
 
diff --git a/lib/errors.mli b/lib/errors.mli
index 03caa6a9f8..5bd5724746 100644
--- a/lib/errors.mli
+++ b/lib/errors.mli
@@ -80,6 +80,7 @@ val iprint : Exninfo.iexn -> Pp.std_ppcmds
 (** Same as [print], except that the "Please report" part of an anomaly
     isn't printed (used in Ltac debugging). *)
 val print_no_report : exn -> Pp.std_ppcmds
+val iprint_no_report : Exninfo.iexn -> Pp.std_ppcmds
 
 (** Critical exceptions should not be caught and ignored by mistake
     by inner functions during a [vernacinterp]. They should be handled
-- 
cgit v1.2.3


From 98a710caf5e907344329ee9e9f7b5fd87c50836f Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Wed, 22 Apr 2015 09:15:39 +0200
Subject: Do not use list concatenation when gluing streams together, just mark
 them as glued.

Possible improvement: rotate using the left children in the glue function,
so that the iter function becomes mostly tail-recursive. Drawback: two
allocations per glue instead of a single one.

This commit makes the following command go from 7.9s to 3.0s:

coqtop <<< "Require Import BigZ ZBinary Reals OrdersEx. Time SearchPattern _." | tail -n 1
---
 lib/pp.ml | 29 ++++++++++++++++++++++-------
 1 file changed, 22 insertions(+), 7 deletions(-)

(limited to 'lib')

diff --git a/lib/pp.ml b/lib/pp.ml
index 76046a7f91..e8b42ed797 100644
--- a/lib/pp.ml
+++ b/lib/pp.ml
@@ -26,15 +26,30 @@ module Glue : sig
 
 end = struct
 
-  type 'a t = 'a list
+  type 'a t = GEmpty | GLeaf of 'a | GNode of 'a t * 'a t
 
-  let atom x = [x]
-  let glue x y = y @ x
-  let empty = []
-  let is_empty x = x = []
+  let atom x = GLeaf x
+
+  let glue x y =
+    match x, y with
+    | GEmpty, _ -> y
+    | _, GEmpty -> x
+    | _, _ -> GNode (x,y)
+
+  let empty = GEmpty
+
+  let is_empty x = x = GEmpty
+
+  let rec iter f = function
+    | GEmpty -> ()
+    | GLeaf x -> f x
+    | GNode (x,y) -> iter f x; iter f y
+
+  let rec map f = function
+    | GEmpty -> GEmpty
+    | GLeaf x -> GLeaf (f x)
+    | GNode (x,y) -> GNode (map f x, map f y)
 
-  let iter f g = List.iter f (List.rev g)
-  let map = List.map
 end
 
 module Tag :
-- 
cgit v1.2.3


From 74d7dd7ae08dedfd80c056a345c1b3398eb91b5e Mon Sep 17 00:00:00 2001
From: Arnaud Spiwack
Date: Wed, 22 Apr 2015 17:39:42 +0200
Subject: Pp: obsolete comment.

Was made incorrect by 98a710caf5e907344329ee9e9f7b5fd87c50836f .---
 lib/pp.ml | 8 ++------
 1 file changed, 2 insertions(+), 6 deletions(-)

(limited to 'lib')

diff --git a/lib/pp.ml b/lib/pp.ml
index e8b42ed797..6e6b32c590 100644
--- a/lib/pp.ml
+++ b/lib/pp.ml
@@ -8,13 +8,9 @@
 
 module Glue : sig
 
-  (* A left associative glue implements efficient glue operator
-     when used as left associative.  If glue is denoted ++ then
+  (** The [Glue] module implements a container data structure with
+      efficient concatenation. *)
 
-        a ++ b ++ c ++ d = ((a ++ b) ++ c) ++ d = [d] @ ([c] @ ([b] @  [a]))
-
-     I.e. if the short list is the second argument
-  *)
   type 'a t
 
   val atom : 'a -> 'a t
-- 
cgit v1.2.3


From 0a2dfa5e5d17ccf58328432888dff345ef0bf5e6 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 23 Apr 2015 14:06:19 +0200
Subject: Removing dead code in Pp.

---
 lib/pp.ml  | 21 ---------------------
 lib/pp.mli |  3 ---
 2 files changed, 24 deletions(-)

(limited to 'lib')

diff --git a/lib/pp.ml b/lib/pp.ml
index 6e6b32c590..d672f06dbb 100644
--- a/lib/pp.ml
+++ b/lib/pp.ml
@@ -18,7 +18,6 @@ module Glue : sig
   val empty : 'a t
   val is_empty : 'a t -> bool
   val iter : ('a -> unit) -> 'a t -> unit
-  val map : ('a -> 'b) -> 'a t -> 'b t
 
 end = struct
 
@@ -41,11 +40,6 @@ end = struct
     | GLeaf x -> f x
     | GNode (x,y) -> iter f x; iter f y
 
-  let rec map f = function
-    | GEmpty -> GEmpty
-    | GLeaf x -> GLeaf (f x)
-    | GNode (x,y) -> GNode (map f x, map f y)
-
 end
 
 module Tag :
@@ -156,21 +150,6 @@ let app = Glue.glue
 
 let is_empty g = Glue.is_empty g
 
-let rewrite f p =
-  let strtoken = function
-    | Str_len (s, n) ->
-      let s' = f s in
-      Str_len (s', String.length s')
-    | Str_def s ->
-      Str_def (f s)
-  in
-  let rec ppcmd_token = function
-    | Ppcmd_print x -> Ppcmd_print (strtoken x)
-    | Ppcmd_box (bt, g) -> Ppcmd_box (bt, Glue.map ppcmd_token g)
-    | p -> p
-  in
-  Glue.map ppcmd_token p
-
 (* Compute length of an UTF-8 encoded string
    Rem 1 : utf8_length <= String.length (equal if pure ascii)
    Rem 2 : if used for an iso8859_1 encoded string, the result is
diff --git a/lib/pp.mli b/lib/pp.mli
index 5dd2686d14..e20e5ca82a 100644
--- a/lib/pp.mli
+++ b/lib/pp.mli
@@ -46,9 +46,6 @@ val eval_ppcmds : std_ppcmds -> std_ppcmds
 val is_empty : std_ppcmds -> bool
 (** Test emptyness. *)
 
-val rewrite : (string -> string) -> std_ppcmds -> std_ppcmds
-(** [rewrite f pps] applies [f] to all strings that appear in [pps]. *)
-
 (** {6 Derived commands} *)
 
 val spc : unit -> std_ppcmds
-- 
cgit v1.2.3


From 16d301bab5b7dec53be4786b3b6815bca54ae539 Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Thu, 23 Apr 2015 14:55:11 +0200
Subject: Remove almost all the uses of string concatenation when building
 error messages.

Since error messages are ultimately passed to Format, which has its own
buffers for concatenating strings, using concatenation for preparing error
messages just doubles the workload and increases memory pressure.
---
 lib/dyn.ml    |  9 ++++-----
 lib/errors.ml |  6 +++---
 lib/pp.ml     |  2 +-
 lib/system.ml | 11 +++++++----
 4 files changed, 15 insertions(+), 13 deletions(-)

(limited to 'lib')

diff --git a/lib/dyn.ml b/lib/dyn.ml
index a5e8fb9c2b..056b687313 100644
--- a/lib/dyn.ml
+++ b/lib/dyn.ml
@@ -7,6 +7,7 @@
 (************************************************************************)
 
 open Errors
+open Pp
 
 (* Dynamics, programmed with DANGER !!! *)
 
@@ -23,7 +24,7 @@ let create (s : string) =
   let () =
     if Int.Map.mem hash !dyntab then
       let old = Int.Map.find hash !dyntab in
-      let msg = Pp.str ("Dynamic tag collision: " ^ s ^ " vs. " ^ old) in
+      let msg = str "Dynamic tag collision: " ++ str s ++ str " vs. " ++ str old in
       anomaly ~label:"Dyn.create" msg
   in
   let () = dyntab := Int.Map.add hash s !dyntab in
@@ -31,8 +32,7 @@ let create (s : string) =
   let outfun (nh, rv) =
     if Int.equal hash nh then Obj.magic rv
     else
-      let msg = (Pp.str ("dyn_out: expected " ^ s)) in
-      anomaly msg
+      anomaly (str "dyn_out: expected " ++ str s)
   in
   (infun, outfun)
 
@@ -43,8 +43,7 @@ let has_tag (s, _) tag =
 let tag (s,_) =
   try Int.Map.find s !dyntab
   with Not_found ->
-    let msg = Pp.str ("Unknown dynamic tag " ^ (string_of_int s)) in
-    anomaly msg
+    anomaly (str "Unknown dynamic tag " ++ int s)
 
 let pointer_equal (t1,o1) (t2,o2) = t1 = t2 && o1 == o2
 
diff --git a/lib/errors.ml b/lib/errors.ml
index 13f3916477..999d99ee08 100644
--- a/lib/errors.ml
+++ b/lib/errors.ml
@@ -69,12 +69,12 @@ let rec print_gen bottom stk e =
 let where = function
 | None -> mt ()
 | Some s ->
-  if !Flags.debug then str ("in "^s^":") ++ spc () else mt ()
+  if !Flags.debug then str "in " ++ str s ++ str ":" ++ spc () else mt ()
 
 let raw_anomaly e = match e with
   | Anomaly (s, pps) -> where s ++ pps ++ str "."
-  | Assert_failure _ | Match_failure _ -> str (Printexc.to_string e ^ ".")
-  | _ -> str ("Uncaught exception " ^ Printexc.to_string e ^ ".")
+  | Assert_failure _ | Match_failure _ -> str (Printexc.to_string e) ++ str "."
+  | _ -> str "Uncaught exception " ++ str (Printexc.to_string e) ++ str "."
 
 let print_backtrace e = match Backtrace.get_backtrace e with
 | None -> mt ()
diff --git a/lib/pp.ml b/lib/pp.ml
index d672f06dbb..9667f7270e 100644
--- a/lib/pp.ml
+++ b/lib/pp.ml
@@ -249,7 +249,7 @@ let escape_string s =
     else escape_at s (i-1) in
   escape_at s (String.length s - 1)
 
-let qstring s = str ("\""^escape_string s^"\"")
+let qstring s = str "\"" ++ str (escape_string s) ++ str "\""
 let qs = qstring
 let quote s = h 0 (str "\"" ++ s ++ str "\"")
 
diff --git a/lib/system.ml b/lib/system.ml
index 73095f9cd6..d1cdd8efc9 100644
--- a/lib/system.ml
+++ b/lib/system.ml
@@ -118,7 +118,8 @@ let is_in_system_path filename =
 
 let open_trapping_failure name =
   try open_out_bin name
-  with e when Errors.noncritical e -> error ("Can't open " ^ name)
+  with e when Errors.noncritical e ->
+    errorlabstrm "System.open" (str "Can't open " ++ str name)
 
 let try_remove filename =
   try Sys.remove filename
@@ -126,7 +127,8 @@ let try_remove filename =
     msg_warning
       (str"Could not remove file " ++ str filename ++ str" which is corrupted!")
 
-let error_corrupted file s = error (file ^": " ^ s ^ ". Try to rebuild it.")
+let error_corrupted file s =
+  errorlabstrm "System" (str file ++ str ": " ++ str s ++ str ". Try to rebuild it.")
 
 let input_binary_int f ch =
   try input_binary_int ch
@@ -201,7 +203,8 @@ let extern_intern ?(warn=true) magic =
 	let reraise = Errors.push reraise in
         let () = try_remove filename in
         iraise reraise
-    with Sys_error s -> error ("System error: " ^ s)
+    with Sys_error s ->
+      errorlabstrm "System.extern_state" (str "System error: " ++ str s)
   and intern_state paths name =
     try
       let _,filename = find_file_in_path ~warn paths name in
@@ -210,7 +213,7 @@ let extern_intern ?(warn=true) magic =
       close_in channel;
       v
     with Sys_error s ->
-      error("System error: " ^ s)
+      errorlabstrm "System.intern_state" (str "System error: " ++ str s)
   in
   (extern_state,intern_state)
 
-- 
cgit v1.2.3


From 2a295131a1a72dd56e6e7abdeaeca07b1b69ab6d Mon Sep 17 00:00:00 2001
From: Clément Pit--Claudel
Date: Thu, 23 Apr 2015 01:14:49 -0400
Subject: Add a [Redirect] vernacular command

The command [Redirect "filename" (...)] redirects all the output of
[(...)]  to file "filename.out". This is useful for storing the results of
an [Eval compute], for redirecting the results of a large search, for
automatically generating traces of interesting developments, and so on.
---
 lib/pp.ml  | 21 +++++++++++++++++++++
 lib/pp.mli |  2 ++
 2 files changed, 23 insertions(+)

(limited to 'lib')

diff --git a/lib/pp.ml b/lib/pp.ml
index 9667f7270e..30bc30a9ad 100644
--- a/lib/pp.ml
+++ b/lib/pp.ml
@@ -448,6 +448,27 @@ let logger = ref std_logger
 let make_pp_emacs() = print_emacs:=true; logger:=emacs_logger
 let make_pp_nonemacs() = print_emacs:=false; logger := std_logger
 
+let ft_logger old_logger ft ~id level mesg = match level with
+  | Debug _ -> msgnl_with ft (debugbody mesg)
+  | Info -> msgnl_with ft (infobody mesg)
+  | Notice -> msgnl_with ft mesg
+  | Warning -> old_logger ~id:id level mesg
+  | Error -> old_logger ~id:id level mesg
+
+let with_output_to_file fname func input =
+  let old_logger = !logger in
+  let channel = open_out (String.concat "." [fname; "out"]) in
+  logger := ft_logger old_logger (Format.formatter_of_out_channel channel);
+  try
+    let output = func input in
+    logger := old_logger;
+    close_out channel;
+    output
+  with reraise ->
+    let reraise = Backtrace.add_backtrace reraise in
+    logger := old_logger;
+    close_out channel;
+    Exninfo.iraise reraise
 
 let feedback_id = ref (Feedback.Edit 0)
 let feedback_route = ref Feedback.default_route
diff --git a/lib/pp.mli b/lib/pp.mli
index e20e5ca82a..3b1123a9dc 100644
--- a/lib/pp.mli
+++ b/lib/pp.mli
@@ -12,6 +12,8 @@
 val make_pp_emacs:unit -> unit
 val make_pp_nonemacs:unit -> unit
 
+val with_output_to_file : string -> ('a -> 'b) -> 'a -> 'b
+
 (** Pretty-printers. *)
 
 type std_ppcmds
-- 
cgit v1.2.3