[Date Prev][Date Next] [Thread Prev][Thread Next] [Date Index] [Thread Index]

Bug#794130: marked as done (coq: please make the build reproducible (timestamps))

Your message dated Mon, 13 Jan 2020 10:00:11 +0000
with message-id <E1iqwW3-000FWu-0S@fasolo.debian.org>
and subject line Bug#794130: fixed in coq 8.10.2-1
has caused the Debian Bug report #794130,
regarding coq: please make the build reproducible (timestamps)
to be marked as done.

This means that you claim that the problem has been dealt with.
If this is not the case it is now your responsibility to reopen the
Bug report if necessary, and/or fix the problem forthwith.

(NB: If you are a system administrator and have no idea what this
message is talking about, this may indicate a serious mail system
misconfiguration somewhere. Please contact owner@bugs.debian.org
immediately.)


-- 
794130: https://bugs.debian.org/cgi-bin/bugreport.cgi?bug=794130
Debian Bug Tracking System
Contact owner@bugs.debian.org with problems
--- Begin Message --- 
Source: coq
Version: 8.4pl4dfsg-1
Severity: wishlist
Tags: patch
User: reproducible-builds@lists.alioth.debian.org
Usertags: timestamps
X-Debbugs-Cc: reproducible-builds@lists.alioth.debian.org

Hi!

While working on the “reproducible builds” effort [1], we have noticed
that foo could not be built reproducibly.

The attached patch removes extra timestamps from the build system. Once
applied, and after ocamlc is patched to remove nondeterminism, coq will
be buildable reproducibly in our experimental framework.

 [1]: https://wiki.debian.org/ReproducibleBuilds

Regards,
Valentin

--- coq-8.4pl4dfsg/configure	2015-07-30 17:44:11.635304955 +0000
+++ coq-8.4pl4dfsg/configure	2015-07-30 19:06:43.000000000 +0000
@@ -9,7 +9,7 @@
 VERSION=8.4pl4
 VOMAGIC=08400
 STATEMAGIC=58400
-DATE=`LC_ALL=C LANG=C dpkg-parsechangelog -S date | date --file=- +"%B %Y"`
+DATE=`dpkg-parsechangelog -S date | LC_ALL=C LANG=C date -u --file=- +"%B %Y"`
 
 # Create the bin/ directory if non-existent
 test -d bin || mkdir bin
@@ -271,7 +271,7 @@
     "") echo "I can't find the program \"date\" in your path."
         echo "Please give me the current date"
 	read COMPILEDATE;;
-    *)  COMPILEDATE=`LC_ALL=C LANG=C dpkg-parsechangelog -S date | date --file=- +"%b %d %Y %H:%M:%S"`;;
+    *)  COMPILEDATE=`dpkg-parsechangelog -S date | LC_ALL=C LANG=C date -u --file=- +"%b %d %Y %H:%M:%S"`;;
 esac
 
 # Architecture

--- End Message ---
--- Begin Message --- 
Source: coq
Source-Version: 8.10.2-1

We believe that the bug you reported is fixed in the latest version of
coq, 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 794130@bugs.debian.org,
and the maintainer will reopen the bug report if appropriate.

Debian distribution maintenance software
pp.
Ralf Treinen <treinen@debian.org> (supplier of updated coq 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)


-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA256

Format: 1.8
Date: Wed, 01 Jan 2020 20:25:21 +0100
Source: coq
Binary: coq coq-dbgsym coq-theories coq-theories-dbgsym coqide coqide-dbgsym libcoq-ocaml libcoq-ocaml-dbgsym libcoq-ocaml-dev
Architecture: source amd64
Version: 8.10.2-1
Distribution: experimental
Urgency: medium
Maintainer: Debian OCaml Maintainers <debian-ocaml-maint@lists.debian.org>
Changed-By: Ralf Treinen <treinen@debian.org>
Description:
 coq        - proof assistant for higher-order logic (toplevel and compiler)
 coq-theories - proof assistant for higher-order logic (theories)
 coqide     - proof assistant for higher-order logic (gtk interface)
 libcoq-ocaml - runtime libraries for Coq
 libcoq-ocaml-dev - development libraries and tools for Coq
Closes: 794130 920589 946580
Changes:
 coq (8.10.2-1) experimental; urgency=medium
 .
   * New upstream release
     - update COQ_VERSION in debian/rules
   * Refreshed patches:
     - remove-heavy-tests.patch: drop removal of test-suite/bugs/closed/5127.v
       as this file is no longer distributed by upstream
     - avoid-usr-bin-env
     - python-scripts-libraries
     - verbose-build
     - remove-bytecode-failing-tests
     - remove-tests-that-need-coqlib.patch
   * Dropped patches:
     - remove-time-sensitive-tests, as none of these tests is distributed
       by upstream any more
     - 0013-Remove-test-failing-with-OCaml-4.08.0 as that test is no longer
       distributed by upstream
     - 0012-ocaml-4.08-does-not-allow-dynamic-loading-of-already
   * New patch use-changelog-date: use the date from the debian changelog
     entry, instead of the real time of compilation, in order to improve
     reproducibility. Based on a patch by Valentin Lorentz  (thanks!)
     (closes: #794130).
   * Reactivate building of coqide (closes: #920589, #946580)
     - put back the coqide paragraph in debian/control
     - bump build-dependencies on lablgtk to version 3
     - coq suggests coqide as an alternative to proofgeneral
     - mention coqide in the long description of coq
     - put back debian/coqide.{1,desktop,dirs,install,links.in} from version
       8.6-5
     - update debian/*.install and debian/not-installed files
   * Build-Conflicts with libcoq-ocaml. This seems to be necessary to avoid
     that coq depends on two versions of libcoq-ocaml: the one being build,
     and the one currently installed.
   * Update libcoq-ocaml{-dev}.install.in
   * Move coqidetop from the coqide package to the coq package, following advice
     by upstream
   * Update docs
   * Generate html pages for the stdlib using HTMLSTYLE=simple, to avoid
     linking to external stylesheets
   * Build-depend on debhelper-compat, drop file debian/compat
   * Debhelper compatibility level 11
     - debian/rules: use "dh_missing --fail-missing" instead of
       "dh_install --fail-missing"
   * Standards-Version 4.4.1 (no change)
   * debian/copyright: updates of copyright holders in many files.
   * Add lintian-overrides for filenames containing wildcard characters
     in package coq-theories
   * debian/gbp.conf:
     - add doc/whodidwhat to the filter as this is part of the non-free
       reference manual
     - drop plugins/ssrmatching/g_ssrmatching.mli from the filter as
       upstream has fixed its license.
Checksums-Sha1:
 8fb5489a5918e7d11c2ba782294f64a69c57ced8 2475 coq_8.10.2-1.dsc
 7f955cdc03c86ebe016f30f8315149f9c5b0bb26 5510559 coq_8.10.2.orig.tar.gz
 9bc658762a2b727c7dc28f9cc58ad797d70bbcdb 24364 coq_8.10.2-1.debian.tar.xz
 87d3c74a4861e44a46e08f7f4893b670a389a079 6797928 coq-dbgsym_8.10.2-1_amd64.deb
 0a7beb556208bf270e382f923fce7fd1fca1fc54 818180 coq-theories-dbgsym_8.10.2-1_amd64.deb
 8645d72de90c10f2cf5386a03774ff31bed2adf4 32011444 coq-theories_8.10.2-1_amd64.deb
 9b6be8da7e434ed096b594b72b4291fc53e01667 18528 coq_8.10.2-1_amd64.buildinfo
 3a70fbcad1fdfe3f8d210e14f9c822afed3e57f0 75531436 coq_8.10.2-1_amd64.deb
 e090d11d01f8b19e0788b667d5af7ae1ca2158c7 592756 coqide-dbgsym_8.10.2-1_amd64.deb
 ee575c783cce5d9010772b1968627def1cec781b 1955832 coqide_8.10.2-1_amd64.deb
 7ad0a6eb99d79345efdef71760018d3ee5e43c55 560760 libcoq-ocaml-dbgsym_8.10.2-1_amd64.deb
 9a61fdf76eabea2aa6a980ecad7abe0db10aea29 15520308 libcoq-ocaml-dev_8.10.2-1_amd64.deb
 850bb5e9d60131f5d8f77a2e7123009e1ce2ab67 5487892 libcoq-ocaml_8.10.2-1_amd64.deb
Checksums-Sha256:
 7e566501c92735cb0b5910175b4c25aa2ecc218fcb72a2f3ab900219c6c145b6 2475 coq_8.10.2-1.dsc
 0a9c0c31cbaa53781e7fc8003f8d31dc612cf444053733b2827615409508f92b 5510559 coq_8.10.2.orig.tar.gz
 f963a2dd86f58c733796cc970128459296ee3e5863e5bd55a4a4a237256421e5 24364 coq_8.10.2-1.debian.tar.xz
 fd1508b21756f543e1781cb26ff91ae229027218e48a7b1230a0def312e83d2d 6797928 coq-dbgsym_8.10.2-1_amd64.deb
 33ee4c786eca94f7fa9c6689d97af04fec81d56fa50481fdff559a89198469c4 818180 coq-theories-dbgsym_8.10.2-1_amd64.deb
 659ef837eeb34c218757a9154fc9d9ce8097b7b8225701a6c13b5deef57f5a9f 32011444 coq-theories_8.10.2-1_amd64.deb
 39b440808975c5e1bbe9a741b6be091e5c8081ef243be8f4e8633035b2a4240a 18528 coq_8.10.2-1_amd64.buildinfo
 7ee2585ba9209fff2cc744c7f38b8c457d995d0bb7bc4dcb3bf093b7a202783b 75531436 coq_8.10.2-1_amd64.deb
 f3257abb90f5b6f3873e7fe02dcacb526ecb09295e7ee5b307bf06daf8109b43 592756 coqide-dbgsym_8.10.2-1_amd64.deb
 cbdf51d6c635c04d790bbd1a836ce74a25f5c587c7a41a7556846442d9e4afa5 1955832 coqide_8.10.2-1_amd64.deb
 1affe232bd3572b9e8cbba3f8bd29047986a0663dd1575729eb0ebada20073c3 560760 libcoq-ocaml-dbgsym_8.10.2-1_amd64.deb
 140950e04fadf92c68b660d161196768ce8a66a8586047d1de64b60301cbf281 15520308 libcoq-ocaml-dev_8.10.2-1_amd64.deb
 0e7b97db188056b5c6234ebbc42be9825869b4a767980653b748a9175c55be8f 5487892 libcoq-ocaml_8.10.2-1_amd64.deb
Files:
 5d1651243469f21f00c3a60420e8375b 2475 math optional coq_8.10.2-1.dsc
 0de1eb43e07d99c4aba3a1c990ef8258 5510559 math optional coq_8.10.2.orig.tar.gz
 9afb49f01f9f1a1871de6f45cb5c199a 24364 math optional coq_8.10.2-1.debian.tar.xz
 2d498b14b4e9ef00094f0ff29ccb3c4e 6797928 debug optional coq-dbgsym_8.10.2-1_amd64.deb
 81c4aef5bb619ef64f9bdddf260351b2 818180 debug optional coq-theories-dbgsym_8.10.2-1_amd64.deb
 50a087d03eafa446e24d4aa77ce4f568 32011444 math optional coq-theories_8.10.2-1_amd64.deb
 65897eadd30d6be65e1c9350c31932da 18528 math optional coq_8.10.2-1_amd64.buildinfo
 4cc00a32ec30caca0c21169694c52e0e 75531436 math optional coq_8.10.2-1_amd64.deb
 bbadeee6d375db9ffe11e4a0c61f2ea2 592756 debug optional coqide-dbgsym_8.10.2-1_amd64.deb
 92fad909df109f142d61c139c2ca8d5e 1955832 math optional coqide_8.10.2-1_amd64.deb
 cd5160f6e9976949558b89d1675a79df 560760 debug optional libcoq-ocaml-dbgsym_8.10.2-1_amd64.deb
 4d9e2bea91d442da3d6823caec7d3592 15520308 ocaml optional libcoq-ocaml-dev_8.10.2-1_amd64.deb
 522f89b95b12b75d965707f6ce892ac4 5487892 ocaml optional libcoq-ocaml_8.10.2-1_amd64.deb

-----BEGIN PGP SIGNATURE-----

iQIzBAEBCAAdFiEEAgVIKeEtDyqOZI5idFxHZtTKzf8FAl4NAUQACgkQdFxHZtTK
zf/Y+BAArqeLi/3+CAZuycnR86zDR5K253vNJgFGtsSU08AAYfiGzZuaxcbYGeXN
nmvqyslho0uPQv7nMQBZRtY717sL4AF3tySjSTRdbYO5FbT9EkLIhke2vbK7CMBP
1icSIc9ypfFScOt1jDjyZEIA+66HUVXpkrE6VnvrrMbHhrPvvPLRR2JRJKyPCGz1
Ms3cQIDo7Gvn9OLm9F6HurhQ0eygx8P1+WEj2s6IlNpEE7ovzoIMC9r5bo8gOH86
c1rkY5KZO9lfwCRP3N6SwMvoJTxQIbizYKaFSvM5RqShDRWB1uEvih7YLgcfS8C5
yrSywAaY+6Ger8d7G+UEQYyDXrqAHisbeLxipHmTRw+nxGTWru6qgXR2JxY1NEWZ
07ivP7UxUaRbJzzFMRGXyX7BZLGiXvg/+akMmRL8fKZOWJevYFepAS3/t5wypavS
ixh0uQ+naJfNHpQyEo0mA2emSJWG1P8AHZL9i/UpzhQhGGx5Q2AtJEsXVMkYMiuo
zCav1AQikUt7yjylGgt0wep/nwfZTVhwTxMw5Ao2WRwd4KU3f+cxo875/jrM3QLP
asl9ctsBOGRi3KQ67Aj7cFK1WxS5FvorD1JSWkufO2QsfE4SVMx3fz8qD+QXGqED
hZV8nzHgSPMdAuefr7lvNI0/5tnVxE5qDQr4wdK5B2gRe7paOps=
=Jc1d
-----END PGP SIGNATURE-----

--- End Message ---
Reply to: