[Reproducible-builds] Bug#813459: aac-tactics: FTBFS: Error: The constructor vcons (in type vT) expects 2 arguments.
Chris Lamb
lamby at debian.org
Tue Feb 2 09:14:04 UTC 2016
Source: aac-tactics
Version: 0.4-5
Severity: serious
Justification: fails to build from source
User: reproducible-builds at lists.alioth.debian.org
Usertags: ftbfs
X-Debbugs-Cc: reproducible-builds at 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 <glondu at 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
`. `'` lamby at debian.org / chris-lamb.co.uk
`-
-------------- next part --------------
A non-text attachment was scrubbed...
Name: aac-tactics.0.4-5.unstable.amd64.log.txt.gz
Type: application/octet-stream
Size: 1843 bytes
Desc: not available
URL: <http://lists.alioth.debian.org/pipermail/reproducible-builds/attachments/20160202/02f55f57/attachment.obj>
More information about the Reproducible-builds
mailing list