Package: src:coq
Version: 8.12.0-3
Severity: serious
Control: close -1 8.16.1+dfsg-1
Tags: ftbfs bullseye
Dear maintainer:
During a rebuild of all packages in bullseye, your package failed to build:
--------------------------------------------------------------------------------
[...]
debian/rules binary
dh binary --with ocaml,python3
debian/rules build
make[1]: Entering directory '/<<PKGBUILDDIR>>'
dh build --with ocaml,python3
dh_update_autotools_config
dh_autoreconf
dh_ocamlinit
debian/rules override_dh_auto_configure
make[2]: Entering directory '/<<PKGBUILDDIR>>'
./configure -arch Linux -prefix /usr -mandir /usr/share/man -configdir /etc/xdg/coq -browser
"/usr/bin/x-www-browser %s &" -with-doc no
You have OCaml 4.11.1. Good!
You have OCamlfind 1.8.1. Good!
[... snipped ...]
TEST micromega/bug_11191b.v
CHECK micromega/bug_11191b.v
TEST micromega/bug_11270.v
CHECK micromega/bug_11270.v
TEST micromega/bug_11436.v
CHECK micromega/bug_11436.v
TEST micromega/bug_12210.v
CHECK micromega/bug_12210.v
TEST micromega/bug_9162.v
CHECK micromega/bug_9162.v
TEST micromega/evars_loops_in_8_10_fixed_8_11.v
CHECK micromega/evars_loops_in_8_10_fixed_8_11.v
TEST micromega/example.v
CHECK micromega/example.v
TEST micromega/example_nia.v
CHECK micromega/example_nia.v
TEST micromega/heap3_vcgen_25.v
CHECK micromega/heap3_vcgen_25.v
TEST micromega/non_lin_ci.v
CHECK micromega/non_lin_ci.v
TEST micromega/qexample.v
CHECK micromega/qexample.v
TEST micromega/rexample.v
CHECK micromega/rexample.v
TEST micromega/rsyntax.v
CHECK micromega/rsyntax.v
TEST micromega/square.v
CHECK micromega/square.v
TEST micromega/zomicron.v
CHECK micromega/zomicron.v
TEST modules/plik.v
CHECK modules/plik.v
TEST modules/Nat.v
CHECK modules/Nat.v
TEST modules/Demo.v
CHECK modules/Demo.v
TEST modules/PO.v
CHECK modules/PO.v
TEST modules/Przyklad.v
CHECK modules/Przyklad.v
TEST modules/SeveralWith.v
CHECK modules/SeveralWith.v
TEST modules/Tescik.v
CHECK modules/Tescik.v
TEST modules/WithDefUBinders.v
CHECK modules/WithDefUBinders.v
TEST modules/cumpoly.v
CHECK modules/cumpoly.v
TEST modules/errors.v (-impredicative-set)
CHECK modules/errors.v
TEST modules/fun_objects.v (-impredicative-set)
CHECK modules/fun_objects.v
TEST modules/grammar.v
CHECK modules/grammar.v
TEST modules/ind.v
CHECK modules/ind.v
TEST modules/injection_discriminate_inversion.v
CHECK modules/injection_discriminate_inversion.v
TEST modules/mod_decl.v
CHECK modules/mod_decl.v
TEST modules/modeq.v (-top modeq)
CHECK modules/modeq.v
TEST modules/modul.v (-top modul)
CHECK modules/modul.v
TEST modules/nested_mod_types.v
CHECK modules/nested_mod_types.v
TEST modules/obj.v
CHECK modules/obj.v
TEST modules/objects.v
CHECK modules/objects.v
TEST modules/objects2.v
CHECK modules/objects2.v
TEST modules/pliczek.v
CHECK modules/pliczek.v
TEST modules/polymorphism.v
CHECK modules/polymorphism.v
TEST modules/polymorphism2.v
CHECK modules/polymorphism2.v
TEST modules/pseudo_circular_with.v
CHECK modules/pseudo_circular_with.v
TEST modules/resolver.v
CHECK modules/resolver.v
TEST modules/sig.v
CHECK modules/sig.v
TEST modules/sub_objects.v
CHECK modules/sub_objects.v
TEST modules/subtyping.v
CHECK modules/subtyping.v
TEST stm/Nijmegen_QArithSternBrocot_Zaux.v
CHECK stm/Nijmegen_QArithSternBrocot_Zaux.v
TEST stm/arg_filter_1.v (-async-proofs-tac-j 1)
CHECK stm/arg_filter_1.v
TEST stm/classify_set_proof_mode_9093.v (-async-proofs on -noinit)
CHECK stm/classify_set_proof_mode_9093.v
TEST stm/delayed_restrict_univs_9093.v (-async-proofs on)
CHECK stm/delayed_restrict_univs_9093.v
TEST coqdoc/Record.v
TEST coqdoc/binder.v
TEST coqdoc/bug11194.v
TEST coqdoc/bug11353.v (-g)
TEST coqdoc/bug12742.v
TEST coqdoc/bug5648.v
TEST coqdoc/bug5700.v
TEST coqdoc/links.v
TEST ssr/absevarprop.v
CHECK ssr/absevarprop.v
TEST ssr/abstract_var2.v
CHECK ssr/abstract_var2.v
TEST ssr/autoclean.v
CHECK ssr/autoclean.v
TEST ssr/bang_rewrite.v
CHECK ssr/bang_rewrite.v
TEST ssr/binders.v
CHECK ssr/binders.v
TEST ssr/binders_of.v
CHECK ssr/binders_of.v
TEST ssr/case_TC.v
CHECK ssr/case_TC.v
TEST ssr/case_TC2.v
CHECK ssr/case_TC2.v
TEST ssr/case_TC3.v
CHECK ssr/case_TC3.v
TEST ssr/case_polyuniv.v
CHECK ssr/case_polyuniv.v
TEST ssr/caseview.v
CHECK ssr/caseview.v
TEST ssr/congr.v
CHECK ssr/congr.v
TEST ssr/deferclear.v
CHECK ssr/deferclear.v
TEST ssr/delayed_clear_rename.v
CHECK ssr/delayed_clear_rename.v
TEST ssr/dependent_type_err.v
CHECK ssr/dependent_type_err.v
TEST ssr/derive_inversion.v
CHECK ssr/derive_inversion.v
TEST ssr/elim.v
CHECK ssr/elim.v
TEST ssr/elim2.v
CHECK ssr/elim2.v
TEST ssr/elim_noquant.v
CHECK ssr/elim_noquant.v
TEST ssr/elim_pattern.v
CHECK ssr/elim_pattern.v
TEST ssr/first_n.v
CHECK ssr/first_n.v
TEST ssr/gen_have.v
CHECK ssr/gen_have.v
TEST ssr/gen_pattern.v
CHECK ssr/gen_pattern.v
TEST ssr/have_TC.v
CHECK ssr/have_TC.v
TEST ssr/have_transp.v
CHECK ssr/have_transp.v
TEST ssr/have_view_idiom.v
CHECK ssr/have_view_idiom.v
TEST ssr/havesuff.v
CHECK ssr/havesuff.v
TEST ssr/if_isnt.v
CHECK ssr/if_isnt.v
TEST ssr/intro_beta.v
CHECK ssr/intro_beta.v
TEST ssr/intro_noop.v
CHECK ssr/intro_noop.v
TEST ssr/ipat_clear_if_id.v
CHECK ssr/ipat_clear_if_id.v
TEST ssr/ipat_fast_any.v
CHECK ssr/ipat_fast_any.v
TEST ssr/ipat_fastid.v
CHECK ssr/ipat_fastid.v
TEST ssr/ipat_replace.v
CHECK ssr/ipat_replace.v
TEST ssr/ipat_seed.v
CHECK ssr/ipat_seed.v
TEST ssr/ipat_tac.v
CHECK ssr/ipat_tac.v
TEST ssr/ipat_tmp.v
CHECK ssr/ipat_tmp.v
TEST ssr/ipatalternation.v
CHECK ssr/ipatalternation.v
TEST ssr/ltac_have.v
CHECK ssr/ltac_have.v
TEST ssr/ltac_in.v
CHECK ssr/ltac_in.v
TEST ssr/misc_extended.v
CHECK ssr/misc_extended.v
TEST ssr/misc_tc.v
CHECK ssr/misc_tc.v
TEST ssr/move_after.v
CHECK ssr/move_after.v
TEST ssr/multiview.v
CHECK ssr/multiview.v
TEST ssr/nonPropType.v
CHECK ssr/nonPropType.v
TEST ssr/occarrow.v
CHECK ssr/occarrow.v
TEST ssr/over.v
CHECK ssr/over.v
TEST ssr/patnoX.v
CHECK ssr/patnoX.v
TEST ssr/pattern.v
CHECK ssr/pattern.v
TEST ssr/predRewrite.v
CHECK ssr/predRewrite.v
TEST ssr/primproj.v
CHECK ssr/primproj.v
TEST ssr/rew_polyuniv.v
CHECK ssr/rew_polyuniv.v
TEST ssr/rewpatterns.v
CHECK ssr/rewpatterns.v
TEST ssr/rewrite_illtyped.v
CHECK ssr/rewrite_illtyped.v
TEST ssr/rewrtite_err_msg.v
CHECK ssr/rewrtite_err_msg.v
TEST ssr/set_lamda.v
CHECK ssr/set_lamda.v
TEST ssr/set_pattern.v
CHECK ssr/set_pattern.v
TEST ssr/set_polyuniv.v
CHECK ssr/set_polyuniv.v
TEST ssr/simpl_done.v
CHECK ssr/simpl_done.v
TEST ssr/ssrpattern.v
CHECK ssr/ssrpattern.v
TEST ssr/ssrsyntax2.v
CHECK ssr/ssrsyntax2.v
TEST ssr/tc.v
CHECK ssr/tc.v
TEST ssr/try_case.v
CHECK ssr/try_case.v
TEST ssr/typeof.v
CHECK ssr/typeof.v
TEST ssr/under.v
CHECK ssr/under.v
TEST ssr/unfold_Opaque.v
CHECK ssr/unfold_Opaque.v
TEST ssr/unfold_fold_polyuniv.v
CHECK ssr/unfold_fold_polyuniv.v
TEST ssr/unkeyed.v
CHECK ssr/unkeyed.v
TEST ssr/view_case.v
CHECK ssr/view_case.v
TEST ssr/wlog_suff.v
CHECK ssr/wlog_suff.v
TEST ssr/wlogletin.v
CHECK ssr/wlogletin.v
TEST ssr/wlong_intro.v
CHECK ssr/wlong_intro.v
TEST primitive/uint63/add.v
CHECK primitive/uint63/add.v
TEST primitive/uint63/addc.v
CHECK primitive/uint63/addc.v
TEST primitive/uint63/addcarryc.v
CHECK primitive/uint63/addcarryc.v
TEST primitive/uint63/addmuldiv.v
CHECK primitive/uint63/addmuldiv.v
TEST primitive/uint63/compare.v
CHECK primitive/uint63/compare.v
TEST primitive/uint63/div.v
CHECK primitive/uint63/div.v
TEST primitive/uint63/diveucl.v
CHECK primitive/uint63/diveucl.v
TEST primitive/uint63/diveucl_21.v
CHECK primitive/uint63/diveucl_21.v
TEST primitive/uint63/eqb.v
CHECK primitive/uint63/eqb.v
TEST primitive/uint63/head0.v
CHECK primitive/uint63/head0.v
TEST primitive/uint63/isint.v
CHECK primitive/uint63/isint.v
TEST primitive/uint63/land.v
CHECK primitive/uint63/land.v
TEST primitive/uint63/leb.v
CHECK primitive/uint63/leb.v
TEST primitive/uint63/lor.v
CHECK primitive/uint63/lor.v
TEST primitive/uint63/lsl.v
CHECK primitive/uint63/lsl.v
TEST primitive/uint63/lsr.v
CHECK primitive/uint63/lsr.v
TEST primitive/uint63/ltb.v
CHECK primitive/uint63/ltb.v
TEST primitive/uint63/lxor.v
CHECK primitive/uint63/lxor.v
TEST primitive/uint63/mod.v
CHECK primitive/uint63/mod.v
TEST primitive/uint63/mul.v
CHECK primitive/uint63/mul.v
TEST primitive/uint63/mulc.v
CHECK primitive/uint63/mulc.v
TEST primitive/uint63/reduction.v
CHECK primitive/uint63/reduction.v
TEST primitive/uint63/sub.v
CHECK primitive/uint63/sub.v
TEST primitive/uint63/subc.v
CHECK primitive/uint63/subc.v
TEST primitive/uint63/subcarryc.v
CHECK primitive/uint63/subcarryc.v
TEST primitive/uint63/tail0.v
CHECK primitive/uint63/tail0.v
TEST primitive/uint63/unsigned.v
CHECK primitive/uint63/unsigned.v
TEST primitive/float/add.v
CHECK primitive/float/add.v
TEST primitive/float/classify.v
CHECK primitive/float/classify.v
TEST primitive/float/compare.v
CHECK primitive/float/compare.v
TEST primitive/float/coq_env_double_array.v
CHECK primitive/float/coq_env_double_array.v
TEST primitive/float/div.v
CHECK primitive/float/div.v
TEST primitive/float/double_rounding.v
CHECK primitive/float/double_rounding.v
TEST primitive/float/frexp.v
CHECK primitive/float/frexp.v
TEST primitive/float/ldexp.v
CHECK primitive/float/ldexp.v
TEST primitive/float/mul.v
CHECK primitive/float/mul.v
TEST primitive/float/next_up_down.v
CHECK primitive/float/next_up_down.v
TEST primitive/float/normfr_mantissa.v
CHECK primitive/float/normfr_mantissa.v
TEST primitive/float/spec_conv.v
CHECK primitive/float/spec_conv.v
TEST primitive/float/sqrt.v
CHECK primitive/float/sqrt.v
TEST primitive/float/sub.v
CHECK primitive/float/sub.v
TEST primitive/float/syntax.v
CHECK primitive/float/syntax.v
TEST primitive/float/valid_binary_conv.v
CHECK primitive/float/valid_binary_conv.v
TEST primitive/float/zero.v
CHECK primitive/float/zero.v
TEST ltac2/array_lib.v
CHECK ltac2/array_lib.v
TEST ltac2/binder.v
CHECK ltac2/binder.v
TEST ltac2/compat.v
CHECK ltac2/compat.v
TEST ltac2/constr.v
CHECK ltac2/constr.v
TEST ltac2/errors.v
CHECK ltac2/errors.v
TEST ltac2/example1.v
CHECK ltac2/example1.v
TEST ltac2/example2.v
CHECK ltac2/example2.v
TEST ltac2/ltac2env.v
CHECK ltac2/ltac2env.v
TEST ltac2/matching.v
CHECK ltac2/matching.v
TEST ltac2/notations.v
CHECK ltac2/notations.v
TEST ltac2/quot.v
CHECK ltac2/quot.v
TEST ltac2/rebind.v
CHECK ltac2/rebind.v
TEST ltac2/syntax.v
CHECK ltac2/syntax.v
TEST ltac2/tacticals.v
CHECK ltac2/tacticals.v
TEST ltac2/term_notations.v
CHECK ltac2/term_notations.v
TEST ltac2/typing.v
CHECK ltac2/typing.v
TEST misc/4722.sh
TEST misc/7595.sh
TEST misc/7704.sh
TEST misc/changelog.sh
TEST misc/coqc_dash_o.sh
TEST misc/deps-checksum.sh
TEST misc/deps-order.sh
TEST misc/deps-utf8.sh
TEST misc/exitstatus.sh
TEST misc/poly-capture-global-univs.sh
TEST misc/quick-include.sh
TEST misc/quotation_token.sh
TEST misc/redirect_printing.sh
TEST misc/side-eff-leak-univs.sh
TEST misc/universes.sh
TEST misc/votour.sh
TEST ide/blocking-futures.fake
TEST ide/bug4246.fake
TEST ide/bug4249.fake
TEST ide/bug7088.fake
TEST ide/debug_ltac.fake
TEST ide/join-sync.fake
TEST ide/join.fake
TEST ide/load.fake
TEST ide/reopen.fake
TEST ide/reopen1.fake
TEST ide/undo001.fake
TEST ide/undo002.fake
TEST ide/undo003.fake
TEST ide/undo004.fake
TEST ide/undo005.fake
TEST ide/undo006.fake
TEST ide/undo008.fake
TEST ide/undo009.fake
TEST ide/undo010.fake
TEST ide/undo012.fake
TEST ide/undo013.fake
TEST ide/undo014.fake
TEST ide/undo015.fake
TEST ide/undo016.fake
TEST ide/undo017.fake
TEST ide/undo018.fake
TEST ide/undo019.fake
TEST ide/undo020.fake
TEST ide/undo021.fake
TEST ide/undo022.fake
TEST ide/univ.fake
TEST coqchk/bug_7539.v
TEST coqchk/bug_8655.v
TEST coqchk/bug_8876.v
TEST coqchk/bug_8881.v
TEST coqchk/bug_8937.v
TEST coqchk/cumulativity.v
TEST coqchk/include.v
TEST coqchk/include_primproj.v
TEST coqchk/inductive_functor_params.v
TEST coqchk/inductive_functor_squash.v
TEST coqchk/inductive_functor_template.v
TEST coqchk/primproj.v
TEST coqchk/primproj2.v
TEST coqchk/univ.v
TEST output-coqchk/bug_5030.v
CHECK output-coqchk/bug_5030.v
TEST coq-makefile/camldep
TEST coq-makefile/missing-install
TEST coq-makefile/native1
TEST coq-makefile/native2
TEST tools/update-compat
make[6]: Entering directory '/<<PKGBUILDDIR>>/test-suite'
logs/bugs/opened/bug_3395.v.log
==========> TESTING bugs/opened/bug_3395.v <==========
File "./bugs/opened/bug_3395.v", line 15, characters 0-45:
Warning: Notation "_ = _" was already used in scope type_scope.
[notation-overridden,parsing]
File "./bugs/opened/bug_3395.v", line 20, characters 0-43:
Warning: Declaring a scope implicitly is deprecated; use in advance an
explicit "Declare Scope morphism_scope.". [undeclared-scope,deprecated]
File "./bugs/opened/bug_3395.v", line 21, characters 0-43:
Warning: Declaring a scope implicitly is deprecated; use in advance an
explicit "Declare Scope category_scope.". [undeclared-scope,deprecated]
File "./bugs/opened/bug_3395.v", line 22, characters 0-39:
Warning: Declaring a scope implicitly is deprecated; use in advance an
explicit "Declare Scope object_scope.". [undeclared-scope,deprecated]
File "./bugs/opened/bug_3395.v", line 55, characters 0-41:
Warning: Declaring a scope implicitly is deprecated; use in advance an
explicit "Declare Scope functor_scope.". [undeclared-scope,deprecated]
Finished transaction in 0.008 secs (0.008u,0.s) (successful)
Finished transaction in 1.812 secs (1.808u,0.003s) (successful)
File "./bugs/opened/bug_3395.v", line 222, characters 0-23:
Error: The command has not failed!
0m0.000000s 0m0.000000s
0m4.850000s 0m0.060000s
==========> FAILURE <==========
bugs/opened/bug_3395.v...Error! (bug seems to be closed, please check)
FAILURES
bugs/opened/bug_3395.v...Error! (bug seems to be closed, please check)
make[6]: *** [Makefile:216: report] Error 1
make[6]: Leaving directory '/<<PKGBUILDDIR>>/test-suite'
make[5]: *** [Makefile:134: all] Error 2
make[5]: Leaving directory '/<<PKGBUILDDIR>>/test-suite'
make[4]: *** [Makefile.build:618: test-suite] Error 2
make[4]: Leaving directory '/<<PKGBUILDDIR>>'
make[3]: *** [Makefile.make:179: submake] Error 2
make[3]: Leaving directory '/<<PKGBUILDDIR>>'
make[2]: *** [debian/rules:90: override_dh_auto_test] Error 2
make[2]: Leaving directory '/<<PKGBUILDDIR>>'
make[1]: *** [debian/rules:58: build] Error 2
make[1]: Leaving directory '/<<PKGBUILDDIR>>'
make: *** [debian/rules:52: binary] Error 2
dpkg-buildpackage: error: debian/rules binary subprocess returned exit status 2
--------------------------------------------------------------------------------
The above is just how the build ends and not necessarily the most relevant part.
If required, the full build log is available here:
https://people.debian.org/~sanvila/build-logs/bullseye/
About the archive rebuild: The build was made on virtual machines
of type m6a.large and r6a.large from AWS, using sbuild and a
reduced chroot with only build-essential packages.
If you could not reproduce the bug please contact me privately, as I
am willing to provide ssh access to a virtual machine where the bug is
fully reproducible.
If this is really a bug in one of the build-depends, please use
reassign and affects, so that this is still visible in the BTS web
page for this package.
Thanks.
