Coq

coq version 8.3.pl3+dfsg-1build1 FTBFS on armhf in precise

Bug #935063 reported by Andreas Moog on 2012-02-18
24
This bug affects 3 people
Affects Status Importance Assigned to Milestone
Coq
New
Undecided
Unassigned
coq (Ubuntu)
High
Unassigned
Precise
High
Unassigned
Quantal
High
Unassigned

Bug Description

This is a semi-automatic report based on the latest archive rebuild results [1].
Apologies if it reaches you in error.

Excerpt from the buildlog:

"ocamlopt" -rectypes -I config -I tools -I tools/coqdoc -I scripts -I lib -I kernel -I kernel/byterun -I library -I proofs -I tactics -I pretyping -I interp -I toplevel -I parsing -I ide/utils -I ide -I plugins/omega -I plugins/romega -I plugins/micromega -I plugins/quote -I plugins/ring -I plugins/dp -I plugins/setoid_ring -I plugins/xml -I plugins/extraction -I plugins/fourier -I plugins/cc -I plugins/funind -I plugins/firstorder -I plugins/field -I plugins/subtac -I plugins/rtauto -I plugins/nsatz -I plugins/syntax -I "+camlp5" -c plugins/syntax/ascii_syntax.ml
"ocamlopt" -rectypes -I config -I tools -I tools/coqdoc -I scripts -I lib -I kernel -I kernel/byterun -I library -I proofs -I tactics -I pretyping -I interp -I toplevel -I parsing -I ide/utils -I ide -I plugins/omega -I plugins/romega -I plugins/micromega -I plugins/quote -I plugins/ring -I plugins/dp -I plugins/setoid_ring -I plugins/xml -I plugins/extraction -I plugins/fourier -I plugins/cc -I plugins/funind -I plugins/firstorder -I plugins/field -I plugins/subtac -I plugins/rtauto -I plugins/nsatz -I plugins/syntax -I "+camlp5" -c plugins/syntax/ascii_syntax_plugin_mod.ml
"ocamlopt" -rectypes -I config -I tools -I tools/coqdoc -I scripts -I lib -I kernel -I kernel/byterun -I library -I proofs -I tactics -I pretyping -I interp -I toplevel -I parsing -I ide/utils -I ide -I plugins/omega -I plugins/romega -I plugins/micromega -I plugins/quote -I plugins/ring -I plugins/dp -I plugins/setoid_ring -I plugins/xml -I plugins/extraction -I plugins/fourier -I plugins/cc -I plugins/funind -I plugins/firstorder -I plugins/field -I plugins/subtac -I plugins/rtauto -I plugins/nsatz -I plugins/syntax -I "+camlp5" -a -o plugins/syntax/ascii_syntax_plugin.cmxa plugins/syntax/ascii_syntax.cmx plugins/syntax/ascii_syntax_plugin_mod.cmx
"ocamlopt" -rectypes -I config -I tools -I tools/coqdoc -I scripts -I lib -I kernel -I kernel/byterun -I library -I proofs -I tactics -I pretyping -I interp -I toplevel -I parsing -I ide/utils -I ide -I plugins/omega -I plugins/romega -I plugins/micromega -I plugins/quote -I plugins/ring -I plugins/dp -I plugins/setoid_ring -I plugins/xml -I plugins/extraction -I plugins/fourier -I plugins/cc -I plugins/funind -I plugins/firstorder -I plugins/field -I plugins/subtac -I plugins/rtauto -I plugins/nsatz -I plugins/syntax -I "+camlp5" -c plugins/syntax/string_syntax.ml
"ocamlopt" -rectypes -I config -I tools -I tools/coqdoc -I scripts -I lib -I kernel -I kernel/byterun -I library -I proofs -I tactics -I pretyping -I interp -I toplevel -I parsing -I ide/utils -I ide -I plugins/omega -I plugins/romega -I plugins/micromega -I plugins/quote -I plugins/ring -I plugins/dp -I plugins/setoid_ring -I plugins/xml -I plugins/extraction -I plugins/fourier -I plugins/cc -I plugins/funind -I plugins/firstorder -I plugins/field -I plugins/subtac -I plugins/rtauto -I plugins/nsatz -I plugins/syntax -I "+camlp5" -c plugins/syntax/string_syntax_plugin_mod.ml
"ocamlopt" -rectypes -I config -I tools -I tools/coqdoc -I scripts -I lib -I kernel -I kernel/byterun -I library -I proofs -I tactics -I pretyping -I interp -I toplevel -I parsing -I ide/utils -I ide -I plugins/omega -I plugins/romega -I plugins/micromega -I plugins/quote -I plugins/ring -I plugins/dp -I plugins/setoid_ring -I plugins/xml -I plugins/extraction -I plugins/fourier -I plugins/cc -I plugins/funind -I plugins/firstorder -I plugins/field -I plugins/subtac -I plugins/rtauto -I plugins/nsatz -I plugins/syntax -I "+camlp5" -a -o plugins/syntax/string_syntax_plugin.cmxa plugins/syntax/string_syntax.cmx plugins/syntax/string_syntax_plugin_mod.cmx
cd kernel/byterun/ && "ocamlc" -rectypes -ccopt "-fno-defer-pop -Wall -Wno-unused" -c coq_fix_code.c
cd kernel/byterun/ && "ocamlc" -rectypes -ccopt "-fno-defer-pop -Wall -Wno-unused" -c coq_memory.c
cd kernel/byterun/ && "ocamlc" -rectypes -ccopt "-fno-defer-pop -Wall -Wno-unused" -c coq_values.c
cd kernel/byterun/ && "ocamlc" -rectypes -ccopt "-fno-defer-pop -Wall -Wno-unused" -c coq_interp.c
cd kernel/byterun/ && \
 "ocamlmklib" -oc coqrun coq_fix_code.o coq_memory.o coq_values.o coq_interp.o
"ranlib" kernel/byterun/libcoqrun.a
bin/coqmktop -boot -opt -I config -I tools -I tools/coqdoc -I scripts -I lib -I kernel -I kernel/byterun -I library -I proofs -I tactics -I pretyping -I interp -I toplevel -I parsing -I ide/utils -I ide -I plugins/omega -I plugins/romega -I plugins/micromega -I plugins/quote -I plugins/ring -I plugins/dp -I plugins/setoid_ring -I plugins/xml -I plugins/extraction -I plugins/fourier -I plugins/cc -I plugins/funind -I plugins/firstorder -I plugins/field -I plugins/subtac -I plugins/rtauto -I plugins/nsatz -I plugins/syntax -I "+camlp5" -o bin/coqtop.opt
Fatal error: exception Invalid_argument("index out of bounds")
make[3]: *** [bin/coqtop.opt] Error 2
make[3]: Leaving directory `/build/buildd/coq-8.3.pl3+dfsg'
make[2]: *** [world] Error 2
make[2]: Leaving directory `/build/buildd/coq-8.3.pl3+dfsg'
make[1]: *** [override_dh_auto_build] Error 2
make[1]: Leaving directory `/build/buildd/coq-8.3.pl3+dfsg'
make: *** [build] Error 2
dpkg-buildpackage: error: debian/rules build gave error exit status 2
******************************************************************************
Build finished at 20120206-2305
FAILED [dpkg-buildpackage died]

The full buidlog can be found at https://launchpad.net/ubuntu/+archive/test-rebuild-20120201/+build/3142339/+files/buildlog_ubuntu-precise-armhf.coq_8.3.pl3+dfsg-1build1_FAILEDTOBUILD.txt.gz.

[1] http://people.ubuntuwire.org/~wgrant/rebuild-ftbfs-test/test-rebuild-20120201-precise.html

Andreas Moog (ampelbein) on 2012-02-18
Changed in coq (Ubuntu):
importance: Undecided → High
tags: added: arm-porting-queue
Changed in coq (Ubuntu Precise):
status: New → Confirmed
Micah Gersten (micahg) on 2012-05-16
tags: added: quantal
tags: added: rls-q-incoming
Colin Watson (cjwatson) wrote :

Universe; not committing to fix build failures.

tags: added: rls-q-notfixing
removed: rls-q-incoming
Ivan Zakharyaschev (imz) wrote :

Can I install armel coq in Ubuntu armhf (on Toshiba AC100), or it won't work?

Rolf Leggewie (r0lf) wrote :

quantal has seen the end of its life and is no longer receiving any updates. Marking the quantal task for this ticket as "Won't Fix".

Changed in coq (Ubuntu Quantal):
status: Confirmed → Won't Fix
Andreas Moog (ampelbein) wrote :

This is fixed in the current Ubuntu development release.
Precise is EoL, setting task to Won't Fix.

Changed in coq (Ubuntu):
status: Confirmed → Fix Released
Changed in coq (Ubuntu Precise):
status: Confirmed → Won't Fix
To post a comment you must log in.
This report contains Public information  Edit
Everyone can see this information.

Duplicates of this bug

Other bug subscribers