Bug#622882: marked as done (coq: please add fix for thumb2 (in armhf))
Your message dated Tue, 19 Apr 2011 17:32:26 +0000
with message-id <E1QCEmo-0001kb-4i@franck.debian.org>
and subject line Bug#622882: fixed in coq 8.3.pl2+dfsg-1
has caused the Debian Bug report #622882,
regarding coq: please add fix for thumb2 (in armhf)
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.)
--
622882: http://bugs.debian.org/cgi-bin/bugreport.cgi?bug=622882
Debian Bug Tracking System
Contact owner@bugs.debian.org with problems
--- Begin Message ---
Source: coq
Severity: important
Tags: patch
This is a patch backported from coq in Ubuntu. It fixes a thumb2-related
build error. Please consider applying the patch, the package builds
successfully with this patch
Regards
Konstantinos
-- System Information:
Debian Release: squeeze/sid
Architecture: armhf (armv7l)
Kernel: Linux 2.6.31.14-efikamx (PREEMPT)
Locale: LANG=en_US.UTF-8, LC_CTYPE=en_US.UTF-8 (charmap=UTF-8)
Shell: /bin/sh linked to /bin/dash
diff -ruN coq-8.2.pl2+dfsg/debian/patches/0003-Fix-armel-ftbfs.patch coq-8.2.pl2+dfsg.armhf//debian/patches/0003-Fix-armel-ftbfs.patch
--- coq-8.2.pl2+dfsg/debian/patches/0003-Fix-armel-ftbfs.patch 1970-01-01 02:00:00.000000000 +0200
+++ coq-8.2.pl2+dfsg.armhf//debian/patches/0003-Fix-armel-ftbfs.patch 2011-04-15 00:21:47.897311987 +0300
@@ -0,0 +1,11 @@
+--- coq-8.2.pl2+dfsg.orig/kernel/byterun/coq_interp.c
++++ coq-8.2.pl2+dfsg/kernel/byterun/coq_interp.c
+@@ -144,7 +144,7 @@ sp is a local copy of the global variabl
+ #define SP_REG asm("a4")
+ #define ACCU_REG asm("d7")
+ #endif
+-#ifdef __arm__
++#if defined(__arm__) && !defined(__thumb2__)
+ #define PC_REG asm("r9")
+ #define SP_REG asm("r8")
+ #define ACCU_REG asm("r7")
diff -ruN coq-8.2.pl2+dfsg/debian/patches/series coq-8.2.pl2+dfsg.armhf//debian/patches/series
--- coq-8.2.pl2+dfsg/debian/patches/series 2011-02-21 16:15:35.000000000 +0200
+++ coq-8.2.pl2+dfsg.armhf//debian/patches/series 2011-04-15 00:22:24.127317116 +0300
@@ -1,3 +1,4 @@
0001-Disable-micromega-tests.patch
0002-Remove-dependency-to-Unix-from-module-Profile.patch
0003-Fix-build-with-camlp5-6.02.1.patch
+0003-Fix-armel-ftbfs.patch
--- End Message ---
--- Begin Message ---
Source: coq
Source-Version: 8.3.pl2+dfsg-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:
coq-theories_8.3.pl2+dfsg-1_all.deb
to main/c/coq/coq-theories_8.3.pl2+dfsg-1_all.deb
coq_8.3.pl2+dfsg-1.debian.tar.gz
to main/c/coq/coq_8.3.pl2+dfsg-1.debian.tar.gz
coq_8.3.pl2+dfsg-1.dsc
to main/c/coq/coq_8.3.pl2+dfsg-1.dsc
coq_8.3.pl2+dfsg-1_amd64.deb
to main/c/coq/coq_8.3.pl2+dfsg-1_amd64.deb
coq_8.3.pl2+dfsg.orig.tar.gz
to main/c/coq/coq_8.3.pl2+dfsg.orig.tar.gz
coqide_8.3.pl2+dfsg-1_amd64.deb
to main/c/coq/coqide_8.3.pl2+dfsg-1_amd64.deb
libcoq-ocaml-dev_8.3.pl2+dfsg-1_amd64.deb
to main/c/coq/libcoq-ocaml-dev_8.3.pl2+dfsg-1_amd64.deb
libcoq-ocaml_8.3.pl2+dfsg-1_amd64.deb
to main/c/coq/libcoq-ocaml_8.3.pl2+dfsg-1_amd64.deb
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 622882@bugs.debian.org,
and the maintainer will reopen the bug report if appropriate.
Debian distribution maintenance software
pp.
Stéphane Glondu <glondu@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@debian.org)
-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA512
Format: 1.8
Date: Tue, 19 Apr 2011 17:37:30 +0200
Source: coq
Binary: coq coqide coq-theories libcoq-ocaml libcoq-ocaml-dev
Architecture: source amd64 all
Version: 8.3.pl2+dfsg-1
Distribution: unstable
Urgency: low
Maintainer: Debian OCaml Maintainers <debian-ocaml-maint@lists.debian.org>
Changed-By: Stéphane Glondu <glondu@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: 622882
Changes:
coq (8.3.pl2+dfsg-1) unstable; urgency=low
.
* New upstream release
* Add patch to fix thumb2-related build error (Closes: #622882)
* Upload to unstable
Checksums-Sha1:
7b9323d228eb79cf1eb354223a35f2119e5f2617 2175 coq_8.3.pl2+dfsg-1.dsc
e0e7751104afe8466ca7a7a2aeb46d43e18c984a 3147573 coq_8.3.pl2+dfsg.orig.tar.gz
c00490f436acf4c129ffbf428eb10b5506b93ff4 16199 coq_8.3.pl2+dfsg-1.debian.tar.gz
22264069adc9f22ca17fd181539ec03ec6826f6f 5672486 coq_8.3.pl2+dfsg-1_amd64.deb
ccd036b964daf4d1eb4316e1f8a9156a9d146e12 5608962 coqide_8.3.pl2+dfsg-1_amd64.deb
598831b4f70389d0104661fb93651614a2a79fb8 53335646 coq-theories_8.3.pl2+dfsg-1_all.deb
9b753a9140b4e5372327de7e1deb13ab856010ec 2089828 libcoq-ocaml_8.3.pl2+dfsg-1_amd64.deb
2d7c822e87d09a481de594a7792cf6fce5c47290 5919874 libcoq-ocaml-dev_8.3.pl2+dfsg-1_amd64.deb
Checksums-Sha256:
7d65e81d24815945fd9d4f91587678ec589780dbd17e4363c79faea51cb5bbc4 2175 coq_8.3.pl2+dfsg-1.dsc
7f4a1d846bc02a4403a5b2aa7977313dde9032e88684d510e9ffb42062d384cb 3147573 coq_8.3.pl2+dfsg.orig.tar.gz
6ebb08c91c203946fbbbf3489d7ab566c367d6dcbc5cbb101af25aa2cb777f7b 16199 coq_8.3.pl2+dfsg-1.debian.tar.gz
430b40774c342a9fbb174b587d9af659d5b111562ef856ee4998107337824d0a 5672486 coq_8.3.pl2+dfsg-1_amd64.deb
4064c33cc0229acc56e29b888984b01b4ff532c9e1900d8424a1530e01ca1960 5608962 coqide_8.3.pl2+dfsg-1_amd64.deb
6d6b33902425af0c468ac6589b3c14b898bbef01989fade0b028d8dc9da25de2 53335646 coq-theories_8.3.pl2+dfsg-1_all.deb
856a123e5a14a14eea586c0bd343c93409c97bdde7f8e9127d7acbb395975e0d 2089828 libcoq-ocaml_8.3.pl2+dfsg-1_amd64.deb
85540194a3451fffd4cb7928f6bfd1d142dce99dacf49eee6788309cfb11c6f7 5919874 libcoq-ocaml-dev_8.3.pl2+dfsg-1_amd64.deb
Files:
31bfb6ccbd6b6c815d4614b8b44e3251 2175 math optional coq_8.3.pl2+dfsg-1.dsc
70ece28030a20c19b9292cb0c7d5be4a 3147573 math optional coq_8.3.pl2+dfsg.orig.tar.gz
ec34c774da06f8f2b9be7fd261b16503 16199 math optional coq_8.3.pl2+dfsg-1.debian.tar.gz
889500750e1509b5f6c95ce94a51005a 5672486 math optional coq_8.3.pl2+dfsg-1_amd64.deb
c35dd80fc299c59455b4b638734e1d71 5608962 math optional coqide_8.3.pl2+dfsg-1_amd64.deb
dcb2c98e72bd2017e8c7e6ff21574054 53335646 math optional coq-theories_8.3.pl2+dfsg-1_all.deb
0405b0091add22263d9e78cfd3aaa204 2089828 ocaml optional libcoq-ocaml_8.3.pl2+dfsg-1_amd64.deb
a2648fc52103d0847d577b916baf77ae 5919874 ocaml optional libcoq-ocaml-dev_8.3.pl2+dfsg-1_amd64.deb
-----BEGIN PGP SIGNATURE-----
Version: GnuPG v1.4.10 (GNU/Linux)
iQIcBAEBCgAGBQJNrcKhAAoJEHhT2k1JiBrTIL0P/j91x7g+5Gadf659JBjbUJ8G
jEtKZSmz8bxF8HWYa6kFjp8PehqNRjVyTuEm928HwTtonyhxZGPCRw2Q3gV5lEoQ
61cbIqdJ9WC+n31Zy/g7Ktebi+ZS6LwVlTVixnSez+HI8eJmkA+e0eWU7Dcq3yR2
CMdTT08JTw05dcBOAuBdow0PfbVB1UAHfmYRGdECsSsVOqgLWiC1R1NECRcUEx/p
vMbaRhM/4hQeHnZVazd9iJtsGSrDc+CzHM/NOynkDQf2mbMM1hzUw5aTu4fGZfGs
L/Ta5YKW3GRdCb4ojvQU7q+dqDvzP3zT+n7r2uAYvmVo9N5xzoh2XQYKA5Hyg7CV
/0C5uqTOHSPbYyIdJLDmxfQsiNEPi8EphlJ/UbXqCvZSvhRbkFwR8SZi9X3uVKD5
2V5bTh1W/ZjZ+HKyNczNlqVpTR5zp86rk3unjUuVwg8YxpkcIUXUYH9NXw/dNEfd
7S3TBx4As49VIVAVQ2vUClSgH3jlk7NPAhQGLWF4AzjbVZU4TM5jS/Lnba/KvFwd
eG1YBmxhroR6FfOrtERvpP2AgbSKdI9H+C0Rnr7kTgf/hLIFXDZXcJGZdB25dpgo
z5q8srYFw7BxW+U0FBnypxGKCEilkEoCPlLtQVTiIIhZclOu8EWd9KfQjAHicnZh
By+Lp87YNiYi1oD/P2iT
=KWb0
-----END PGP SIGNATURE-----
--- End Message ---
Reply to: