Source: aac-tactics Version: 0.4-5 Severity: serious Justification: fails to build from source User: reproducible-bui...@lists.alioth.debian.org Usertags: ftbfs X-Debbugs-Cc: reproducible-bui...@lists.alioth.debian.org
Dear Maintainer, aac-tactics fails to build from source in unstable/amd64: [..] dpkg-buildpackage -rfakeroot -D -us -uc -b dpkg-buildpackage: source package aac-tactics dpkg-buildpackage: source version 0.4-5 dpkg-buildpackage: source distribution unstable dpkg-buildpackage: source changed by Stéphane Glondu <glo...@debian.org> dpkg-source --before-build aac-tactics-0.4 dpkg-buildpackage: host architecture amd64 fakeroot debian/rules clean dh clean --with ocaml dh_testdir dh_auto_clean make -j1 clean make[1]: Entering directory '/home/lamby/temp/cdt.20160202094640.LVv9Qbd0KW/aac-tactics-0.4' coq_makefile -R . AAC_tactics coq.mli helper.mli search_monad.mli matcher.mli theory.mli print.mli evm_compute.mli evm_compute.ml coq.ml helper.ml search_monad.ml matcher.ml theory.ml print.ml rewrite.ml4 aac.mlpack AAC.v Instances.v Tutorial.v Caveats.v -o Makefile.coq make -f Makefile.coq clean make[2]: Entering directory '/home/lamby/temp/cdt.20160202094640.LVv9Qbd0KW/aac-tactics-0.4' rm -f rewrite.cmo evm_compute.cmo coq.cmo helper.cmo search_monad.cmo matcher.cmo theory.cmo print.cmo aac.cmo aac.cmi coq.cmi evm_compute.cmi helper.cmi matcher.cmi print.cmi rewrite.cmi search_monad.cmi theory.cmi rm -f rewrite.cmx evm_compute.cmx coq.cmx helper.cmx search_monad.cmx matcher.cmx theory.cmx print.cmx aac.cmx rewrite.cmxs evm_compute.cmxs coq.cmxs helper.cmxs search_monad.cmxs matcher.cmxs theory.cmxs print.cmxs aac.cmxs rewrite.o evm_compute.o coq.o helper.o search_monad.o matcher.o theory.o print.o aac.o rm -f evm_compute.ml.d coq.ml.d helper.ml.d search_monad.ml.d matcher.ml.d theory.ml.d print.ml.d coq.mli.d helper.mli.d search_monad.mli.d matcher.mli.d theory.mli.d print.mli.d evm_compute.mli.d rewrite.ml4.d aac.mlpack.d rm -f find . -name .coq-native -type d -empty -delete rm -f AAC.vo Instances.vo Tutorial.vo Caveats.vo AAC.vio Instances.vio Tutorial.vio Caveats.vio AAC.g Instances.g Tutorial.g Caveats.g AAC.v.d Instances.v.d Tutorial.v.d Caveats.v.d AAC.v.beautified Instances.v.beautified Tutorial.v.beautified Caveats.v.beautified AAC.v.old Instances.v.old Tutorial.v.old Caveats.v.old rm -f all.ps all-gal.ps all.pdf all-gal.pdf all.glob AAC.glob Instances.glob Tutorial.glob Caveats.glob AAC.tex Instances.tex Tutorial.tex Caveats.tex AAC.g.tex Instances.g.tex Tutorial.g.tex Caveats.g.tex all-mli.tex rm -rf html mlihtml uninstall_me.sh make[2]: Leaving directory '/home/lamby/temp/cdt.20160202094640.LVv9Qbd0KW/aac-tactics-0.4' rm -f Makefile.coq .depend make[1]: Leaving directory '/home/lamby/temp/cdt.20160202094640.LVv9Qbd0KW/aac-tactics-0.4' dh_ocamlclean dh_clean debian/rules build dh build --with ocaml dh_testdir dh_update_autotools_config dh_ocamlinit dh_auto_configure debian/rules override_dh_auto_build make[1]: Entering directory '/home/lamby/temp/cdt.20160202094640.LVv9Qbd0KW/aac-tactics-0.4' /usr/bin/make Makefile.coq make[2]: Entering directory '/home/lamby/temp/cdt.20160202094640.LVv9Qbd0KW/aac-tactics-0.4' coq_makefile -R . AAC_tactics coq.mli helper.mli search_monad.mli matcher.mli theory.mli print.mli evm_compute.mli evm_compute.ml coq.ml helper.ml search_monad.ml matcher.ml theory.ml print.ml rewrite.ml4 aac.mlpack AAC.v Instances.v Tutorial.v Caveats.v -o Makefile.coq make[2]: Leaving directory '/home/lamby/temp/cdt.20160202094640.LVv9Qbd0KW/aac-tactics-0.4' /usr/bin/make -f Makefile.coq opt html make[2]: Entering directory '/home/lamby/temp/cdt.20160202094640.LVv9Qbd0KW/aac-tactics-0.4' /usr/bin/ocamldep.opt -slash "evm_compute.mli" > "evm_compute.mli.d" || ( RV=$?; rm -f "evm_compute.mli.d"; exit ${RV} ) /usr/bin/ocamldep.opt -slash "print.mli" > "print.mli.d" || ( RV=$?; rm -f "print.mli.d"; exit ${RV} ) /usr/bin/ocamldep.opt -slash "theory.mli" > "theory.mli.d" || ( RV=$?; rm -f "theory.mli.d"; exit ${RV} ) /usr/bin/ocamldep.opt -slash "matcher.mli" > "matcher.mli.d" || ( RV=$?; rm -f "matcher.mli.d"; exit ${RV} ) /usr/bin/ocamldep.opt -slash "search_monad.mli" > "search_monad.mli.d" || ( RV=$?; rm -f "search_monad.mli.d"; exit ${RV} ) /usr/bin/ocamldep.opt -slash "helper.mli" > "helper.mli.d" || ( RV=$?; rm -f "helper.mli.d"; exit ${RV} ) /usr/bin/ocamldep.opt -slash "coq.mli" > "coq.mli.d" || ( RV=$?; rm -f "coq.mli.d"; exit ${RV} ) "coqdep" -c -c "aac.mlpack" > "aac.mlpack.d" || ( RV=$?; rm -f "aac.mlpack.d"; exit ${RV} ) /usr/bin/ocamldep.opt -slash "print.ml" > "print.ml.d" || ( RV=$?; rm -f "print.ml.d"; exit ${RV} ) /usr/bin/ocamldep.opt -slash "theory.ml" > "theory.ml.d" || ( RV=$?; rm -f "theory.ml.d"; exit ${RV} ) /usr/bin/ocamldep.opt -slash "matcher.ml" > "matcher.ml.d" || ( RV=$?; rm -f "matcher.ml.d"; exit ${RV} ) /usr/bin/ocamldep.opt -slash "search_monad.ml" > "search_monad.ml.d" || ( RV=$?; rm -f "search_monad.ml.d"; exit ${RV} ) /usr/bin/ocamldep.opt -slash "helper.ml" > "helper.ml.d" || ( RV=$?; rm -f "helper.ml.d"; exit ${RV} ) /usr/bin/ocamldep.opt -slash "coq.ml" > "coq.ml.d" || ( RV=$?; rm -f "coq.ml.d"; exit ${RV} ) /usr/bin/ocamldep.opt -slash "evm_compute.ml" > "evm_compute.ml.d" || ( RV=$?; rm -f "evm_compute.ml.d"; exit ${RV} ) /usr/bin/ocamldep.opt -slash -pp '/usr/bin/camlp5o -I /usr/lib/ocaml/ -I /usr/lib/ocaml/threads/ -I "/usr/lib/coq/kernel" -I "/usr/lib/coq/lib" -I "/usr/lib/coq/library" -I "/usr/lib/coq/parsing" -I "/usr/lib/coq/pretyping" -I "/usr/lib/coq/interp" -I "/usr/lib/coq/printing" -I "/usr/lib/coq/intf" -I "/usr/lib/coq/proofs" -I "/usr/lib/coq/tactics" -I "/usr/lib/coq/tools" -I "/usr/lib/coq/toplevel" -I "/usr/lib/coq/stm" -I "/usr/lib/coq/grammar" -I "/usr/lib/coq/config" -I "/usr/lib/coq//plugins/btauto" -I "/usr/lib/coq//plugins/cc" -I "/usr/lib/coq//plugins/decl_mode" -I "/usr/lib/coq//plugins/derive" -I "/usr/lib/coq//plugins/extraction" -I "/usr/lib/coq//plugins/firstorder" -I "/usr/lib/coq//plugins/fourier" -I "/usr/lib/coq//plugins/funind" -I "/usr/lib/coq//plugins/micromega" -I "/usr/lib/coq//plugins/nsatz" -I "/usr/lib/coq//plugins/omega" -I "/usr/lib/coq//plugins/quote" -I "/usr/lib/coq//plugins/romega" -I "/usr/lib/coq//plugins/rtauto" -I "/usr/lib/coq//plugins/setoid_ring" -I "/usr/lib/coq//plugins/syntax" -I "/usr/lib/coq//plugins/xml" compat5.cmo pa_extend.cmo q_MLast.cmo pa_macro.cmo unix.cma threads.cma grammar.cma -loc loc -impl' -impl "rewrite.ml4" > "rewrite.ml4.d" || ( RV=$?; rm -f "rewrite.ml4.d"; exit ${RV} ) "coqdep" -c -R "." AAC_tactics "Caveats.v" > "Caveats.v.d" || ( RV=$?; rm -f "Caveats.v.d"; exit ${RV} ) "coqdep" -c -R "." AAC_tactics "Tutorial.v" > "Tutorial.v.d" || ( RV=$?; rm -f "Tutorial.v.d"; exit ${RV} ) "coqdep" -c -R "." AAC_tactics "Instances.v" > "Instances.v.d" || ( RV=$?; rm -f "Instances.v.d"; exit ${RV} ) "coqdep" -c -R "." AAC_tactics "AAC.v" > "AAC.v.d" || ( RV=$?; rm -f "AAC.v.d"; exit ${RV} ) *** Warning: in file AAC.v, declared ML module aac has not been found! *** Warning: in file AAC.v, declared ML module aac has not been found! /usr/bin/make all "OPT:=-opt" make[3]: Entering directory '/home/lamby/temp/cdt.20160202094640.LVv9Qbd0KW/aac-tactics-0.4' /usr/bin/make -f Makefile.coq all make[4]: Entering directory '/home/lamby/temp/cdt.20160202094640.LVv9Qbd0KW/aac-tactics-0.4' "coqc" -q -opt -R "." AAC_tactics AAC File "./AAC.v", line 497, characters 8-20: Error: The constructor vcons (in type vT) expects 2 arguments. Makefile.coq:424: recipe for target 'AAC.vo' failed make[4]: *** [AAC.vo] Error 1 make[4]: Leaving directory '/home/lamby/temp/cdt.20160202094640.LVv9Qbd0KW/aac-tactics-0.4' Makefile:16: recipe for target 'all' failed make[3]: *** [all] Error 2 make[3]: Leaving directory '/home/lamby/temp/cdt.20160202094640.LVv9Qbd0KW/aac-tactics-0.4' Makefile.coq:307: recipe for target 'opt' failed make[2]: *** [opt] Error 2 make[2]: Leaving directory '/home/lamby/temp/cdt.20160202094640.LVv9Qbd0KW/aac-tactics-0.4' debian/rules:18: recipe for target 'override_dh_auto_build' failed make[1]: *** [override_dh_auto_build] Error 2 make[1]: Leaving directory '/home/lamby/temp/cdt.20160202094640.LVv9Qbd0KW/aac-tactics-0.4' debian/rules:14: recipe for target 'build' failed make: *** [build] Error 2 [..] The full build log is attached. Regards, -- ,''`. : :' : Chris Lamb `. `'` la...@debian.org / chris-lamb.co.uk `-
aac-tactics.0.4-5.unstable.amd64.log.txt.gz
Description: Binary data