From 0929a78f9a663ac2bcdf1294de93797b9fdfefad Mon Sep 17 00:00:00 2001
From: Pierre Letouzey
Date: Sat, 4 Feb 2017 01:50:58 +0100
Subject: Extraction: fix complexity issue #5310

  A double call to pp_module_type inside Ocaml.pp_specif was
  causing an complexity blowup when pretty-printing heavily modular
  extracted code.

  I wasn't able to figure out why this double call is there. It could
  be the leftover of some intermediate work in 2007 before commit 350398eae
  (which introduced global printing phases Pre/Impl/Intf).

  Anyway I'm reasonably sure that today these two pp_module_type calls produce
  the exact same pretty-printed signature (even if there's a large bunch of
  imperative states around). Moreover, this duplicated signature is actually
  slightly wrong: when we alias a module M with a unambiguous name like Coq__123,
  the type of Coq__123 should not be an exact copy of the type of M, but rather
  a "strengthened" version of it (with equality between inductive types).
  So the best solution is now to use this funny feature of OCaml introduced in 3.12 :

  module Coq__123 : module type of struct include M end

  This "module type of struct include" is slightly awkward, but short, correct,
  and trivial to produce :-). And I doubt anybody will object to the (rare) use
  of some 3.12 features in extracted code of 2017...
---
 plugins/extraction/ocaml.ml | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

(limited to 'plugins/extraction')

diff --git a/plugins/extraction/ocaml.ml b/plugins/extraction/ocaml.ml
index 1c29a9bc24..5d10cb939d 100644
--- a/plugins/extraction/ocaml.ml
+++ b/plugins/extraction/ocaml.ml
@@ -618,12 +618,13 @@ let rec pp_specif = function
        with Not_found -> pp_spec s)
   | (l,Smodule mt) ->
       let def = pp_module_type [] mt in
-      let def' = pp_module_type [] mt in
       let name = pp_modname (MPdot (top_visible_mp (), l)) in
       hov 1 (str "module " ++ name ++ str " :" ++ fnl () ++ def) ++
       (try
 	 let ren = Common.check_duplicate (top_visible_mp ()) l in
-	 fnl () ++ hov 1 (str ("module "^ren^" :") ++ fnl () ++ def')
+         fnl () ++
+         hov 1 (str ("module "^ren^" :") ++ spc () ++
+                str "module type of struct include " ++ name ++ str " end")
        with Not_found -> Pp.mt ())
   | (l,Smodtype mt) ->
       let def = pp_module_type [] mt in
-- 
cgit v1.2.3


From ebc0870ca932acf0ceea5fe513e2ca40e74c2a02 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 6 Oct 2016 17:34:12 +0200
Subject: Moving the Ltac plugin to a pack-based one.

This is cumbersome, because now code may fail at link time if it's not
referring to the correct module name. Therefore, one has to add corresponding
open statements a the top of every file depending on a Ltac module. This
includes seemingly unrelated files that use EXTEND statements.
---
 plugins/extraction/g_extraction.ml4 | 1 +
 1 file changed, 1 insertion(+)

(limited to 'plugins/extraction')

diff --git a/plugins/extraction/g_extraction.ml4 b/plugins/extraction/g_extraction.ml4
index e1d6bb4a84..3ed959cf2c 100644
--- a/plugins/extraction/g_extraction.ml4
+++ b/plugins/extraction/g_extraction.ml4
@@ -12,6 +12,7 @@ DECLARE PLUGIN "extraction_plugin"
 
 (* ML names *)
 
+open Ltac_plugin
 open Genarg
 open Stdarg
 open Pcoq.Prim
-- 
cgit v1.2.3


From 6b78d0602d46520ed1bd0cfbef120de3b06ca826 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Thu, 23 Feb 2017 13:32:46 +0100
Subject: [safe-string] plugins/extraction

No functional change.
---
 plugins/extraction/common.ml | 5 +----
 plugins/extraction/scheme.ml | 6 +-----
 plugins/extraction/table.ml  | 4 +---
 3 files changed, 3 insertions(+), 12 deletions(-)

(limited to 'plugins/extraction')

diff --git a/plugins/extraction/common.ml b/plugins/extraction/common.ml
index de97ba97c3..0a591e786f 100644
--- a/plugins/extraction/common.ml
+++ b/plugins/extraction/common.ml
@@ -91,10 +91,7 @@ let begins_with_CoqXX s =
 
 let unquote s =
   if lang () != Scheme then s
-  else
-    let s = String.copy s in
-    for i=0 to String.length s - 1 do if s.[i] == '\'' then s.[i] <- '~' done;
-    s
+  else String.map (fun c -> if c == '\'' then '~' else c) s
 
 let rec qualify delim = function
   | [] -> assert false
diff --git a/plugins/extraction/scheme.ml b/plugins/extraction/scheme.ml
index a6309e61f9..8d0cc4a0db 100644
--- a/plugins/extraction/scheme.ml
+++ b/plugins/extraction/scheme.ml
@@ -40,11 +40,7 @@ let preamble _ comment _ usf =
   (if usf.mldummy then str "(define __ (lambda (_) __))\n\n" else mt ())
 
 let pr_id id =
-  let s = Id.to_string id in
-  for i = 0 to String.length s - 1 do
-    if s.[i] == '\'' then s.[i] <- '~'
-  done;
-  str s
+  str @@ String.map (fun c -> if c == '\'' then '~' else c) (Id.to_string id)
 
 let paren = pp_par true
 
diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml
index 5e7d810c93..d6a334c5fe 100644
--- a/plugins/extraction/table.ml
+++ b/plugins/extraction/table.ml
@@ -773,9 +773,7 @@ let file_of_modfile mp =
     | MPfile f -> Id.to_string (List.hd (DirPath.repr f))
     | _ -> assert false
   in
-  let s = String.copy (string_of_modfile mp) in
-  if s.[0] != s0.[0] then s.[0] <- s0.[0];
-  s
+  String.mapi (fun i c -> if i = 0 then s0.[0] else c) (string_of_modfile mp)
 
 let add_blacklist_entries l =
   blacklist_table :=
-- 
cgit v1.2.3


From 2617a83e572531e26734cff8b9eb8aa09d49b850 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Tue, 27 Sep 2016 16:33:47 +0200
Subject: [pp] Remove `Pp.stras`.

Mostly unused, we ought to limit spacing in the boxes themselves.
---
 plugins/extraction/common.ml | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

(limited to 'plugins/extraction')

diff --git a/plugins/extraction/common.ml b/plugins/extraction/common.ml
index 0a591e786f..fc8d5356c8 100644
--- a/plugins/extraction/common.ml
+++ b/plugins/extraction/common.ml
@@ -67,7 +67,9 @@ let pp_boxed_tuple f = function
     blocks is less that a line length. To avoid this awkward situation,
     we attach a big virtual size to [fnl] newlines. *)
 
-let fnl () = stras (1000000,"") ++ fnl ()
+(* EG: This looks quite suspicious... but beware of bugs *)
+(* let fnl () = stras (1000000,"") ++ fnl () *)
+let fnl () = fnl ()
 
 let fnl2 () = fnl () ++ fnl ()
 
-- 
cgit v1.2.3


From 8f8af9e4ebf1ea1ed15f765196ef5af8a77d3c27 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Thu, 29 Sep 2016 16:06:43 +0200
Subject: [pp] Prepare for serialization, remove opaque glue.

We also remove flushing operations `msg_with`, now the flushing
responsibility belong to the owner of the formatter.
---
 plugins/extraction/ocaml.ml | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

(limited to 'plugins/extraction')

diff --git a/plugins/extraction/ocaml.ml b/plugins/extraction/ocaml.ml
index d89bf95ee8..d8e3821557 100644
--- a/plugins/extraction/ocaml.ml
+++ b/plugins/extraction/ocaml.ml
@@ -66,7 +66,7 @@ let pp_header_comment = function
   | None -> mt ()
   | Some com -> pp_comment com ++ fnl2 ()
 
-let then_nl pp = if Pp.is_empty pp then mt () else pp ++ fnl ()
+let then_nl pp = if Pp.ismt pp then mt () else pp ++ fnl ()
 
 let pp_tdummy usf =
   if usf.tdummy || usf.tunknown then str "type __ = Obj.t" ++ fnl () else mt ()
@@ -618,7 +618,7 @@ and pp_module_type params = function
       push_visible mp params;
       let try_pp_specif l x =
         let px = pp_specif x in
-        if Pp.is_empty px then l else px::l
+        if Pp.ismt px then l else px::l
       in
       (* We cannot use fold_right here due to side effects in pp_specif *)
       let l = List.fold_left try_pp_specif [] sign in
@@ -696,7 +696,7 @@ and pp_module_expr params = function
       push_visible mp params;
       let try_pp_structure_elem l x =
         let px = pp_structure_elem x in
-        if Pp.is_empty px then l else px::l
+        if Pp.ismt px then l else px::l
       in
       (* We cannot use fold_right here due to side effects in pp_structure_elem *)
       let l = List.fold_left try_pp_structure_elem [] sel in
@@ -714,7 +714,7 @@ let rec prlist_sep_nonempty sep f = function
   | h::t ->
      let e = f h in
      let r = prlist_sep_nonempty sep f t in
-     if Pp.is_empty e then r
+     if Pp.ismt e then r
      else e ++ sep () ++ r
 
 let do_struct f s =
-- 
cgit v1.2.3


From 5b8bfee9d80e550cd81e326ec134430b2a4797a5 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Thu, 29 Sep 2016 16:30:21 +0200
Subject: [pp] Make feedback the only logging mechanism.

Previously to this patch, Coq featured to distinct logging paths: the
console legacy one, based on `Pp.std_ppcmds` and Ocaml's `Format`
module, and the `Feedback` one, intended to encapsulate message inside a
more general, GUI-based feedback protocol.

This patch removes the legacy logging path and makes feedback
canonical. Thus, the core of Coq has no dependency on console code
anymore.

Additionally, this patch resolves the duplication of "document" formats
present in the same situation. The original console-based printing code
relied on an opaque datatype `std_ppcmds`, (mostly a reification of
`Format`'s format strings) that could be then rendered to the console.

However, the feedback path couldn't reuse this type due to its opaque
nature. The first versions just embedded rending of `std_ppcmds` to a
string, however in 8.5 a new "rich printing" type, `Richpp.richpp` was
introduced.

The idea for this type was to be serializable, however it brought
several problems: it didn't have proper document manipulation
operations, its format was overly verbose and didn't preserve the full
layout, and it still relied on `Format` for generation, making
client-side rendering difficult.

We thus follow the plan outlined in CEP#9, that is to say, we take a
public and refactored version of `std_ppcmds` as the canonical "document
type", and move feedback to be over there. The toplevel now is
implemented as a feedback listener and has ownership of the console.

`richpp` is now IDE-specific, and only used for legacy rendering. It
could go away in future versions. `std_ppcmds` carries strictly more
information and is friendlier to client-side rendering and display
control.

Thus, the new panorama is:

- `Feedback` has become a very module for event dispatching.
- `Pp` contains a target-independent box-based document format.
  It also contains the `Format`-based renderer.
- All console access lives in `toplevel`, with console handlers private
  to coqtop.

_NOTE_: After this patch, many printing parameters such as printing
width or depth should be set client-side. This works better IMO,
clients don't need to notify Coq about resizing anywmore. Indeed, for
box-based capable backends such as HTML or LaTeX, the UI can directly
render and let the engine perform the word breaking work.

_NOTE_: Many messages could benefit from new features of the output
format, however we have chosen not to alter them to preserve output.

A Future commits will move console tag handling in `Pp_style` to
`toplevel/`, where it logically belongs.

The only change with regards to printing is that the "Error:" header was
added to console output in several different positions, we have removed
some of this duplication, now error messages should be a bit more
consistent.
---
 plugins/extraction/extract_env.ml | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

(limited to 'plugins/extraction')

diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml
index e019bb3c2a..ee623c5ca0 100644
--- a/plugins/extraction/extract_env.ml
+++ b/plugins/extraction/extract_env.ml
@@ -472,13 +472,14 @@ let formatter dry file =
     if dry then Format.make_formatter (fun _ _ _ -> ()) (fun _ -> ())
     else
       match file with
-	| Some f -> Pp_control.with_output_to f
+	| Some f -> Topfmt.with_output_to f
 	| None -> Format.formatter_of_buffer buf
   in
+  (* XXX: Fixme, this shouldn't depend on Topfmt *)
   (* We never want to see ellipsis ... in extracted code *)
   Format.pp_set_max_boxes ft max_int;
   (* We reuse the width information given via "Set Printing Width" *)
-  (match Pp_control.get_margin () with
+  (match Topfmt.get_margin () with
     | None -> ()
     | Some i ->
       Format.pp_set_margin ft i;
-- 
cgit v1.2.3


From 00b1ceb18db39334a357784a114e45a9012cf594 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Mon, 6 Feb 2017 04:52:43 +0100
Subject: [extraction] Flush formatters at end of output.

Previous implementations of `Pp` flushed on newline, however,
depending on the formatter this may not be always the case.

We now alwayas flush the formatters before closing the file as this is
the intended behavior.
---
 plugins/extraction/extract_env.ml | 4 ++++
 1 file changed, 4 insertions(+)

(limited to 'plugins/extraction')

diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml
index ee623c5ca0..2b12462ad5 100644
--- a/plugins/extraction/extract_env.ml
+++ b/plugins/extraction/extract_env.ml
@@ -519,8 +519,10 @@ let print_structure_to_file (fn,si,mo) dry struc =
     set_phase Impl;
     pp_with ft (d.preamble mo comment opened unsafe_needs);
     pp_with ft (d.pp_struct struc);
+    Format.pp_print_flush ft ();
     Option.iter close_out cout;
   with reraise ->
+    Format.pp_print_flush ft ();
     Option.iter close_out cout; raise reraise
   end;
   if not dry then Option.iter info_file fn;
@@ -533,8 +535,10 @@ let print_structure_to_file (fn,si,mo) dry struc =
 	 set_phase Intf;
 	 pp_with ft (d.sig_preamble mo comment opened unsafe_needs);
 	 pp_with ft (d.pp_sig (signature_of_structure struc));
+         Format.pp_print_flush ft ();
 	 close_out cout;
        with reraise ->
+         Format.pp_print_flush ft ();
 	 close_out cout; raise reraise
        end;
        info_file si)
-- 
cgit v1.2.3


From 6d2802075606dcddb02dd13cbaf38ff76f8bf242 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Thu, 23 Mar 2017 01:13:38 +0100
Subject: Add empty Extraction.v and FunInd.v to prepare landing of PR#220.

This way, after we merge PR#220, scripts can be fixed in a way that is
compatible with the 8.6 and trunk branches.
---
 plugins/extraction/Extraction.v | 0
 plugins/extraction/vo.itarget   | 1 +
 2 files changed, 1 insertion(+)
 create mode 100644 plugins/extraction/Extraction.v

(limited to 'plugins/extraction')

diff --git a/plugins/extraction/Extraction.v b/plugins/extraction/Extraction.v
new file mode 100644
index 0000000000..e69de29bb2
diff --git a/plugins/extraction/vo.itarget b/plugins/extraction/vo.itarget
index 9c30c5eb3e..3563f71dfc 100644
--- a/plugins/extraction/vo.itarget
+++ b/plugins/extraction/vo.itarget
@@ -1,3 +1,4 @@
+Extraction.vo
 ExtrHaskellBasic.vo
 ExtrHaskellNatNum.vo
 ExtrHaskellNatInt.vo
-- 
cgit v1.2.3


From 9c38a23ae84e1542ab1eeab6ded4201718ec1cf8 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Thu, 23 Mar 2017 14:50:56 +0100
Subject: Revert "Add empty Extraction.v and FunInd.v to prepare landing of
 PR#220."

This reverts commit 6d2802075606dcddb02dd13cbaf38ff76f8bf242, which is
an 8.6 only commit.
---
 plugins/extraction/Extraction.v | 0
 plugins/extraction/vo.itarget   | 1 -
 2 files changed, 1 deletion(-)
 delete mode 100644 plugins/extraction/Extraction.v

(limited to 'plugins/extraction')

diff --git a/plugins/extraction/Extraction.v b/plugins/extraction/Extraction.v
deleted file mode 100644
index e69de29bb2..0000000000
diff --git a/plugins/extraction/vo.itarget b/plugins/extraction/vo.itarget
index 3563f71dfc..9c30c5eb3e 100644
--- a/plugins/extraction/vo.itarget
+++ b/plugins/extraction/vo.itarget
@@ -1,4 +1,3 @@
-Extraction.vo
 ExtrHaskellBasic.vo
 ExtrHaskellNatNum.vo
 ExtrHaskellNatInt.vo
-- 
cgit v1.2.3