package rocqide

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

Install 

dune-project
 Dependency

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

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.1.1.tar.gz
sha256=35cd03fc4193969b1cce01190340e5c129c1ba8f02242a9e6dff4b83be118759

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: 23 Feb 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