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

Bug #935063 reported by Andreas Moog
24
This bug affects 3 people
Affects Status Importance Assigned to Milestone
Coq
New
Undecided
Unassigned
coq (Ubuntu)
Fix Released
High
Unassigned
Precise
Won't Fix
High
Unassigned
Quantal
Won't Fix
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)
Changed in coq (Ubuntu):
importance: Undecided → High
tags: added: arm-porting-queue
Changed in coq (Ubuntu Precise):
status: New → Confirmed
Micah Gersten (micahg)
tags: added: quantal
tags: added: rls-q-incoming
Revision history for this message
Colin Watson (cjwatson) wrote :

Universe; not committing to fix build failures.

tags: added: rls-q-notfixing
removed: rls-q-incoming
Revision history for this message
Ivan Zakharyaschev (imz) wrote :

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

Revision history for this message
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
Revision history for this message
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  
Everyone can see this information.

Duplicates of this bug

Other bug subscribers

Remote bug watches

Bug watches keep track of this bug in other bug trackers.