Fabre

#1128188 libcoq-stdlib lacks dependencies #1128188

Package:: src:rocq-stdlib

Source:: src:rocq-stdlib

Submitter:: Adrian Bunk

Date:: 2026-07-22 18:35:03 UTC

Severity:: normal

Tags:

#1128188#5

Date:: 2026-02-16 08:37:01 UTC

From:

To:

https://buildd.debian.org/status/fetch.php?pkg=aac-tactics&arch=ppc64&ver=9.0.0-1&stamp=1761723185&raw=0

...
Unpacking coq (9.1.0+dfsg-1~ppc64) ...
...
Unpacking libcoq-stdlib (8.19.1+dfsg-3) ...
...

libcoq-stdlib needs automatic generation of some OCaml/Coq dependencies.


Technically the lack of dependencies is not a new bug, but when
libcoq-stdlib was built from src:coq the dependencies of the coq
binary package at least ensured that libcoq-stdlib was rebuilt
when necessary. Currently this causes FTBFS in rdeps when the
Provides of coq changes.

#1128188#16

Date:: 2026-07-22 18:33:56 UTC

From:

To:

We believe that the bug you reported is fixed in the latest version of
rocq-stdlib, which is due to be installed in the Debian FTP archive.

A summary of the changes between this version and the previous one is
attached.

Thank you for reporting the bug, which will now be closed.  If you
have further comments please address them to 1128188@bugs.debian.org,
and the maintainer will reopen the bug report if appropriate.

Debian distribution maintenance software
pp.
Julien Puydt <jpuydt@debian.org> (supplier of updated rocq-stdlib package)

(This message was generated automatically at their request; if you
believe that there is a problem with it please contact the archive
administrators by mailing ftpmaster@ftp-master.debian.org)
Format: 1.8
Date: Wed, 22 Jul 2026 20:00:28 +0200
Source: rocq-stdlib
Binary: libcoq-stdlib
Architecture: source amd64
Version: 9.1.0-2
Distribution: unstable
Urgency: medium
Maintainer: Julien Puydt <jpuydt@debian.org>
Changed-By: Julien Puydt <jpuydt@debian.org>
Description:
 libcoq-stdlib - Standard library for the Rocq Theorem Prover
Closes: 1128188 1141880
Changes:
 rocq-stdlib (9.1.0-2) unstable; urgency=medium
 .
   * Add missing dep on libcoq-stdlib (Closes: #1141880).
   * Fix depends (Closes: #1128188).
Checksums-Sha1:
 f2a9b3d81db3a8b07db0e6ead8e3a4883eeba80a 2030 rocq-stdlib_9.1.0-2.dsc
 a92b88f0ea5d7ab4f7c3533691d6f2eaad476acd 1864765 rocq-stdlib_9.1.0.orig.tar.gz
 6acb5968e111845ac2139935f676245c5da23ebc 2432 rocq-stdlib_9.1.0-2.debian.tar.xz
 0916a8bdea9467f6a000eed7dbcde1a685d92d03 20078312 libcoq-stdlib_9.1.0-2_amd64.deb
 ef96ce6aab935c64d7d3592cbc7f3210abae3e95 6787 rocq-stdlib_9.1.0-2_amd64.buildinfo
Checksums-Sha256:
 1ccc2b270802b85ddb51f9784d893647040ba7bdea40700d82159a4516696af3 2030 rocq-stdlib_9.1.0-2.dsc
 4ddeaa7ebb580780d34f655834ef6c0daa64a2b07f930056976866862fb1f76f 1864765 rocq-stdlib_9.1.0.orig.tar.gz
 df3bb0e9afa3d1cb39f690577bdd5080859b0dbddc59027a16594a75e49f02fb 2432 rocq-stdlib_9.1.0-2.debian.tar.xz
 9819c325d808363fa32d5cec7ceda2158249cc72c28afee65916cba7f9b308a5 20078312 libcoq-stdlib_9.1.0-2_amd64.deb
 2449ec02e75d4def86e80962ca78104393d2bb587fab8f13bb19ae98f4df4c81 6787 rocq-stdlib_9.1.0-2_amd64.buildinfo
Files:
 d56380051598d7484b3ac24a127302f2 2030 math optional rocq-stdlib_9.1.0-2.dsc
 a8b0043d624e8bb44d46d22e741f329c 1864765 math optional rocq-stdlib_9.1.0.orig.tar.gz
 68dca703196537db9190c9c43f531fea 2432 math optional rocq-stdlib_9.1.0-2.debian.tar.xz
 910e9c610a06775257248dec14b604c6 20078312 math optional libcoq-stdlib_9.1.0-2_amd64.deb
 f00fce37207f325906d42f7d4c6a4d16 6787 math optional rocq-stdlib_9.1.0-2_amd64.buildinfo
-----BEGIN PGP SIGNATURE-----

iQJNBAEBCgA3FiEEgS7v2KP7pKzk3xFLBMU71/4DBVEFAmphCC4ZHGp1bGllbi5w
dXlkdEBsYXBvc3RlLm5ldAAKCRAExTvX/gMFUY1LEACIBTb4Kc8FmzMssa9SQVy/
dj5kshLfcNw/4q7yHUZZps9pdMZWVZ7/XhWkebP5e4btqG74tSf9xI1mO69ZMjNz
dI325GcRJKbBpLCn0uJgbiDSZasE1HAwiqafh0KSfN7VE+U/HCkGVZ4bOpU+j31I
R26glZ5iqEtpnN70nDWheQzijTxEa+y6EJOUieWiVWJO4RDSL6qGOs7yZB9kyiaw
DDb8mg4lAXt6IcjRuu++TGRYJcK7mPA36TUto7tlmyjmszFq7rHzT/OSWyQ4OnJq
313LGmaRZOz/c/lw1UWqHbQ4I0NqJLXFGnSGiadSC/s38WCTnc2XvA7gQneWo6E8
DhbQmQUj2depW8gDH0Pj+TwG5h4N1iFf1bOfYd3K0csNLNbEY+SGl59NfmIcGw13
cf/P2ZwQfyTaGGZzR9xutuDCKa9jmmRM/r3b7F5Tsq0/5EF1ttLW63g1VAcHvpNt
3qTZsVA45ZOYuL+Su650gLIIjYrV0KXQkdc13zoXv1cZyVMmnsF9rWCiIKkA1veF
oZMFMNv+f3jluH6QhcAlha6Xau4J8x98lUVIvJhtPd2pBzatkZQidsNqtOiu0wxU
FVBAwmk22eZS9th/0TMGlPFmR2JctLTCfilhMC/rlxgtrbuVX9KtM6cgOCFcNK0X
JWiemhRR5vqZ0L6/vIjDyw==
=ny1u
-----END PGP SIGNATURE-----

#1128188#21

Date:: 2026-07-22 18:33:56 UTC

From:

To:

We believe that the bug you reported is fixed in the latest version of
rocq-stdlib, which is due to be installed in the Debian FTP archive.

A summary of the changes between this version and the previous one is
attached.

Thank you for reporting the bug, which will now be closed.  If you
have further comments please address them to 1141880@bugs.debian.org,
and the maintainer will reopen the bug report if appropriate.

Debian distribution maintenance software
pp.
Julien Puydt <jpuydt@debian.org> (supplier of updated rocq-stdlib package)

(This message was generated automatically at their request; if you
believe that there is a problem with it please contact the archive
administrators by mailing ftpmaster@ftp-master.debian.org)
Format: 1.8
Date: Wed, 22 Jul 2026 20:00:28 +0200
Source: rocq-stdlib
Binary: libcoq-stdlib
Architecture: source amd64
Version: 9.1.0-2
Distribution: unstable
Urgency: medium
Maintainer: Julien Puydt <jpuydt@debian.org>
Changed-By: Julien Puydt <jpuydt@debian.org>
Description:
 libcoq-stdlib - Standard library for the Rocq Theorem Prover
Closes: 1128188 1141880
Changes:
 rocq-stdlib (9.1.0-2) unstable; urgency=medium
 .
   * Add missing dep on libcoq-stdlib (Closes: #1141880).
   * Fix depends (Closes: #1128188).
Checksums-Sha1:
 f2a9b3d81db3a8b07db0e6ead8e3a4883eeba80a 2030 rocq-stdlib_9.1.0-2.dsc
 a92b88f0ea5d7ab4f7c3533691d6f2eaad476acd 1864765 rocq-stdlib_9.1.0.orig.tar.gz
 6acb5968e111845ac2139935f676245c5da23ebc 2432 rocq-stdlib_9.1.0-2.debian.tar.xz
 0916a8bdea9467f6a000eed7dbcde1a685d92d03 20078312 libcoq-stdlib_9.1.0-2_amd64.deb
 ef96ce6aab935c64d7d3592cbc7f3210abae3e95 6787 rocq-stdlib_9.1.0-2_amd64.buildinfo
Checksums-Sha256:
 1ccc2b270802b85ddb51f9784d893647040ba7bdea40700d82159a4516696af3 2030 rocq-stdlib_9.1.0-2.dsc
 4ddeaa7ebb580780d34f655834ef6c0daa64a2b07f930056976866862fb1f76f 1864765 rocq-stdlib_9.1.0.orig.tar.gz
 df3bb0e9afa3d1cb39f690577bdd5080859b0dbddc59027a16594a75e49f02fb 2432 rocq-stdlib_9.1.0-2.debian.tar.xz
 9819c325d808363fa32d5cec7ceda2158249cc72c28afee65916cba7f9b308a5 20078312 libcoq-stdlib_9.1.0-2_amd64.deb
 2449ec02e75d4def86e80962ca78104393d2bb587fab8f13bb19ae98f4df4c81 6787 rocq-stdlib_9.1.0-2_amd64.buildinfo
Files:
 d56380051598d7484b3ac24a127302f2 2030 math optional rocq-stdlib_9.1.0-2.dsc
 a8b0043d624e8bb44d46d22e741f329c 1864765 math optional rocq-stdlib_9.1.0.orig.tar.gz
 68dca703196537db9190c9c43f531fea 2432 math optional rocq-stdlib_9.1.0-2.debian.tar.xz
 910e9c610a06775257248dec14b604c6 20078312 math optional libcoq-stdlib_9.1.0-2_amd64.deb
 f00fce37207f325906d42f7d4c6a4d16 6787 math optional rocq-stdlib_9.1.0-2_amd64.buildinfo
-----BEGIN PGP SIGNATURE-----

iQJNBAEBCgA3FiEEgS7v2KP7pKzk3xFLBMU71/4DBVEFAmphCC4ZHGp1bGllbi5w
dXlkdEBsYXBvc3RlLm5ldAAKCRAExTvX/gMFUY1LEACIBTb4Kc8FmzMssa9SQVy/
dj5kshLfcNw/4q7yHUZZps9pdMZWVZ7/XhWkebP5e4btqG74tSf9xI1mO69ZMjNz
dI325GcRJKbBpLCn0uJgbiDSZasE1HAwiqafh0KSfN7VE+U/HCkGVZ4bOpU+j31I
R26glZ5iqEtpnN70nDWheQzijTxEa+y6EJOUieWiVWJO4RDSL6qGOs7yZB9kyiaw
DDb8mg4lAXt6IcjRuu++TGRYJcK7mPA36TUto7tlmyjmszFq7rHzT/OSWyQ4OnJq
313LGmaRZOz/c/lw1UWqHbQ4I0NqJLXFGnSGiadSC/s38WCTnc2XvA7gQneWo6E8
DhbQmQUj2depW8gDH0Pj+TwG5h4N1iFf1bOfYd3K0csNLNbEY+SGl59NfmIcGw13
cf/P2ZwQfyTaGGZzR9xutuDCKa9jmmRM/r3b7F5Tsq0/5EF1ttLW63g1VAcHvpNt
3qTZsVA45ZOYuL+Su650gLIIjYrV0KXQkdc13zoXv1cZyVMmnsF9rWCiIKkA1veF
oZMFMNv+f3jluH6QhcAlha6Xau4J8x98lUVIvJhtPd2pBzatkZQidsNqtOiu0wxU
FVBAwmk22eZS9th/0TMGlPFmR2JctLTCfilhMC/rlxgtrbuVX9KtM6cgOCFcNK0X
JWiemhRR5vqZ0L6/vIjDyw==
=ny1u
-----END PGP SIGNATURE-----

#1128188 libcoq-stdlib lacks dependencies #1128188

Just Reply to ...

Reply to submitter ...

Send control command (Silently)

Set Architecture Tags (Silently)