coq version 8.3.pl3+dfsg-1build1 FTBFS on armhf in precise
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/
"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/
"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/
"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/
"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/
"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/
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/
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_
make[3]: *** [bin/coqtop.opt] Error 2
make[3]: Leaving directory `/build/
make[2]: *** [world] Error 2
make[2]: Leaving directory `/build/
make[1]: *** [override_
make[1]: Leaving directory `/build/
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:/
[1] http://
Changed in coq (Ubuntu): | |
importance: | Undecided → High |
tags: | added: arm-porting-queue |
Changed in coq (Ubuntu Precise): | |
status: | New → Confirmed |
tags: | added: quantal |
tags: | added: rls-q-incoming |
Universe; not committing to fix build failures.