Stepping through a rocq script programatically?

Using Rocq
1

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 !

2

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 . At last Rocq’n’share, there was also a presentation of GitHub - SkyLabsAI/rocq-agent-toolkit: Agent infrastructure for Rocq · GitHub, which is not an MCP but provides similar programmatic tooling for interacting with Rocq scripts.