2 files changed, 108 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/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.