Public bug reported:

Binary package hint: coq

builds in debian

http://launchpadlibrarian.net/52602138/buildlog_ubuntu-maverick-
armel.coq_8.2.pl2%2Bdfsg-1_FAILEDTOBUILD.txt.gz

"ocamlc" -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 contrib/omega -I contrib/romega 
-I contrib/micromega -I contrib/ring -I contrib/dp -I contrib/setoid_ring -I 
contrib/xml -I contrib/extraction -I contrib/interface -I contrib/fourier -I 
contrib/cc -I contrib/funind -I contrib/firstorder -I contrib/field -I 
contrib/subtac -I contrib/rtauto  -I "+camlp5"   -a -o contrib/contrib.cma 
contrib/omega/omega.cmo contrib/omega/coq_omega.cmo contrib/omega/g_omega.cmo  
contrib/romega/const_omega.cmo contrib/romega/refl_omega.cmo 
contrib/romega/g_romega.cmo contrib/micromega/mutils.cmo 
contrib/micromega/vector.cmo contrib/micromega/micromega.cmo 
contrib/micromega/mfourier.cmo contrib/micromega/certificate.cmo 
contrib/micromega/coq_micromega.cmo contrib/micromega/g_micromega.cmo 
contrib/ring/quote.cmo contrib/ring/g_quote.cmo contrib/ring/ring.cmo 
contrib/ring/g_ring.cmo  contrib/setoid_ring/newring.cmo contrib/dp/dp_why.cmo 
contrib/dp/dp_zenon.cmo contrib/dp/dp.cmo contrib/dp/dp_gappa.cmo 
contrib/dp/g_dp.cmo contrib/field/field.cmo  contrib/fourier/fourier.cmo 
contrib/fourier/fourierR.cmo contrib/fourier/g_fourier.cmo 
contrib/extraction/table.cmo contrib/extraction/mlutil.cmo 
contrib/extraction/modutil.cmo contrib/extraction/extraction.cmo 
contrib/extraction/common.cmo contrib/extraction/ocaml.cmo 
contrib/extraction/haskell.cmo contrib/extraction/scheme.cmo 
contrib/extraction/extract_env.cmo contrib/extraction/g_extraction.cmo 
contrib/xml/unshare.cmo contrib/xml/xml.cmo contrib/xml/acic.cmo 
contrib/xml/doubleTypeInference.cmo contrib/xml/cic2acic.cmo 
contrib/xml/acic2Xml.cmo contrib/xml/proof2aproof.cmo 
contrib/xml/xmlcommand.cmo contrib/xml/proofTree2Xml.cmo 
contrib/xml/xmlentries.cmo    contrib/xml/cic2Xml.cmo contrib/xml/dumptree.cmo 
contrib/cc/ccalgo.cmo contrib/cc/ccproof.cmo contrib/cc/cctac.cmo 
contrib/cc/g_congruence.cmo   contrib/firstorder/formula.cmo 
contrib/firstorder/unify.cmo contrib/firstorder/sequent.cmo 
contrib/firstorder/rules.cmo contrib/firstorder/instances.cmo 
contrib/firstorder/ground.cmo contrib/firstorder/g_ground.cmo 
contrib/subtac/subtac_utils.cmo contrib/subtac/eterm.cmo 
contrib/subtac/g_eterm.cmo contrib/subtac/subtac_errors.cmo 
contrib/subtac/subtac_coercion.cmo contrib/subtac/subtac_obligations.cmo 
contrib/subtac/subtac_cases.cmo contrib/subtac/subtac_pretyping_F.cmo 
contrib/subtac/subtac_pretyping.cmo contrib/subtac/subtac_command.cmo 
contrib/subtac/subtac_classes.cmo contrib/subtac/subtac.cmo 
contrib/subtac/g_subtac.cmo contrib/subtac/equations.cmo 
contrib/rtauto/proof_search.cmo contrib/rtauto/refl_tauto.cmo 
contrib/rtauto/g_rtauto.cmo contrib/funind/indfun_common.cmo 
contrib/funind/rawtermops.cmo contrib/funind/recdef.cmo 
contrib/funind/rawterm_to_relation.cmo 
contrib/funind/functional_principles_proofs.cmo 
contrib/funind/functional_principles_types.cmo contrib/funind/invfun.cmo 
contrib/funind/indfun.cmo contrib/funind/merge.cmo contrib/funind/g_indfun.cmo
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
coq_interp.c: In function 'coq_interprete':
coq_interp.c:1393: error: r7 cannot be used in asm here
make[3]: *** [kernel/byterun/coq_interp.o] Error 2
make[3]: Leaving directory `/build/buildd/coq-8.2.pl2+dfsg'
make[2]: *** [check] Error 2

** Affects: coq (Ubuntu)
     Importance: High
         Status: Confirmed


** Tags: armel armv7

** Changed in: coq (Ubuntu)
   Importance: Undecided => High

** Changed in: coq (Ubuntu)
       Status: New => Confirmed

-- 
armel build failure (armv7 specific?)
https://bugs.launchpad.net/bugs/636229
You received this bug notification because you are a member of Ubuntu
Bugs, which is subscribed to Ubuntu.

-- 
ubuntu-bugs mailing list
ubuntu-bugs@lists.ubuntu.com
https://lists.ubuntu.com/mailman/listinfo/ubuntu-bugs

Reply via email to