Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Bug ocamlopt powerPC & sparc ? #3180

Closed
vicuna opened this issue Feb 1, 2002 · 2 comments
Closed

Bug ocamlopt powerPC & sparc ? #3180

vicuna opened this issue Feb 1, 2002 · 2 comments
Labels

Comments

@vicuna
Copy link

vicuna commented Feb 1, 2002

Original bug ID: 848
Reporter: administrator
Status: closed
Resolution: not a bug
Priority: normal
Severity: minor
Category: ~DO NOT USE (was: OCaml general)

Bug description

Full_Name: Judicaël Courant
Version: 3.04
OS: Linux
Submission from: ext2.lri.fr (129.175.15.5)

Bonjour,

[ cf http://buildd.debian.org/build.php?arch=&pkg=coq pour les logs complets de
tout ce que je mentionne ici ; regarder la version 7.2-3 ]

Tout d'abord une bonne nouvelle : coq semble compiler en natif sur
IA64 sans problème, même s'il y a des warnings de la part de
l'assembleur.

Ensuite, deux choses assez troublantes : la compilation de coq échoue
en natif (je n'ai pas encore pu essayer en bytecode) sur sparc et
powerpc à cause d'erreurs à l'exécution des binaires compilés par
ocamlopt :

  • sur sparc accès d'un tableau en-dehors de ses bornes, alors que tout se passe
    bien sur x86, ia64, arm, hppa, mips et mipsel :

bin/coqtop -boot -opt -compile theories/Reals/Rfunctions
bin/coqtop -boot -opt -compile theories/Reals/Rderiv
Fatal error: out-of-bound access in array or string
make[1]: *** [theories/Reals/Rderiv.vo] Error 2
make[1]: Leaving directory `/build/buildd/coq-7.2'
WARNING: NATIVE CODE COMPILATION FAILED

  • sur powerpc, erreur différente :

bin/coqtop.opt -boot -batch -silent -nois -I syntax -load-vernac-source
syntax/MakeBare.v -outputstate states/barestate.coq
make[1]: *** [states/barestate.coq] Terminated
make: *** wait: No child processes. Stop.
make: *** Waiting for unfinished jobs....
make: *** wait: No child processes. Stop.
Build killed with signal 15 after 90 minutes of inactivity

Ce qui veut dire j'imagine que coqtop.opt s'est mis à boucler.

Je n'ai pas accès directement à des machines avec ces architectures, donc
j'aurai malheureusement du mal à vous en dire plus...

Judicaël.

@vicuna
Copy link
Author

vicuna commented Feb 1, 2002

Comment author: administrator

Full_Name: Judicaël Courant

Salut Judicael,

en natif (je n'ai pas encore pu essayer en bytecode) sur sparc et
powerpc à cause d'erreurs à l'exécution des binaires compilés par
ocamlopt :

S'il s'agit bien de la release 3.04, ocamlopt ne marche pas vraiment sur PPC
pour plusieurs raisons. Par contre, avec la version CVS de O'Caml et de Coq,
j'arrive a tout compiler sans probleme, et les contribs passent a part
quelques problemes de makefile.

Je n'ai pas accès directement à des machines avec ces architectures, donc
j'aurai malheureusement du mal à vous en dire plus...

C'est maintenant fixe pour PPC: toul.inria.fr avec ton home-dir de pauillac.
La premiere chose a faire pour porter Coq c'est de renommer les fichiers qui
ont des noms identiques modulo majuscules... CVS n'est pas content.

-- Damien

@vicuna
Copy link
Author

vicuna commented Jan 3, 2003

Comment author: administrator

Sur PowerPC le bug a disparu (?) -- Damien

On ne sait pas reproduire le bug, et il ne semble plus exister. -- Damien

@vicuna vicuna closed this as completed Jan 3, 2003
@vicuna vicuna added the bug label Mar 19, 2019
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
Projects
None yet
Development

No branches or pull requests

1 participant