3 files changed, 138 insertions, 0 deletions
diff --git a/dev/doc/changes.txt b/dev/doc/changes.txt
index 4a0130bef0..4135ddd2db 100644
--- a/dev/doc/changes.txt
+++ b/dev/doc/changes.txt
@@ -148,6 +148,38 @@ define_evar_* mostly used internally in the unification engine.
 
 - The Refine module was move out of Proofview.
 
+    Proofview.Refine.* --->  Refine.*
+
+- A statically monotonous evarmap type was introduced in Sigma. Not all the API
+  has been converted, so that the user may want to use compatibility functions
+  Sigma.to_evar_map and Sigma.Unsafe.of_evar_map or Sigma.Unsafe.of_pair when
+  needed. Code can be straightforwardly adapted in the following way:
+
+  let (sigma, x1) = ... in
+  ...
+  let (sigma, xn) = ... in
+  (sigma, ans)
+
+  should be turned into:
+
+  open Sigma.Notations
+
+  let Sigma (x1, sigma, p1) = ... in
+  ...
+  let Sigma (xn, sigma, pn) = ... in
+  Sigma (ans, sigma, p1 +> ... +> pn)
+
+- The Proofview.Goal.*enter family of functions now takes a polymorphic
+  continuation given as a record as an argument.
+
+  Proofview.Goal.enter begin fun gl -> ... end
+
+  should be turned into
+
+  open Proofview.Notations
+
+  Proofview.Goal.enter { enter = begin fun gl -> ... end }
+
 =========================================
 = CHANGES BETWEEN COQ V8.4 AND COQ V8.5 =
 =========================================
diff --git a/dev/doc/ocamlbuild.txt b/dev/doc/ocamlbuild.txt
new file mode 100644
index 0000000000..efedbc506e
--- /dev/null
+++ b/dev/doc/ocamlbuild.txt
@@ -0,0 +1,30 @@
+Ocamlbuild & Coq
+----------------
+
+A quick note in case someone else gets interested someday in compiling
+Coq via ocamlbuild : such an experimental build system has existed
+in the past (more or less maintained from 2009 to 2013), in addition
+to the official build system via gnu make. But this build via
+ocamlbuild has been severly broken since early 2014 (and don't work
+in 8.5, for instance). This experiment has attracted very limited
+interest from other developers over the years, and has been quite
+cumbersome to maintain, so it is now officially discontinued.
+If you want to have a look at the files of this build system
+(especially myocamlbuild.ml), you can fetch :
+ - my last effort at repairing this build system (up to coqtop.native) :
+   https://github.com/letouzey/coq-wip/tree/ocamlbuild-partial-repair
+ - coq official v8.5 branch (recent but broken)
+ - coq v8.4 branch(less up-to-date, but works).
+
+For the record, the three main drawbacks of this experiments were:
+ - recurrent issues with circularities reported by ocamlbuild
+   (even though make was happy) during the evolution of Coq sources
+ - no proper support of parallel build
+ - quite slow re-traversal of already built things
+See the two corresponding bug reports on Mantis, or
+https://github.com/ocaml/ocamlbuild/issues/52
+
+As an interesting feature, I successfully used this to cross-compile
+Coq 8.4 from linux to win32 via mingw.
+
+Pierre Letouzey, june 2016
diff --git a/dev/doc/profiling.txt b/dev/doc/profiling.txt
new file mode 100644
index 0000000000..9d2ebf0d4c
--- /dev/null
+++ b/dev/doc/profiling.txt
@@ -0,0 +1,76 @@
+# How to profile Coq?
+
+I (Pierre-Marie Pédrot) mainly use two OCaml branches to profile Coq, whether I
+want to profile time or memory consumption. AFAIK, this only works for Linux.
+
+## Time
+
+In Coq source folder:
+
+opam switch 4.02.1+fp
+./configure -local -debug
+make
+perf record -g bin/coqtop -compile file.v
+perf report -g fractal,callee --no-children
+
+To profile only part of a file, first load it using
+
+bin/coqtop -l file.v
+
+and plug into the process
+
+perf record -g -p PID
+
+## Memory
+
+You first need a few commits atop trunk for this to work.
+
+git remote add ppedrot https://github.com/ppedrot/coq.git
+git fetch ppedrot
+git checkout ppedrot/allocation-profiling
+git rebase master
+
+Then:
+
+opam switch 4.00.1+alloc-profiling
+./configure -local -debug
+make
+
+Note that linking the coqtop binary takes quite an amount of time with this
+branch, so do not worry too much. There are more recent branches of
+alloc-profiling on mshinwell's repo which can be found at:
+
+https://github.com/mshinwell/opam-repo-dev
+
+### For memory dump:
+
+CAMLRUNPARAM=T,mj bin/coqtop -compile file.v
+
+In another terminal:
+
+pkill -SIGUSR1 $COQTOPPID
+...
+pkill -SIGUSR1 $COQTOPPID
+dev/decode-major-heap.sh heap.$COQTOPPID.$N bin/coqtop
+
+where $COQTOPPID is coqtop pid and $N the index of the call to pkill.
+
+First column is the memory taken by the objects (in words), second one is the
+number of objects and third is the place where the objects where allocated.
+
+### For complete memory graph:
+
+CAMLRUNPARAM=T,gr bin/coqtop -compile file.v
+
+In another terminal:
+
+pkill -SIGUSR1 $COQTOPPID
+...
+pkill -SIGUSR1 $COQTOPPID
+ocaml dev/decodegraph.ml edge.$COQTOPPID.$N bin/coqtop > memory.dot
+dot -Tpdf -o memory.pdf memory.dot
+
+where $COQTOPPID is coqtop pid and $N the index of the call to pkill.
+
+The pdf produced by the last command gives a compact graphical representation of
+the various objects allocated.