Register | Log in

coq

proof assistant for higher-order logic (toplevel and compiler)

Choose email to subscribe with

general

source: coq (main)
version: 9.2.0+dfsg-3
maintainer: Debian OCaml Maintainers (archive) (DMD)
uploaders: Ralf Treinen [DMD] – Stéphane Glondu [DMD] – Julien Puydt [DMD]
arch: any
std-ver: 4.7.4
VCS: Git (Browse, QA)

versions [more versions can be listed by madison] [old versions available from snapshot.debian.org]

[pool directory]

o-o-stable: 8.12.0-3
oldstable: 8.16.1+dfsg-1
stable: 8.20.1+dfsg-1
testing: 9.2.0+dfsg-3
unstable: 9.2.0+dfsg-4

versioned links

8.12.0-3: [.dsc, use dget on this link to retrieve source package] [changelog] [copyright] [rules] [control]
8.16.1+dfsg-1: [.dsc, use dget on this link to retrieve source package] [changelog] [copyright] [rules] [control]
8.20.1+dfsg-1: [.dsc, use dget on this link to retrieve source package] [changelog] [copyright] [rules] [control]
9.2.0+dfsg-3: [.dsc, use dget on this link to retrieve source package] [changelog] [copyright] [rules] [control]
9.2.0+dfsg-4: [.dsc, use dget on this link to retrieve source package] [changelog] [copyright] [rules] [control]

binaries

coq
libcoq-core
libcoq-core-ocaml
libcoq-core-ocaml-dev
rocqide

action needed

debian/patches: 1 patch with invalid metadata high

Among the 5 debian patches available in version 9.2.0+dfsg-3 of the package, we noticed the following issues:

1 patch with invalid metadata that ought to be fixed.

Created: 2026-07-28 Last update: 2026-07-28 10:02

AppStream hints: 1 warning for rocqide normal

AppStream found metadata issues for packages:

rocqide: 1 warning

You should get rid of them to provide more metadata about this software.

Created: 2020-01-25 Last update: 2026-07-23 05:00

testing migrations

excuses:
- Migration status for coq (9.2.0+dfsg-3 to 9.2.0+dfsg-4): BLOCKED: Rejected/violates migration policy/introduces a regression
- Issues preventing migration:
- ∙ ∙ Autopkgtest for coq/9.2.0+dfsg-4: amd64: Pass, arm64: Test triggered, armhf: Pass, i386: Test triggered, loong64: Test triggered, ppc64el: Test triggered, s390x: Test triggered
- ∙ ∙ Autopkgtest for coq-bignums/9.0.0+rocq9.2-3: amd64: Regression ♻ (reference ♻), arm64: Test triggered, ppc64el: Test triggered, s390x: Test triggered
- ∙ ∙ Autopkgtest for coq-dpdgraph/1.0+9.1-2: amd64: Regression ♻ (reference ♻), arm64: Test triggered, ppc64el: Test triggered, s390x: Test triggered
- ∙ ∙ Autopkgtest for coq-equations/1.3.2-9.2-2: amd64: Regression ♻ (reference ♻), arm64: Test triggered, ppc64el: Test triggered, s390x: Test triggered
- ∙ ∙ Autopkgtest for coq-ext-lib/0.13.1-2: amd64: Regression ♻ (reference ♻), arm64: Test triggered, armhf: Pass, i386: Test triggered, loong64: Test triggered, ppc64el: Test triggered, s390x: Test triggered
- ∙ ∙ Autopkgtest for coq-gappa/1.11.0-1: amd64: Regression ♻ (reference ♻), arm64: Test triggered, ppc64el: Test triggered, s390x: Test triggered
- ∙ ∙ Autopkgtest for coq-hammer/1.3.3+9.2-2: amd64: Regression ♻ (reference ♻), arm64: Test triggered, ppc64el: Test triggered, s390x: Test triggered
- ∙ ∙ Autopkgtest for coq-hott/9.1-2: amd64: Regression ♻ (reference ♻), arm64: Test triggered, armhf: Pass, i386: Test triggered, loong64: Test triggered, ppc64el: Test triggered, s390x: Test triggered
- ∙ ∙ Autopkgtest for coq-iris/4.5.0-2: amd64: Regression ♻ (reference ♻), arm64: Test triggered, armhf: Pass, i386: Test triggered, loong64: Test triggered, ppc64el: Test triggered, s390x: Test triggered
- ∙ ∙ Autopkgtest for coq-libhyps/5.0.0-2: amd64: Regression ♻ (reference ♻), arm64: Test triggered, armhf: Pass, i386: Test triggered, loong64: Test triggered, ppc64el: Test triggered, s390x: Test triggered
- ∙ ∙ Autopkgtest for coq-math-classes/9.2.0-1: amd64: Regression ♻ (reference ♻), arm64: Test triggered, ppc64el: Test triggered, s390x: Test triggered
- ∙ ∙ Autopkgtest for coq-menhirlib/20260209+ds-2: amd64: Regression ♻ (reference ♻), arm64: Test triggered, armhf: Pass, i386: Test triggered, loong64: Test triggered, ppc64el: Test triggered, s390x: Test triggered
- ∙ ∙ Autopkgtest for coq-mtac2/1.4-rocq9.1-2: amd64: Regression ♻ (reference ♻), arm64: Test triggered, ppc64el: Test triggered, s390x: Test triggered
- ∙ ∙ Autopkgtest for coq-record-update/0.3.7-3: amd64: Regression ♻ (reference ♻), arm64: Test triggered, armhf: Pass, i386: Test triggered, loong64: Test triggered, ppc64el: Test triggered, s390x: Test triggered
- ∙ ∙ Autopkgtest for coq-reduction-effects/0.1.6-4: amd64: Regression ♻ (reference ♻), arm64: Test triggered, ppc64el: Test triggered, s390x: Test triggered
- ∙ ∙ Autopkgtest for coq-simple-io/1.11.0-5: amd64: Reference test triggered, but real test failed already ♻, arm64: Test triggered, armhf: Pass, i386: Test triggered, loong64: Test triggered, ppc64el: Test triggered, s390x: Test triggered
- ∙ ∙ Autopkgtest for coq-stdpp/1.13.0-2: amd64: Regression ♻ (reference ♻), arm64: Test triggered, armhf: Pass, i386: Test triggered, loong64: Test triggered, ppc64el: Test triggered, s390x: Test triggered
- ∙ ∙ Autopkgtest for coq-unicoq/1.6-9.1-2: amd64: Regression ♻ (reference ♻), arm64: Test triggered, ppc64el: Test triggered, s390x: Test triggered
- ∙ ∙ Autopkgtest for coq-unimath/20260603-2: amd64: Regression ♻ (reference ♻), arm64: Test triggered, armhf: Pass, i386: Test triggered, ppc64el: Test triggered, s390x: Test triggered
- ∙ ∙ Autopkgtest for coqprime/8.20.1-5: amd64: Regression ♻ (reference ♻), arm64: Test triggered, ppc64el: Test triggered, s390x: Test triggered
- ∙ ∙ Autopkgtest for flocq/4.2.2-2: amd64: Regression ♻ (reference ♻), arm64: Test triggered, armhf: Pass, i386: Test triggered, loong64: Test triggered, ppc64el: Test triggered, s390x: Test triggered
- ∙ ∙ Autopkgtest for ott/0.34+ds-5: amd64: Regression ♻ (reference ♻), arm64: Test triggered, ppc64el: Test triggered, s390x: Test triggered
- ∙ ∙ Missing build on riscv64
- ∙ ∙ Piuparts check waiting for test results - https://piuparts.debian.org/sid/source/c/coq.html
- ∙ ∙ Autopkgtest deferred on riscv64: missing arch:riscv64 build
- ∙ ∙ Lintian check waiting for test results - info
- ∙ ∙ Reproducibility check waiting for results on arm64 - info
- ∙ ∙ Reproducibility check waiting for results on armhf - info
- ∙ ∙ Reproducibility check waiting for results on i386 - info
- ∙ ∙ Too young, only 0 of 5 days old
- Additional info (not blocking):
- ∙ ∙ Not reproduced on amd64 (not a regression): coq, libcoq-core-ocaml, libcoq-core-ocaml-dev
- Not considered

news

[2026-08-25] Accepted coq 9.2.0+dfsg-4 (source) into unstable (Stéphane Glondu)
[2026-08-10] coq 9.2.0+dfsg-3 MIGRATED to testing (Debian testing watch)
[2026-07-27] Accepted coq 9.2.0+dfsg-3 (source amd64) into unstable (Julien Puydt)
[2026-07-21] Accepted coq 9.2.0+dfsg-2 (source amd64) into unstable (Julien Puydt)
[2026-07-10] Accepted coq 9.2.0+dfsg-1 (source amd64) into experimental (Julien Puydt)
[2025-11-11] Accepted coq 9.1.0+dfsg-3 (source amd64) into experimental (Julien Puydt)
[2025-10-29] Accepted coq 9.1.0+dfsg-2 (source amd64) into experimental (Julien Puydt)
[2025-09-21] Accepted coq 9.1.0+dfsg-1 (source amd64) into experimental (Debian FTP Masters) (signed by: Julien Puydt)
[2025-02-26] coq 8.20.1+dfsg-1 MIGRATED to testing (Debian testing watch)
[2025-02-17] Accepted coq 8.20.1+dfsg-1 (source) into unstable (Julien Puydt)
[2024-11-29] coq 8.20.0+dfsg-1 MIGRATED to testing (Debian testing watch)
[2024-11-20] Accepted coq 8.20.0+dfsg-1 (source) into unstable (Julien Puydt)
[2024-09-05] coq 8.19.1+dfsg-3 MIGRATED to testing (Debian testing watch)
[2024-08-17] coq REMOVED from testing (Debian testing watch)
[2024-08-03] Accepted coq 8.19.1+dfsg-3 (source) into unstable (Stéphane Glondu)
[2024-06-24] coq 8.19.1+dfsg-2 MIGRATED to testing (Debian testing watch)
[2024-06-15] Accepted coq 8.19.1+dfsg-2 (source) into unstable (Stéphane Glondu)
[2024-04-26] Accepted coq 8.19.1+dfsg-1 (source) into unstable (Julien Puydt)
[2024-01-23] coq 8.18.0+dfsg-1 MIGRATED to testing (Debian testing watch)
[2023-12-21] Accepted coq 8.18.0+dfsg-1 (source) into unstable (Julien Puydt)
[2023-06-24] coq 8.17.0+dfsg-1 MIGRATED to testing (Debian testing watch)
[2023-06-12] Accepted coq 8.17.0+dfsg-1 (source) into unstable (Julien Puydt)
[2022-12-02] coq 8.16.1+dfsg-1 MIGRATED to testing (Debian testing watch)
[2022-12-02] coq 8.16.1+dfsg-1 MIGRATED to testing (Debian testing watch)
[2022-11-29] Accepted coq 8.16.1+dfsg-1 (source) into unstable (Julien Puydt)
[2022-09-17] coq 8.16.0+dfsg-1 MIGRATED to testing (Debian testing watch)
[2022-09-06] Accepted coq 8.16.0+dfsg-1 (source) into unstable (Julien Puydt)
[2022-07-10] coq 8.15.2+dfsg-2 MIGRATED to testing (Debian testing watch)
[2022-06-11] Accepted coq 8.15.2+dfsg-2 (source) into unstable (Julien Puydt)
[2022-05-31] Accepted coq 8.15.2+dfsg-1 (source) into unstable (Julien Puydt)

1
2

bugs [bug history graph]

all: 2
RC: 0
I&N: 1
M&W: 1
F&P: 0
patch: 0

links

homepage
buildd: logs, reproducibility, cross
popcon
browse source code
other distros
debian patches
debci

ubuntu

[Information about Ubuntu for Debian Developers]

version: 8.20.1+dfsg-1build4

Debian Package Tracker — Copyright 2013-2025 The Distro Tracker Developers

Report problems to the tracker.debian.org pseudo-package in the Debian BTS.

Documentation — Bugs — Git Repository — Contributing