Rocq is an interactive theorem prover, or proof assistant. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive development of machine-checked proofs.

This package provides the coqidetop language server, an implementation of Rocq's XML protocol which allows clients, such as RocqIDE, to interact with the Rocq Prover in a structured way.