armel build failure (armv7 specific?)

Bug #636229 reported by Matthias Klose on 2010-09-12
This bug affects 1 person
Affects Status Importance Assigned to Milestone
coq (Ubuntu)

Bug Description

Binary package hint: coq

builds in debian

"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

Related branches

Matthias Klose (doko) on 2010-09-12
Changed in coq (Ubuntu):
importance: Undecided → High
status: New → Confirmed
Launchpad Janitor (janitor) wrote :

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

Changed in coq (Ubuntu):
status: Confirmed → Fix Released
Matthias Klose (doko) wrote :

reopen the issue; needs an update for thumb

Changed in coq (Ubuntu):
status: Fix Released → Confirmed
tags: added: arm-mode
Yao Qi (yao-codesourcery) wrote :

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.

Steve Langasek (vorlon) on 2011-02-15
tags: added: arm-porting-queue
Jani Monoses (jani) wrote :

This was fixed in Maverick already by doko.

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

Other bug subscribers