Debugging Fixpoint execution

Using Coq
1

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?

2

After some searching, there is this merged PR (#714), a continuation of the unmerged #85, which adds support for the reduction effects plugin (which is not yet available on opam; I have submitted an issue).

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.

2 Likes
3

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


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

4

I’ve never actually used the plugin. I’d suggest checking out the version of Coq right after #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.

5

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

1 Like