Coq Interactive Theorem Prover

Coq Interactive Theorem Prover

Coq Development Team (coq-team) Publisher

Install latest/stable of Coq Interactive Theorem Prover

Ubuntu 16.04 or later?

Make sure snap support is enabled in your Desktop store.

Install using the command line

sudo snap install coq-prover

Don't have snapd? Get set up for snaps.

Channel Version Published

Coq and its Platform

The Coq interactive prover 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 snap contains the Coq prover version 8.13.2 along with CoqIDE and the following packages:

  • aac-tactics: Coq plugin providing tactics for rewriting universally quantified equations, modulo associative (and possibly commutative) operators (version: 8.13.0, license: LGPL-3.0-or-later)
  • bignums: Bignums, the Coq library of arbitrary large numbers (version: 8.13.0, license: LGPL-2.1-only)
  • compcert: The CompCert C compiler (64 bit) (version: 3.8, license: INRIA Non-Commercial License Agreement)
  • coquelicot: A Coq formalization of real analysis compatible with the standard library (version: 3.1.0, license: LGPL-3.0-or-later)
  • elpi: Elpi extension language for Coq (version: 1.8.1, license: LGPL-2.1-or-later)
  • equations: A function definition package for Coq (version: 1.2.3+8.13, license: LGPL-2.1-or-later)
  • ext-lib: A library of Coq definitions, theorems, and tactics (version: 0.11.3, license: BSD-2-Clause-FreeBSD)
  • flocq: A formalization of floating-point arithmetic for the Coq system (version: 3.3.1, license: LGPL-3.0-or-later)
  • gappa: A Coq tactic for discharging goals about floating-point arithmetic and round-off errors using the Gappa prover (version: 1.4.6, license: LGPL-3.0-or-later)
  • hierarchy-builder: High level commands to declare and evolve a hierarchy based on packed classes (version: 1.0.0, license: MIT)
  • hott: The Homotopy Type Theory library (version: 8.13, license: BSD-2-Clause)
  • interval: A Coq tactic for proving bounds on real-valued expressions automatically (version: 4.1.1, license: CeCILL-C)
  • mathcomp-algebra: Mathematical Components Library on Algebra (version: 1.12.0, license: CECILL-B)
  • mathcomp-bigenough: A small library to do epsilon - N reasonning (version: 1.0.0, license: CeCILL-B)
  • mathcomp-character: Mathematical Components Library on character theory (version: 1.12.0, license: CECILL-B)
  • mathcomp-field: Mathematical Components Library on Fields (version: 1.12.0, license: CECILL-B)
  • mathcomp-fingroup: Mathematical Components Library on finite groups (version: 1.12.0, license: CECILL-B)
  • mathcomp-finmap: Finite sets, finite maps, finitely supported functions (version: 1.5.1, license: CECILL-B)
  • mathcomp-real-closed: Mathematical Components Library on real closed fields (version: 1.1.2, license: CECILL-B)
  • mathcomp-solvable: Mathematical Components Library on finite groups (II) (version: 1.12.0, license: CECILL-B)
  • mathcomp-ssreflect: Small Scale Reflection (version: 1.12.0, license: CECILL-B)
  • menhirlib: A support library for verified Coq parsers produced by Menhir (version: 20200624, license: LGPL-3.0-or-later)
  • mtac2: Mtac2: Typed Tactics for Coq (version: 1.4+8.13, license: MIT)
  • quickchick: Randomized Property-Based Testing Plugin for Coq (version: 1.5.0, license: MIT)
  • simple-io: IO monad for Coq (version: 1.5.0, license: MIT)
  • unicoq: An enhanced unification algorithm for Coq (version: 1.5+8.13, license: MIT)
  • vst: Verified Software Toolchain (version: 2.7.1, license:

Developer website

Contact Coq Development Team

Details for Coq Interactive Theorem Prover

Last updated
9 April 2021

Share this snap

Generate an embeddable card to be shared on external websites.

Related blog posts

Where people are using Coq Interactive Theorem Prover

Users by distribution (log)

Ubuntu 20.04
Ubuntu 18.04
Ubuntu 21.04
Debian 10
Ubuntu 20.10
pop 21.04
Ubuntu 16.04
Linux Mint 20.1
Ubuntu 21.10
Linux Mint 19.3
Debian 11
pop 20.04

Install Coq Interactive Theorem Prover on your Linux distribution

Choose your Linux distribution to get detailed installation instructions. If yours is not shown, get more details on the installing snapd documentation.

Is there a problem with Coq Interactive Theorem Prover? Report this app