armel build failure (armv7 specific?)

[Matthias Klose]

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

[Launchpad Janitor (janitor)]

This bug was fixed in the package coq - 8.2.pl2+dfsg-1ubuntu1

---------------
coq (8.2.pl2+dfsg-1ubuntu1) maverick; urgency=low

  * Do not hardcode register names for thumb mode on armel. LP: #636229 .
 -- Matthias Klose <email address hidden> Sat, 18 Sep 2010 18:24:09 +0200

[Matthias Klose (doko)]

reopen the issue; needs an update for thumb

[Yao Qi (yao-codesourcery)]

Reduced test case to gcc is here,
void coq_interprete()
{
  register int accu asm("r7");
  accu = 0;
}

# gcc-4.5 -S /home/yao/test.c
/home/yao/test.c: In function 'coq_interprete':
/home/yao/test.c:6: error: r7 cannot be used in asm here

No error if compiled with -fomit-frame-pointer
# gcc-4.5 -fomit-frame-pointer -S /home/yao/test.c

In thumb mode, r7 is used as frame pointer register. AFAIK, it is correct to report an error like this. Fix to this problem can be either using another register for variable accu on thumb mode or add -fomit-frame-pointer in gcc commandline.

[Jani Monoses (jani)]

This was fixed in Maverick already by doko.