# Debugging Fixpoint execution

**URL:** <https://discourse.rocq-prover.org/t/debugging-fixpoint-execution/183>\
**Category:** Using Rocq\
**Created:** [March 3, 2019, 6:24pm UTC](https://discourse.rocq-prover.org/t/debugging-fixpoint-execution/183 "2019-03-03T18:24:16Z")\
**Posts on this page:** 5\
**Page:** 1

<div class="post-metadata">

**Author:** ![Lys](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/lys/32/48_2.png) [@Lys](https://discourse.rocq-prover.org/u/Lys)\
**Post date:** [March 3, 2019, 6:24pm UTC](https://discourse.rocq-prover.org/t/debugging-fixpoint-execution/183/1 "2019-03-03T18:24:16Z")

</div>

Say that I wrote a Fixpoint function but didn’t Compute as expected, and hope to locate the bug by dumping the call stack. Is there a convenient way to print arguments during execution?

---

<div class="post-metadata">

**Author:** ![JasonGross](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/jasongross/32/32_2.png) [@JasonGross](https://discourse.rocq-prover.org/u/JasonGross)\
**Post date:** [March 4, 2019, 5:20pm UTC](https://discourse.rocq-prover.org/t/debugging-fixpoint-execution/183/2 "2019-03-04T17:20:13Z")

</div>

After some searching, there is [this merged PR (#714)](https://github.com/coq/coq/pull/714), a continuation [of the unmerged #85](https://github.com/coq/coq/pull/85), which adds support for [the reduction effects plugin](https://github.com/herbelin/reduction-effects) (which is not yet available on opam; I have submitted [an issue](https://github.com/herbelin/reduction-effects/issues/1)).

Quoting Hugo (the plugin author):

> Currently, this [plugin] provides a generic `print` of type `forall A, A -> unit` which prints its second argument and a generic `print_id` of type `forall A, A -> A` which also prints its second argument.

Note that these functions print their arguments when reduced.

---

<div class="post-metadata">

**Author:** ![Lys](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/lys/32/48_2.png) [@Lys](https://discourse.rocq-prover.org/u/Lys)\
**Post date:** [March 6, 2019, 4:13pm UTC](https://discourse.rocq-prover.org/t/debugging-fixpoint-execution/183/3 "2019-03-06T16:13:43Z")

</div>

Have you got an example that runs properly? My fork compiles but doesn’t print.

> <https://github.com/herbelin/reduction-effects/pull/2#issuecomment-469968428>

  
Update: printing now works properly, but compilation does not.

---

<div class="post-metadata">

**Author:** ![JasonGross](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/jasongross/32/32_2.png) [@JasonGross](https://discourse.rocq-prover.org/u/JasonGross)\
**Post date:** [March 6, 2019, 4:52pm UTC](https://discourse.rocq-prover.org/t/debugging-fixpoint-execution/183/4 "2019-03-06T16:52:58Z")

</div>

I’ve never actually used the plugin. I’d suggest checking out the version of Coq right after [#714](https://github.com/coq/coq/pull/714) was merged, and building that Coq and building the plugin with that Coq, and seeing if it works there. If it does, then you can bisect Coq (or just report a regression on the Coq issue tracker). If it doesn’t, then we probably need to summon @herbelin for help / explanation.

---

<div class="post-metadata">

**Author:** ![Lys](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/lys/32/48_2.png) [@Lys](https://discourse.rocq-prover.org/u/Lys)\
**Post date:** [May 4, 2019, 7:28pm UTC](https://discourse.rocq-prover.org/t/debugging-fixpoint-execution/183/5 "2019-05-04T19:28:44Z")

</div>

To close up this thread: the plugin is now available via OPAM as `coq-reduction-effects`.  
Here’s an example of using it:

> <https://github.com/coq-community/reduction-effects/blob/master/tests/PrintEffect.v>