package rocqide

  1. Overview
  2. No Docs
The Rocq Prover --- GTK3 IDE

Install 

dune-project
 Dependency

rocq-prover.org Edit opam file Versions (5)

Authors

  1. T
    The Rocq development team, INRIA, CNRS, and contributors

Maintainers

  1. T
    The Rocq development team <rocq+rocq-development@discoursemail.com>

Sources

rocq-9.2.0.tar.gz
sha256=a45280ab4fbaac7540b136a6b073b4a6db15739ec1e149bded43fa6f4fc25f20

Description

The Rocq Prover 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 RocqIDE, a graphical user interface for the development of interactive proofs.

Published: 02 Apr 2026

Dependencies (7)

  1. lablgtk3-sourceview3 >= "3.1.2" & (>= "3.1.5" | os-family != "windows")
  2. cairo2 >= "0.6.4"
  3. coqide-server = version
  4. conf-adwaita-icon-theme
  5. conf-findutils build
  6. ocamlfind build
  7. dune >= "3.8"

Dev Dependencies (1)

  1. odoc with-doc

Used by

None

Conflicts

None