# Stepping through a rocq script programatically?

**URL:** <https://discourse.rocq-prover.org/t/stepping-through-a-rocq-script-programatically/3070>\
**Category:** Using Rocq\
**Created:** [July 9, 2026, 10:45am UTC](https://discourse.rocq-prover.org/t/stepping-through-a-rocq-script-programatically/3070 "2026-07-09T10:45:26Z")\
**Posts on this page:** 2\
**Page:** 1

<div class="post-metadata">

**Author:** ![NyuB](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/nyub/32/1280_2.png) [@NyuB](https://discourse.rocq-prover.org/u/NyuB)\
**Post date:** [July 9, 2026, 10:45am UTC](https://discourse.rocq-prover.org/t/stepping-through-a-rocq-script-programatically/3070/1 "2026-07-09T10:45:26Z")

</div>

Hi, I would like to drive the execution of a rocq file programatically (ideally from OCaml but anything would do), and being able to observe the sate at each anytime, like proof goal hypthesis etc. Basically what the rocq-lsp allows to do within the IDE.

I’m a bit lost between the available options, as I feel most of them can do much more than what I’m looking for and thus seem a bit rough to use. Use the full rocq-lsp even though the goal is much simpler than interactive editing ? Find an entrypoint in the low-level coq OCAml API and work my way up ? Use Fleche ? Petanque ? Pytanque ?

If anyone here has encountered the same prolem I would be curious about the chosen option.

Thanks !

---

<div class="post-metadata">

**Author:** ![Zimmi48](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/zimmi48/32/7_2.png) [@Zimmi48](https://discourse.rocq-prover.org/u/Zimmi48)\
**Post date:** [July 10, 2026, 10:47am UTC](https://discourse.rocq-prover.org/t/stepping-through-a-rocq-script-programatically/3070/2 "2026-07-10T10:47:08Z")

</div>

Even if your personal goal might not be AI-related, what you are looking to do seems to require the same kind of tools that people doing AI with Rocq need. So it might be worth looking into MCP implementations. A new one was recently discussed on [Public view of The Rocq Prover | Zulip team chat](https://rocq-prover.zulipchat.com/#narrow/channel/252087-Machine-learning-and-automation/topic/an.20AI-native.20MCP.20server.20for.20Rocq) . At last Rocq’n’share, there was also a presentation of [GitHub - SkyLabsAI/rocq-agent-toolkit: Agent infrastructure for Rocq · GitHub](https://github.com/SkylabsAI/rocq-agent-toolkit), which is not an MCP but provides similar programmatic tooling for interacting with Rocq scripts.