Merge PR #6497: Add optimize_heap tactic for #6488

6 files changed, 41 insertions, 4 deletions

diff --git a/CHANGES b/CHANGES
index cbaa2c5e2..ead751147 100644
--- a/CHANGES
+++ b/CHANGES
@@ -37,6 +37,9 @@ Tactics
 - Added tactics reset ltac profile, show ltac profile (and variants)
 - Added tactics restart_timer, finish_timing, and time_constr as an
   experimental way of timing Ltac's evaluation phase
+- Added tactic optimize_heap, analogous to the Vernacular Optimize
+  Heap, which performs a major garbage collection and heap compaction
+  in the OCaml run-time system.
 
 Vernacular Commands
 
diff --git a/doc/refman/RefMan-ltac.tex b/doc/refman/RefMan-ltac.tex
index ef0f4af8f..c4c0435c5 100644
--- a/doc/refman/RefMan-ltac.tex
+++ b/doc/refman/RefMan-ltac.tex
@@ -1426,6 +1426,16 @@ You can also pass the {\tt -profile-ltac} command line option to {\tt coqc}, whi
 
 Note that the profiler currently does not handle backtracking into multi-success tactics, and issues a warning to this effect in many cases when such backtracking occurs.
 
+\subsection[Run-time optimization tactic]{Run-time optimization tactic\label{tactic-optimizeheap}}.
+
+The following tactic behaves like {\tt idtac}, and running it compacts the heap in the
+OCaml run-time system. It is analogous to the Vernacular command {\tt Optimize Heap} (see~\ref{vernac-optimizeheap}).
+
+\tacindex{optimize\_heap}
+\begin{quote}
+{\tt optimize\_heap}.
+\end{quote}
+
 \endinput
 
 \subsection{Permutation on closed lists}
diff --git a/doc/refman/RefMan-pro.tex b/doc/refman/RefMan-pro.tex
index 1d3311edc..3d4c885b3 100644
--- a/doc/refman/RefMan-pro.tex
+++ b/doc/refman/RefMan-pro.tex
@@ -555,12 +555,12 @@ used to force Coq to optimize some of its internal data structures.
 This command forces Coq to shrink the data structure used to represent
 the ongoing proof.
 
-\subsection[\tt Optimize Heap.]{\tt Optimize Heap.}
+\subsection[\tt Optimize Heap.]{\tt Optimize Heap.\label{vernac-optimizeheap}}
 
 This command forces the OCaml runtime to perform a heap compaction.
-This is in general an expensive operation.  See:
-  \url{http://caml.inria.fr/pub/docs/manual-ocaml/libref/Gc.html#VALcompact}
-
+This is in general an expensive operation.  See: \\
+\ \url{http://caml.inria.fr/pub/docs/manual-ocaml/libref/Gc.html#VALcompact} \\
+There is also an analogous tactic {\tt optimize\_heap} (see~\ref{tactic-optimizeheap}).
 
 %%% Local Variables: 
 %%% mode: latex
diff --git a/plugins/ltac/extratactics.ml4 b/plugins/ltac/extratactics.ml4
index cf5125757..3e3965b94 100644
--- a/plugins/ltac/extratactics.ml4
+++ b/plugins/ltac/extratactics.ml4
@@ -1125,3 +1125,12 @@ VERNAC COMMAND EXTEND OptimizeProof
 | [ "Optimize" "Heap" ] => [ Vernac_classifier.classify_as_proofstep ] ->
   [ Gc.compact () ]
 END
+
+(** tactic analogous to "OPTIMIZE HEAP" *)
+
+let tclOPTIMIZE_HEAP =
+  Proofview.tclLIFT (Proofview.NonLogical.make (fun () -> Gc.compact ()))
+
+TACTIC EXTEND optimize_heap
+| [ "optimize_heap" ] -> [ tclOPTIMIZE_HEAP ]
+END
diff --git a/test-suite/output/optimize_heap.out b/test-suite/output/optimize_heap.out
new file mode 100644
index 000000000..94a0b1911
--- /dev/null
+++ b/test-suite/output/optimize_heap.out
@@ -0,0 +1,8 @@
+1 subgoal
+  
+  ============================
+  True
+1 subgoal
+  
+  ============================
+  True
diff --git a/test-suite/output/optimize_heap.v b/test-suite/output/optimize_heap.v
new file mode 100644
index 000000000..e566bd7ba
--- /dev/null
+++ b/test-suite/output/optimize_heap.v
@@ -0,0 +1,7 @@
+(* optimize_heap should not affect the proof state *)
+
+Goal True.
+  idtac.
+  Show.
+  optimize_heap.
+  Show.