Ubuntu

armel build failure (armv7 specific?)

Reported by Matthias Klose on 2010-09-12
6
This bug affects 1 person
Affects Status Importance Assigned to Milestone
coq (Ubuntu)
High
Unassigned

Bug Description

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

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