Bug#399919: marked as done (coq_8.1~gamma-1(hppa/experimental): FTBFS: test failures)
Your message dated Thu, 23 Nov 2006 22:02:04 +0000
with message-id <E1GnMdw-0005yD-Ms@ries.debian.org>
and subject line Bug#399919: fixed in coq 8.1~gamma-2
has caused the attached Bug report 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 I am
talking about this indicates a serious mail system misconfiguration
somewhere. Please contact me immediately.)
Debian bug tracking system administrator
(administrator, Debian Bugs database)
--- Begin Message ---
Package: coq
Version: 8.1~gamma-1
Severity: serious
Hi,
your package failed to build from source while running the test cases.
| Automatic build of coq_8.1~gamma-1 on meitner by sbuild/hppa 79
| Build started at 20061122-1437
| ******************************************************************************
| Checking available source versions...
| Fetching source files...
| Reading package lists...
| Building dependency tree...
| Need to get 2957kB of source archives.
| Get:1 http://ftp.de.debian.org experimental/main coq 8.1~gamma-1 (dsc) [923B]
| Get:2 http://ftp.de.debian.org experimental/main coq 8.1~gamma-1 (tar) [2943kB]
| Get:3 http://ftp.de.debian.org experimental/main coq 8.1~gamma-1 (diff) [13.3kB]
| Fetched 2957kB in 58s (50.6kB/s)
| Download complete and in download only mode
| ** Using build dependencies supplied by package:
| Build-Depends: debhelper (>= 4.0.0), dpkg-dev (>= 1.13.19), dpatch, ocaml-nox (>= 3.09.0), ocaml-best-compilers, liblablgtk2-ocaml-dev (>= 2.4.0), tetex-extra, hevea
| ** Filtered missing central deps that are dependencies of or provide build-deps:
| libncurses5-dev (>= 5.3.20030510-1)
| **** Warning:
| **** The following central src deps are (probably) missing:
| camlp4, emacsen, ocaml
| Checking for already installed source dependencies...
| debhelper: missing
| Using default version 5.0.42
| dpkg-dev: already installed (1.13.24 >= 1.13.19 is satisfied)
| dpatch: missing
| ocaml-nox: missing
| Using default version 3.09.2-7
| ocaml-best-compilers: missing
| liblablgtk2-ocaml-dev: missing
| Using default version 2.6.0-7
| tetex-extra: missing
| hevea: missing
| Checking for source dependency conflicts...
[...]
| cd test-suite; \
| env COQBIN=../bin COQLIB=.. ./check -byte | tee check.log
| Success tests
| success/Abstract.v...Ok
| success/CanonicalStructure.v...Ok
| success/Case1.v...Ok
| success/Case10.v...Ok
| success/Case11.v...Ok
| success/Case12.v...Ok
| success/Case13.v...Ok
| success/Case14.v...Ok
| success/Case15.v...Ok
| success/Case16.v...Ok
| success/Case17.v...Ok
| success/Case18.v...Ok
| success/Case19.v...Ok
| success/Case2.v...Ok
| success/Case5.v...Ok
| success/Case6.v...Ok
| success/Case7.v...Ok
| success/Case8.v...Ok
| success/Case9.v...Ok
| success/CaseAlias.v...Ok
| success/Cases.v...Ok
| success/CasesDep.v...Ok
| success/Check.v...Ok
| success/Conjecture.v...Ok
| success/DHyp.v...Ok
| success/Decompose.v...Ok
| success/DiscrR.v...Ok
| success/Discriminate.v...Ok
| success/Field.v...Ok
| success/Fixpoint.v...Ok
| success/Fourier.v...Ok
| success/Funind.v...Ok
| success/Generalize.v...Ok
| success/Hints.v...Ok
| success/ImplicitTactic.v...Ok
| success/Inductive.v...Ok
| success/Injection.v...Ok
| success/Inversion.v...Ok
| success/LegacyField.v...Ok
| success/LetIn.v...Ok
| success/MatchFail.v...Ok
| success/Mod_ltac.v...Ok
| success/Mod_params.v...Ok
| success/Mod_strengthen.v...Ok
| success/Mod_type.v...Ok
| success/NatRing.v...Ok
| success/Notations.v...Ok
| success/Omega.v...Ok
| success/Omega0.v...Ok
| success/Omega2.v...Ok
| success/PPFix.v...Ok
| success/Print.v...Ok
| success/Projection.v...Ok
| success/ROmega.v...Ok
| success/ROmega0.v...Ok
| success/ROmega2.v...Ok
| success/RecTutorial.v...Ok
| success/Record.v...Ok
| success/Reg.v...Ok
| success/Remark.v...Ok
| success/Rename.v...Ok
| success/Require.v...Ok
| success/Reset.v...Ok
| success/Scopes.v...Ok
| success/Simplify_eq.v...Ok
| success/Tauto.v...Ok
| success/TestRefine.v...Ok
| success/Try.v...Ok
| success/apply.v...Ok
| success/autorewritein.v...Ok
| success/cc.v...Ok
| success/coercions.v...Ok
| success/coqbugs0181.v...Ok
| success/destruct.v...Ok
| success/eauto.v...Ok
| success/eqdecide.v...Ok
| success/evars.v...Ok
| success/extraction.v...Ok
| success/fix.v...Ok
| success/if.v...Ok
| success/implicit.v...Ok
| success/import_lib.v...Ok
| success/import_mod.v...Ok
| success/inds_type_sec.v...Ok
| success/induct.v...Ok
| success/intros.v...Ok
| success/ltac.v...Ok
| success/mutual_ind.v...Ok
| success/options.v...Ok
| success/params_ind.v...Ok
| success/polymorphism.v...Ok
| success/refine.v...Ok
| success/replace.v...Ok
| success/rewrite.v...Ok
| success/set.v...Ok
| success/setoid_ring_module.v...Ok
| success/setoid_test.v...Ok
| success/setoid_test2.v...Ok
| success/setoid_test_function_space.v...Ok
| success/simpl.v...Ok
| success/unfold.v...Ok
| success/unicode_utf8.v...Ok
| success/unification.v...Ok
| success/univers.v...Ok
| Failure tests
| failure/Case1.v...Ok
| failure/Case10.v...Ok
| failure/Case11.v...Ok
| failure/Case12.v...Ok
| failure/Case13.v...Ok
| failure/Case14.v...Ok
| failure/Case15.v...Ok
| failure/Case16.v...Ok
| failure/Case2.v...Ok
| failure/Case3.v...Ok
| failure/Case4.v...Ok
| failure/Case5.v...Ok
| failure/Case6.v...Ok
| failure/Case7.v...Ok
| failure/Case8.v...Ok
| failure/Case9.v...Ok
| failure/ClearBody.v...Ok
| failure/Notations.v...Ok
| failure/Tauto.v...Ok
| failure/Uminus.v...Ok
| failure/autorewritein.v...Ok
| failure/cases.v...Ok
| failure/check.v...Ok
| failure/clash_cons.v...Ok
| failure/clashes.v...Ok
| failure/coqbugs0266.v...Ok
| failure/fixpoint1.v...Ok
| failure/illtype1.v...Ok
| failure/inductive1.v...Ok
| failure/inductive2.v...Ok
| failure/inductive3.v...Ok
| failure/ltac1.v...Ok
| failure/ltac2.v...Ok
| failure/ltac4.v...Ok
| failure/pattern.v...Ok
| failure/positivity.v...Ok
| failure/proofirrelevance.v...Ok
| failure/redef.v...Ok
| failure/rewrite_in_goal.v...Ok
| failure/rewrite_in_hyp.v...Ok
| failure/search.v...Ok
| failure/universes-buraliforti-redef.v...Ok
| failure/universes-buraliforti.v...Ok
| failure/universes-sections1.v...Ok
| failure/universes-sections2.v...Ok
| failure/universes.v...Ok
| failure/universes2.v...Ok
| Output tests
| output/Cases.v...Ok
| output/Coercions.v...Ok
| output/Fixpoint.v...Ok
| output/Implicit.v...Ok
| output/InitSyntax.v...Ok
| output/Intuition.v...Ok
| output/Nametab.v...Ok
| output/Notations.v...Ok
| output/RealSyntax.v...Ok
| output/Sum.v...Ok
| output/Tactics.v...Ok
| output/TranspModtype.v...Ok
| output/ZSyntax.v...Ok
| Parser tests
| Interactive tests
| interactive/Back.v...Ok
| interactive/Evar.v...Ok
| Complexity tests
| complexity/pretyping.v...Error! (should run faster)
| complexity/setoid_rewrite.v...Ok
| Module tests
| modules/Demo.v...Ok
| modules/Nat.v...Ok
| modules/PO.v...Ok
| modules/Przyklad.v...Ok
| modules/Tescik.v...Ok
| modules/fun_objects.v...Ok
| modules/grammar.v...Ok
| modules/ind.v...Ok
| modules/mod_decl.v...Ok
| modules/modeq.v...Ok
| modules/modul.v...Ok
| modules/nested_mod_types.v...Ok
| modules/obj.v...Ok
| modules/objects.v...Ok
| modules/objects2.v...Ok
| modules/pliczek.v...Ok
| modules/plik.v...Ok
| modules/sig.v...Ok
| modules/sub_objects.v...Ok
|
| 186 tests passed over 187, i.e. 99 %
| if grep -F 'Error!' test-suite/check.log ; then false; fi
| complexity/pretyping.v...Error! (should run faster)
| make[1]: *** [check] Error 1
| make[1]: Leaving directory `/build/buildd/coq-8.1~gamma'
| make: *** [build-stamp] Error 2
| ******************************************************************************
| Build finished at 20061122-1635
| FAILED [dpkg-buildpackage died]
Full build log(s): http://experimental.ftbfs.de/build.php?&ver=8.1~gamma-1&pkg=coq&arch=hppa
Gruesse,
--
Frank Lichtenheld <frank@lichtenheld.de>
www: http://www.djpig.de/
--- End Message ---
--- Begin Message ---
Source: coq
Source-Version: 8.1~gamma-2
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-libs_8.1~gamma-2_all.deb
to pool/main/c/coq/coq-libs_8.1~gamma-2_all.deb
coq_8.1~gamma-2.diff.gz
to pool/main/c/coq/coq_8.1~gamma-2.diff.gz
coq_8.1~gamma-2.dsc
to pool/main/c/coq/coq_8.1~gamma-2.dsc
coq_8.1~gamma-2_i386.deb
to pool/main/c/coq/coq_8.1~gamma-2_i386.deb
coqide_8.1~gamma-2_i386.deb
to pool/main/c/coq/coqide_8.1~gamma-2_i386.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 399919@bugs.debian.org,
and the maintainer will reopen the bug report if appropriate.
Debian distribution maintenance software
pp.
Samuel Mimram <smimram@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: SHA1
Format: 1.7
Date: Thu, 23 Nov 2006 14:27:15 +0000
Source: coq
Binary: coqide coq-libs coq
Architecture: source i386 all
Version: 8.1~gamma-2
Distribution: experimental
Urgency: low
Maintainer: Debian OCaml Maintainers <debian-ocaml-maint@lists.debian.org>
Changed-By: Samuel Mimram <smimram@debian.org>
Description:
coq - proof assistant for higher-order logic (toplevel and compiler)
coq-libs - proof assistant for higher-order logic (theories)
coqide - proof assistant for higher-order logic (gtk interface)
Closes: 399919
Changes:
coq (8.1~gamma-2) experimental; urgency=low
.
* Added no-complexity-test.dpatch to skip complexity checks (thanks Julien
Cristau), closes: #399919.
Files:
7e7556f28487dbb1c3e5283e03ebea8e 923 math optional coq_8.1~gamma-2.dsc
95407d72bb1c2f9e7d3ef0b3831f04fa 13585 math optional coq_8.1~gamma-2.diff.gz
0340264d637a67b33c1a0f889f80b27f 14580806 math optional coq-libs_8.1~gamma-2_all.deb
9508bd7fb550c5095df7b7b2261547d5 6303954 math optional coq_8.1~gamma-2_i386.deb
4cc9c66745c16b3b72b5283889f2c74d 4587052 math optional coqide_8.1~gamma-2_i386.deb
-----BEGIN PGP SIGNATURE-----
Version: GnuPG v1.4.5 (GNU/Linux)
iD8DBQFFZhhCIae1O4AJae8RAm46AJ9uSN/0ei2fCplqwYFfHFFeJeRjsgCfcD2S
iIu/FMb6bwtkLM3QWT29RJc=
=/Rw3
-----END PGP SIGNATURE-----
--- End Message ---
Reply to: